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
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.
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$.
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, 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}))$
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
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
there exists a unique function $u_B:[A]_0 \to B$ such that $u_B([a]_0) = f(a)$ for all $a:A$.
Formation rules for set truncations:
Introduction rules for set truncations:
Dependent universal property of set truncations:
A choice of unique representatives for propositional truncation consists of a type family $C(x)$ indexed by $x:A$, and an element of type
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
Then
is the set truncation of $A$.
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)$.
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)$, .
For set truncations in dependent type theory, see section 18.5 of:
and section 6.9 and 7.3 of:
Last revised on February 20, 2024 at 19:04:09. See the history of this page for a list of all contributions to it.