--- a/nat.agda	Sun Jul 07 18:45:48 2013 +0900
+++ b/nat.agda	Sun Jul 07 19:20:37 2013 +0900
@@ -165,6 +165,20 @@
   _∎ :   {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
   _ ∎  = relTo ( refl-hom )
 
+
+Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
+                 { a b : Obj A } 
+                 { f : Hom A a b }
+                      -> A  [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
+Lemma61 c = IsCategory.identityL (Category.isCategory c) 
+        
+--      -> let open ≈-Reasoning c in
+--      begin  
+--           c [ (Id {_} {_} {_} {c} b) o f ]
+--      ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
+--           f
+--      ∎
+
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
                  { T : Functor A A }
@@ -175,8 +189,13 @@
                  { M : Monad A T η μ } 
                  ( K : Kleisli A T η μ M) 
                       -> A  [ join K b (Trans η b) f  ≈ f ]
-Lemma7 c k = {!!}
-
+Lemma7 c k = 
+--              { a b : Obj c} 
+--              { T : Functor c c }
+--              { η : NTrans c c identityFunctor T }
+--              { f : Hom c a ( FObj T b) }  
+         {!!}
+     
 
 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                  { T : Functor A A }