Mercurial > hg > Members > kono > Proof > category

changeset 450:e9ece23ab94e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bottom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Feb 2017 21:20:34 +0900
parents 156e64d1bce0
children 3ee32e4df4c7
files discrete.agda
diffstat 1 files changed, 15 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/discrete.agda	Mon Jan 02 11:26:21 2017 +0900
+++ b/discrete.agda	Mon Feb 27 21:20:34 2017 +0900
@@ -34,9 +34,9 @@
 record TwoHom {c₁ c₂ : Level} (a b : TwoObject {c₁}  ) : Set ( c₂)  where
    field
        hom   :  Maybe ( Arrow {c₁} {c₂} a b )
-   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe ( Set zero )
+   constraint1 :  {c₁ c₂ : Level } → TwoObject {c₁}  → TwoObject {c₁} → Maybe ( TwoObject {c₁} -> Set   )
    constraint1 t0 t0  = nothing
-   constraint1 {_} {c₂} t0 t1  = just  ⊥ 
+   constraint1 {c₁} {c₂} t0 t1  = just ( \ (X : TwoObject   {c₁} ) ->  ⊥  )
    constraint1 t1 t0  = nothing
    constraint1 t1 t1  = nothing
 
@@ -167,7 +167,6 @@
 TwoId {_} {_} t0 = record { hom =  just id-t0 }
 TwoId {_} {_} t1 = record { hom =  just id-t1 }
 
-
 open import Relation.Binary
 TwoCat : {c₁ c₂ ℓ : Level  } →  Category   c₁  c₂  c₂
 TwoCat   {c₁}  {c₂} {ℓ} = record {
@@ -185,19 +184,20 @@
        }
    }  where
         identityL :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →  hom ((TwoId B)  × f)  == hom f
-        identityL  {c₁}  {c₂}  {_} {_} {f}  with hom f
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
-        identityL  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
-        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
-        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _  = ?
+        identityL  {c₁}  {c₂}  {a} {b} {f}  with hom f | constraint1 f a b
+        identityL  {c₁}  {c₂}  {a} {_} {f} | _  | just C = ⊥-elim C
+        identityL  {c₁}  {c₂}  {t0} {t0} {_} | nothing  | _ = nothing
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | nothing  | _ = nothing
+        identityL  {c₁}  {c₂}  {t1} {t0} {_} | nothing  | _ = nothing
+        identityL  {c₁}  {c₂}  {t1} {t1} {_} | nothing  | _ = nothing
+        identityL  {c₁}  {c₂}  {t1} {t1} {_} | just id-t1  | _ = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 | _ = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f | _ = ==refl
+        identityL  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g | _ = ==refl
+        identityL  {c₁}  {c₂}  {t1} {t0} {_} | just _ | _ = ⊥-elim {!!}
         identityR :  {c₁  c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁}  {c₂ } A B) } →   hom ( f × TwoId A )  == hom f
         identityR  {c₁}  {c₂}  {_} {_} {f}  with hom f
-        identityR  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing
+        identityR  {c₁}  {c₂}  {t0} {t0} {_} | nothing  = nothing 
         identityR  {c₁}  {c₂}  {t0} {t1} {_} | nothing  = nothing
         identityR  {c₁}  {c₂}  {t1} {t0} {_} | nothing  = nothing
         identityR  {c₁}  {c₂}  {t1} {t1} {_} | nothing  = nothing
@@ -205,7 +205,7 @@
         identityR  {c₁}  {c₂}  {t0} {t0} {_} | just id-t0 = ==refl
         identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-f = ==refl
         identityR  {c₁}  {c₂}  {t0} {t1} {_} | just arrow-g = ==refl
-        identityR  {c₁}  {c₂}  {t1} {t0} {_} | just _  = ?
+        identityR  {c₁}  {c₂}  {t1} {t0} {_} | just _  = {!!}
         o-resp-≈ :  {c₁  c₂ : Level } {A B C : TwoObject  {c₁} } {f g :  ( TwoHom {c₁}  {c₂ } A B)} {h i : ( TwoHom B C)} →
             hom f == hom g → hom h == hom i → hom ( h × f ) == hom ( i × g )
         o-resp-≈  {c₁}  {c₂} {a} {b} {c} {f} {g} {h} {i}  f==g h==i  =