# Universal property of suspensions ```agda module synthetic-homotopy-theory.universal-property-suspensions where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea Since suspensions are just [pushouts](synthetic-homotopy-theory.pushouts.md), they retain the expected [universal property](synthetic-homotopy-theory.universal-property-pushouts.md), 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 ```agda 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 ```agda 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 ```agda 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) ```