[[!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 $merid : A \to (\mathrm{N} =_{\Sigma A} \mathrm{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