--- 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 }