Homotopy Type Theory shape > history (changes)

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

Contents

< shape modality

Definition

For a space SS, the shape esh(S)\esh(S) is defined as

esh(S)p *(p !(S))\esh(S) \coloneqq p^*(p_!(S))

where p *(T)p^*(T) is the discrete space of the homotopy type TT and p !(S)p_!(S) is the fundamental homotopy type of the space SS.

See also

Last revised on June 18, 2022 at 11:53:30. See the history of this page for a list of all contributions to it.