Universal property of suspensions

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

Created on 2023-08-28.
Last modified on 2023-11-09.

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

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-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.

Definition

The universal property of the suspension as a pushout

universal-property-suspension' :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2)
  (s : suspension-structure X Y) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension' l X Y s =
  universal-property-pushout l
    ( const X unit star)
    ( const X unit star)
    ( cocone-suspension-structure X Y s)

is-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (lsuc l ⊔ l1 ⊔ l2)
is-suspension l X Y =
  Σ (suspension-structure X Y) (universal-property-suspension' l X Y)

The universal property of the suspension reforum

ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  (s : suspension-structure X Y) →
  (Z : UU l3) → (Y → Z) → suspension-structure X Z
ev-suspension (pair N (pair S merid)) Z h =
  pair (h N) (pair (h S) (h ·l merid))

universal-property-suspension :
  (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) →
  suspension-structure X Y → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-suspension l X Y s =
  (Z : UU l) → is-equiv (ev-suspension s Z)

Properties

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

is-equiv-ev-suspension :
  { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} →
  ( s : suspension-structure X Y) →
  ( up-Y : universal-property-suspension' l3 X Y s) →
  ( 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)
    ( map-equiv-suspension-structure-suspension-cocone X Z)
    ( cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X _ s))
    ( inv-htpy (triangle-ev-suspension s Z))
    ( up-Y Z)
    ( is-equiv-map-equiv-suspension-structure-suspension-cocone X Z)

Recent changes