Truncation

Idea

In Homotopy Type Theory, truncation refers to collapsing higher homotopy groups of a type. An n-truncated type has trivial homotopy groups above dimension $n$.

Definition

1. $X$ is n-truncated (i.e., all homotopy groups above degree $n$ vanish; equivalently, for all $xy:X$, the identity type $(x\equiv y)$ is $(n-1)$-truncated).
2. For every base point $x_0:X$, the $(n+1)$-fold loop space ${\Omega }^{n+1}(X,x_0)$ is contractible.
3. For every base point $x_0:X$, the type of pointed maps $S^{n+1}{\to }_{\ast }(X,x_0)$ is contractible (every pointed map is homotopic to the constant map at $x_0$).

Levels

• $(-2)$-truncated: Contractible types
• $(-1)$-truncated: Propositions (mere propositions)
• $0$-truncated: Sets (hSet)
• $1$-truncated: Groupoids

Propositional Truncation

The propositional truncation $\Vert A\Vert$ of a type $A$ is the $(-1)$-truncation, which forgets all information except whether $A$ is inhabited. This operation:

• Preserves inhabitation: if $A$ is inhabited, so is $\Vert A\Vert$
• Makes the result proof-irrelevant: any two elements of $\Vert A\Vert$ are equal
• Is used to express existence without providing a specific witness

Related Concepts

• Homotopy Level: The classification of types by truncation level
• Type Theory: The formal system where truncation is precisely defined
• Higher Inductive Type: Used to construct truncation operations

Sources

https://ncatlab.org/nlab/show/suspension+type hott2013-book