module Homotopy.Space.Suspension where


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
  : βˆ€ {β„“ β„“'} {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

  1. Diagrams are hard, okay?!β†©οΈŽ