# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1375405575 -32400
# Node ID 3e05417b08762593f47e7baf2bda303f94890842
# Parent  f117cba465326a09e653641ffc2c0c25f553dadc
Comparison Functor for  Eilenberg-Moore  Category is constructed.

diff -r f117cba46532 -r 3e05417b0876 comparison-em.agda
--- a/comparison-em.agda	Fri Aug 02 09:59:38 2013 +0900
+++ b/comparison-em.agda	Fri Aug 02 10:06:15 2013 +0900
@@ -111,21 +111,25 @@
          identity {a} = let open ≈-Reasoning (A) in
            begin
               EMap (emkmap (id1 B a))
-           ≈⟨ {!!} ⟩
+           ≈⟨⟩
+              FMap U^K (id1 B a) 
+           ≈⟨ IsFunctor.identity (isFunctor U^K) ⟩
+              id1 A ( FObj U^K 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)
-           ≈⟨ {!!} ⟩
+           ≈⟨ IsFunctor.≈-cong (isFunctor U^K) f≈g ⟩
                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 ] ))
-           ≈⟨ {!!} ⟩
+           ≈⟨ distr U^K ⟩
               EMap (emkmap g ∙ emkmap f)
            ∎