suspension (Rev #3, changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

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

The suspension of a type $A$ is~~ a~~ the~~ type~~~~$\Sigma A$~~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)$

The suspension of a type $A$ is a the ~~homotopy pushout?~~pushout of $\mathbf 1 \leftarrow A \rightarrow \mathbf 1$.

These two definitions are equivalent.

category: homotopy theory

Revision on September 4, 2018 at 05:17:51 by Ali Caglayan. See the history of this page for a list of all contributions to it.