Homotopy Type Theory suspension > history (Rev #2)

Definitions

Def 1

The suspension of a type AA is a 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(N= ΣAS)\mathrm{merid} : A \to (N =_{\Sigma A} S)

Def 2

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

These two definitions are equivalent.

category: homotopy theory

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