--- a/nat.agda	Sat Jul 27 21:19:58 2013 +0900
+++ b/nat.agda	Sun Jul 28 08:04:01 2013 +0900
@@ -210,16 +210,19 @@
 --  Hom in Kleisli Category
 --
 
-record KHom (a : Obj A)  (b : Obj A)
+
+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 )
 
+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 KHom
+open KleisliHom 
 
 _⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
@@ -514,7 +517,7 @@
                ∎ 
            adjoint2 :   {a : Obj A} →
                      KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a ))  o ( FMap F_T ( TMap nat-η a )) ]  
-                            ≈ id1 KleisliCategory (FObj F_T a) ]
+                                     ≈ id1 KleisliCategory (FObj F_T a) ]
            adjoint2 {a} =  let open ≈-Reasoning (A) in
                begin
                   KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) )
@@ -536,36 +539,33 @@
                   KMap (id1 KleisliCategory (FObj F_T a))
                ∎
 
-nat-μ : NTrans A A (( U_T ○ F_T ) ○  (U_T ○ F_T))  (U_T ○ F_T)
-nat-μ = {!!}
+open MResolution
 
-M_T : Monad  A ( U_T ○ F_T ) nat-η nat-μ 
-M_T = {!!}
-
-Resolution_T : Resolution A KleisliCategory T M U_T F_T Adj_T 
+Resolution_T : MResolution A KleisliCategory T M U_T F_T Adj_T 
 Resolution_T = record {
-      T=UF  = {!!} ;
-      μ=UεF  = {!!}
+      T=UF   = Lemma11;
+      μ=UεF  = Lemma12 
   }
 
 
-module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁ c₂ ℓ ) 
+module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U_K : Functor B A } { F_K : Functor A B }
       { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
       { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 
       { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
-      ( MK :  Monad A (U_K ○ F_K) η_K μ_K )
+      ( K :  Monad A (U_K ○ F_K) η_K μ_K )
       ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      ( ResK : Resolution A B T M AdjK )
+      (ResK : MResolution A B T M U_K F_K AdjK )
   where
 
-        kfmap : {!!}
-        kfmap = {!!}
+        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) ]
 
         K_T : Functor KleisliCategory B 
         K_T = record {
                   FObj = FObj F_K
-                ; FMap = kfmap
+                ; FMap = {!!} -- kfmap
                 ; isFunctor = record
                 {      ≈-cong   = {!!} -- ≈-cong
                      ; identity = {!!} -- identity