Homotopy Type Theory
suspension (changes)

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


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


Def 1

The suspension of a type AA is the higher inductive type ΣA\Sigma A with the following generators

  • A point N:ΣA\mathrm{N} : \Sigma A
  • A point S:ΣA\mathrm{S} : \Sigma A
  • A function merid:A(NN= ΣASS) \mathrm{merid} merid : A \to (N (\mathrm{N} =_{\Sigma A} S) \mathrm{S})

Def 2

The suspension of a type AA is a the pushout of 1A1\mathbf 1 \leftarrow A \rightarrow \mathbf 1.

These two definitions are equivalent.


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.