Universal property of suspensions

Content created by Fredrik Bakke, Egbert Rijke and Raymond Baker.

Created on 2023-08-28.
Last modified on 2024-04-25.

module synthetic-homotopy-theory.universal-property-suspensions where
Imports 
open import foundation.constant-maps
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.unit-type
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.suspension-structures
open import synthetic-homotopy-theory.universal-property-pushouts

Idea

Since suspensions are just pushouts, they retain the expected universal property, which states that the map cocone-map is a equivalence. We denote this universal property by universal-property-pushout-suspension. But, due to the special nature of the span being pushed out, the suspension of a type enjoys an equivalent universal property, here denoted by universal-property-suspension. This universal property states that the map ev-suspension is an equivalence.

Definitions

The universal property of the suspension

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  (s : suspension-structure X Y)
  where

  ev-suspension :
    {l3 : Level} (Z : UU l3) → (Y → Z) → suspension-structure X Z
  pr1 (ev-suspension Z h) = h (north-suspension-structure s)
  pr1 (pr2 (ev-suspension Z h)) = h (south-suspension-structure s)
  pr2 (pr2 (ev-suspension Z h)) = h ·l meridian-suspension-structure s

  universal-property-suspension : UUω
  universal-property-suspension =
    {l : Level} (Z : UU l) → is-equiv (ev-suspension Z)

The universal property of the suspension at a universe level as a pushout

universal-property-pushout-suspension :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2)
  (s : suspension-structure X Y) → UUω
universal-property-pushout-suspension X Y s =
  universal-property-pushout
    ( terminal-map X)
    ( terminal-map X)
    ( suspension-cocone-suspension-structure s)

Properties

triangle-ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (s : suspension-structure X Y) →
  (Z : UU l3) →
  ( ( suspension-structure-suspension-cocone) ∘
    ( cocone-map
      ( terminal-map X)
      ( terminal-map X)
      ( suspension-cocone-suspension-structure s))) ~
  ( ev-suspension s Z)
triangle-ev-suspension (N , S , merid) Z h = refl

is-equiv-ev-suspension :
  { l1 l2 : Level} {X : UU l1} {Y : UU l2} →
  ( s : suspension-structure X Y) →
  universal-property-pushout-suspension X Y s →
  { l3 : Level} (Z : UU l3) → is-equiv (ev-suspension s Z)
is-equiv-ev-suspension {X = X} s up-Y Z =
  is-equiv-left-map-triangle
    ( ev-suspension s Z)
    ( suspension-structure-suspension-cocone)
    ( cocone-map
      ( terminal-map X)
      ( terminal-map X)
      ( suspension-cocone-suspension-structure s))
    ( inv-htpy (triangle-ev-suspension s Z))
    ( up-Y Z)
    ( is-equiv-suspension-structure-suspension-cocone)

Recent changes