## Definitions ## ### Def 1 ### The suspension of a type $A$ is a 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 [[homotopy pushout]] of $\mathbf 1 \leftarrow A \rightarrow \mathbf 1$. These two definitions are equivalent.