Truncations and truncated higher inductive types

Homotopy Type Theory

Truncation is a homotopy-theoretic construction that given a space $latex A$ and an integer n returns an n-truncated space $latex tau_{le{}n}A$ together with a map $latex p:Atotau_{le{}n}A$ in an universal way. More precisely, if i is the inclusion of n-truncated spaces into spaces, then n-truncation is left adjoint to i. ($latex tau_{le{}n}A$ is the free n-truncated space built from $latex A$).

Moreover, the notion of truncated object is something already known in homotopy type theory: a type is n-truncated precisely if it is of h-level n+2.

Truncations are very useful in homotopy theory, and are also useful for foundations of mathematics, especially for n=-1,0:

  • The (-1)-truncation is also known as isinhab: given a type A it returns a proposition isinhab A which is true if and only if A is inhabited (by « proposition » and « set » I will always mean « h-proposition » and…

View original post 1 740 mots de plus