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

module Homotopy.Space.Suspension where

private variable
  ℓ : Level
  A B C : Type ℓ
  A∙ B∙ C∙ : Type∙ ℓ

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
  north : Susp A
  south : Susp A
  merid : A → north ≡ south

The names north and south 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.

Σ∙ : ∀ {ℓ} (A : Type ℓ) → Type∙ ℓ
Σ∙ A = Susp A , north

Σ¹ : ∀ {ℓ} → Type∙ ℓ → Type∙ ℓ
Σ¹ (A , _) = Σ∙ A

Susp-elim
  : ∀ {ℓ ℓ'} {A : Type ℓ} (P : Susp A → Type ℓ')
  → (pN : P north) (pS : P south)
  → (∀ x → PathP (λ i → P (merid x i)) pN pS)
  → ∀ x → P x
Susp-elim P pN pS pmerid north = pN
Susp-elim P pN pS pmerid south = pS
Susp-elim P pN pS pmerid (merid x i) = pmerid x i

unquoteDecl Susp-elim-prop = make-elim-n  Susp-elim-prop (quote Susp)

Every suspension admits a surjection from the booleans:

2→Σ : ∀ {ℓ} {A : Type ℓ} → Bool → Susp A
2→Σ true  = north
2→Σ false = south

2→Σ-surjective : is-surjective (2→Σ {A = A})
2→Σ-surjective = Susp-elim-prop (λ _ → hlevel )
  (inc (true , refl)) (inc (false , refl))

Suspension extends to a functor in the evident way.

Susp-map : (A → B) → Susp A → Susp B
Susp-map f north = north
Susp-map f south = south
Susp-map f (merid x i) = merid (f x) i

Susp-map∙ : (A∙ →∙ B∙) → Σ¹ A∙ →∙ Σ¹ B∙
Susp-map∙ (f , pt) = Susp-map f , refl

Susp-map∙-id : Susp-map∙ {A∙ = A∙} id∙ ≡ id∙
Susp-map∙-id = funext∙ (Susp-elim _ refl refl λ x i j → merid x i) refl

Susp-map∙-∘
  : (f : B∙ →∙ C∙) (g : A∙ →∙ B∙)
  → Susp-map∙ (f ∘∙ g) ≡ Susp-map∙ f ∘∙ Susp-map∙ g
Susp-map∙-∘ (f , _) (g , _) =
  funext∙ (Susp-elim _ refl refl (λ x i j → merid (f (g x)) i)) (sym (∙-idl _))

Susp-map∙-zero : Susp-map∙ (zero∙ {A = A∙} {B = B∙}) ≡ zero∙
Susp-map∙-zero {B∙ = B , b₀} =
  funext∙ (Susp-elim _ refl (sym (merid b₀)) λ a i j → merid b₀ (i ∧ ~ j)) refl

Susp-Maps∙ : Maps∙ A∙ B∙ →∙ Maps∙ (Σ¹ A∙) (Σ¹ B∙)
Susp-Maps∙ .fst = Susp-map∙
Susp-Maps∙ {A∙ = A∙} {B∙ = B∙} .snd = Susp-map∙-zero {A∙ = A∙} {B∙ = B∙}

Susp-ap : A ≃ B → Susp A ≃ Susp B
Susp-ap e .fst = Susp-map (e .fst)
Susp-ap e .snd = is-iso→is-equiv λ where
  .is-iso.from → Susp-elim _ north south (λ x → merid (Equiv.from e x))
  .is-iso.rinv → Susp-elim _ refl refl (λ x i j → merid (Equiv.ε e x j) i)
  .is-iso.linv → Susp-elim _ refl refl (λ x i j → merid (Equiv.η e x j) i)

Susp-ap∙ : A∙ ≃∙ B∙ → Σ¹ A∙ ≃∙ Σ¹ B∙
Susp-ap∙ (e , pt) .fst = Susp-ap e
Susp-ap∙ (e , pt) .snd = refl