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

module Homotopy.Space.Suspension where

Suspension🔗

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

We have the north and south poles $N$ and $S$ above and below a copy of the space $A\text{,}$ which is diagrammatically represented by the shaded region. In the type theory, we can’t really “see” this copy of $A\text{:}$ 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\text{-connected,}$ then $\Sigma A$ is $(1+n)\text{-connected.}$ Unfolding this a bit further, if $A$ is a type whose homotopy groups below $n$ are trivial, then $\Sigma A$ will have trivial homotopy groups below $1+n\text{.}$