The flattening lemma for coequalizers

Content created by Vojtěch Štěpančík, Egbert Rijke and Fredrik Bakke.

Created on 2023-09-20.
Last modified on 2024-04-25.

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.double-arrows
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 : double-arrow l1 l2) {X : UU l3}
  (P : X → UU l4) (e : cofork a X)
  where

  left-map-double-arrow-flattening-lemma-coequalizer :
    Σ (domain-double-arrow a) (P ∘ map-cofork a e ∘ left-map-double-arrow a) →
    Σ (codomain-double-arrow a) (P ∘ map-cofork a e)
  left-map-double-arrow-flattening-lemma-coequalizer =
    map-Σ-map-base
      ( left-map-double-arrow a)
      ( P ∘ map-cofork a e)

  right-map-double-arrow-flattening-lemma-coequalizer :
    Σ (domain-double-arrow a) (P ∘ map-cofork a e ∘ left-map-double-arrow a) →
    Σ (codomain-double-arrow a) (P ∘ map-cofork a e)
  right-map-double-arrow-flattening-lemma-coequalizer =
    map-Σ
      ( P ∘ map-cofork a e)
      ( right-map-double-arrow a)
      ( λ x → tr P (coh-cofork a e x))

  double-arrow-flattening-lemma-coequalizer : double-arrow (l1 ⊔ l4) (l2 ⊔ l4)
  double-arrow-flattening-lemma-coequalizer =
    make-double-arrow
      ( left-map-double-arrow-flattening-lemma-coequalizer)
      ( right-map-double-arrow-flattening-lemma-coequalizer)

  cofork-flattening-lemma-coequalizer :
    cofork double-arrow-flattening-lemma-coequalizer (Σ X P)
  pr1 cofork-flattening-lemma-coequalizer = map-Σ-map-base (map-cofork a e) P
  pr2 cofork-flattening-lemma-coequalizer =
    coherence-square-maps-map-Σ-map-base P
      ( right-map-double-arrow a)
      ( left-map-double-arrow a)
      ( map-cofork a e)
      ( map-cofork a e)
      ( coh-cofork a e)

  flattening-lemma-coequalizer-statement : UUω
  flattening-lemma-coequalizer-statement =
    dependent-universal-property-coequalizer a e →
    universal-property-coequalizer
      ( double-arrow-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 : double-arrow l1 l2) {X : UU l3}
  ( P : X → UU l4) (e : cofork a X)
  where

  abstract
    flattening-lemma-coequalizer : flattening-lemma-coequalizer-statement a P e
    flattening-lemma-coequalizer dup-coequalizer =
      universal-property-coequalizer-universal-property-pushout
        ( double-arrow-flattening-lemma-coequalizer a P e)
        ( cofork-flattening-lemma-coequalizer a P e)
        ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv
          ( vertical-map-span-cocone-cofork
            ( double-arrow-flattening-lemma-coequalizer a P e))
          ( horizontal-map-span-cocone-cofork
            ( double-arrow-flattening-lemma-coequalizer a P e))
          ( horizontal-map-cocone-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( vertical-map-cocone-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( vertical-map-span-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( horizontal-map-span-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( horizontal-map-cocone-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( vertical-map-cocone-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( map-equiv
            ( right-distributive-Σ-coproduct
              ( domain-double-arrow a)
              ( domain-double-arrow a)
              ( ( P) ∘
                ( horizontal-map-cocone-cofork a e) ∘
                ( vertical-map-span-cocone-cofork a))))
          ( id)
          ( id)
          ( id)
          ( coherence-square-cocone-flattening-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e))
          ( ind-Σ (ind-coproduct _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
          ( ind-Σ (ind-coproduct _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
          ( refl-htpy)
          ( refl-htpy)
          ( coherence-square-cocone-cofork
            ( double-arrow-flattening-lemma-coequalizer a P e)
            ( cofork-flattening-lemma-coequalizer a P e))
          ( ind-Σ
            ( ind-coproduct _
              ( ev-pair refl-htpy)
              ( ev-pair (λ t → ap-id _ ∙ inv right-unit))))
          ( is-equiv-map-equiv
            ( right-distributive-Σ-coproduct
              ( domain-double-arrow a)
              ( domain-double-arrow a)
              ( ( P) ∘
                ( horizontal-map-cocone-cofork a e) ∘
                ( vertical-map-span-cocone-cofork a))))
          ( is-equiv-id)
          ( is-equiv-id)
          ( is-equiv-id)
          ( flattening-lemma-pushout P
            ( vertical-map-span-cocone-cofork a)
            ( horizontal-map-span-cocone-cofork a)
            ( cocone-codiagonal-cofork a e)
            ( dependent-universal-property-pushout-dependent-universal-property-coequalizer
              ( a)
              ( e)
              ( dup-coequalizer))))

Recent changes