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