nLab n-truncation modality

Idea

For all $n \in \{-2, -1, 0,1,2,3, \cdots\}$, $n$-truncation is a modality (in homotopy type theory).

Definition

The following applies to dependent type theory with suspension types and localizations, such as to standard homotopy type theory.

Recall:

Definition

($n$-sphere type $S^n$)

• $S^{-1}$ is the empty type,

• $S^0$ (the 0-sphere) is the boolean domain type

• $S^{n+1} \,\coloneqq\, \Sigma S^n$ is the suspension type of the sphere type of dimension lower.

As nullification of the $n+1$-sphere

The $n$-truncation modality may also be defined to be the localization at the unique function from the $(n + 1)$-dimensional sphere type (Def. ) to the unit type $S^{n + 1} \to \mathbb{1}$

$$\left[A\right]_n \coloneqq L_{S^{n + 1}}(A)$$

By definition, the type of functions $(\mathbb{1} \to \left[A\right]_n) \to (S^{n + 1} \to \left[A\right]_n)$ is an equivalence of types.

Explicit inference rules

The following are the inference rules for the $n$-truncation $[X]_n$ of a given $X \,\colon\, Type$ regarded as a higher inductive type according to UFP13, §7.3, p. 223 (the diagram indicates the categorical semantics, for orientation):

type formation rule:

$$\frac{ X \,\colon\, Type \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} [X]_n \,\colon\, Type }$$

term introduction rule:

$$\frac{ x \,\colon\, X \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} \eta_X(x) \,\colon\, [X]_n } \;\;\;\;\;\;\;\;\; \frac{ \phi \,\colon\, S^{n+1} \to [X]_n \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} hub_X^{\phi} \,\colon\, [X]_n } \;\;\;\;\;\;\;\;\; \frac{ \phi \,\colon\, S^{n+1} \to [X]_n \;; \;\;\; s \,\colon\, S^{n+1} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} hmt_X^{\phi}(s) \,\colon\, Id_{[X]_n}\big( \phi(s) ,\, hub_X^{\phi} \big) }$$

term elimination rules:

$$\frac{ \begin{array}{l} \overline{x} \,\colon\, [X]_n \;\vdash\; D(\overline{x}) \,\colon\, Type \;; \\ x \,\colon\, X \;\vdash\; \eta_D(x) \,\colon\, D\big( \eta_X(x) \big) \;; \\ \phi \,\colon\, S^{n+1} \to [X]_n \,, \; \phi_D \,\colon\, \underset{s \,\colon\,S^{n+1}}{\prod} \, D\big( \phi(s) \big) \;\;\vdash\;\; hub^{\phi_D}_D \,\colon\, D\big( hub_X^\phi \big) \;; \\ \phi \,\colon\, S^{n+1} \to [X]_n \,, \; \phi_D \,\colon\, \underset{s \,\colon\,S^{n+1}}{\prod} \, D\big( \phi(s) \big) \,, \; s \,\colon\, S^{n+1} \;\;\vdash\;\; hmt_D^{\phi_D}(s) \,\colon\, Id_{D\big(hub_X^{\phi}\big)}\Big( \big(hmt^{\phi}_X(s)\big)_\ast \phi_D(s) ,\, hub_D^{\phi_D} \Big) \mathclap{\phantom{\vert^{\vert^{\vert}}}} \end{array} }{ \mathclap{\phantom{\vert^{\vert_{\vert}}}} ind_{\big(D,\,\eta_D,\, hub_D,\, hmt_D \big)} \,\colon\, \underset{\overline{x}\colon [X]_n}{\prod} \, D(\overline{x}) }$$

computation rule:

$$ind_{\big(D,\,\eta_D,\, hub_D,\, hmt_D \big)} \big( \eta(x) \big) \;=\; \eta_D(x)$$

Properties

In low degree

$(-2)$-truncation is the unit type modality (constant on the unit type).

$(-1)$-truncation is given by forming bracket types, turning types into genuine propositions.

Classically, this is the same as the double negation modality; in general, the bracket type ${\|A\|_{-1}}$ only entails the double negation $\neg(\neg{A})$:

there is a canonical function

$${\|A\|_{-1}} \longrightarrow \neg(\neg{A})$$

and this is a 1-epimorphism precisely if the law of excluded middle holds.

Related concepts

• decategorification, core

• cone type, bracket type, set truncation

homotopy level	n-truncation	homotopy theory	higher category theory	higher topos theory	homotopy type theory
h-level 0	(-2)-truncated	contractible space	(-2)-groupoid		true/​unit type/​contractible type
h-level 1	(-1)-truncated	contractible-if-inhabited	(-1)-groupoid/​truth value	(0,1)-sheaf/​ideal	mere proposition/​h-proposition
h-level 2	0-truncated	homotopy 0-type	0-groupoid/​set	sheaf	h-set
h-level 3	1-truncated	homotopy 1-type	1-groupoid/​groupoid	(2,1)-sheaf/​stack	h-groupoid
h-level 4	2-truncated	homotopy 2-type	2-groupoid	(3,1)-sheaf/​2-stack	h-2-groupoid
h-level 5	3-truncated	homotopy 3-type	3-groupoid	(4,1)-sheaf/​3-stack	h-3-groupoid
h-level $n+2$	$n$-truncated	homotopy n-type	n-groupoid	(n+1,1)-sheaf/​n-stack	h-$n$-groupoid
h-level $\infty$	untruncated	homotopy type	∞-groupoid	(∞,1)-sheaf/​∞-stack	h-$\infty$-groupoid

References

Construction of $n$-truncation as a one-step higher inductive type in homotopy type theory:

• Univalent Foundations Project, §6.9 & §7.3 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

Alternative construction of $n$-truncation as an iterated pushout type is (somewhat implicit) in:

• Egbert Rijke, Section 7.2 (culminating in Thm. 7.2.10) of: Classifying Types [arXiv:1906.09435]

Discussion of $n$-truncation as a modality:

• Egbert Rijke, Mike Shulman, Bas Spitters, Exp. 1.6 in: Modalities in homotopy type theory, Logical Methods in Computer Science, 16 1 (2020) [arXiv:1706.07526, doi:10.23638/LMCS-16(1:2)2020]

and in addition via lifting properties against n-spheres:

• Felix Cherubini, Egbert Rijke, Thm. 3.10 in: Modal Descent, Mathematical Structures in Computer Science 31 4 (2021) 363-391 [arXiv:2003.09713, doi:10.1017/S0960129520000201]

Earlier discussion (and in view of homotopy levels):

• Nicolai Kraus, Def. 2.3.8 in: Truncation levels in Homotopy Type Theory, Nottingham (2015) [pdf, eprints:28986]

Precursor discussion of the material that became UFP (2013, §7.3):

• Peter LeFanu Lumsdaine, Reducing all HIT’s to 1-HIT’s (May 2012) [blog posy]

• Guillaume Brunerie, Truncations and higher inductive types (September 2012) [blog post]

and precursur discussion of the material that became RSS (2020):

• Mike Shulman, Higher modalities, talk at UF-IAS-2012 (October 2012) [pdf]

• Mike Shulman, All modalities are Higher Inductive Types (November 2012) [blog post]

Considering the combination of $n$-truncation modality and shape modality:

• David Jaz Myers, Def. 3.0.1 in: Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory (arXiv:2205.15887)