Redirected from "à la Russell".
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.
Definition of a single Russell universe
If the type theory has a separate type judgment , then one could define a single Russell universe in the type theory. We merely have
Dependent type theories typically come with a hierarchy of Russell universes, so that all types in the dependent type theory are elements of Russell universes. This is especially the case for dependent type theories without any separate type judgments at all, where types are necessarily defined as terms of Russell universes.
Without a separate type judgment
One formal definition of a type theory with a hierarchy of Russell universes is as follows:
The type theory has judgments
-
, that is a context
-
, that is a universe level,
-
, that is a proposition,
-
, that is a true proposition,
and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order and upwardly unbounded, where is true for all indices .
Now, we introduce 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:
In addition, we have rules for contexts which state that one could add typing judgments to the list of contexts:
as well as rules saying that equality is preserved across universe levels:
With a type judgment for each universe
One could also define a hierarchy of Russell universes à la Coquand, in that the type theory has a type judgment for each universe . Using the dependent type theory with no separate type judgment, instead of having only one term judgment , for level and type , we instead have an infinite number of type judgments, one type judgment for every level , indicating that is a type with level , in addition to the term judgments . Then, one has the following rules for Russell universes à la Coquand:
In addition, we have rules for contexts which state that one could add typing judgments to the list of contexts:
One could derive from these rules the above rules for Russell universes and context extension
With a single separate type judgment
It is also possible to define the hierarchy of Russell universes with a single separate type judgment, such that every single type is in a Russell universe. The advantage of doing so is that one doesn’t need to define the theory of universe levels before defining the type theory; one could instead simply define the natural numbers inside of the type theory itself, along with the hierarchy of Russell universes:
In particular, every type has a universe level, which is a natural number, and the universe level of is zero and the universe level of given natural number is the successor .
Furthermore, every type of level lifts to another type of level , such that is a negative copy of :
Next are the rules for function types, which are necessary to define type families as elements of a type for dependent product types and the induction principle of the natural numbers type. Here, function types are indexed by the universe level , since the function type indexed by are only definable for -small types, aka types with level .
Similarly, the rules for dependent function types are as follows:
Finally, we have for each universe level a natural numbers type such that and . In addition, each has element and function , defined via lifting the elements of across universe levels. Finally, each satisfies the induction principle of the natural numbers type over the universe .
- Formation rules for natural numbers types:
- Introduction rules for natural numbers types:
- Elimination rules for natural numbers types:
- Computation rules for natural numbers types:
Something similar could be done for Coquand universes.
Analogues in set theory
There are analogues of cumulative Russell universes in set theory.
With a single set judgment
One formal definition of a set theory with cumulative Russell universes is as follows:
The set theory has judgments
-
, that is a context
-
, that is a universe level,
-
, that is a proposition,
-
, that is a true proposition,
and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order and upwardly unbounded, where is true for all indices .
Now, we introduce a single set judgment which says that is a set, as well as the membership relation , which says that in the set . We introduce a special kind of set called a cumulative Russell universe or cumulative universe à la Russell, which formalized with the following rules:
With a separate set judgment for each set theory
There are also analogues of cumulative Russell universes à la Coquand in set theory. Instead of having a single set theory, one has a whole collection of set theories which embed into each other, with indices indicating which level the set theory lies on.
One formal definition of a set theory with cumulative Russell universes à la Coquand is as follows:
The set theory has judgments
-
, that is a context
-
, that is a level of set theory,
-
, that is a proposition,
-
, that is a true proposition,
and consists of the formal signature and inference rules of first-order Heyting arithmetic or Peano arithmetic. These rules ensure that there are an infinite number of indices, which are strictly ordered with strict total order and upwardly unbounded, where is true for all indices .
This allows us to add an infinite number of set judgments, one set judgment for every level , indicating that is a set with level , as well as an infinite number of membership relations , one for each set judgment . Then, one has the following inference rules for cumulative Russell universes à la Coquand:
This says that each is a set which satisfies a reflection principle.
See also
References
The notion is due to:
For more see the references at type universe.