A.1.1 Type universes
We postulate^{} a hierarchy of universes^{} denoted by primitive constants
$${\mathrm{\pi \x9d\x92\xb0}}_{0},{\mathrm{\pi \x9d\x92\xb0}}_{1},{\mathrm{\pi \x9d\x92\xb0}}_{2},\mathrm{\beta \x80\xa6}$$ 
The first two rules for universes say that they form a cumulative hierarchy of types:

β’
${\mathrm{\pi \x9d\x92\xb0}}_{m}:{\mathrm{\pi \x9d\x92\xb0}}_{n}$ for $$,

β’
if $A:{\mathrm{\pi \x9d\x92\xb0}}_{m}$ and $m\beta \x89\u20acn$, then $A:{\mathrm{\pi \x9d\x92\xb0}}_{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 $\mathrm{\Xi \x93}\beta \x8a\u2019A:{\mathrm{\pi \x9d\x92\xb0}}_{n}$, and $x$ is a new variable,^{1}^{1}By βnewβ we mean that it does not appear in $\mathrm{\Xi \x93}$ or $A$. then $\beta \x8a\u2019(\mathrm{\Xi \x93},x:A)\mathrm{\pi \x9d\x96\u038c\pi \x9d\x97\x8d\pi \x9d\x97\x91}$.
In the body of the book, an equality judgment $A\beta \x89\u2018B:{\mathrm{\pi \x9d\x92\xb0}}_{n}$ between types $A$ and $B$ is usually abbreviated to $A\beta \x89\u2018B$. 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\beta \x89\u2018B$ then $a:B$.
Title  A.1.1 Type universes 

\metatable 