# Contents

## 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:

• $\mathrm{set}:\left(\sum_{A:U} T(A) \to V_U\right) \to V_U$
• $\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.