--- a/kleisli.agda	Tue Mar 07 03:21:46 2017 +0900
+++ b/kleisli.agda	Tue Mar 07 08:27:33 2017 +0900
@@ -192,12 +192,14 @@
 --
 Lemma10 :  {a b c : Obj A} → (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
                           A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
-Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
+Lemma10 {a} {b} {c} f g h i f≈g h≈i = let open ≈-Reasoning (A) in
    begin 
        join M h f
    ≈⟨⟩
        TMap μ c  o ( FMap T h  o f )
-   ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
+   ≈⟨ cdr ( car ( fcong T h≈i )) ⟩
+       TMap μ c  o ( FMap T i  o f )
+   ≈⟨ cdr ( cdr f≈g ) ⟩
        TMap μ c  o ( FMap T i  o g )
    ≈⟨⟩
        join M i g
@@ -332,7 +334,7 @@
 
 
 ffmap :  {a b : Obj A} (f : Hom A a b) → KHom a b
-ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] }
+ffmap {a} {b} f = record { KMap = A [ TMap η b o f ] }
 
 F_T : Functor A KleisliCategory
 F_T = record {
@@ -347,10 +349,10 @@
         identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
         identity {a} = IsCategory.identityR ( Category.isCategory A)
         --  Category.cod A f and Category.cod A g are actualy the same b, so we don't need cong-≈, just refl
-        lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b  ≈  TMap η b ]
-        lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
-        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ]
-        ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
+        lemma1 : {b : Obj A} → A [ TMap η b  ≈  TMap η b ]
+        lemma1 = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η b o f ] ≈ A [ TMap η b o g ] ]
+        ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g lemma1 
         distr1 :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
                  ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
         distr1 {a} {b} {c} {f} {g} =  let open ≈-Reasoning (A) in