open import 1Lab.Reflection.Induction
open import 1Lab.Prelude

module Homotopy.Space.Suspension where


# Suspensionπ

Given a type its (reduced) suspension 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 north and south poles of a sphere, respectively, and the name merid should evoke the meridians. Indeed, we can picture a suspension like a sphere1:

We have the north and south poles and above and below a copy of the space which is diagrammatically represented by the shaded region. In the type theory, we canβt really βseeβ this copy of 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 is then is Unfolding this a bit further, if is a type whose homotopy groups below are trivial, then will have trivial homotopy groups below