Although reasoning about type functionality via a type of all types is impossible, one might still reason about it by adding a form of assertion about it, as Martin-Lof did in his 1980 type system from which Nuprl stems. Despite the advantages of reasoning about type-functionality explicitly, the original designers of Nuprl hoped to simplify their design by not doing so (however, such rules are likely to be incorporated eventually); rather, the primitive rules of Nuprl simply approximate most reasoning about "all types" by reasoning instead about a hierarchy of types

So, rather than having a rule saying, for example, that *A*+*B**A**B**A*+*B* Type{i}*A* Type{i}*B* Type{i}*A*,*B*:Type{i}. *A*+*B* Type{i}

Notice that in the statement of *A*,*B*:Type{i}. *A*+*B* Type{i}

Consider *A*:Type{i}, *B*:Type{j}. *A*+*B* Type{[i | j]}

This says that the disjoint union of two types from any two universe levels is a type in the universe whose level is the maximum of the two levels. So, there is a "max" operation you can use in universe level expressions.

There is also a successor operation:

As a convenience, there is also an offset operation that adds a constant to a level:

Although there is no need to do so in a theorem statement, one can also use constant level expressions:

The forms of level expression may be freely combined.

**Universe Polymorphism.
**

The reason it is practical to use these variables in level expressions (but note that they are not like other ordinary variables of the logic -- you cannot bind them) is that any true sequent remains true if all the level variables throughout it are uniformly replaced by level expressions of your choice.So from *A*:Type{i}, *B*:Type{j}. *A*+*B* Type{[i | j]}"*A*:Type{3}, *B*:Type{k'}. *A*+*B* Type{[3 | k']}"

It also follows that *A*,*B*:Type{i}. *A*+*B* Type{[i | i]}"*A*,*B*:Type{i}. *A*+*B* Type{i}"

In a typical sequent, it turns out, all the universe level expressions are the same and consist of simply a level variable. When this is so, we normally choose to display the universe expression simply as *A*,*B*:Type{i}. *A*+*B* Type{i}"*A*,*B*:Type. *A*+*B* Type"

The same level expressions are used as indices to

About: