# A.1.1 Type universes

We postulate a hierarchy of denoted by primitive constants

 $\mathcal{U}_{0},\quad\mathcal{U}_{1},\quad\mathcal{U}_{2},\quad\ldots$

The first two rules for universes say that they form a cumulative hierarchy of types:

• β’

$\mathcal{U}_{m}:\mathcal{U}_{n}$ for $m,

• β’

if $A:\mathcal{U}_{m}$ and $m\leq n$, then $A:\mathcal{U}_{n}$,

and the third expresses the idea that an object of a universe can serve as a type and stand to the right of a colon in judgments:

• β’

if $\Gamma\vdash A:\mathcal{U}_{n}$, and $x$ is a new variable,11By βnewβ we mean that it does not appear in $\Gamma$ or $A$. then $\vdash(\Gamma,x:A)\;\mathsf{ctx}$.

In the body of the book, an equality judgment $A\equiv B:\mathcal{U}_{n}$ between types $A$ and $B$ is usually abbreviated to $A\equiv B$. This is an instance of typical ambiguity, as we can always switch to a larger universe, which however does not affect the validity of the judgment.

The following conversion rule allows us to replace a type by one equal to it in a typing judgment:

• β’

if $a:A$ and $A\equiv B$ then $a:B$.

Title A.1.1 Type universes
\metatable