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 , the type of connected components of is a set.
Suppose that the dependent type theory has propositional truncations and quotient sets. Then given a type , the type family indexed by and defined by the propositional truncation of the identity type of , is an equivalence relation. The set truncation of is the quotient set of by : .
Suppose that dependent type theory has localizations of types and the circle type . Then the set truncation of a type is the localization of at :
As a higher inductive type, the set truncation of a type is a type inductively generated by
A function
For each point and path , a 2-path
Equivalently, it is the higher inductive type generated by
A function
For each function from the circle type, a 2-path
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 is a type inductively generated by
A function
For each point and path , a definitional equality
The recursion principle of definitional set truncations says that given a type with
A function
For each point and path , a definitional equality
there exists a unique function such that for all .
Equivalently, the definitional set truncation of a type is generated by
A function
For each function from the circle type, a definitional equality
Similarly, the recursion principle of this kind of definitional set truncations says that given a type with
A function
For each function from the circle type, a definitional equality
there exists a unique function such that for all .
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 indexed by , and an element of type
Then the type is the set truncation of .
Equivalently, one could use functions instead of type families, and say that a choice of unique representatives is a type with a function and an element of type
Then
is the set truncation of .
The universal property of set truncations says that given a type , a set , and a function , there exists a unique function such that for all , .
Given a type and a subtype , by propositional extensionality and the universal property of set truncations, one can construct a subtype of the set truncation of such that for all , , .
For set truncations in dependent type theory, see section 18.5 of:
and section 6.9 and 7.3 of:
see also:
Last revised on September 13, 2024 at 22:52:38. See the history of this page for a list of all contributions to it.