--- a/nat.agda	Sun Jul 28 08:04:01 2013 +0900
+++ b/nat.agda	Sun Jul 28 09:10:44 2013 +0900
@@ -216,13 +216,13 @@
    field
        KMap :  Hom A a ( FObj T b )
 
-KHom  = \(a b : Obj A) -> KleisliHom { c₁} {c₂} {ℓ} {A} {T} a b
+open KleisliHom 
+KHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
 
 K-id :  {a : Obj A} → KHom a a
 K-id {a = a} = record { KMap =  TMap η a } 
 
 open import Relation.Binary.Core
-open KleisliHom 
 
 _⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
@@ -555,17 +555,22 @@
       { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
       ( K :  Monad A (U_K ○ F_K) η_K μ_K )
       ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      (ResK : MResolution A B T M U_K F_K AdjK )
+      ( RK : MResolution A B T M U_K F_K AdjK )
   where
 
+        KtoT : {!!}
+        KtoT = {!!}
         RHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
-        kfmap : {a b : Obj A} (f : RHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
-        kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
+        RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) 
+        RMap f = KtoT (RK T=UF) f
+
+        kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
+        kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ]
 
         K_T : Functor KleisliCategory B 
         K_T = record {
                   FObj = FObj F_K
-                ; FMap = {!!} -- kfmap
+                ; FMap = kfmap
                 ; isFunctor = record
                 {      ≈-cong   = {!!} -- ≈-cong
                      ; identity = {!!} -- identity