Coequalizers

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

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

module synthetic-homotopy-theory.coequalizers where
Imports 
open import foundation.double-arrows
open import foundation.equivalences
open import foundation.identity-types
open import foundation.transport-along-identifications
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-universal-property-coequalizers
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.universal-property-coequalizers

Idea

The coequalizer of a double arrow f, g : A → B is the colimiting cofork, i.e. a cofork with the universal property of coequalizers.

Properties

All double arrows admit a coequalizer

The standard coequalizer may be obtained as a pushout of the span

     ∇         [f,g]
A <----- A + A -----> B

where the left map is the codiagonal map, sending inl(a) and inr(a) to a, and the right map is defined by the universal property of coproducts to send inl(a) to f(a) and inr(a) to g(a).

The pushout thus constructed will consist of a copy of B, a copy of A, and for every point a of A there will be a path from f(a) to a and to g(a), which corresponds to having a copy of B with paths connecting every f(a) to g(a).

The construction from pushouts itself is an implementation detail, which is why the definition is marked abstract.

module _
  {l1 l2 : Level} (a : double-arrow l1 l2)
  where

  abstract
    standard-coequalizer : UU (l1 ⊔ l2)
    standard-coequalizer =
      pushout
        ( vertical-map-span-cocone-cofork a)
        ( horizontal-map-span-cocone-cofork a)

    cofork-standard-coequalizer : cofork a standard-coequalizer
    cofork-standard-coequalizer =
      cofork-cocone-codiagonal a
        ( cocone-pushout
          ( vertical-map-span-cocone-cofork a)
          ( horizontal-map-span-cocone-cofork a))

    dup-standard-coequalizer :
      dependent-universal-property-coequalizer a cofork-standard-coequalizer
    dup-standard-coequalizer =
      dependent-universal-property-coequalizer-dependent-universal-property-pushout
        ( a)
        ( cofork-standard-coequalizer)
        ( λ P →
          tr
            ( λ c →
              is-equiv
                ( dependent-cocone-map
                  ( vertical-map-span-cocone-cofork a)
                  ( horizontal-map-span-cocone-cofork a)
                  ( c)
                  ( P)))
            ( inv
              ( is-retraction-map-inv-is-equiv
                ( is-equiv-cofork-cocone-codiagonal a)
                ( cocone-pushout
                  ( vertical-map-span-cocone-cofork a)
                  ( horizontal-map-span-cocone-cofork a))))
            ( dup-pushout
              ( vertical-map-span-cocone-cofork a)
              ( horizontal-map-span-cocone-cofork a)
              ( P)))

    up-standard-coequalizer :
      universal-property-coequalizer a cofork-standard-coequalizer
    up-standard-coequalizer =
      universal-property-dependent-universal-property-coequalizer a
        ( cofork-standard-coequalizer)
        ( dup-standard-coequalizer)

Recent changes