--- a/nat.agda	Sat Jul 27 03:52:24 2013 +0900
+++ b/nat.agda	Sat Jul 27 05:20:33 2013 +0900
@@ -376,28 +376,73 @@
              KMap  ( ffmap g * ffmap f )
           ∎
 
+Lemma11-1 :  ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f  ≈ FMap (U_T ○ F_T) f ]
+Lemma11-1 {a} {b} f = let open ≈-Reasoning (A) in
+     sym ( begin
+          FMap (U_T ○ F_T) f
+     ≈⟨⟩
+          FMap U_T ( FMap F_T f )
+     ≈⟨⟩  
+           TMap μ (b)  o FMap T (KMap ( ffmap f ) )
+     ≈⟨⟩  
+           TMap μ (b)  o FMap T (TMap η (b) o f)
+     ≈⟨ cdr (distr T ) ⟩  
+           TMap μ (b)  o ( FMap T (TMap η (b)) o FMap T f)
+     ≈⟨ assoc  ⟩
+           (TMap μ (b)  o  FMap T (TMap η (b))) o FMap T f
+     ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩
+           id1 A (FObj T b) o FMap T f
+     ≈⟨ idL ⟩
+           FMap T f 
+     ∎ )
+
+-- Lemma11 :  T ≃  (U_T ○ F_T)
+--Lemma11 = {!!} -- Lemma11-1
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
+       naturality1 :  {a b : Obj A} {f : Hom A a b}
+            → A [ A [ (  FMap ( U_T ○ F_T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
+       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 
+          ≈⟨ nat η ⟩
+              (TMap η b ) o  f
+          ∎ 
        isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
-       isNTrans1 = {!!}
+       isNTrans1 = record { naturality = naturality1 } 
 
-tmap-ε : (a : Obj A) -> KHom ? ?
+tmap-ε : (a : Obj A) -> KHom (FObj T a) a
 tmap-ε a = record { KMap = id1 A (FObj T a) }
 
 nat-ε : NTrans KleisliCategory KleisliCategory  ( F_T ○ U_T ) identityFunctor
 nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where
-       naturality : {a b : Obj A} {f : KHom a b}
+       naturality1 : {a b : Obj A} {f : KHom a b}
             →  (f * ( tmap-ε a ) ) ⋍   (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ) )
-       naturality = {!!}
+       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+          sym ( begin
+              KMap (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ))
+          ≈⟨ ? ⟩
+              KMap (f * ( tmap-ε a ))
+          ∎ )
        isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
-       isNTrans1 = record { naturality = naturality } 
+       isNTrans1 = record { naturality = naturality1 } 
 
-Lemma11 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
-Lemma11 = {!!}
+Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+Lemma12 = {!!}
 
-Lemma12 : T ≃  (U_T ○ F_T)
-Lemma12 = {!!}
 
 -- Resoution_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
 -- Resoution_T = record {