module Homotopy.Space.Suspension where

# Suspensionπ

Given a type
$A,$
its **(reduced) suspension**
$Ξ£A$
is the higher-inductive type generated by the following
constructors:

data Susp {β} (A : Type β) : Type β where N S : Susp A merid : A β N β‘ S

The names `N`

and `S`

are meant to
evoke the *n*orth and *s*outh poles of a sphere,
respectively, and the name `merid`

should evoke
the *merid*ians. Indeed, we can picture a suspension like a
sphere^{1}:

We have the north and south poles
$N$
and
$S$
above and below a copy of the space
$A,$
which is diagrammatically represented by the shaded region. In the type theory, we canβt really
βseeβ this copy of
$A:$
we only see its *ghost*, as something keeping all the meridians
from collapsing.

By convention, we see the suspension as a pointed type with the
*north* pole as the base point.

Suspβ : β {β} (A : Type β) β Typeβ β Suspβ A = Susp A , N

Susp-elim : β {β β'} {A : Type β} (P : Susp A β Type β') β (pN : P N) (pS : P S) β (β x β PathP (Ξ» i β P (merid x i)) pN pS) β β x β P x Susp-elim P pN pS pmerid N = pN Susp-elim P pN pS pmerid S = pS Susp-elim P pN pS pmerid (merid x i) = pmerid x i unquoteDecl Susp-elim-prop = make-elim-n 1 Susp-elim-prop (quote Susp)

Every suspension admits a surjection from the booleans:

2βΞ£ : β {β} {A : Type β} β Bool β Susp A 2βΞ£ true = N 2βΞ£ false = S 2βΞ£-surjective : β {β} {A : Type β} β is-surjective (2βΞ£ {A = A}) 2βΞ£-surjective = Susp-elim-prop (Ξ» _ β hlevel 1) (inc (true , refl)) (inc (false , refl))

The suspension operation increases the connectedness of spaces: if $A$ is $n-connected,$ then $Ξ£A$ is $(1+n)-connected.$ Unfolding this a bit further, if $A$ is a type whose homotopy groups below $n$ are trivial, then $Ξ£A$ will have trivial homotopy groups below $1+n.$

Diagrams are hard, okay?!β©οΈ