Universe

Definition

In type theory, a universe is a type whose terms are themselves types. We typically denote a universe by $\mathcal{U}$ or $\mathsf{Type}$. If $A$ is a type belonging to the universe, we write $A:\mathcal{U}$. Universes are required to be closed under the type formers of the theory:

• If $A:\mathcal{U}$ and $B:A\to \mathcal{U}$, then ${\sum }_{x:A}B(x):\mathcal{U}$ and ${\prod }_{x:A}B(x):\mathcal{U}$.
• $\mathcal{U}$ is closed under inductive types (e.g., $\mathbb{N}:\mathcal{U}$) and the identity type.

Paradoxes and Hierarchies

To avoid Girard’s Paradox (the type-theoretic analogue of Russell’s Paradox), a universe cannot be a term of itself ($\mathcal{U}:\mathcal{U}$ is inconsistent). Most systems resolve this by introducing a cumulative hierarchy of universes:

${\mathcal{U}}_0:{\mathcal{U}}_1:{\mathcal{U}}_2:\dots$

where every type in ${\mathcal{U}}_i$ is also in ${\mathcal{U}}_{i+1}$.

Russell vs. Tarski Styles

1. Russell-style: Types are terms of the universe directly. If $A:\mathcal{U}$, then $A$ is also a type.
2. Tarski-style: The universe $\mathcal{U}$ is a type of codes. A separate decoding function $\mathsf{El}:\mathcal{U}\to \mathsf{Type}$ is used to translate a code into an actual type.

Predicativity

• Predicative: A universe $\mathcal{U}$ is predicative if it only contains types whose definitions do not involve quantification over $\mathcal{U}$ itself.
• Impredicative: A universe (often denoted $\mathsf{Prop}$) is impredicative if it is closed under quantification over any universe level. The Calculus of Constructions utilizes an impredicative universe at the base of its hierarchy.

See also

• Tarski Universe
• Russell’s Paradox
• Cumulative Hierarchy

References

hott2013-book coquand1986-girard-paradox