Pushouts

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Raymond Baker.

Created on 2022-07-29.
Last modified on 2023-09-10.

module synthetic-homotopy-theory.pushouts where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.26-descent
open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-universal-property-pushouts
open import synthetic-homotopy-theory.universal-property-pushouts

Idea

Consider a span 𝒮 of types

      f     g
  A <--- S ---> B.

A pushout of 𝒮 is an initial type X equipped with a cocone structure of 𝒮 in X. In other words, a pushout X of 𝒮 comes equipped with a cocone structure (i , j , H) where

        g
    S -----> B
    |        |
  f |   H    | j
    V        V
    A -----> X,
        i

such that for any type Y, the following evaluation map is an equivalence

  (X → Y) → cocone 𝒮 Y.

This condition is the universal property of the pushout of 𝒮.

The idea is that the pushout of 𝒮 is the universal type that contains the elements of the types A and B via the 'inclusions' i : A → X and j : B → X, and furthermore an identification i a ＝ j b for every s : S such that f s ＝ a and g s ＝ b.

Examples of pushouts include suspensions, spheres, joins, and the smash product.

Postulates

We will assume that for any span

      f     g
  A <--- S ---> B,

where S : UU l1, A : UU l2, and B : UU l3 there is a pushout in UU (l1 ⊔ l2 ⊔ l3).

postulate
  pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) → UU (l1 ⊔ l2 ⊔ l3)

postulate
  inl-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) → A → pushout f g

postulate
  inr-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) → B → pushout f g

postulate
  glue-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) → ((inl-pushout f g) ∘ f) ~ ((inr-pushout f g) ∘ g)

cocone-pushout :
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) → cocone f g (pushout f g)
pr1 (cocone-pushout f g) = inl-pushout f g
pr1 (pr2 (cocone-pushout f g)) = inr-pushout f g
pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g

postulate
  up-pushout :
    {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S → A) (g : S → B) →
    universal-property-pushout l4 f g (cocone-pushout f g)

equiv-up-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) (X : UU l4) → (pushout f g → X) ≃ (cocone f g X)
pr1 (equiv-up-pushout f g X) = cocone-map f g (cocone-pushout f g)
pr2 (equiv-up-pushout f g X) = up-pushout f g X

Definitions

The cogap map

cogap :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) →
  { X : UU l4} → cocone f g X → pushout f g → X
cogap f g {X} = map-inv-equiv (equiv-up-pushout f g X)

The is-pushout predicate

is-pushout :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
is-pushout f g c = is-equiv (cogap f g c)

Properties

The pushout of a span has the dependent universal property

module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  where

  dependent-up-pushout :
    (f : S → A) (g : S → B) →
    dependent-universal-property-pushout l4 f g (cocone-pushout f g)
  dependent-up-pushout f g =
    dependent-universal-property-universal-property-pushout
    ( f)
    ( g)
    ( cocone-pushout f g)
    ( λ l → up-pushout f g)
    ( l4)

Computation with the cogap map

module _
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  ( f : S → A) (g : S → B)
  { X : UU l4} (c : cocone f g X)
  where

  private
    htpy-cc =
      htpy-cocone-map-universal-property-pushout
        ( f)
        ( g)
        ( cocone-pushout f g)
        ( up-pushout f g)
        ( c)

  compute-inl-cogap :
    ( a : A) → cogap f g c (inl-pushout f g a) ＝ horizontal-map-cocone f g c a
  compute-inl-cogap = pr1 htpy-cc

  compute-inr-cogap :
    ( b : B) → cogap f g c (inr-pushout f g b) ＝ vertical-map-cocone f g c b
  compute-inr-cogap = pr1 (pr2 htpy-cc)

  compute-glue-cogap :
    ( s : S) →
    ( ap (cogap f g c) (glue-pushout f g s)) ＝
    ( ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) ∙
      ( inv (compute-inr-cogap (g s))))
  compute-glue-cogap s =
    right-transpose-eq-concat
      ( ap (cogap f g c) (glue-pushout f g s))
      ( compute-inr-cogap (g s))
      ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s)
      ( pr2 (pr2 htpy-cc) s)

Recent changes