--- a/comparison-em.agda	Fri Aug 02 08:36:44 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 08:50:22 2013 +0900
@@ -49,18 +49,19 @@
 
 emkobj : Obj B -> EMObj
 emkobj b = record { 
-     a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1; eval = eval1 }
+     a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
   } where
-      identity1 : ?
-      identity1 = ?
-      eval1 : ?
-      eval1 = ?
+      identity1 :  (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ]
+      identity1 b = {!!}
+      eval1 :  (b : Obj B) -> A [ A [ (FMap U^K (TMap ε^K b))  o TMap μ^K' (FObj U^K b) ] ≈ A [ (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b)) ] ]
+      eval1 b = {!!}
 
+open EMObj
 emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b)
-emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 
+emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 a b f
   } where
-      homomorphism1 : ?
-      homomorphism1 = ?
+      homomorphism1 : (a b : Obj B) (f : Hom B a b) -> A [ A [ (φ (emkobj b))  o FMap T^K (FMap U^K f) ]  ≈ A [ (FMap U^K f) o (φ (emkobj a)) ] ]
+      homomorphism1 a b f = {!!}
 
 K^T : Functor B Eilenberg-MooreCategory 
 K^T = record {
@@ -76,21 +77,21 @@
          identity {a} = let open ≈-Reasoning (A) in
            begin
               EMap (emkmap (id1 B a))
-           ≈⟨ ? ⟩
+           ≈⟨ {!!} ⟩
               EMap (EM-id {emkobj a})
            ∎
          ≈-cong : {a b : Obj B} -> {f g : Hom B a b} → B [ f ≈ g ] →  emkmap f ≗ emkmap g 
          ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
            begin
                EMap (emkmap f)
-           ≈⟨ ? ⟩
+           ≈⟨ {!!} ⟩
                EMap (emkmap g)
            ∎
          distr1 :  {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} → ( (emkmap (B [ g o f ])) ≗  (emkmap g ∙ emkmap f)  )
          distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
            begin
               EMap (emkmap (B [ g o f ] ))
-           ≈⟨ ? ⟩
+           ≈⟨ {!!} ⟩
               EMap (emkmap g ∙ emkmap f)
            ∎