Dependent type theory: universes may have a type?

85 Views Asked by At

In Dependent Type Theory, as described in Appendix A of Homotopy Type Theory, it is immediate to prove that $\Gamma \vdash \mathcal{U}_i : \mathcal{U}_j$ with $j > i$. So every universe has another universe as its type.

My question is: is it possible to prove $\Gamma \vdash \mathcal{U}_i : B$ for some context $\Gamma$ and some type $B$ which is not a universe?