But often we build complex expressions for types out of operations on types themselves. To characterize such operations on types as functions the domain would need to include the types we wish to take as arguments. If there were a type of all types then we'd be done, but there are theoretical obstacles to construction of such a type, and indeed there are demonstrations of its impossibility.
So, we instead build large collections of types, each closed under all the usual type constructors; the first universe
The universes are "cumulative":
Technically, the members of universes are types "in intension", or "intensional types" (see
Universes approximate the possibly desired but impossible type of all types.
One essential aspect of a family of universes is that every type inhabits one of the family. For this reason, the family of universes cannot be represented by a type-valued function over some type. For example, if there is a denumerable hierarchy of universes, then there can be no operator
In Nuprl we have followed Martin-Lof 1980 making the expressions for universes atomic, i.e. they have no subterms, and no universe expression can be generated by evaluating expressions that don't already contain it. This means that a finite segment of the universe hierarchy is adequate for explaining any finite collection of type expressions, since only finitely many universe expressions can be used in it.
The inability to explicitly quantify over all types is somewhat mitigated in Nuprl by the use of universe level variables instead of constants.