Mercurial > hg > Members > kono > Proof > category

changeset 109:ca1de7cbdf6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
idL, idR
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 21:31:23 +0900
parents e763efd30868
children 1db2b43a1a36
files em-category.agda
diffstat 1 files changed, 23 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 21:02:32 2013 +0900
+++ b/em-category.agda	Wed Jul 31 21:31:23 2013 +0900
@@ -140,6 +140,24 @@
             (g : EMHom {x} {y} {φ} {φ'} {α'} a b ) -> Set ℓ 
 _≗_ {_} {_} {_} {_} {α} {α'} f g = A [ α ≈ α' ]
 
+Lemma-EM3 : {x y : Obj A}
+            {φ   : Hom A  (FObj T x) x}
+            {φ'  : Hom A  (FObj T y) y}
+            {α  : Hom A x y}
+            (a : EMObj {x} {φ}   )
+            (b : EMObj {y} {φ'}  ) 
+            (f : EMHom {x} {y} {φ} {φ'} {α} a b) -> (EM-id ∙ f) ≗ f
+Lemma-EM3 {_} {y} {_} {_} {α} a b f = let open ≈-Reasoning (A) in
+   begin
+      EMap (EM-id ∙ f)
+   ≈⟨⟩
+     id1 A y  o  α
+   ≈⟨ idL ⟩
+     α
+   ≈⟨⟩
+      EMap f
+   ∎
+
 -- isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                     ; identityL =   EMidL
@@ -149,17 +167,18 @@
                     }
      where
          open ≈-Reasoning (A) 
-         isEquivalence :  { a b : EMObj } ->
-               IsEquivalence {_} {_} {EMHom a b} _≗_
+         isEquivalence : {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
+            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}} ->
+               IsEquivalence {_} {_} {EMHom {x} {y} {φ} {φ'} {α}  a b } _≗_
          isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
              ; sym   = sym
              ; trans = trans-hom
              } 
          EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f
-         EMidL {_} {_} {f} =  {!!} -- Lemma7 (EMap f) 
+         EMidL {a} {b} {f} =  idL 
          EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f
-         EMidR {_} {_} {f} =  {!!} -- Lemma8 (EMap f) 
+         EMidR {_} {_} {f} =  idR
          EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                           f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
          EMo-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = {!!} -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi