<!--
```
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$.
