--- a/kleisli.agda	Sat Mar 04 16:57:58 2017 +0900
+++ b/kleisli.agda	Sun Mar 05 11:14:32 2017 +0900
@@ -209,11 +209,13 @@
 
 
 record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A)  (b : Obj A)
-     : Set c₂ where
-   field
-       KMap :  Hom A a ( FObj T b )
+      : Set c₂ where
+    field
+        KMap :  Hom A a ( FObj T b )
+ 
+open KleisliHom 
 
-open KleisliHom 
+-- we need this to make agda check stop
 KHom  = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
 
 K-id :  {a : Obj A} → KHom a a
@@ -420,10 +422,10 @@
 --
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
-nat-η = record { TMap = λ x → TMap η x ; isNTrans = isNTrans1 } where
-       commute1 :  {a b : Obj A} {f : Hom A a b}
+nat-η = record { TMap = λ x → TMap η x ; isNTrans =  record { commute = commute } } where
+       commute :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ (  FMap ( U_T ○ F_T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
-       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute {a} {b} {f} =  let open ≈-Reasoning (A) in
           begin
               ( FMap ( U_T ○ F_T ) f ) o  ( TMap η a )
           ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩
@@ -431,8 +433,6 @@
           ≈⟨ nat η ⟩
               TMap η b o f
           ∎ 
-       isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (λ a → TMap η a)
-       isNTrans1 = record { commute = commute1 } 
 
 tmap-ε : (a : Obj A) → KHom (FObj T a) a
 tmap-ε a = record { KMap = id1 A (FObj T a) }