Mercurial > hg > Members > kono > Proof > category
diff discrete.agda @ 457:0ba86e29f492
limit-to and discrete clean up
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Mar 2017 18:30:58 +0900 |
| parents | 4d97955ea419 |
| children | fd79b6d9f350 |
line wrap: on
line diff
--- a/discrete.agda Thu Mar 02 17:41:20 2017 +0900 +++ b/discrete.agda Thu Mar 02 18:30:58 2017 +0900 @@ -4,14 +4,6 @@ module discrete where open import Relation.Binary.Core -open import Relation.Nullary -open import Data.Empty -open import Data.Unit -open import Data.Maybe -open import cat-utility -open import HomReasoning - -open Functor data TwoObject {c₁ : Level} : Set c₁ where t0 : TwoObject @@ -25,6 +17,8 @@ --- 0 1 --- -----→ --- g +-- +-- missing arrows are constrainted by TwoHom data data TwoHom {c₁ c₂ : Level } : TwoObject {c₁} → TwoObject {c₁} → Set c₂ where id-t0 : TwoHom t0 t0 @@ -57,21 +51,19 @@ {g : (TwoHom {c₁} {c₂ } b c )} → {h : (TwoHom {c₁} {c₂ } a b )} → ( f × (g × h)) ≡ ((f × g) × h ) -assoc-× {c₁} {c₂} {a} {b} {c} {d} {f} {g} {h} with 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} {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₂} {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 TwoId : {c₁ c₂ : Level } (a : TwoObject {c₁} ) → (TwoHom {c₁} {c₂ } a a ) TwoId {_} {_} t0 = id-t0 TwoId {_} {_} t1 = id-t1 -open import Relation.Binary open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) TwoCat : {c₁ c₂ : Level } → Category c₁ c₂ c₂ @@ -90,17 +82,15 @@ } } where identityL : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ((TwoId B) × f) ≡ f - identityL {c₁} {c₂} {a} {b} {f} with f - identityL {c₁} {c₂} {t1} {t1} | id-t1 = refl - identityL {c₁} {c₂} {t0} {t0} | id-t0 = refl - identityL {c₁} {c₂} {t0} {t1} | arrow-f = refl - identityL {c₁} {c₂} {t0} {t1} | arrow-g = refl + identityL {c₁} {c₂} {t1} {t1} { id-t1 } = refl + identityL {c₁} {c₂} {t0} {t0} { id-t0 } = refl + identityL {c₁} {c₂} {t0} {t1} { arrow-f } = refl + identityL {c₁} {c₂} {t0} {t1} { arrow-g } = refl identityR : {c₁ c₂ : Level } {A B : TwoObject {c₁}} {f : ( TwoHom {c₁} {c₂ } A B) } → ( f × TwoId A ) ≡ f - identityR {c₁} {c₂} {_} {_} {f} with f - identityR {c₁} {c₂} {t1} {t1} | id-t1 = refl - identityR {c₁} {c₂} {t0} {t0} | id-t0 = refl - identityR {c₁} {c₂} {t0} {t1} | arrow-f = refl - identityR {c₁} {c₂} {t0} {t1} | arrow-g = refl + identityR {c₁} {c₂} {t1} {t1} { id-t1 } = refl + identityR {c₁} {c₂} {t0} {t0} { id-t0 } = refl + identityR {c₁} {c₂} {t0} {t1} { arrow-f } = refl + identityR {c₁} {c₂} {t0} {t1} { arrow-g } = refl o-resp-≈ : {c₁ c₂ : Level } {A B C : TwoObject {c₁} } {f g : ( TwoHom {c₁} {c₂ } A B)} {h i : ( TwoHom B C)} → f ≡ g → h ≡ i → ( h × f ) ≡ ( i × g ) o-resp-≈ {c₁} {c₂} {a} {b} {c} {f} {g} {h} {i} f==g h==i = @@ -116,190 +106,3 @@ ( i × g ) ∎ -indexFunctor : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( a b : Obj A) ( f g : Hom A a b ) → Functor (TwoCat {c₁} {c₂}) A -indexFunctor {c₁} {c₂} {ℓ} A a b f g = record { - FObj = λ a → fobj a - ; FMap = λ {a} {b} f → fmap {a} {b} f - ; isFunctor = record { - identity = λ{x} → identity x - ; distr = λ {a} {b} {c} {f} {g} → distr1 {a} {b} {c} {f} {g} - ; ≈-cong = λ {a} {b} {c} {f} → ≈-cong {a} {b} {c} {f} - } - } where - T = TwoCat {c₁} {c₂} - fobj : Obj T → Obj A - fobj t0 = a - fobj t1 = b - fmap : {x y : Obj T } → (Hom T x y ) → Hom A (fobj x) (fobj y) - fmap {t0} {t0} id-t0 = id1 A a - fmap {t1} {t1} id-t1 = id1 A b - fmap {t0} {t1} arrow-f = f - fmap {t0} {t1} arrow-g = g - ≈-cong : {a : Obj T} {b : Obj T} {f g : Hom T a b} → T [ f ≈ g ] → A [ fmap f ≈ fmap g ] - ≈-cong {a} {b} {f} {.f} refl = let open ≈-Reasoning A in refl-hom - identity : (x : Obj T ) -> A [ fmap (id1 T x) ≈ id1 A (fobj x) ] - identity t0 = let open ≈-Reasoning A in refl-hom - identity t1 = let open ≈-Reasoning A in refl-hom - distr1 : {a : Obj T} {b : Obj T} {c : Obj T} {f : Hom T a b} {g : Hom T b c} → - A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] - distr1 {a} {b} {c} {f} {g} with f | g - distr1 {t0} {t0} {t0} {f} {g} | id-t0 | id-t0 = let open ≈-Reasoning A in sym-hom idL - distr1 {t1} {t1} {t1} {f} {g} | id-t1 | id-t1 = let open ≈-Reasoning A in begin - id1 A b - ≈↑⟨ idL ⟩ - id1 A b o id1 A b - ∎ - distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-f = let open ≈-Reasoning A in begin - fmap (comp arrow-f id-t0) - ≈⟨⟩ - fmap arrow-f - ≈↑⟨ idR ⟩ - fmap arrow-f o id1 A a - ∎ - distr1 {t0} {t0} {t1} {f} {g} | id-t0 | arrow-g = let open ≈-Reasoning A in begin - fmap (comp arrow-g id-t0) - ≈⟨⟩ - fmap arrow-g - ≈↑⟨ idR ⟩ - fmap arrow-g o id1 A a - ∎ - distr1 {t0} {t1} {t1} {f} {g} | arrow-f | id-t1 = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-f) - ≈⟨⟩ - fmap arrow-f - ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-f - ∎ - distr1 {t0} {t1} {t1} {f} {g} | arrow-g | id-t1 = let open ≈-Reasoning A in begin - fmap (comp id-t1 arrow-g) - ≈⟨⟩ - fmap arrow-g - ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-g - ∎ - ---- Equalizer ---- f ---- e -----→ ---- c -----→ a b ---- ^ / -----→ ---- |k h g ---- | / ---- | / ^ ---- | / | ---- |/ | Γ ---- d _ | ---- |\ | ---- \ K af ---- \ -----→ ---- \ t0 t1 ---- -----→ ---- ag ---- ---- - -open Complete -open Limit -open NTrans - -equlimit : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A} -> (f g : Hom A a b) (comp : Complete A (TwoCat {c₁} {c₂} )) -> - Hom A ( limit-c comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) a -equlimit {c₁} {c₂} {ℓ} A {a} {b} f g comp = ? -- TMap (limit-u comp (indexFunctor {c₁} {c₂} {ℓ} A a b f g)) t0 - -lim-to-equ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - (comp : Complete A (TwoCat {c₁} {c₂} ) ) - → {a b : Obj A} (f g : Hom A a b ) - → (fe=ge : A [ A [ f o (equlimit A f g comp ) ] ≈ A [ g o (equlimit A f g comp ) ] ] ) - → IsEqualizer A (equlimit A f g comp ) f g -lim-to-equ {c₁} {c₂} {ℓ} A comp {a} {b} f g fe=ge = record { - fe=ge = fe=ge - ; k = λ {d} h fh=gh → k {d} h fh=gh - ; ek=h = λ {d} {h} {fh=gh} → ek=h d h fh=gh - ; uniqueness = λ {d} {h} {fh=gh} {k'} → uniquness d h fh=gh k' - } where - I = TwoCat {c₁} {c₂} - Γ : Functor I A - Γ = indexFunctor {c₁} {c₂} {ℓ} A a b f g - c = limit-c comp Γ - k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - nmap : (x : Obj I ) ( d : Obj (A) ) (h : Hom A d a ) → Hom A (FObj (K A I d) x) (FObj Γ x) - nmap x d h with x - ... | t0 = h - ... | t1 = A [ f o h ] - commute1 : {x y : Obj I} {f' : Hom I x y} (d : Obj A) (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] - → A [ A [ FMap Γ f' o nmap x d h ] ≈ A [ nmap y d h o FMap (K A I d) f' ] ] - commute1 {x} {y} {f'} d h fh=gh with f' - commute1 {t0} {t1} {f'} d h fh=gh | arrow-f = let open ≈-Reasoning A in begin - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t1} {f'} d h fh=gh | arrow-g = let open ≈-Reasoning A in begin - g o h - ≈↑⟨ fh=gh ⟩ - f o h - ≈↑⟨ idR ⟩ - (f o h ) o id1 A d - ∎ - commute1 {t0} {t0} {f'} d h fh=gh | id-t0 = let open ≈-Reasoning A in begin - id1 A a o h - ≈⟨ idL ⟩ - h - ≈↑⟨ idR ⟩ - h o id1 A d - ∎ - commute1 {t1} {t1} {f'} d h fh=gh | id-t1 = let open ≈-Reasoning A in begin - id1 A b o ( f o h ) - ≈⟨ idL ⟩ - f o h - ≈↑⟨ idR ⟩ - ( f o h ) o id1 A d - ∎ - nat1 : (d : Obj A) → (h : Hom A d a ) → A [ A [ f o h ] ≈ A [ g o h ] ] → NTrans I A (K A I d) Γ - nat1 d h fh=gh = record { - TMap = λ x → nmap x d h ; - isNTrans = record { - commute = λ {x} {y} {f'} → commute1 {x} {y} {f'} d h fh=gh - } - } - e = equlimit A f g comp - eqlim = isLimit comp Γ (nat1 c e fe=ge ) - k {d} h fh=gh = limit eqlim d (nat1 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 - ≈⟨ t0f=t eqlim {d} {nat1 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 (nat1 c e fe=ge ) i o k' ] ≈ TMap (nat1 d h fh=gh) i ] - uniq-nat {t0} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin - (nmap t0 c e ) o k' - ≈⟨⟩ - e o k' - ≈⟨ ek'=h ⟩ - h - ≈⟨⟩ - nmap t0 d h - ∎ - uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin - (nmap t1 c e ) o k' - ≈⟨⟩ - (f o e ) o k' - ≈↑⟨ assoc ⟩ - f o ( e o k' ) - ≈⟨ cdr ek'=h ⟩ - f o h - ≈⟨⟩ - TMap (nat1 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 ) - → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] - uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin - k h fh=gh - ≈⟨ limit-uniqueness eqlim k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ - k' - ∎ -