Suspension (HIT)

Definition

The suspension $\Sigma A$ of a type $A$ is a Higher Inductive Type defined as the pushout of the terminal maps $1\leftarrow A\to 1$.

Constructors:

• $N:\Sigma A$ (north pole)
• $S:\Sigma A$ (south pole)
• $\mathrm{merid}:A\to (N=S)$ (meridian)

The suspension can be visualized as taking a type $A$ and placing it as the “equator” between two poles, with paths (meridians) connecting the north pole to the south pole through each point of $A$.

Properties

The suspension operation increases the dimension of a type by one in a homotopical sense. For example, the suspension of the circle $S^1$ is homotopy equivalent to the 2-sphere $S^2$.

Related Concepts

Higher Inductive Type Pushout (HIT) Spheres (HIT) Circle (HIT) Loop Space