Mercurial > hg > Members > kono > Proof > category

changeset 407:7bdc93de2d6e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Mar 2016 21:08:46 +0900
parents 2fbd92ddecb5
children b265e02b0e0b
files limit-to.agda
diffstat 1 files changed, 13 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- 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  = {!!} ;