type of classes in nLab

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Type theory
+-- {: .hide}
[[!include type theory - contents]]
=--
=--
=--


\tableofcontents

## 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 set theory|material]] [[cumulative hierarchy]] [[higher inductive type]] $V_U$ constructed from $U$ to the [[type of propositions|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 in homotopy type theory|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) &lbrack;[web](http://homotopytypetheory.org/book/), [pdf](http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf)&rbrack;