Homotopy Type Theory
suspension

Idea

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

Definitions

Def 1

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

Def 2

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

These two definitions are equivalent.

References

category: homotopy theory