This type-theoretic universe \(\U\) is analogous to a Grothendieck universe in set theory which is a set of sets closed under all the ways sets can be constructed in Zermelo-Fraenkel set theory. The existence of a Grothendieck universe cannot be proved from the usual axioms of Zermelo-Fraenkel set theory but needs a new axiom.