nLab type of classes

Idea

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.

 Definition

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

  $$\mathrm{set}:\left(\sum_{A:U} T(A) \to V_U\right) \to V_U$$

• An equivalence

  $$\mathrm{idVchar}:\prod_{A:U} \prod_{B:U} \prod_{f:T(A) \to V_U} \prod_{g:T(B) \to V_U} (\mathrm{set}(A, f) =_{V_U} \mathrm{set}(B, g)) \simeq \left(\left(\prod_{a:T(A)} \left| \sum_{b:T(B)} f(a) =_{V_U} g(b) \right|\right) \times \left(\prod_{b:T(B)} \left| \sum_{a:T(A)} f(a) =_{V_U} g(b) \right|\right) \right)$$

• A set-truncator

  $$\tau_0:\mathrm{isSet}(V_U)$$

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.

See also

• class

• class theory

• category of classes

 References

The type of classes is defined in section 10.5.3 of:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics, Institute for Advanced Study (2013) [web, pdf]