[[!redirects Suspension]] ## 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 ## category: homotopy theory