⚠️ This module is not part of this project and is only included for reference.
It is either part of the 1lab, the cubical library, or a built-in Agda module.
<!--
```
open import 1Lab.Reflection.Induction
open import 1Lab.Prelude
```
-->
```agda
module Homotopy.Space.Suspension where
```
# Suspension {defines="suspension"}
Given a type $A$, its **(reduced) suspension** $\Susp A$ is the
higher-inductive type generated by the following constructors:
```agda
data Susp {ℓ} (A : Type ℓ) : Type ℓ where
N S : Susp A
merid : A → N ≡ S
```
The names `N`{.Agda} and `S`{.Agda} are meant to evoke the *n*orth and
*s*outh poles of a sphere, respectively, and the name `merid`{.Agda}
should evoke the *merid*ians. Indeed, we can picture a suspension like a
sphere[^diamond]:
[^diamond]: Diagrams are hard, okay?!
~~~{.quiver}
\begin{tikzpicture}
\node[draw,circle,fill,minimum width=1.2pt,inner sep=0,outer sep=2pt,label={[right,yshift=-2.6pt]\tiny N}] (N) at (0,+1.25) {};
\node[draw,circle,fill,minimum width=1.2pt,inner sep=0,outer sep=2pt,label={[right,yshift=-2.6pt]\tiny S}] (S) at (0,-1.25) {};
\coordinate (L) at (-0.8,0);
\coordinate (R) at (+0.8,0);
\coordinate (T) at (+0.25,+0.525);
\coordinate (B) at (-0.25,-0.525);
\filldraw[fill=diagramshaded] (T) -- (R) -- (B) -- (L) -- (T);
\draw (N) -- (L);
\draw (N) -- (R);
\draw (N) -- (B);
\draw[dashed] (N) -- (T);
\draw (S) -- (L);
\draw (S) -- (R);
\draw (S) -- (B);
\node[color=diagramshadedtext] (A) at (0,0) {\tiny $A$};
\end{tikzpicture}
~~~
We have the north and south poles $N$ and $S$ above and below a copy of
the space $A$, which is diagrammatically represented by the <span
class=shaded>shaded</span> region. In the type theory, we can't really
"see" this copy of $A$: 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.
```agda
Susp∙ : ∀ {ℓ} (A : Type ℓ) → Type∙ ℓ
Susp∙ A = Susp A , N
```
```agda
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:
```agda
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|connectedness of suspensions]] the
[[connectedness]] of spaces: if $A$ is $n$-connected, then $\Susp A$ is
$(1+n)$-connected. Unfolding this a bit further, if $A$ is a type whose
homotopy groups below $n$ are trivial, then $\Susp A$ will have trivial
homotopy groups below $1 + n$.