Mercurial > hg > Members > kono > Proof > category
diff discrete.agda @ 466:44bd77c80555
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Mar 2017 16:57:58 +0900 |
| parents | 8436a018f88a |
| children | c375d8f93a2c |
line wrap: on
line diff
--- a/discrete.agda Sat Mar 04 16:26:57 2017 +0900 +++ b/discrete.agda Sat Mar 04 16:57:58 2017 +0900 @@ -21,19 +21,19 @@ -- missing arrows are constrainted by TwoHom data data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where - id-t0 : TwoHom t0 t0 - id-t1 : TwoHom t1 t1 + id-t0 : TwoHom t0 t0 + id-t1 : TwoHom t1 t1 arrow-f : TwoHom t0 t1 arrow-g : TwoHom t0 t1 _×_ : ∀ {c₁ c₂} → {a b c : TwoObject {c₁}} → TwoHom {c₁} {c₂} b c → TwoHom {c₁} {c₂} a b → TwoHom {c₁} {c₂} a c -_×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f -_×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g -_×_ {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 -_×_ {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f -_×_ {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g -_×_ {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 +_×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-f = arrow-f +_×_ {_} {_} {t0} {t1} {t1} id-t1 arrow-g = arrow-g +_×_ {_} {_} {t1} {t1} {t1} id-t1 id-t1 = id-t1 +_×_ {_} {_} {t0} {t0} {t1} arrow-f id-t0 = arrow-f +_×_ {_} {_} {t0} {t0} {t1} arrow-g id-t0 = arrow-g +_×_ {_} {_} {t0} {t0} {t0} id-t0 id-t0 = id-t0 open TwoHom @@ -43,24 +43,22 @@ -- It can be proved without TwoHom constraints assoc-× : {c₁ c₂ : Level } {a b c d : TwoObject {c₁} } - {f : (TwoHom {c₁} {c₂ } c d )} → - {g : (TwoHom b c )} → - {h : (TwoHom a b )} → + {f : (TwoHom {c₁} {c₂ } c d )} → {g : (TwoHom b c )} → {h : (TwoHom a b )} → ( f × (g × h)) ≡ ((f × g) × h ) -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl -assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl -assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t0} { id-t0 }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-f }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t0} {t1} { arrow-g }{ id-t0 }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-f }{ id-t0 } = refl +assoc-× {c₁} {c₂} {t0} {t0} {t1} {t1} { id-t1 }{ arrow-g }{ id-t0 } = refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-f } = refl assoc-× {c₁} {c₂} {t0} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ arrow-g } = refl -assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl +assoc-× {c₁} {c₂} {t1} {t1} {t1} {t1} { id-t1 }{ id-t1 }{ id-t1 } = refl TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = id-t0 TwoId {_} {_} t1 = id-t1 -open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) +open import Relation.Binary.PropositionalEquality TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ TwoCat {c₁} {c₂} = record {