The dependent universal property of pushouts
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-06-10.
Last modified on 2023-09-11.
module synthetic-homotopy-theory.dependent-universal-property-pushouts where
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.pullbacks open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-pullback-property-pushouts open import synthetic-homotopy-theory.induction-principle-pushouts
Idea
The dependent universal property of pushouts asserts that every section of a type family over a pushout corresponds in a canonical way uniquely to a dependent cocone over the cocone structure on the pushout.
Definition
The dependent universal property of pushouts
dependent-universal-property-pushout : {l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) dependent-universal-property-pushout l f g {X} c = (P : X → UU l) → is-equiv (dependent-cocone-map f g c P)
Properties
Sections defined by the dependent universal property are unique up to homotopy
abstract uniqueness-dependent-universal-property-pushout : { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} → ( f : S → A) (g : S → B) (c : cocone f g X) ( dup-c : dependent-universal-property-pushout l f g c) → ( P : X → UU l) ( h : dependent-cocone f g c P) → is-contr ( Σ ( (x : X) → P x) ( λ k → htpy-dependent-cocone f g c P (dependent-cocone-map f g c P k) h)) uniqueness-dependent-universal-property-pushout f g c dup-c P h = is-contr-is-equiv' ( fiber (dependent-cocone-map f g c P) h) ( tot ( λ k → htpy-eq-dependent-cocone f g c P (dependent-cocone-map f g c P k) h)) ( is-equiv-tot-is-fiberwise-equiv ( λ k → is-equiv-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P k) ( h))) ( is-contr-map-is-equiv (dup-c P) h)
The induction principle of pushouts is equivalent to the dependent universal property of pushouts
The induction principle of pushouts implies the dependent universal property of pushouts
htpy-eq-dependent-cocone-map : { l1 l2 l3 l4 l : Level} {S : UU l1} {A : UU l2} {B : UU l3} ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → ( H : induction-principle-pushout l f g c) { P : X → UU l} (h h' : (x : X) → P x) → dependent-cocone-map f g c P h = dependent-cocone-map f g c P h' → h ~ h' htpy-eq-dependent-cocone-map f g c ind-c {P} h h' p = ind-induction-principle-pushout f g c ind-c ( λ x → Id (h x) (h' x)) ( pair ( horizontal-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P h) ( dependent-cocone-map f g c P h') ( p)) ( pair ( vertical-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P h) ( dependent-cocone-map f g c P h') ( p)) ( λ s → map-compute-dependent-identification-eq-value h h' ( coherence-square-cocone f g c s) ( horizontal-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P h) ( dependent-cocone-map f g c P h') ( p) ( f s)) ( vertical-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P h) ( dependent-cocone-map f g c P h') ( p) ( g s)) ( coherence-square-htpy-eq-dependent-cocone f g c P ( dependent-cocone-map f g c P h) ( dependent-cocone-map f g c P h') ( p) ( s))))) dependent-universal-property-pushout-induction-principle-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → ((l : Level) → induction-principle-pushout l f g c) → ((l : Level) → dependent-universal-property-pushout l f g c) dependent-universal-property-pushout-induction-principle-pushout f g c ind-c l P = is-equiv-is-invertible ( ind-induction-principle-pushout f g c (ind-c l) P) ( pr2 (ind-c l P)) ( λ h → eq-htpy (htpy-eq-dependent-cocone-map f g c ( ind-c l) ( ind-induction-principle-pushout f g c ( ind-c l) ( P) ( dependent-cocone-map f g c P h)) ( h) ( pr2 (ind-c l P) (dependent-cocone-map f g c P h))))
The dependent universal property of pushouts implies the induction principle of pushouts
induction-principle-pushout-dependent-universal-property-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → ((l : Level) → dependent-universal-property-pushout l f g c) → ((l : Level) → induction-principle-pushout l f g c) induction-principle-pushout-dependent-universal-property-pushout f g c dup-c l P = pr1 (dup-c l P)
The dependent pullback property of pushouts is equivalent to the dependent universal property of pushouts
The dependent universal property of pushouts implies the dependent pullback property of pushouts
triangle-dependent-pullback-property-pushout : {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) → let i = pr1 c j = pr1 (pr2 c) H = pr2 (pr2 c) in ( dependent-cocone-map f g c P) ~ ( ( tot (λ h → tot (λ h' → htpy-eq))) ∘ ( gap ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s))) ( λ (h : (b : B) → P (j b)) → λ s → h (g s)) ( cone-dependent-pullback-property-pushout f g c P))) triangle-dependent-pullback-property-pushout f g (pair i (pair j H)) P h = eq-pair-Σ refl (eq-pair-Σ refl (inv (is-section-eq-htpy (apd h ∘ H)))) dependent-pullback-property-dependent-universal-property-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → ((l : Level) → dependent-universal-property-pushout l f g c) → ((l : Level) → dependent-pullback-property-pushout l f g c) dependent-pullback-property-dependent-universal-property-pushout f g (pair i (pair j H)) I l P = let c = (pair i (pair j H)) in is-equiv-right-factor-htpy ( dependent-cocone-map f g c P) ( tot (λ h → tot (λ h' → htpy-eq))) ( gap ( λ h x → tr P (H x) (h (f x))) ( _∘ g) ( cone-dependent-pullback-property-pushout f g c P)) ( triangle-dependent-pullback-property-pushout f g c P) ( is-equiv-tot-is-fiberwise-equiv ( λ h → is-equiv-tot-is-fiberwise-equiv ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g)))) ( I l P)
The dependent pullback property of pushouts implies the dependent universal property of pushouts
dependent-universal-property-dependent-pullback-property-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → ((l : Level) → dependent-pullback-property-pushout l f g c) → ((l : Level) → dependent-universal-property-pushout l f g c) dependent-universal-property-dependent-pullback-property-pushout f g (pair i (pair j H)) dpullback-c l P = let c = (pair i (pair j H)) in is-equiv-comp-htpy ( dependent-cocone-map f g c P) ( tot (λ h → tot (λ h' → htpy-eq))) ( gap ( λ h x → tr P (H x) (h (f x))) ( _∘ g) ( cone-dependent-pullback-property-pushout f g c P)) ( triangle-dependent-pullback-property-pushout f g c P) ( dpullback-c l P) ( is-equiv-tot-is-fiberwise-equiv ( λ h → is-equiv-tot-is-fiberwise-equiv ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659).