--- a/nat.agda	Sat Jul 27 05:20:33 2013 +0900
+++ b/nat.agda	Sat Jul 27 11:52:10 2013 +0900
@@ -263,6 +263,9 @@
          ; isCategory = isKleisliCategory
          }
 
+ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
+ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
+
 U_T : Functor KleisliCategory A
 U_T = record {
         FObj = FObj T
@@ -273,8 +276,6 @@
              ; distr    = distr1
         }
      } where
-        ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
-        ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
         identity : {a : Obj A} →  A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ]
         identity {a} = let open ≈-Reasoning (A) in
           begin
@@ -434,27 +435,63 @@
        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin
               KMap (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ))
-          ≈⟨ ? ⟩
+          ≈⟨⟩
+              TMap μ b  o ( FMap T ( id1 A (FObj T b) )  o (  KMap (FMap (F_T ○ U_T) f ) ))
+          ≈⟨ cdr ( cdr (
+               begin
+                  KMap (FMap (F_T ○ U_T) f ) 
+               ≈⟨⟩
+                  KMap (FMap F_T (FMap U_T f))
+               ≈⟨⟩
+                 TMap η (FObj T b) o (TMap μ (b)  o FMap T (KMap f))
+               ∎  
+          ))  ⟩
+              TMap μ b  o ( FMap T ( id1 A (FObj T b) )  o (TMap η (FObj T b) o (TMap μ (b)  o FMap T (KMap f))))
+          ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩
+              TMap μ b  o ( id1 A (FObj T (FObj T b) )  o (TMap η (FObj T b) o (TMap μ (b)  o FMap T (KMap f))))
+          ≈⟨ cdr idL ⟩
+              TMap μ b  o  (TMap η (FObj T b) o (TMap μ (b)  o FMap T (KMap f)))
+          ≈⟨ assoc ⟩
+              (TMap μ b  o  (TMap η (FObj T b))) o (TMap μ (b)  o FMap T (KMap f))
+          ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩
+              id1 A (FObj T b) o (TMap μ (b)  o FMap T (KMap f))
+          ≈⟨ idL ⟩
+              TMap μ b  o FMap T (KMap f) 
+          ≈⟨ cdr (sym idR) ⟩
+              TMap μ b  o ( FMap T (KMap f)  o id1 A (FObj T a) )
+          ≈⟨⟩
               KMap (f * ( tmap-ε a ))
           ∎ )
        isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
        isNTrans1 = record { naturality = naturality1 } 
 
 Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
-Lemma12 = {!!}
+Lemma12 {x} = let open ≈-Reasoning (A) in
+          sym ( begin
+              FMap U_T ( TMap nat-ε ( FObj F_T x ) )
+          ≈⟨⟩
+              TMap μ x  o FMap T (id1 A (FObj T x) )
+          ≈⟨  cdr (IsFunctor.identity (isFunctor T)) ⟩
+              TMap μ x  o id1 A (FObj T (FObj T x) )
+          ≈⟨ idR ⟩
+              TMap μ x
+          ∎ )
 
 
--- Resoution_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
--- Resoution_T = record {
---            isAdjunction = record {
---                adjoint1 = adjoint1 ; 
---                adjoint2 = adjoint2
---            } 
---        } where
---            adjoint1 : ?
---            adjoint1 = ?
---            adjoint2 : ?
---            adjoint2 = ?
+Resoution_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
+Resoution_T = record {
+           isAdjunction = record {
+               adjoint1 = adjoint1 ; 
+               adjoint2 = adjoint2
+           } 
+       } where
+           adjoint1 :   { b : Obj KleisliCategory } →
+                     A [ A [ ( FMap U_T ( TMap nat-ε b))  o ( TMap nat-η ( FObj U_T b )) ]  ≈ id1 A (FObj U_T b) ]
+           adjoint1 = {!!}
+           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) ]
+           adjoint2 = {!!}