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.