Mercurial > hg > Members > kono > Proof > category

changeset 134:de1c3443f10d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
M x A done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Aug 2013 16:35:15 +0900
parents 731e00f31f4f
children 3f3870e867f2
files monoid-monad.agda
diffstat 1 files changed, 37 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/monoid-monad.agda	Sun Aug 11 16:11:55 2013 +0900
+++ b/monoid-monad.agda	Sun Aug 11 16:35:15 2013 +0900
@@ -26,14 +26,45 @@
        T1Map  : Hom A  (T1Obj a) (T1Obj b )
 
 open T1Hom
-_*_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c
-_*_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
-
-
+_∙_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c
+_∙_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
+infixr 9 _∙_ 
 
 
+T1-id :  {a : T1 M A} → T1Hom a a
+T1-id {a = a} = record { T1Map =  id1 A (T1Obj a) } 
 
+open import Relation.Binary.Core
+
+_⋍_ : { a : T1 M A } { b : T1 M A } (f g  : T1Hom a b ) -> Set ℓ 
+_⋍_ {a} {b} f g = A [ T1Map f ≈ T1Map g ]
+infix 4 _⋍_ 
+
+isT1Category : IsCategory ( T1 M A ) T1Hom _⋍_ _∙_ T1-id 
+isT1Category  = record  { isEquivalence =  isEquivalence 
+                    ; identityL =   IsCategory.identityL (Category.isCategory A)
+                    ; identityR =   IsCategory.identityR (Category.isCategory A)
+                    ; o-resp-≈ =    IsCategory.o-resp-≈ ( Category.isCategory A )
+                    ; associative = IsCategory.associative (Category.isCategory A)
+                    }
+     where
+         open ≈-Reasoning (A) 
+         isEquivalence :  { a b : T1 M A } ->
+               IsEquivalence {_} {_} {T1Hom 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
+             } 
+
+T1Category : Category  (ℓ ⊔ (c₂ ⊔ c₁))  (ℓ ⊔ (c₂ ⊔ c₁)) ℓ
+T1Category =
+  record { Obj = T1 M A
+         ; Hom = T1Hom
+         ; _o_ = _∙_
+         ; _≈_ = _⋍_
+         ; Id  = T1-id
+         ; isCategory = isT1Category
+         }
 
 
-
-