nLab n-truncation modality

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

judgement
hypothetical judgement, sequent
- antecedents $\vdash$ consequent, succedents

type theory (dependent, intensional, observational type theory, homotopy type theory)

calculus of constructions

syntax object language

theory, axiom
proposition/type (propositions as types)
definition/proof/program (proofs as programs)
theorem

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logic	set theory (internal logic of)	category theory	type theory
proposition	set	object	type
predicate	family of sets	display morphism	dependent type
proof	element	generalized element	term/program
cut rule		composition of classifying morphisms / pullback of display maps	substitution
introduction rule for implication		counit for hom-tensor adjunction	lambda
elimination rule for implication		unit for hom-tensor adjunction	application
cut elimination for implication		one of the zigzag identities for hom-tensor adjunction	beta reduction
identity elimination for implication		the other zigzag identity for hom-tensor adjunction	eta conversion
true	singleton	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	empty set	initial object	empty type
proposition, truth value	subsingleton	subterminal object/(-1)-truncated object	h-proposition, mere proposition
logical conjunction	cartesian product	product	product type
disjunction	disjoint union (support of)	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	function set (into subsingleton)	internal hom (into subterminal object)	function type (into h-proposition)
negation	function set into empty set	internal hom into initial object	function type into empty type
universal quantification	indexed cartesian product (of family of subsingletons)	dependent product (of family of subterminal objects)	dependent product type (of family of h-propositions)
existential quantification	indexed disjoint union (support of)	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
logical equivalence	bijection set	object of isomorphisms	equivalence type
	support set	support object/(-1)-truncation	propositional truncation/bracket type
		n-image of morphism into terminal object/n-truncation	n-truncation modality
equality	diagonal function/diagonal subset/diagonal relation	path space object	identity type/path type
completely presented set	set	discrete object/0-truncated object	h-level 2-type/set/h-set
set	set with equivalence relation	internal 0-groupoid	Bishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
	equivalence class/quotient set	quotient	quotient type
induction		colimit	inductive type, W-type, M-type
higher induction		higher colimit	higher inductive type
-		0-truncated higher colimit	quotient inductive type
coinduction		limit	coinductive type
	preset		type without identity types
	set of truth values	subobject classifier	type of propositions
domain of discourse	universe	object classifier	type universe
modality		closure operator, (idempotent) monad	modal type theory, monad (in computer science)
linear logic		(symmetric, closed) monoidal category	linear type theory/quantum computation
proof net		string diagram	quantum circuit
(absence of) contraction rule		(absence of) diagonal	no-cloning theorem
		synthetic mathematics	domain specific embedded programming language

homotopy levels

semantics

Edit this sidebar

As nullification of the $n+1$ -sphere
Explicit inference rules

Properties

In low degree

Related concepts
References

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

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)

Last revised on February 20, 2024 at 12:44:33. See the history of this page for a list of all contributions to it.

nLab n-truncation modality

Context

Type theory

Higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Contents

Idea

Definition

Definition

As nullification of the $n+1$ -sphere

Explicit inference rules

Properties

In low degree

Related concepts

References

nLab n-truncation modality

Context

Type theory

Higher category theory

Basic concepts

Basic theorems

Applications

Models

Morphisms

Functors

Universal constructions

Extra properties and structure

1-categorical presentations

Contents

Idea

Definition

Definition

As nullification of the n+1n+1-sphere

Explicit inference rules

Properties

In low degree

Related concepts

References

As nullification of the $n+1$ -sphere