Mercurial > hg > Members > kono > Proof > category
diff nat.agda @ 22:b3cb592d7b9d
add some law
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 15:15:50 +0900 |
| parents | a7b0f7ab9881 |
| children | 736df1a35807 |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 13:39:33 2013 +0900 +++ b/nat.agda Fri Jul 12 15:15:50 2013 +0900 @@ -3,7 +3,7 @@ -- Monad -- Category A -- A = Category --- Functor T : A -> A +-- Functor T : A → A --T(a) = t(a) --T(f) = tf(f) @@ -13,17 +13,17 @@ --T(g f) = T(g) T(f) -Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) -> {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } - -> A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] -Lemma1 = \t -> IsFunctor.distr ( isFunctor t ) +Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } + → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] +Lemma1 = \t → IsFunctor.distr ( isFunctor t ) -- F(f) --- F(a) ----> F(b) +-- F(a) ---→ F(b) -- | | -- |t(a) |t(b) G(f)t(a) = t(b)F(f) -- | | -- v v --- G(a) ----> G(b) +-- G(a) ---→ G(b) -- G(f) record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) @@ -45,14 +45,14 @@ open NTrans Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} - -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b } - -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] -Lemma2 = \n -> IsNTrans.naturality ( isNTrans n ) + → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b } + → A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] +Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) open import Category.Cat --- η : 1_A -> T --- μ : TT -> T +-- η : 1_A → T +-- μ : TT → T -- μ(a)η(T(a)) = a -- μ(a)T(η(a)) = a -- μ(a)(μ(T(a))) = μ(a)T(μ(a)) @@ -63,9 +63,9 @@ ( μ : NTrans A A (T ○ T) T) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where field - assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] - unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + assoc : {a : Obj A} → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] + unity1 : {a : Obj A} → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} → A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where @@ -81,40 +81,40 @@ { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } - { a : Obj A } -> + { a : Obj A } → ( M : Monad A T η μ ) - -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] -Lemma3 = \m -> IsMonad.assoc ( isMonad m ) + → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] +Lemma3 = \m → IsMonad.assoc ( isMonad m ) Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b} - -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] -Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a ) + → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ] +Lemma4 = \a → IsCategory.identityL ( Category.isCategory a ) Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } - { a : Obj A } -> + { a : Obj A } → ( M : Monad A T η μ ) - -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] -Lemma5 = \m -> IsMonad.unity1 ( isMonad m ) + → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] +Lemma5 = \m → IsMonad.unity1 ( isMonad m ) Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } - { a : Obj A } -> + { a : Obj A } → ( M : Monad A T η μ ) - -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] -Lemma6 = \m -> IsMonad.unity2 ( isMonad m ) + → A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] +Lemma6 = \m → IsMonad.unity2 ( isMonad m ) -- T = M x A -- nat of η -- g ○ f = μ(c) T(g) f --- h ○ (g ○ f) = (h ○ g) ○ f -- η(b) ○ f = f -- f ○ η(a) = f +-- h ○ (g ○ f) = (h ○ g) ○ f record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( T : Functor A A ) @@ -123,14 +123,15 @@ ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where monad : Monad A T η μ monad = M - join : { a b : Obj A } -> ( c : Obj A ) -> - ( Hom A b ( FObj T c )) -> ( Hom A a ( FObj T b)) -> Hom A a ( FObj T c ) + -- g ○ f = μ(c) T(g) f + join : { a b : Obj A } → ( c : Obj A ) → + ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) join c g f = A [ Trans μ c o A [ FMap T g o f ] ] module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where - open import Relation.Binary.Core + open import Relation.Binary.Core renaming ( Trans to Trasn1 ) refl-hom : {a b : Obj A } { x : Hom A a b } → A [ x ≈ x ] @@ -141,6 +142,38 @@ A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ] trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory A ))) b c + -- some short cuts + + car-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) → + A [ x ≈ y ] → A [ A [ x o f ] ≈ A [ y o f ] ] + car-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq + + cdr-eq : {a b c : Obj A } {x y : Hom A a b } ( f : Hom A b c ) → + A [ x ≈ y ] → A [ A [ f o x ] ≈ A [ f o y ] ] + cdr-eq f eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) + + id : (a : Obj A ) → Hom A a a + id a = (Id {_} {_} {_} {A} a) + + idL : {a b : Obj A } { f : Hom A b a } → A [ A [ id a o f ] ≈ f ] + idL = IsCategory.identityL (Category.isCategory A) + + idR : {a b : Obj A } { f : Hom A a b } → A [ A [ f o id a ] ≈ f ] + idR = IsCategory.identityR (Category.isCategory A) + + assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} + → A [ A [ f o A [ g o h ] ] ≈ A [ A [ f o g ] o h ] ] + assoc = IsCategory.associative (Category.isCategory A) + + distr : (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b } + → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ] + distr t = IsFunctor.distr ( isFunctor t ) + + nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A } + → (η : NTrans D A F G ) + → A [ A [ ( FMap G f ) o ( Trans η a ) ] ≈ A [ (Trans η b ) o (FMap F f) ] ] + nat _ η = IsNTrans.naturality ( isNTrans η ) + infixr 2 _∎ infixr 2 _≈⟨_⟩_ infix 1 begin_ @@ -161,16 +194,16 @@ _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x _∎ _ = relTo refl-hom -lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } -> - ( x : Hom L c a ) -> ( y : Hom L b c ) -> L [ L [ x o y ] ≈ L [ x o y ] ] +lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → + ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ] lemma12 L x y = let open ≈-Reasoning ( L ) in begin L [ x o y ] ∎ -Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> - { a : Obj A } ( b : Obj A ) -> +Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → + { a : Obj A } ( b : Obj A ) → ( f : Hom A a b ) - -> A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] + → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ] Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) let open ≈-Reasoning (c) in begin @@ -179,20 +212,17 @@ g ∎ -lemma70 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {x y : Hom A a b } ( f : Hom A c a ) -> - A [ x ≈ y ] -> A [ A [ x o f ] ≈ A [ y o f ] ] -lemma70 c f eq = ( IsCategory.o-resp-≈ ( Category.isCategory c )) ( ≈-Reasoning.refl-hom c ) eq - open Kleisli -Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> +-- η(b) ○ f = f +Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A ) ( η : NTrans A A identityFunctor T ) { μ : NTrans A A (T ○ T) T } { a : Obj A } ( b : Obj A ) ( f : Hom A a ( FObj T b) ) - ( M : Monad A T η μ ) - ( K : Kleisli A T η μ M) - -> A [ join K b (Trans η b) f ≈ f ] + ( m : Monad A T η μ ) + ( k : Kleisli A T η μ m) + → A [ join k b (Trans η b) f ≈ f ] Lemma7 c T η b f m k = let open ≈-Reasoning (c) μ = mu ( monad k ) @@ -203,23 +233,40 @@ c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] - ≈⟨ lemma70 c f ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ - c [ Id {_} {_} {_} {c} (FObj T b) o f ] + ≈⟨ car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ + c [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ f ∎ -Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} - { T : Functor A A } - { η : NTrans A A identityFunctor T } +-- f ○ η(a) = f +Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A identityFunctor T ) { μ : NTrans A A (T ○ T) T } - { a b : Obj A } - { f : Hom A a ( FObj T b) } - { M : Monad A T η μ } - ( K : Kleisli A T η μ M) - -> A [ join K b f (Trans η a) ≈ f ] -Lemma8 k = {!!} + ( a : Obj A ) ( b : Obj A ) + ( f : Hom A a ( FObj T b) ) + ( m : Monad A T η μ ) + ( k : Kleisli A T η μ m) + → A [ join k b f (Trans η a) ≈ f ] +Lemma8 c T η a b f m k = + begin + join k b f (Trans η a) + ≈⟨ refl-hom ⟩ + c [ Trans μ b o c [ FMap T f o (Trans η a) ] ] + ≈⟨ cdr-eq (Trans μ b) ( IsNTrans.naturality ( isNTrans η )) ⟩ + c [ Trans μ b o c [ (Trans η ( FObj T b)) o f ] ] + ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ + c [ c [ Trans μ b o (Trans η ( FObj T b)) ] o f ] + ≈⟨ car-eq f ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ + c [ id (FObj T b) o f ] + ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ + f + ∎ where + open ≈-Reasoning (c) + μ = mu ( monad k ) +-- h ○ (g ○ f) = (h ○ g) ○ f Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } { η : NTrans A A identityFunctor T } @@ -228,9 +275,9 @@ { f : Hom A a ( FObj T b) } { g : Hom A b ( FObj T c) } { h : Hom A c ( FObj T d) } - { M : Monad A T η μ } - ( K : Kleisli A T η μ M) - -> A [ join K d h (join K c g f) ≈ join K d ( join K d h g) f ] + { m : Monad A T η μ } + ( k : Kleisli A T η μ m) + → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ] Lemma9 k = {!!}