module Homotopy.Space.Suspension where

# Suspension🔗

Given a type `A`

, the type `Susp A`

is defined
by the property that `Susp A`

has two *poles* denoted
`N`

and `S`

and an `A`

-indexed family
of paths `N ≡ S`

.

data Susp {ℓ} (A : Type ℓ) : Type ℓ where N S : Susp A merid : A → N ≡ S

*TODO*: Draw a picture and explain!

Suspension is an operation that increases the connectivity of a type: suspending an empty type makes it inhabited, suspending an inhabited type makes it connected, suspending a connected type makes it 1-connected, etc.