Homotopy Type Theory suspension > history (Rev #3)

Idea

The suspension is the universal way to make points into paths.

Definitions

Def 1

The suspension of a type $A$ is the higher inductive type $\Sigma A$ with the following generators

• A point $\mathrm{N} : \Sigma A$
• A point $\mathrm{S} : \Sigma A$
• A function $\mathrm{merid} : A \to (N =_{\Sigma A} S)$

Def 2

The suspension of a type $A$ is a the pushout of $\mathbf 1 \leftarrow A \rightarrow \mathbf 1$.

These two definitions are equivalent.

References