open import 1Lab.Path open import 1Lab.Type module 1Lab.HIT.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.