{-# OPTIONS --hidden-argument-puns #-}
open import 1Lab.Prelude

open import Homotopy.Space.Suspension

module Homotopy.Pushout where

private variable
  ℓ ℓ' ℓ'' : Level
  A B C X : Type ℓ

Pushouts🔗

Given the following span:

The pushout of this span is defined as the higher inductive type presented by:

data Pushout (C : Type ℓ) (f : C → A) (g : C → B) : Type (level-of A ⊔ level-of B ⊔ ℓ) where
  inl  : A → Pushout C f g
  inr  : B → Pushout C f g
  glue : ∀ c → inl (f c) ≡ inr (g c)

These combine to give the following:

Suspensions as pushouts🔗

The suspension of a type $A$ can be expressed as the Pushout of the span $⊤ \leftarrow A \to ⊤ :$

There is only one element of ⊤, and hence only one choice for the function projecting into ⊤ - const tt.

If one considers the structure we’re creating, it becomes very obvious that this is equivalent to suspension - because both of our non-path constructors have input ⊤, they’re indistinguishable from members of the pushout; therefore, we take the inl and inr to N and S respectively. Likewise, we take glue to merid.

Susp→Pushout-⊤←A→⊤ : Susp A → Pushout A (λ _ → tt) (λ _ → tt)
Susp→Pushout-⊤←A→⊤ north       = inl tt
Susp→Pushout-⊤←A→⊤ south       = inr tt
Susp→Pushout-⊤←A→⊤ (merid x i) = glue x i

Pushout-⊤←A→⊤-to-Susp : Pushout A (λ _ → tt) (λ _ → tt) → Susp A
Pushout-⊤←A→⊤-to-Susp (inl tt)   = north
Pushout-⊤←A→⊤-to-Susp (inr tt)   = south
Pushout-⊤←A→⊤-to-Susp (glue c i) = merid c i

So we then have:

Susp≃pushout : Susp A ≃ Pushout A (λ _ → tt) (λ _ → tt)
Susp≃pushout = (Susp→Pushout-⊤←A→⊤ , is-iso→is-equiv iso-pf) where

We then verify that our two functions above are in fact inverse equivalences. This is entirely refl, due to the noted similarities in structure.

  open is-iso

  iso-pf : is-iso Susp→Pushout-⊤←A→⊤
  iso-pf .from = Pushout-⊤←A→⊤-to-Susp
  iso-pf .rinv (inl x)    = refl
  iso-pf .rinv (inr x)    = refl
  iso-pf .rinv (glue c i) = refl

  iso-pf .linv north       = refl
  iso-pf .linv south       = refl
  iso-pf .linv (merid x i) = refl

The universal property of pushouts🔗

To formulate the universal property of a pushout, we first introduce cocones. A Cocone, given a type D and a span:

consists of functions $i : A \to D,$ $j : B \to D,$ and a homotopy $h : (c : C) \to i (f c) \equiv j (g c),$ forming:

One can then note the similarities between this definition, and our previous Pushout definition. We define the type of Cocones as:

Cocone : {C A B : Type} → (f : C → A) → (g : C → B) → (D : Type) → Type
Cocone {C} {A} {B} f g D =
  Σ[ i ∈ (A → D) ]
  Σ[ j ∈ (B → D) ]
  ((c : C) → i (f c) ≡ j (g c))

We can then show that the canonical Cocone consisting of a Pushout is the universal Cocone.

Pushout-is-universal-cocone
  : ∀ {f : C → A} {g : C → B} → (Pushout C f g → X) ≃ Cocone f g X
Pushout-is-universal-cocone {C} {X} {f} {g} = to , is-iso→is-equiv iso-pc where

Once again we show that the above is an equivalence; this proof is essentially a transcription of Lemma 6.8.2 in the HoTT book, and again mostly reduces to refl.

  open is-iso

  to : (Pushout C f g → X) → Cocone f g X
  to t = t ∘ inl , t ∘ inr , ap t ∘ glue

  iso-pc : is-iso to
  iso-pc .from (l , r , g) (inl x)    = l x
  iso-pc .from (l , r , g) (inr x)    = r x
  iso-pc .from (l , r , g) (glue c i) = g c i

  iso-pc .rinv _ = refl
  iso-pc .linv _ = funext λ where
    (inl y) → refl
    (inr y) → refl
    (glue c i) → refl