open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HIT.Suspension where


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.