# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375343184 -32400
# Node ID 494f870ad54b26ad054397a605c98805b25d7c35
# Parent  32ef4cdb18a2b3c7060a347520510b7b9838fce9
EM Resolution complete

diff -r 32ef4cdb18a2 -r 494f870ad54b em-category.agda
--- a/em-category.agda	Thu Aug 01 15:01:31 2013 +0900
+++ b/em-category.agda	Thu Aug 01 16:46:24 2013 +0900
@@ -286,17 +286,11 @@
 -- μ = U^T ε U^F
 --
 
-b : Obj A
-b = {!!}
-
-f : {a : Obj A} -> Hom A a b
-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
+μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
+μ^T = 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 {a} {b} {f} =  let open ≈-Reasoning (A) in
@@ -314,13 +308,60 @@
         isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
         isNTrans1 = record { naturality = naturality1 }
 
+Lemma-EM10 : {x : Obj A } -> A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
+Lemma-EM10 {x} = let open ≈-Reasoning (A) in
+          sym ( begin
+              FMap U^T ( TMap ε^T ( FObj F^T x ) )
+          ≈⟨⟩
+              emap-μ x
+          ≈⟨⟩
+              TMap μ^T x
+          ∎ )
 
---open MResolution
+Lemma-EM11 : {x : Obj A } -> A [ TMap μ x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
+Lemma-EM11 {x} = let open ≈-Reasoning (A) in
+          sym ( begin
+              FMap U^T ( TMap ε^T ( FObj F^T x ) )
+          ≈⟨⟩
+              TMap μ x
+          ∎ )
 
---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 
---}
+Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
+Adj^T = record {
+           isAdjunction = record {
+               adjoint1 = adjoint1 ;
+               adjoint2 = adjoint2
+           }
+       } where
+           adjoint1 :   { b : Obj Eilenberg-MooreCategory } →
+                     A [ A [ ( FMap U^T ( TMap ε^T b))  o ( TMap η^T ( FObj U^T b )) ]  ≈ id1 A (FObj U^T b) ]
+           adjoint1 {b} =  let open ≈-Reasoning (A) in
+               begin
+                  ( FMap U^T ( TMap ε^T b))  o ( TMap η^T ( FObj U^T b ))
+               ≈⟨⟩ 
+                   φ b  o TMap η (obj b)
+               ≈⟨ IsAlgebra.identity (isAlgebra b ) ⟩
+                  id1 A (FObj U^T b)
+               ∎
+           adjoint2 :   {a : Obj A} →
+                     Eilenberg-MooreCategory [ Eilenberg-MooreCategory [ ( TMap ε^T ( FObj F^T a ))  o ( FMap F^T ( TMap η^T a )) ]
+                                     ≈ id1 Eilenberg-MooreCategory (FObj F^T a) ]
+           adjoint2 {a} =  let open ≈-Reasoning (A) in
+               begin
+                  EMap (( TMap ε^T ( FObj F^T a )) ∙ ( FMap F^T ( TMap η^T a )) )
+               ≈⟨⟩
+                  TMap μ a  o FMap T ( TMap η a )
+               ≈⟨ IsMonad.unity2 (isMonad M) ⟩
+                  EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
+               ∎
 
--- -- end
+open MResolution
+
+Resolution^T : MResolution A Eilenberg-MooreCategory T U^T F^T {η^T} {ε^T} {μ^T} Adj^T 
+Resolution^T = record {
+     T=UF = Lemma-EM8;
+     μ=UεF  = Lemma-EM11
+ }
+
+
+-- end