Mercurial > hg > Members > kono > Proof > category

changeset 361:e9d4e6ab6cd1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Jun 2015 19:18:57 +0900
parents 29e0f0bd4d2c
children c18b209a662a
files limit-to.agda
diffstat 1 files changed, 15 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/limit-to.agda	Fri Jun 26 19:03:54 2015 +0900
+++ b/limit-to.agda	Fri Jun 26 19:18:57 2015 +0900
@@ -108,17 +108,30 @@
 Two-id t0  = record { Map = id-0 ; isMap = refl }
 Two-id t1  = record { Map = id-1 ; isMap = refl }
 
+-- arrow composition
+
+_×_ :  {A B C : Two} → Two-Hom B C → Two-Hom A B → Two-Hom A C
+_×_  {t0} {t0} {t0} a b  = {!!}
+_×_  {t0} {t0} {t1} a b  = {!!}
+_×_  {t0} {t1} {t0} a b  = {!!}
+_×_  {t0} {t1} {t1} a b  = {!!}
+_×_  {t1} {t0} {t1} a b  = {!!}
+_×_  {t1} {t0} {t0} a b  = {!!}
+_×_  {t1} {t1} {t1} a b  = {!!}
+_×_  {t1} {t1} {t0} a b  = {!!}
+
+
 open Two-Hom
 
 twocat :  Category c₁ _ (ℓ ⊔ (suc c₂ ⊔ c₁))
 twocat  = record {
     Obj  = Two ;
     Hom = λ a b →  Two-Hom a b   ; 
-    _o_ =  {!!} ;
+    _o_ =  _×_ ;
     _≈_ = _≡_;
     Id  =  \{a} -> Two-id a ;
     isCategory  = record {
-            isEquivalence = {!!} ;
+            isEquivalence = record {refl = refl ; trans = ≡-trans ; sym = ≡-sym};
             identityL  = {!!} ;
             identityR  = {!!} ;
             o-resp-≈  = {!!} ;