A.1.1 Type universes

We postulate a hierarchy of universes 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<n$ ,
•

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,¹¹By “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