natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
For all $n \in \{-2, -1, 0,1,2,3, \cdots\}$, $n$-truncation is a modality (in homotopy type theory).
The following applies to dependent type theory with suspension types and localizations, such as to standard homotopy type theory.
Recall:
($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.
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}$
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.
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):
$(-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
and this is a 1-epimorphism precisely if the law of excluded middle holds.
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 |
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):
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:
Last revised on April 17, 2023 at 07:15:09. See the history of this page for a list of all contributions to it.