Mercurial > hg > Members > kono > Proof > category

changeset 110:1db2b43a1a36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
resp and assoc
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 21:34:44 +0900
parents ca1de7cbdf6a
children c670d0e6b1e2
files em-category.agda
diffstat 1 files changed, 2 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 21:31:23 2013 +0900
+++ b/em-category.agda	Wed Jul 31 21:34:44 2013 +0900
@@ -140,23 +140,6 @@
             (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 
@@ -181,10 +164,10 @@
          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
+         EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
          EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
-         EMassoc {_} {_} {_} {_} {f} {g} {h} =  {!!} -- Lemma9 (EMap f) (EMap g) (EMap h) 
+         EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
 
 -- Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
 -- Eilenberg-MooreCategory =