# Homotopy Type Theory suspension (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## 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  \mathrm{merid} merid : A \to (N (\mathrm{N} =_{\Sigma A} S) \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

Last revised on September 4, 2018 at 05:48:52. See the history of this page for a list of all contributions to it.