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
basic constructions:
strong axioms
further
In dependent type theory, an axiom of set truncation is a axiom or unjustified rule which implies the uniqueness of identity proofs which states that every type is an h-set. Adding an axiom of set truncation to a dependent type theory results in a set-level type theory.
TODO: show that each of the axioms below implies the uniqueness of identity proofs.
In dependent type theory, uniqueness of identity proofs for identification types is given by the following rule:
There is uniqueness of identity proofs for heterogeneous identification types:
Uniqueness of identity proofs for identification types follows from uniqueness of identity proofs for heterogeneous identification types by taking canonical element $\mathrm{pt}:\mathbb{1}$ of the unit type $\mathbb{1}$, identification $\mathrm{refl}_{\mathbb{1}}(\mathrm{pt}):\mathrm{Id}_{\mathbb{1}}(\mathrm{pt}, \mathrm{pt})$, and elements $a:A$ and $b:A$. Since the following two types are equivalent:
and because $\mathrm{hId}_{A}(\mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}), a, b)$ is always a mere proposition by uniqueness of identity proofs for heterogeneous identification types, it follows that $\mathrm{Id}_{A}(a, b)$ is also always a mere proposition.
Similarly, there is also uniqueness of identity proofs for dependent heterogeneous identification types:
Uniqueness of identity proofs for identification types follows from uniqueness of identity proofs for dependent heterogeneous identification types by defining the type $A$ to be the dependent type $C(\mathrm{pt})$ for type family $x:\mathbb{1} \vdash C(x)$ indexed by the unit type $\mathbb{1}$, and taking the canonical element $\mathrm{pt}:\mathbb{1}$, identification $\mathrm{refl}_{\mathbb{1}}(\mathrm{pt}):\mathrm{Id}_{\mathbb{1}}(\mathrm{pt}, \mathrm{pt})$, and elements $a:C(\mathrm{pt})$ and $b:C(\mathrm{pt})$. Since the two types are equivalent:
and because $\mathrm{hId}_{x:\mathbb{1}.C(x)}(\mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}), a, b)$ is always a mere proposition by uniqueness of identity proofs for dependent heterogeneous identification types, it follows that $\mathrm{Id}_{C(\mathrm{pt})}(a, b)$ and thus by definition $\mathrm{Id}_{A}(a, b)$ is also always a mere proposition.
In dependent type theory, axiom K is given by the following rule:
There is an axiom K for heterogeneous identification types:
Axiom K for identification types follows from axiom K for heterogeneous identification types by taking canonical element $\mathrm{pt}:\mathbb{1}$ of the unit type $\mathbb{1}$, identification $\mathrm{refl}_{\mathbb{1}}(\mathrm{pt}):\mathrm{Id}_{\mathbb{1}}(\mathrm{pt}, \mathrm{pt})$, and elements $a:A$ and $b:A$. Since the following two types are equivalent:
and because $\mathrm{hId}_{A}(\mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}), a, a)$ is always a contractible type with center of contraction $\mathrm{ap}_{A}(f, \mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}))$ for element $a:A$, and function $f:\mathbb{1} \to A$, by axiom K for heterogeneous identification types, it follows that $\mathrm{Id}_{A}(a, a)$ is also always a contractible type, with center of contraction $\mathrm{refl}_A(a)$.
Similarly, there is also an axiom K for dependent heterogeneous identification types:
Axiom K for identification types follows from axiom K for dependent heterogeneous identification types by defining the type $A$ to be the dependent type $C(\mathrm{pt})$ for type family $x:\mathbb{1} \vdash C(x)$ indexed by the unit type $\mathbb{1}$, and taking the canonical element $\mathrm{pt}:\mathbb{1}$, identification $\mathrm{refl}_{\mathbb{1}}(\mathrm{pt}):\mathrm{Id}_{\mathbb{1}}(\mathrm{pt}, \mathrm{pt})$, and elements $a:C(\mathrm{pt})$ and $b:C(\mathrm{pt})$. Since the two types are equivalent:
and because $\mathrm{hId}_{x:\mathbb{1}.C(x)}(\mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}), a, b)$ is always a contractible type with center of contraction $\mathrm{apd}_{x:\mathbb{1}.C(x)}(f, \mathrm{pt}, \mathrm{pt}, \mathrm{refl}_{\mathbb{1}}(\mathrm{pt}))$ for element $a:A$, and dependent function $f:\prod_{x:\mathbb{1}} C(x)$, by axiom K for heterogeneous identification types, it follows that $\mathrm{Id}_{C(\mathrm{pt}}(a, a)$ and thus by definition $\mathrm{Id}_{A}(a, a)$ is also always a contractible type, with center of contraction $\mathrm{refl}_A(a)$.
In dependent type theory with power sets, Leibniz's identity of indiscernibles is given by the following inference rule:
This implies that all types $A$ are sets, because the type
is always a proposition, in the context of weak function extensionality, and thus by the equivalence of types, $\mathrm{Id}_A(x, y)$ is also a proposition for all $x:A$ and $y:A$, which means that $A$ is a set.
In dependent type theory with power sets, the set-theoretic principle of unique choice is given by the following rule:
Because the type $A \times B \to \mathcal{P}(\mathbb{1})$ is a set, the type
is also a set, and the equivalence only exists if the function type $A \to B$ is a set, which only occurs if $B$ is a set. Thus, this rule implies that all types are sets.
In cubical type theory, boundary separation is given by the following rule:
In dependent type theory, the type-theoretic axiom of existence states that every type has a choice operator, a function from its bracket type to the type itself, and is given by the following rule:
Indeed, it suffices for the identity types to have choice operators:
In dependent type theory, equality reflection is given by the following rule:
…
In dependent type theory, the axiom of $S^1$-localization is given by the following rules:
In dependent type theory with dependent product types, dependent sum types, identity types, function extensionality, and a type of all propositions, the axiom of finiteness is given by the following rule:
where
The membership relation and the subtype operations used above are defined in the nLab article on subtypes.
Any one of the following axioms on the circle type implies axiom K or uniqueness of identity proofs for all types in the dependent type theory, and thus is an axiom of set-truncation:
In dependent type theory, in general there are Kuratowski-finite types which are not h-sets, such as the circle type. However, every finite type is an h-set, and hence why they are usually called finite sets.
A naive translation into dependent type theory of the traditional set-theoretic theorem in classical mathematics that “Kuratowski-finite implies finite” results in the statement that every Kuratowski-finite type is finite. This implies that the circle type is a finite type, which implies that the circle type is an h-set, which implies that every type is an h-set. Thus, that every Kuratowski-finite type is finite is an axiom of set truncaiton.
The statement “Kuratowski-finite implies finite” in classical mathematics is really a statement about h-sets, similar to how the axiom of choice is really a statement about h-sets. This is because it is still true in constructive mathematics that every Kuratowski-finite type with decidable equality is a finite type, and in dependent type theory, every type with decidable equality is an h-set.
Last revised on December 12, 2023 at 15:47:17. See the history of this page for a list of all contributions to it.