--- a/comparison-em.agda	Fri Aug 02 09:52:59 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 09:59:38 2013 +0900
@@ -81,7 +81,21 @@
 emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 a b f
   } where
       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 = {!!}
+      homomorphism1 a b f = let open ≈-Reasoning (A) in
+           begin
+                (φ (emkobj b))  o FMap T^K (FMap U^K f)
+           ≈⟨⟩
+                FMap U^K (TMap ε^K b)  o FMap U^K (FMap F^K (FMap U^K f))
+           ≈⟨ sym (distr U^K) ⟩
+                FMap U^K ( B [ TMap ε^K b  o FMap F^K (FMap U^K f) ] )
+           ≈⟨ sym (fcong U^K (nat ε^K)) ⟩
+                FMap U^K ( B [ f o TMap ε^K a ] )
+           ≈⟨ distr U^K ⟩
+                (FMap U^K f) o FMap U^K (TMap ε^K a)
+           ≈⟨⟩
+                (FMap U^K f) o ( φ (emkobj a))
+           ∎
+
 
 K^T : Functor B Eilenberg-MooreCategory 
 K^T = record {