nLab set truncation

Idea

Set truncation is an operation in type theory which turns a type into an h-set. The idea is that given a type $T$, the type of connected components of $T$ is a set.

Definition

With propositional truncations and quotient sets

Suppose that the dependent type theory has propositional truncations and quotient sets. Then given a type $T$, the type family $R(x, y)$ indexed by $x:T$ and $y:T$ defined by the propositional truncation of the identity type of $T$, $R(x, y) \equiv [\mathrm{Id}_T(x, y)]_{-1}$ is an equivalence relation. The set truncation of $T$ is the quotient set of $T$ by $R$: $[T]_0 \equiv T / R$.

With localizations and the circle type

Suppose that dependent type theory has localizations of types and the circle type $S^1$. Then the set truncation of a type $T$ is the localization of $T$ at $S^1$: $[T]_0 \equiv L_{S^1}(T)$

As a higher inductive type

As a higher inductive type, the set truncation of a type $A$ is a type $[A]_0$ inductively generated by

• A function $[-]_0:A \to [A]_0$

• For each point $x:[A]_0$ and path $p:x =_{[A]_0} x$, a 2-path $K_{[A]_0}(x, p):p =_{x =_{[A]_0} x} \mathrm{refl}_A(x)$

Equivalently, it is the higher inductive type generated by

• A function $[-]_0:A \to [A]_0$

• For each function $f:S^1 \to [A]_0$ from the circle type, a 2-path $K_f:\mathrm{ap}_f(\mathrm{loop}) =_{f(\mathrm{base}) =_{[A]_0} f(\mathrm{base})}\mathrm{ap}_f(\mathrm{refl}_{S^1}(\mathrm{base}))$

Definitional set truncations

There are also definitional or judgmental versions of set truncations, similar to how there are definitional and propositional versions of bracket types and squash types:

The definitional set truncation or judgmental set truncation of a type $A$ is a type $[A]_0$ inductively generated by

• A function $[-]_0:A \to [A]_0$

• For each point $x:[A]_0$ and path $p:x =_{[A]_0} x$, a definitional equality $p \equiv \mathrm{refl}_{[A]_0}(x):x =_{[A]_0} x$

The recursion principle of definitional set truncations says that given a type $B$ with

• A function $f:A \to B$

• For each point $y:B$ and path $q:y =_{B} y$, a definitional equality $q \equiv \mathrm{refl}_B(y):y =_{B} y$

there exists a unique function $u_B:[A]_0 \to B$ such that $u_B([a]_0) = f(a)$ for all $a:A$.

Equivalently, the definitional set truncation of a type $A$ is generated by

• A function $[-]_0:A \to [A]_0$

• For each function $l:S^1 \to [A]_0$ from the circle type, a definitional equality

$$\mathrm{ap}_l(\mathrm{loop}) \equiv \mathrm{ap}_l(\mathrm{refl}_{S^1}(\mathrm{base})):l(\mathrm{base}) =_{[A]_0} l(\mathrm{base})$$

Similarly, the recursion principle of this kind of definitional set truncations says that given a type $B$ with

• A function $f:A \to B$

• For each function $l_f:S^1 \to B$ from the circle type, a definitional equality

$$\mathrm{ap}_{l_f}(\mathrm{loop}) \equiv \mathrm{ap}_{l_f}(\mathrm{refl}_{S^1}(\mathrm{base})):l_f(\mathrm{base}) =_{B} l_f(\mathrm{base})$$

there exists a unique function $u_B:[A]_0 \to B$ such that $u_B([a]_0) = f(a)$ for all $a:A$.

Inference rules for set truncations

Formation rules for set truncations:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash [A]_0 \; \mathrm{type}}$$

Introduction rules for set truncations:

$$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{settrunc}_A:A \to [A]_0 \; \mathrm{type}}$$

Dependent universal property of set truncations:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:[A]_0 \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{dup}_{[A]_0}^{B}:\left(\prod_{x:[A]_0} \mathrm{isSet}(B(x))\right) \to \mathrm{isEquiv}\left(\lambda f:\prod_{x:[A]_0} B(x).f \circ \mathrm{settrunc}_A\right)}$$

With a choice of unique representatives

A choice of unique representatives for propositional truncation consists of a type family $C(x)$ indexed by $x:A$, and an element of type

$$\prod_{x:A} \exists!y:A.C(x) \times [x =_A y]$$

Then the type $\sum_{x:A} C(x)$ is the set truncation of $A$.

Equivalently, one could use functions instead of type families, and say that a choice of unique representatives is a type $C$ with a function $f:C \to A$ and an element of type

$$\prod_{x:A} \exists!y:A.\left(\sum_{z:C} f(z) =_A x\right) \times [x =_A y]$$

Then

$$C \simeq \sum_{x:A} \sum_{z:C} f(z) =_A x$$

is the set truncation of $A$.

Properties

 Universal property of set truncations

The universal property of set truncations says that given a type $A$, a set $B$, and a function $f:A \to B$, there exists a unique function $u:[A] \to B$ such that for all $x:A$, $f(x) = u([x]_0)$.

Power sets

Given a type $A$ and a subtype $P:A \to \mathrm{Prop}$, by propositional extensionality and the universal property of set truncations, one can construct a subtype $[P]_0:[A]_0 \to \mathrm{Prop}$ of the set truncation of $A$ such that for all $x:A$, $P(x) = [P]_0([x]_0)$, .

 Related concepts

• quotient set

• cone type, bracket type, set truncation

• localization of a type, circle type

• axiom of set truncation

• n-truncation modality

References

For set truncations in dependent type theory, see section 18.5 of:

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)

and section 6.9 and 7.3 of:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)