#
Homotopy Type Theory
shape > history (changes)

Showing changes from revision #4 to #5:
Added | ~~Removed~~ | ~~Chan~~ged

# Contents

< shape modality

~~
~~## Definition

~~
~~For a space $S$, the **shape** $\esh(S)$ is defined as

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

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

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