Mercurial > hg > Members > kono > Proof > category

changeset 127:3e05417b0876

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Comparison Functor for Eilenberg-Moore Category is constructed.
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 02 Aug 2013 10:06:15 +0900
parents f117cba46532
children 276f33602700
files comparison-em.agda
diffstat 1 files changed, 7 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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)
            ∎