# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375320654 -32400
# Node ID 3249505073624e7a56300615bfd0f9dcd58d43ba
# Parent  d91e89766a76f8f71e2d3ca99c675fc1517e6fa1
ε^T and μ^t

diff -r d91e89766a76 -r 324950507362 em-category.agda
--- a/em-category.agda	Thu Aug 01 09:46:56 2013 +0900
+++ b/em-category.agda	Thu Aug 01 10:30:54 2013 +0900
@@ -251,6 +251,52 @@
        isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
        isNTrans1 = record { naturality = naturality1 }
 
+Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a)  o FMap T (φ a) ]  ≈ A [ (φ a)  o (φ (FObj ( F^T ○ U^T ) a)) ] ]
+Lemma-EM9 a = let open ≈-Reasoning (A) in
+          sym ( begin
+              (φ a)  o (φ (FObj ( F^T ○ U^T ) a))
+          ≈⟨⟩
+              (φ a)  o (TMap μ (obj a))
+          ≈⟨ IsAlgebra.eval (isAlgebra a) ⟩
+              (φ a)  o FMap T (φ a)
+          ∎ )
+
+emap-ε : (a : EMObj ) -> EMHom (FObj ( F^T ○ U^T ) a)  a
+emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a }
+
+ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory  ( F^T ○ U^T ) identityFunctor
+ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
+       naturality1 : {a b : EMObj } {f : EMHom a b}
+            →  (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙(  FMap (F^T ○ U^T) f ) )
+       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+          sym ( begin 
+             EMap (( emap-ε b ) ∙ (  FMap (F^T ○ U^T) f ))
+          ≈⟨⟩
+             φ b  o   FMap T (EMap f)
+          ≈⟨ homomorphism f ⟩
+             EMap f  o φ a
+          ≈⟨⟩
+             EMap (f ∙ ( emap-ε a ))
+          ∎  )
+       isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
+       isNTrans1 = record { naturality = naturality1 }
+
+                                                                                 
+--
+-- μ = U^T ε U^F
+--
+
+emap-μ :  (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
+emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
+
+nat-μ : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
+nat-μ = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
+        naturality1 : {a b : Obj A} {f : Hom A a b}
+             →  A [ A [ (FMap (U^T ○ F^T) f) o  ( emap-μ a) ]  ≈ A [ ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)  ] ]
+        naturality1 = {!!}
+        isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
+        isNTrans1 = record { naturality = naturality1 }
+
 
 --open MResolution