Mercurial > hg > Members > kono > Proof > category
changeset 21:a7b0f7ab9881
unity law 1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 12 Jul 2013 13:39:33 +0900 |
| parents | e34c93046acf |
| children | b3cb592d7b9d |
| files | nat.agda |
| diffstat | 1 files changed, 24 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 12 12:28:14 2013 +0900 +++ b/nat.agda Fri Jul 12 13:39:33 2013 +0900 @@ -179,23 +179,35 @@ 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₂ ℓ) -> - { T : Functor A A } - { η : NTrans A A identityFunctor T } + ( 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 η μ } + { 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 ] -Lemma7 c k = --- { a b : Obj c} --- { T : Functor c c } --- { η : NTrans c c identityFunctor T } --- { f : Hom c a ( FObj T b) } - {!!} - +Lemma7 c T η b f m k = + let open ≈-Reasoning (c) + μ = mu ( monad k ) + in + begin + join k b (Trans η b) f + ≈⟨ refl-hom ⟩ + 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 ] + ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ + f + ∎ Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A }