# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1458562126 -32400
# Node ID 7bdc93de2d6e9c69293408c373dc2975a3d8c54f
# Parent  2fbd92ddecb5e61d4318315f56c48947b83b9a01
...

diff -r 2fbd92ddecb5 -r 7bdc93de2d6e limit-to.agda
--- a/limit-to.agda	Mon Mar 21 20:58:00 2016 +0900
+++ b/limit-to.agda	Mon Mar 21 21:08:46 2016 +0900
@@ -63,14 +63,14 @@
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {nothing} {_} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just _} {just _} {nothing} = nothing
 assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} with ((just g ) × (just h)) | ((just f ) × (just g)  )
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | nothing | _ = nothing
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t0 | just id-t0 = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just id-t1 = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just arrow-f = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just id-t1 | just arrow-g = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just arrow-f | just id-t0  = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just arrow-g | just id-t0  = just refl
-assoc-× {_} {_} {_} {_} {_} {_} {just f} {just g} {just h} | just _ | nothing = nothing
+... | nothing | _ = nothing
+... | just _ | nothing = nothing
+... | just id-t0 | just id-t0 = just refl
+... | just id-t1 | just id-t1 = just refl
+... | just id-t1 | just arrow-f = just refl
+... | just id-t1 | just arrow-g = just refl
+... | just arrow-f | just id-t0  = just refl
+... | just arrow-g | just id-t0  = just refl
 ... | just id-t0 | just id-t1 = nothing
 ... | just id-t0 | (just arrow-f) = nothing
 ... | just id-t0 | (just arrow-g) = nothing
@@ -82,6 +82,10 @@
 ... | just arrow-g | (just arrow-f) = nothing
 ... | just arrow-g | (just arrow-g) = nothing
 
+TwoId :  { c₁  c₂ : Level } {a : TwoObject  { c₁} } ->  Maybe (Arrow  { c₂ })
+TwoId {_} {_} {t0} = just id-t0
+TwoId {_} {_} {t1} = just id-t1
+
 
 open import maybeCat  
 
@@ -93,7 +97,7 @@
     Hom = λ a b →    Maybe ( Arrow  { c₂ } ) ;
     _o_ =  \{a} {b} {c} x y -> _×_ { c₁ } {  c₂} {a} {b} {c} x y ;
     _≈_ =    Eq  _≡_   ;
-    Id  =  \{a} -> just id-t0  ;
+    Id  =  \{a} -> TwoId { c₁ } {  c₂} {a} ;
     isCategory  = record {
             isEquivalence =  record {refl = {!!}  ; trans = {!!}  ; sym = {!!}  } ;
             identityL  = {!!} ;