Universes

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 Type{1} is formed by collecting all the types that don't depend on building universes. The second universe Type{2} is built the same way except that we now add Type{1} as a new type. So, for example, Type{1}  Type{2}. The third universe Type{3} is the same except both Type{1} and Type{2} are made available as types.

The universes are "cumulative": Type{1}  Type{2}, Type{2}  Type{3}, et cetera.

Technically, the members of universes are types "in intension", or "intensional types" (see Intensional Types).

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 V(i) such that, for each i  , V(i) is the universe Type{i}; this is because i:V(i) would be a type but it would not inhabit any universe, contradicting the assumption that V(i) forms a universe hierarchy. And since using any type instead of would fail the same way, it is not possible to internally index the universes with a type.

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.

See Type Functionality Sequents and Prop Levels and Predicativity.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html