--- a/em-category.agda	Thu Aug 01 09:24:53 2013 +0900
+++ b/em-category.agda	Thu Aug 01 09:46:56 2013 +0900
@@ -221,9 +221,40 @@
         distr1    :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
         distr1    =  let  open ≈-Reasoning (A) in ( distr T )
 
+-- T = (U^T ○ F^T)    
+
+Lemma-EM7 :  ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f  ≈ FMap (U^T ○ F^T) f ]
+Lemma-EM7 {a} {b} f = let open ≈-Reasoning (A) in
+     sym ( begin
+          FMap (U^T ○ F^T) f
+     ≈⟨⟩
+          EMap ( ftmap f )
+     ≈⟨⟩
+           FMap T f
+     ∎ )
+
+Lemma-EM8 :  T ≃  (U^T ○ F^T)
+Lemma-EM8 f = Category.Cat.refl (Lemma-EM7 f)
+
+η^T : NTrans A A identityFunctor ( U^T ○ F^T ) 
+η^T = 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 )
+          ≈⟨ sym (resp refl-hom (Lemma-EM7 f)) ⟩
+              FMap T f o TMap η a
+          ≈⟨ nat η ⟩
+              TMap η b o f
+          ∎
+       isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
+       isNTrans1 = record { naturality = naturality1 }
+
+
 --open MResolution
 
---Resolution^T : MResolution A Eilenberg-MooreCategory T^U_T F^T {η^t} {ε^T} {μ^T} Adj_T 
+--Resolution^T : MResolution A Eilenberg-MooreCategory T^U F^T {η^t} {ε^T} {μ^T} Adj_T 
 --Resolution^T = record {
 --        T=UF   = Lemma-EM7;
 --        μ=UεF  = Lemma-EM8