Context
Type theory
Universes
Contents
Idea
Russell universes or universes à la Russell are types whose terms are types. In type theories without a separate type judgment , only typing judgments , what would have been type judgments are represented by typing judgments that is a term of a Russell universe , . Russell universes without a separate type judgment are used in many places in type theory, including in the HoTT book, in Coq, and in Agda.
Without a separate type judgment
Russell universes are formally defined in a two-level type theory. The first level consists of a basic dependent type theory consisting of a type judgment, identity types, and a natural numbers type. The second level only contains term judgments, and is the dependent type theory where the Russell universes live in. To distinguish between the two layers, we shall call the types in the first layer “metatypes”, as the first layer behaves as a metatheory or external theory.
We begin with the formal rules of the first layer. The first layer consists of three judgments: metatype judgments , where we judge to be a metatype, metatyping judgments, where we judge to be an element of , , and metacontext judgments, where we judge to be a metacontext, . Metacontexts are lists of metatyping judgments , , , et cetera, and are formalized by the rules for the empty metacontext and extending the metacontext by a metatyping judgment
The three standard structural rules, the variable rule, the weakening rule, and the substitution rule, are also included in the theory. Let be any arbitrary judgment. Then we have the following rules:
In addition, there are identity metatypes: the natural deduction rules for identity metatypes are as follows
Finally, we have the natural numbers metatype, given by the following natural deduction rules:
Now, we introduce the second layer, which consists of a type theory with only one judgment, the typing judgment , which says that is a term of the type . Instead of type judgments, we introduce a special kind of type called a Russell universe or universe à la Russell, whose terms are the types themselves. Russell universes are formalized with the following rules:
Contexts are defined as a metacontext with a list of typing judgments, with the metacontext always preceding the list of typing judgments:
The general rules for Russell universes then follows:
With a separate type judgment
If the type theory has a separate type judgment , the rules for Russell universes become simpler, as one doesn’t have to assume infinitely many Russell universes and a second level to house the natural numbers type used to index the universes. Instead, we merely have
Furthermore, the separate type judgment amounts to collapsing the two levels in the theory above into one level: Instead of defining the identity type and the type of natural numbers as external to the type theory, we instead define it as normal types internal to the type theory. Then the rules for the infinite tower of Russell universes are as follows:
See also
References
The notion is due to:
For more see the references at type universe.