# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1435313937 -32400
# Node ID e9d4e6ab6cd1ccb2b62463ac6fd1dbaa1e796bc4
# Parent  29e0f0bd4d2c42b3f361af3d5db30c8b82a874da
fix

diff -r 29e0f0bd4d2c -r e9d4e6ab6cd1 limit-to.agda
--- 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-≈  = {!!} ;