--- a/nat.agda	Sat Jul 27 15:07:20 2013 +0900
+++ b/nat.agda	Sat Jul 27 17:32:32 2013 +0900
@@ -427,20 +427,10 @@
        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           begin
               ( FMap ( U_T ○ F_T ) f ) o  ( TMap η a )
-          ≈⟨⟩
-              FMap U_T (FMap F_T f)  o  ( TMap η a )
-          ≈⟨⟩
-              ( TMap μ (b)  o FMap T (TMap η (b) o f))  o  ( TMap η a )
-          ≈⟨ car ( cdr ( distr T )) ⟩
-              ( TMap μ (b)  o (FMap T (TMap η (b)) o FMap T f))  o  ( TMap η a )
-          ≈⟨ car assoc ⟩
-              ( (TMap μ (b)  o FMap T (TMap η (b))) o FMap T f )  o  ( TMap η a )
-          ≈⟨ car (car (IsMonad.unity2 (isMonad M))) ⟩
-              ( id1 A (FObj T b) o FMap T f )  o  ( TMap η a )
-          ≈⟨ car  idL  ⟩
-              FMap T f   o  TMap η a 
+          ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩
+              FMap T f o TMap η a 
           ≈⟨ nat η ⟩
-              (TMap η b ) o  f
+              TMap η b o f
           ∎ 
        isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
        isNTrans1 = record { naturality = naturality1 } 
@@ -501,8 +491,8 @@
           ∎ )
 
 
-Resoution_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
-Resoution_T = record {
+Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
+Adj_T = record {
            isAdjunction = record {
                adjoint1 = adjoint1 ; 
                adjoint2 = adjoint2
@@ -546,6 +536,17 @@
                   KMap (id1 KleisliCategory (FObj F_T a))
                ∎
 
+nat-μ : NTrans A A (( U_T ○ F_T ) ○  (U_T ○ F_T))  (U_T ○ F_T)
+nat-μ = {!!}
+
+M_T : Monad  A ( U_T ○ F_T ) nat-η nat-μ 
+M_T = {!!}
+
+Resolution_T : Resolution A KleisliCategory M_T Adj_T 
+Resolution_T = record {
+      μ=UεF  = {!!}
+  }
+
 
 module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁ c₂ ℓ ) 
       { U_K : Functor B A } { F_K : Functor A B }
@@ -554,38 +555,38 @@
       ( Adj : Adjunction A B U_K F_K η_K ε_K )
   where
 
-        kfmap : ?
-        kfmap = ?
+        kfmap : {!!}
+        kfmap = {!!}
 
         K_T : Functor KleisliCategory B 
         K_T = record {
                   FObj = FObj F_K
                 ; FMap = kfmap
                 ; isFunctor = record
-                {      ≈-cong   = ≈-cong
-                     ; identity = identity
-                     ; distr    = distr1
+                {      ≈-cong   = {!!} -- ≈-cong
+                     ; identity = {!!} -- identity
+                     ; distr    = {!!} -- distr1
                 }
-             } where
-                identity : {a : Obj B} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj T a) ]
-                identity {a} = let open ≈-Reasoning (B) in
-                  begin
-                      ?
-                  ≈⟨ ? ⟩
-                     ?
-                  ∎
-                ≈-cong : {a b : Obj B} {f g : KHom a b} → B [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
-                ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
-                  begin
-                     ?
-                  ≈⟨ ?  ⟩
-                     ?
-                  ∎
-                distr1 :  {a b c : Obj B} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
-                distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
-                  begin
-                     ?
-                  ≈⟨ ?  ⟩
-                     ?
-                  ∎
+             } -- where
+--                 identity : {a : Obj B} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj T a) ]
+--                 identity {a} = let open ≈-Reasoning (B) in
+--                   begin
+--                       ?
+--                   ≈⟨ ? ⟩
+--                      ?
+--                   ∎
+--                 ≈-cong : {a b : Obj B} {f g : KHom a b} → B [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
+--                 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
+--                   begin
+--                      ?
+--                   ≈⟨ ?  ⟩
+--                      ?
+--                   ∎
+--                 distr1 :  {a b c : Obj B} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
+--                 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
+--                   begin
+--                      ?
+--                   ≈⟨ ?  ⟩
+--                      ?
+--                   ∎