Showing changes from revision #2 to #3:
Added | Removed | Changed
The suspension is the universal way to make points into paths.
The suspension of a type is a the typehigher inductive type with the following generators
The suspension of a type is a the homotopy pushout?pushout of .
These two definitions are equivalent.
Revision on September 4, 2018 at 09:17:51 by Ali Caglayan. See the history of this page for a list of all contributions to it.