--- a/comparison-em.agda	Fri Aug 02 08:50:22 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 09:52:59 2013 +0900
@@ -52,9 +52,29 @@
      a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
   } where
       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 = {!!}
+      identity1 b =  let open ≈-Reasoning (A) in
+           begin
+                (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b)
+           ≈⟨ IsAdjunction.adjoint1 (isAdjunction Adj^K) ⟩
+                id1 A (FObj U^K 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 = {!!}
+      eval1 b = let open ≈-Reasoning (A) in
+           begin
+                (FMap U^K (TMap ε^K b)) o TMap μ^K' (FObj U^K b) 
+           ≈⟨⟩
+                (FMap U^K (TMap ε^K b)) o FMap U^K (TMap ε^K ( FObj F^K (FObj U^K b)))
+           ≈⟨ sym (distr U^K) ⟩
+                FMap U^K (B [ TMap ε^K b o (TMap ε^K ( FObj F^K (FObj U^K b))) ] )
+           ≈⟨ fcong U^K (nat ε^K) ⟩   -- Horizontal composition
+                FMap U^K (B [ TMap ε^K b o FMap F^K (FMap U^K (TMap ε^K b)) ] )
+           ≈⟨ distr U^K ⟩
+                (FMap U^K (TMap ε^K b)) o FMap U^K (FMap F^K (FMap U^K (TMap ε^K b)))
+           ≈⟨⟩
+                (FMap U^K (TMap ε^K b)) o FMap T^K (FMap U^K (TMap ε^K b))
+           ∎
+
 
 open EMObj
 emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b)