The dependent universal property of coequalizers
Content created by Egbert Rijke, Vojtěch Štěpančík and Fredrik Bakke.
Created on 2023-09-20.
Last modified on 2023-11-24.
module synthetic-homotopy-theory.dependent-universal-property-coequalizers where
Imports
open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibers-of-maps open import foundation.functoriality-dependent-pair-types open import foundation.universe-levels open import synthetic-homotopy-theory.26-descent open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-coforks open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.universal-property-coequalizers
Idea
The dependent universal property of coequalizers is a property of
coequalizers of a parallel pair
f, g : A → B
, asserting that for any type family P : X → 𝓤
over the
coequalizer e : B → X
, there is an equivalence between sections of P
and
dependent cocones on P
over e
, given by the map
dependent-cofork-map : ((x : X) → P x) → dependent-cocone e P.
Definitions
The dependent universal property of coequalizers
module _ { l1 l2 l3 : Level} (l : Level) {A : UU l1} {B : UU l2} (f g : A → B) { X : UU l3} (e : cofork f g X) where dependent-universal-property-coequalizer : UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l) dependent-universal-property-coequalizer = (P : X → UU l) → is-equiv (dependent-cofork-map f g e {P = P}) module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) {P : X → UU l4} ( dup-coequalizer : dependent-universal-property-coequalizer l4 f g e) where map-dependent-universal-property-coequalizer : dependent-cofork f g e P → (x : X) → P x map-dependent-universal-property-coequalizer = map-inv-is-equiv (dup-coequalizer P)
Properties
The mediating dependent map obtained by the dependent universal property is unique
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) {P : X → UU l4} ( dup-coequalizer : dependent-universal-property-coequalizer l4 f g e) ( k : dependent-cofork f g e P) where htpy-dependent-cofork-dependent-universal-property-coequalizer : htpy-dependent-cofork f g P ( dependent-cofork-map f g e ( map-dependent-universal-property-coequalizer f g e ( dup-coequalizer) ( k))) ( k) htpy-dependent-cofork-dependent-universal-property-coequalizer = htpy-dependent-cofork-eq f g P ( dependent-cofork-map f g e ( map-dependent-universal-property-coequalizer f g e ( dup-coequalizer) ( k))) ( k) ( is-section-map-inv-is-equiv (dup-coequalizer P) k) abstract uniqueness-dependent-universal-property-coequalizer : is-contr ( Σ ((x : X) → P x) ( λ h → htpy-dependent-cofork f g P (dependent-cofork-map f g e h) k)) uniqueness-dependent-universal-property-coequalizer = is-contr-is-equiv' ( fiber (dependent-cofork-map f g e) k) ( tot ( λ h → htpy-dependent-cofork-eq f g P (dependent-cofork-map f g e h) k)) ( is-equiv-tot-is-fiberwise-equiv ( λ h → is-equiv-htpy-dependent-cofork-eq f g P ( dependent-cofork-map f g e h) ( k))) ( is-contr-map-is-equiv (dup-coequalizer P) k)
A cofork has the dependent universal property of coequalizers if and only if the corresponding cocone has the dependent universal property of pushouts
As mentioned in coforks, coforks can be thought of as special cases of cocones under spans. This theorem makes it more precise, asserting that under this mapping, coequalizers correspond to pushouts.
module _ { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f g : A → B) ( e : cofork f g X) where dependent-universal-property-coequalizer-dependent-universal-property-pushout : ( {l : Level} → dependent-universal-property-pushout l ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) → ( {l : Level} → dependent-universal-property-coequalizer l f g e) dependent-universal-property-coequalizer-dependent-universal-property-pushout ( dup-pushout) ( P) = is-equiv-left-map-triangle ( dependent-cofork-map f g e) ( dependent-cofork-dependent-cocone-codiagonal f g e P) ( dependent-cocone-map ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P)) ( triangle-dependent-cofork-dependent-cocone-codiagonal f g e P) ( dup-pushout P) ( is-equiv-dependent-cofork-dependent-cocone-codiagonal f g e P) dependent-universal-property-pushout-dependent-universal-property-coequalizer : ( {l : Level} → dependent-universal-property-coequalizer l f g e) → ( {l : Level} → dependent-universal-property-pushout l ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) dependent-universal-property-pushout-dependent-universal-property-coequalizer ( dup-coequalizer) ( P) = is-equiv-top-map-triangle ( dependent-cofork-map f g e) ( dependent-cofork-dependent-cocone-codiagonal f g e P) ( dependent-cocone-map ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( P)) ( triangle-dependent-cofork-dependent-cocone-codiagonal f g e P) ( is-equiv-dependent-cofork-dependent-cocone-codiagonal f g e P) ( dup-coequalizer P)
The universal property of coequalizers is equivalent to the dependent universal property of coequalizers
module _ { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( e : cofork f g X) where universal-property-dependent-universal-property-coequalizer : ( {l : Level} → dependent-universal-property-coequalizer l f g e) → ( {l : Level} → universal-property-coequalizer l f g e) universal-property-dependent-universal-property-coequalizer ( dup-coequalizer) ( Y) = is-equiv-left-map-triangle ( cofork-map f g e) ( map-compute-dependent-cofork-constant-family f g e Y) ( dependent-cofork-map f g e) ( triangle-compute-dependent-cofork-constant-family f g e Y) ( dup-coequalizer (λ _ → Y)) ( is-equiv-map-equiv ( compute-dependent-cofork-constant-family f g e Y)) dependent-universal-property-universal-property-coequalizer : ( {l : Level} → universal-property-coequalizer l f g e) → ( {l : Level} → dependent-universal-property-coequalizer l f g e) dependent-universal-property-universal-property-coequalizer up-coequalizer = dependent-universal-property-coequalizer-dependent-universal-property-pushout ( f) ( g) ( e) ( dependent-universal-property-universal-property-pushout ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e) ( universal-property-pushout-universal-property-coequalizer f g e ( up-coequalizer)))
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-09. Egbert Rijke and Fredrik Bakke. Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences (#903).
- 2023-10-23. Vojtěch Štěpančík. Sequential colimits (#841).
- 2023-10-16. Fredrik Bakke and Egbert Rijke. Sequential limits (#839).
- 2023-10-12. Vojtěch Štěpančík. Derive the flattening lemma for coequalizers from the flattening lemma for pushouts (#831).