# nLab n-truncation modality

Contents

### Context

#### Higher category theory

higher category theory

# Contents

## 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) }$

$\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.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level $n+2$$n$-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-$n$-groupoid
h-level $\infty$untruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-$\infty$-groupoid

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

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

Discussion of $n$-truncation as a modality:

and in addition via lifting properties against n-spheres:

Earlier discussion (and in view of homotopy levels):

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

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

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