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
  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 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.

Σ∙ :  {} (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 1 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 1)
  (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

  1. Diagrams are hard, okay?!↩︎