A.2.3 Type universes

We postulate an infinite hierarchy of type universes

$${𝒰}_0,{𝒰}_1,{𝒰}_2,\mathrm{\dots }$$

Each universe is contained in the next, and any type in ${𝒰}_i$ is also in ${𝒰}_{i+1}$:*[right=$𝒰$-intro]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢$𝒰$ _i : $𝒰$ _i+1*[right=$𝒰$-cumul]Γ ⊢A : $𝒰$ _iΓ ⊢A : $𝒰$ _i+1We shall set up the rules of type theory in such a way that $\mathrm{\Gamma }⊢a:A$implies $\mathrm{\Gamma }⊢A:{𝒰}_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 $\mathrm{\Gamma }⊢a\equiv b:A$implies $\mathrm{\Gamma }⊢a:A$ and $\mathrm{\Gamma }⊢b:A$.