# A.2.3 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