Universal property of suspensions

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

Created on 2023-08-28.

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)