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 theright 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 oftypical 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$ .