The dependent universal property of 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.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.double-arrows
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.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 double arrow 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} (a : double-arrow l1 l2) {X : UU l3}
  (e : cofork a X)
  where

  dependent-universal-property-coequalizer : UUω
  dependent-universal-property-coequalizer =
    {l : Level} (P : X → UU l) → is-equiv (dependent-cofork-map a e {P = P})

module _
  {l1 l2 l3 l4 : Level} (a : double-arrow l1 l2) {X : UU l3}
  (e : cofork a X) {P : X → UU l4}
  (dup-coequalizer : dependent-universal-property-coequalizer a e)
  where

  map-dependent-universal-property-coequalizer :
    dependent-cofork a 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 : double-arrow l1 l2) {X : UU l3}
  (e : cofork a X) {P : X → UU l4}
  (dup-coequalizer : dependent-universal-property-coequalizer a e)
  (k : dependent-cofork a e P)
  where

  htpy-dependent-cofork-dependent-universal-property-coequalizer :
    htpy-dependent-cofork a P
      ( dependent-cofork-map a e
        ( map-dependent-universal-property-coequalizer a e
          ( dup-coequalizer)
          ( k)))
      ( k)
  htpy-dependent-cofork-dependent-universal-property-coequalizer =
    htpy-dependent-cofork-eq a P
      ( dependent-cofork-map a e
        ( map-dependent-universal-property-coequalizer a 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 a P (dependent-cofork-map a e h) k))
    uniqueness-dependent-universal-property-coequalizer =
      is-contr-is-equiv'
        ( fiber (dependent-cofork-map a e) k)
        ( tot
          ( λ h →
            htpy-dependent-cofork-eq a P (dependent-cofork-map a e h) k))
        ( is-equiv-tot-is-fiberwise-equiv
          ( λ h →
            is-equiv-htpy-dependent-cofork-eq a P
              ( dependent-cofork-map a 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 : double-arrow l1 l2) {X : UU l3}
  (e : cofork a X)
  where

  dependent-universal-property-coequalizer-dependent-universal-property-pushout :
    dependent-universal-property-pushout
      ( vertical-map-span-cocone-cofork a)
      ( horizontal-map-span-cocone-cofork a)
      ( cocone-codiagonal-cofork a e) →
    dependent-universal-property-coequalizer a e
  dependent-universal-property-coequalizer-dependent-universal-property-pushout
    ( dup-pushout)
    ( P) =
    is-equiv-left-map-triangle
      ( dependent-cofork-map a e)
      ( dependent-cofork-dependent-cocone-codiagonal a e P)
      ( dependent-cocone-map
        ( vertical-map-span-cocone-cofork a)
        ( horizontal-map-span-cocone-cofork a)
        ( cocone-codiagonal-cofork a e)
        ( P))
      ( triangle-dependent-cofork-dependent-cocone-codiagonal a e P)
      ( dup-pushout P)
      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal a e P)

  dependent-universal-property-pushout-dependent-universal-property-coequalizer :
    dependent-universal-property-coequalizer a e →
    dependent-universal-property-pushout
      ( 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
    ( dup-coequalizer)
    ( P) =
    is-equiv-top-map-triangle
      ( dependent-cofork-map a e)
      ( dependent-cofork-dependent-cocone-codiagonal a e P)
      ( dependent-cocone-map
        ( vertical-map-span-cocone-cofork a)
        ( horizontal-map-span-cocone-cofork a)
        ( cocone-codiagonal-cofork a e)
        ( P))
      ( triangle-dependent-cofork-dependent-cocone-codiagonal a e P)
      ( is-equiv-dependent-cofork-dependent-cocone-codiagonal a 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 : double-arrow l1 l2) {X : UU l3}
  (e : cofork a X)
  where

  universal-property-dependent-universal-property-coequalizer :
    dependent-universal-property-coequalizer a e →
    universal-property-coequalizer a e
  universal-property-dependent-universal-property-coequalizer
    ( dup-coequalizer)
    ( Y) =
    is-equiv-left-map-triangle
      ( cofork-map a e)
      ( map-compute-dependent-cofork-constant-family a e Y)
      ( dependent-cofork-map a e)
      ( triangle-compute-dependent-cofork-constant-family a e Y)
      ( dup-coequalizer (λ _ → Y))
      ( is-equiv-map-equiv
        ( compute-dependent-cofork-constant-family a e Y))

  dependent-universal-property-universal-property-coequalizer :
    universal-property-coequalizer a e →
    dependent-universal-property-coequalizer a e
  dependent-universal-property-universal-property-coequalizer up-coequalizer =
    dependent-universal-property-coequalizer-dependent-universal-property-pushout
      ( a)
      ( e)
      ( dependent-universal-property-universal-property-pushout
          ( vertical-map-span-cocone-cofork a)
          ( horizontal-map-span-cocone-cofork a)
          ( cocone-codiagonal-cofork a e)
          ( universal-property-pushout-universal-property-coequalizer a e
            ( up-coequalizer)))

Recent changes