Mercurial > hg > Members > kono > Proof > category

changeset 24:171c31acf78e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jul 2013 18:58:16 +0900
parents 736df1a35807
children 8117bafdec7a
files nat.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/nat.agda	Fri Jul 12 17:56:00 2013 +0900
+++ b/nat.agda	Fri Jul 12 18:58:16 2013 +0900
@@ -168,9 +168,9 @@
                                   → 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 )
@@ -281,25 +281,29 @@
                  ( 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 A T η μ a b c d f g h m k =
-  begin
+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 ] ] ] ]
    ≈⟨ {!!} ⟩
+--   ≈⟨ cdr-eq  ( Trans μ d ) ( nat A μ) ⟩
+     A [ A [ A [ Trans μ d  o  Trans μ ( FObj T d)   ]  o FMap T ( A [ FMap T h  o g ] ) ]    o f ]
+   ≈⟨  ⟩
+     A [ A [ A [ Trans μ d  o    FMap T ( Trans μ d) ]  o FMap T ( A [ FMap T h  o g ] ) ]    o f ]
+   ≈⟨ car-eq f (sym assoc) ⟩
+     A [ A [ Trans μ d  o  A   [ FMap T ( Trans μ d )   o FMap T ( A [ FMap T h  o g ] ) ] ]  o f ]
+   ≈⟨ sym assoc ⟩
      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 )))))   ⟩
+   ≈⟨ cdr-eq ( Trans μ d ) ( car-eq f ( sym ( distr T )))   ⟩
      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) 
-
-
+  ∎ where open ≈-Reasoning (A)