Mercurial > hg > Members > kono > Proof > category

changeset 111:c670d0e6b1e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Category._o_ /= Category.Category.Id when checking that the expression _∙_ has type (EMHom .B .C → EMHom .A .B → EMHom .A .C)
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 21:59:02 +0900
parents 1db2b43a1a36
children 5f8d6d1aece4
files em-category.agda
diffstat 1 files changed, 18 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/em-category.agda	Wed Jul 31 21:34:44 2013 +0900
+++ b/em-category.agda	Wed Jul 31 21:59:02 2013 +0900
@@ -83,7 +83,7 @@
        (id1 A x)  o φ
    ∎
 
-EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom a a 
+EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom {x} {x} {φ} {φ} {id1 A x} a a 
 EM-id {x} {φ} {a} = record { 
      isEMHom = record { homomorphism = Lemma-EM1 {x} {φ} a } } 
 
@@ -120,7 +120,7 @@
         ( (EMap g)  o  (EMap f) )  o φ
    ∎
 
-_∙_ : {x y z : Obj A}
+_*_ : {x y z : Obj A}
             {φ   : Hom A  (FObj T x) x}
             {φ'  : Hom A  (FObj T y) y}
             {φ'' : Hom A  (FObj T z) z}
@@ -129,10 +129,14 @@
             {a : EMObj {x} {φ}   } 
             {b : EMObj {y} {φ'}  } 
             {c : EMObj {z} {φ''} } 
-            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c ) ->
+            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c ) 
             (f : EMHom {x} {y} {φ} {φ'} {α} a b) ->
                 (EMHom {x} {z} {φ} {φ''} {A [ α' o  α ] } a c)
-_∙_ {_} {_} {_} {_} {_} {_} {_} {_} {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
+_*_ {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} {a} {b} {c} g f = record { isEMHom = record { homomorphism = 
+     Lemma-EM2 {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} a b c g f } }
+
+_∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
+_∙_ {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
 
 _≗_ :  {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} {φ'}}
@@ -141,7 +145,7 @@
 _≗_ {_} {_} {_} {_} {α} {α'} f g = A [ α ≈ α' ]
 
 
--- isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
+isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
 isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                     ; identityL =   EMidL
                     ; identityR =   EMidR
@@ -169,15 +173,15 @@
                           (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
          EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )
 
--- Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
--- Eilenberg-MooreCategory =
---   record { Obj = EMObj
---          ; Hom = EMHom
---          ; _o_ = _∙_
---          ; _≈_ = _≗_
---          ; Id  = EM-id
---          ; isCategory = isEilenberg-MooreCategory
---          }
+Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
+Eilenberg-MooreCategory =
+  record { Obj = EMObj
+         ; Hom = EMHom
+         ; _o_ = _∙_
+         ; _≈_ = _≗_
+         ; Id  = EM-id
+         ; isCategory = isEilenberg-MooreCategory
+          }
 
 -- --
 -- -- Resolution