Mercurial > hg > Members > kono > Proof > category
changeset 466:44bd77c80555
clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 04 Mar 2017 16:57:58 +0900 |
| parents | d3cd28a71b3f |
| children | ba042c2d3ff5 |
| files | discrete.agda limit-to.agda |
| diffstat | 2 files changed, 25 insertions(+), 29 deletions(-) [+] |
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 {
--- a/limit-to.agda Sat Mar 04 16:26:57 2017 +0900 +++ b/limit-to.agda Sat Mar 04 16:57:58 2017 +0900 @@ -175,27 +175,25 @@ e = equlimit A f g comp c : Obj A c = limit-c comp Γ - natL : NTrans I A (K A I c) Γ - natL = limit-u comp Γ - lim : Limit A I Γ c natL + lim : Limit A I Γ c ( limit-u comp Γ ) lim = isLimit comp Γ - nat0 : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ - nat0 = IndexNat A f g + inat : (d : Obj A) (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ + inat = IndexNat A f g k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - k {d} h fh=gh = limit lim d (nat0 d h fh=gh ) + k {d} h fh=gh = limit lim d (inat d h fh=gh ) ek=h : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → A [ A [ e o k h fh=gh ] ≈ h ] ek=h d h fh=gh = let open ≈-Reasoning A in begin e o k h fh=gh ≈⟨⟩ TMap (limit-u comp Γ) t0 o k h fh=gh - ≈⟨ t0f=t lim {d} {nat0 d h fh=gh } {t0} ⟩ - TMap (nat0 d h fh=gh) t0 + ≈⟨ t0f=t lim {d} {inat d h fh=gh } {t0} ⟩ + TMap (inat d h fh=gh) t0 ≈⟨⟩ h ∎ uniq-nat : {i : Obj I} → (d : Obj A ) (h : Hom A d a ) ( k' : Hom A d c ) ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ]) → A [ A [ e o k' ] ≈ h ] → - A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (nat0 d h fh=gh) i ] + A [ A [ TMap (limit-u comp Γ) i o k' ] ≈ TMap (inat d h fh=gh) i ] uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) t0 o k' ≈⟨⟩ @@ -203,7 +201,7 @@ ≈⟨ ek'=h ⟩ h ≈⟨⟩ - TMap (nat0 d h fh=gh) t0 + TMap (inat d h fh=gh) t0 ∎ uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) t1 o k' @@ -220,7 +218,7 @@ ≈⟨ cdr ek'=h ⟩ f o h ≈⟨⟩ - TMap (nat0 d h fh=gh) t1 + TMap (inat d h fh=gh) t1 ∎ uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → ( k' : Hom A d c )