The flattening lemma for coequalizers
Content created by Vojtěch Štěpančík and Egbert Rijke.
Created on 2023-09-20.
Last modified on 2023-10-12.
module synthetic-homotopy-theory.flattening-lemma-coequalizers where
Imports
open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equality-dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.transport-along-identifications open import foundation.type-arithmetic-coproduct-types open import foundation.universe-levels open import synthetic-homotopy-theory.coforks open import synthetic-homotopy-theory.dependent-universal-property-coequalizers open import synthetic-homotopy-theory.flattening-lemma-pushouts open import synthetic-homotopy-theory.universal-property-coequalizers open import synthetic-homotopy-theory.universal-property-pushouts
Idea
The flattening lemma for coequalizers states that coequalizers commute with dependent pair types. More precisely, given a coequalizer
g
-----> e
A -----> B -----> X
f
with homotopy H : e ∘ f ~ e ∘ g
, and a type family P : X → 𝓤
over X
, the
cofork
----->
Σ (a : A) P(efa) -----> Σ (b : B) P(eb) ---> Σ (x : X) P(x)
is again a coequalizer.
Definitions
The statement of the flattening lemma for coequalizers
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( P : X → UU l4) (e : cofork f g X) where bottom-map-cofork-flattening-lemma-coequalizer : Σ A (P ∘ map-cofork f g e ∘ f) → Σ B (P ∘ map-cofork f g e) bottom-map-cofork-flattening-lemma-coequalizer = map-Σ-map-base f (P ∘ map-cofork f g e) top-map-cofork-flattening-lemma-coequalizer : Σ A (P ∘ map-cofork f g e ∘ f) → Σ B (P ∘ map-cofork f g e) top-map-cofork-flattening-lemma-coequalizer = map-Σ (P ∘ map-cofork f g e) g (λ a → tr P (coherence-cofork f g e a)) cofork-flattening-lemma-coequalizer : cofork ( bottom-map-cofork-flattening-lemma-coequalizer) ( top-map-cofork-flattening-lemma-coequalizer) ( Σ X P) pr1 cofork-flattening-lemma-coequalizer = map-Σ-map-base (map-cofork f g e) P pr2 cofork-flattening-lemma-coequalizer = coherence-square-maps-map-Σ-map-base P g f ( map-cofork f g e) ( map-cofork f g e) ( coherence-cofork f g e) flattening-lemma-coequalizer-statement : UUω flattening-lemma-coequalizer-statement = ( {l : Level} → dependent-universal-property-coequalizer l f g e) → { l : Level} → universal-property-coequalizer l ( bottom-map-cofork-flattening-lemma-coequalizer) ( top-map-cofork-flattening-lemma-coequalizer) ( cofork-flattening-lemma-coequalizer)
Properties
Proof of the flattening lemma for coequalizers
To show that the cofork of total spaces is a coequalizer, it suffices to show that the induced cocone is a pushout. This is accomplished by constructing a commuting cube where the bottom is this cocone, and the top is the cocone of total spaces for the cocone induced by the cofork.
Assuming that the given cofork is a coequalizer, we get that its induced cocone is a pushout, so by the flattening lemma for pushouts, the top square is a pushout as well. The vertical maps of the cube are equivalences, so it follows that the bottom square is a pushout.
module _ { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f g : A → B) {X : UU l3} ( P : X → UU l4) (e : cofork f g X) where abstract flattening-lemma-coequalizer : flattening-lemma-coequalizer-statement f g P e flattening-lemma-coequalizer dup-coequalizer = universal-property-coequalizer-universal-property-pushout ( bottom-map-cofork-flattening-lemma-coequalizer f g P e) ( top-map-cofork-flattening-lemma-coequalizer f g P e) ( cofork-flattening-lemma-coequalizer f g P e) ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv ( vertical-map-span-cocone-cofork ( bottom-map-cofork-flattening-lemma-coequalizer f g P e) ( top-map-cofork-flattening-lemma-coequalizer f g P e)) ( horizontal-map-span-cocone-cofork ( bottom-map-cofork-flattening-lemma-coequalizer f g P e) ( top-map-cofork-flattening-lemma-coequalizer f g P e)) ( horizontal-map-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( vertical-map-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( vertical-map-span-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( horizontal-map-span-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( horizontal-map-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( vertical-map-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( map-equiv ( right-distributive-Σ-coprod A A ( ( P) ∘ ( horizontal-map-cocone-cofork f g e) ∘ ( vertical-map-span-cocone-cofork f g)))) ( id) ( id) ( id) ( coherence-square-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork f g) ( horizontal-map-span-cocone-cofork f g) ( cocone-codiagonal-cofork f g e)) ( λ where (inl a , t) → refl (inr a , t) → refl) ( λ where (inl a , t) → refl (inr a , t) → refl) ( refl-htpy) ( refl-htpy) ( coherence-square-cocone-cofork ( bottom-map-cofork-flattening-lemma-coequalizer f g P e) ( top-map-cofork-flattening-lemma-coequalizer f g P e) ( cofork-flattening-lemma-coequalizer f g P e)) ( λ where (inl a , t) → refl (inr a , t) → ( ap-id ( eq-pair-Σ ( coherence-cofork f g e a) ( refl))) ∙ ( inv right-unit)) ( is-equiv-map-equiv ( right-distributive-Σ-coprod A A ( ( P) ∘ ( horizontal-map-cocone-cofork f g e) ∘ ( vertical-map-span-cocone-cofork f g)))) ( is-equiv-id) ( is-equiv-id) ( is-equiv-id) ( flattening-lemma-pushout P ( 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 ( f) ( g) ( e) ( dup-coequalizer))))
Recent changes
- 2023-10-12. Vojtěch Štěpančík. Derive the flattening lemma for coequalizers from the flattening lemma for pushouts (#831).
- 2023-10-10. Vojtěch Štěpančík and Egbert Rijke. Flattening lemma for pushouts 2: descent data boogaloo (#816).
- 2023-09-20. Vojtěch Štěpančík. Coforks, coequalizers of types, their flattening lemma (#792).