A.2.3 Type universes

We postulate an infinite hierarchy of type universes

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

Each universe is contained in the next, and any type in $\mathcal{U}_{i}$ is also in $\mathcal{U}_{i+1}$ : {mathpar} \inferrule*[right= $\mathcal{U}$ -intro] Γ $\mathsf{ctx}$ Γ ⊢ $\mathcal{U}$ _i : $\mathcal{U}$ _i+1 \inferrule*[right= $\mathcal{U}$ -cumul] Γ ⊢A : $\mathcal{U}$ _i Γ ⊢A : $\mathcal{U}$ _i+1 We shall set up the rules of type theory in such a way that $\Gamma\vdash a:A$ implies $\Gamma\vdash A:\mathcal{U}_{i}$ for some $i$ . In other words, if $A$ plays the role of a type then it is in some universe. Another property of our type system is that $\Gamma\vdash a\equiv b:A$ implies $\Gamma\vdash a:A$ and $\Gamma\vdash b:A$ .

Title	A.2.3 Type universes
\metatable