Mercurial > hg > Members > kono > Proof > category
changeset 23:736df1a35807
join assoc on going...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 17:56:00 +0900 |
| parents | b3cb592d7b9d |
| children | 171c31acf78e |
| files | nat.agda |
| diffstat | 1 files changed, 32 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 15:15:50 2013 +0900 +++ b/nat.agda Fri Jul 12 17:56:00 2013 +0900 @@ -161,13 +161,16 @@ idR : {a b : Obj A } { f : Hom A a b } → A [ A [ f o id a ] ≈ f ] idR = IsCategory.identityR (Category.isCategory A) + sym : {a b : Obj A } { f g : Hom A a b } -> A [ f ≈ g ] -> A [ g ≈ f ] + sym = IsEquivalence.sym (IsCategory.isEquivalence (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 } + 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 ) + 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 ) @@ -267,18 +270,34 @@ μ = 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 } - { μ : NTrans A A (T ○ T) T } - { a b c d : Obj A } - { 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) +Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T ) + ( a b c d : Obj A ) + ( 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 ] -Lemma9 k = {!!} +Lemma9 A T η μ a b c d f g h m k = + begin + join k d h (join k c g f) + ≈⟨ refl-hom ⟩ + join k d h ( A [ Trans μ c o A [ FMap T g o f ] ] ) + ≈⟨ refl-hom ⟩ + A [ Trans μ d o A [ FMap T h o A [ Trans μ c o A [ FMap T g o f ] ] ] ] + ≈⟨ {!!} ⟩ + A [ Trans μ d o A [ A [ FMap T ( Trans μ d ) o FMap T ( A [ FMap T h o g ] ) ] o f ] ] + ≈⟨ cdr-eq ( Trans μ d ) ( car-eq f (( sym ( distr ( sym ))))) ⟩ + A [ Trans μ d o A [ FMap T ( A [ ( Trans μ d ) o A [ FMap T h o g ] ] ) o f ] ] + ≈⟨ refl-hom ⟩ + join k d ( A [ Trans μ d o A [ FMap T h o g ] ] ) f + ≈⟨ refl-hom ⟩ + join k d ( join k d h g) f + ∎ where + open ≈-Reasoning (A)