--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/comparison-em.agda	Thu Aug 01 18:14:42 2013 +0900
@@ -0,0 +1,97 @@
+-- -- -- -- -- -- -- -- 
+--  Comparison Functor of  Eilenberg-Moore  Category
+--  defines U^K and F^K as a resolution of Monad
+--  checks Adjointness
+-- 
+--   Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+-- -- -- -- -- -- -- -- 
+
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+--open import Category.HomReasoning                                                                                                               
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+open import Relation.Binary.Core
+
+module comparison-em 
+      { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { M' : Monad A T η μ }
+      {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
+      { U^K : Functor B A } { F^K : Functor A B }
+      { η^K : NTrans A A identityFunctor ( U^K ○ F^K ) }
+      { ε^K : NTrans B B ( F^K ○ U^K ) identityFunctor } 
+      { μ^K' : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
+      ( Adj^K : Adjunction A B U^K F^K η^K ε^K )
+      ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K'} AdjK )
+where
+
+open import adj-monad
+
+T^K = U^K ○ F^K
+
+M : Monad A (U^K ○ F^K ) η^K μ^K 
+M =  Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K
+
+K : Eilenberg-MooreCategory A (U^K ○ F^K ) η^K μ^K M 
+K = record {}
+
+open import nat {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } { K }
+
+open Functor
+open NTrans
+open Eilenberg-MooreCategory
+open EMHom
+open Adjunction
+open MResolution
+
+emkobj : Obj B -> EMObj
+emkobj b = record { 
+     a = FObj U^K b ; phi = A [ FMap U^K o TMap ε^K b ] ; isAlgebra = record { identity = identity1; eval = eval1 }
+  } where
+      identity1 : ?
+      identity1 = ?
+      eval1 : ?
+      eval1 = ?
+
+emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b)
+emkmap {a} {b} f = record { EMap = FMap U f ; homomorphism = homomorphism1 
+  } where
+      homomorphism1 : ?
+      homomorphism1 = ?
+
+K^T : Functor B Eilenberg-MooreCategory 
+K^T = record {
+          FObj = emkobj
+        ; FMap = emkmap
+        ; isFunctor = record
+        {      ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr1
+        }
+     }  where
+         identity : {a : Obj A} →  B [ emkmap (K-id {a}) ≈ id1 B (FObj F^K a) ]
+         identity {a} = let open ≈-Reasoning (B) in
+           begin
+               emkmap (K-id {a})
+           ≈⟨ ? ⟩
+              id1 B (FObj F^K a)
+           ∎
+         ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ KMap f ≈ KMap g ] → B [ emkmap f ≈ emkmap g ]
+         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
+           begin
+               emkmap f
+           ≈⟨ ? ⟩
+               emkmap g
+           ∎
+         distr1 :  {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g * f) ≈ (B [ emkmap g o emkmap f ] )]
+         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
+           begin
+              emkmap (g * f)
+           ≈⟨ ? ⟩
+              emkmap g o emkmap f
+           ∎
+