--- a/nat.agda	Mon Jul 29 12:41:40 2013 +0900
+++ b/nat.agda	Mon Jul 29 14:08:45 2013 +0900
@@ -481,11 +481,45 @@
 --
 -- μ = U_T ε U_F
 --
-Lemma12 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+tmap-μ :  (a : Obj A) -> Hom A (FObj ( U_T ○ F_T ) (FObj ( U_T ○ F_T ) a)) (FObj ( U_T ○ F_T ) a)
+tmap-μ a = FMap U_T ( TMap nat-ε ( FObj F_T a ))
+
+nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T )
+nat-μ = record { TMap = tmap-μ ; 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  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  ] ]
+        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+          sym ( begin
+             ( tmap-μ b ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  
+          ≈⟨⟩
+             (  FMap U_T ( TMap nat-ε ( FObj F_T b )) ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  
+          ≈⟨ sym ( distr U_T) ⟩
+             FMap U_T ( KleisliCategory [ TMap nat-ε ( FObj F_T b )  o  FMap F_T ( FMap (U_T ○ F_T) f) ] )  
+          ≈⟨ fcong U_T (sym (nat nat-ε)) ⟩
+             FMap U_T ( KleisliCategory [ (FMap  F_T f) o TMap nat-ε ( FObj F_T a ) ] ) 
+          ≈⟨ distr U_T ⟩
+             (FMap U_T (FMap  F_T f)) o   FMap U_T ( TMap nat-ε ( FObj F_T a )) 
+          ≈⟨⟩
+             (FMap (U_T ○ F_T) f) o  ( tmap-μ a) 
+          ∎ )
+        isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ
+        isNTrans1 = record { naturality = naturality1 } 
+
+Lemma12 : {x : Obj A } -> A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma12 {x} = let open ≈-Reasoning (A) in
           sym ( begin
               FMap U_T ( TMap nat-ε ( FObj F_T x ) )
           ≈⟨⟩
+              tmap-μ x
+          ≈⟨⟩
+              TMap nat-μ x
+          ∎ )
+
+Lemma13 : {x : Obj A } -> A [ TMap μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
+Lemma13 {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) )
@@ -493,7 +527,6 @@
               TMap μ x
           ∎ )
 
-
 Adj_T : Adjunction A KleisliCategory U_T F_T nat-η nat-ε 
 Adj_T = record {
            isAdjunction = record {
@@ -541,7 +574,7 @@
 
 open MResolution
 
-Resolution_T : MResolution A KleisliCategory T U_T F_T Adj_T 
+Resolution_T : MResolution A KleisliCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
 Resolution_T = record {
       T=UF   = Lemma11;
       μ=UεF  = Lemma12