# Homotopy Type Theory suspension (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## 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.

category: homotopy theory

Revision on August 25, 2018 at 20:12:56 by Anonymous?. See the history of this page for a list of all contributions to it.