--- a/cat-utility.agda	Sat Jul 27 15:07:20 2013 +0900
+++ b/cat-utility.agda	Sat Jul 27 17:32:32 2013 +0900
@@ -122,3 +122,17 @@
                       ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
      join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
 
+-- T ≃  (U_R ○ F_R)
+-- μ = U_R ε F_R
+--      nat-ε
+--      nat-η     -- same as η but has different types
+
+record Resolution {c₁ c₂ ℓ  c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁ c₂ ℓ ) 
+      { U_R : Functor B A } { F_R : Functor A B }
+      { η : NTrans A A identityFunctor  ( U_R ○ F_R ) }
+      { μ : NTrans A A (  ( U_R ○ F_R ) ○  ( U_R ○ F_R ) )  ( U_R ○ F_R ) }
+      ( M : Monad A  ( U_R ○ F_R ) η μ ) 
+      { ε_R : NTrans B B ( F_R ○ U_R ) identityFunctor } 
+      ( Adj : Adjunction A B U_R F_R η ε_R ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+   field
+      μ=UεF : {x : Obj A } -> A [ TMap μ x ≈ FMap U_R ( TMap ε_R ( FObj F_R x ) ) ]

--- 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
+--                      ?
+--                   ≈⟨ ?  ⟩
+--                      ?
+--                   ∎