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
In dependent type theory, the type of classes relative to a Tarski universe $U$ is the function type $V_U \to \mathrm{Prop}_U$ from the material cumulative hierarchy higher inductive type $V_U$ constructed from $U$ to the type $\mathrm{Prop}_U$ of $U$-small h-propositions.
Let $(U, T)$ be a Tarski universe. The cumulative hierarchy relative to $U$ is the higher inductive type $V_U$ generated by the following:
A function
An equivalence
A set-truncator
The type of all $U$-small propositions is defined as
$\mathrm{Prop}_U \coloneqq \sum_{A:U} \mathrm{isProp}(A)$
The type of classes relative to $U$ is the function type $V_U \to \mathrm{Prop}_U$, and a class relative to $U$ is just a function $C:V_U \to \mathrm{Prop}_U$.
The type of classes provides a general model of material class theory.
The type of classes is defined in section 10.5.3 of:
Last revised on November 19, 2022 at 10:38:50. See the history of this page for a list of all contributions to it.