The suspension is the universal way to make points into paths.
The suspension of a type is the higher inductive type with the following generators
The suspension of a type is a the pushout of .
These two definitions are equivalent.
Last revised on September 4, 2018 at 05:48:52. See the history of this page for a list of all contributions to it.