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
Notice that in the statement of
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.
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
It also follows that
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
The same level expressions are used as indices to