Showing changes from revision #8 to #9:
Added | Removed | Changed
There are several kinds of universes that one can consider in type theory, which vary along many different axes.
A universe a la Russell is a type whose terms are types. In the presence of a separate judgment? “$A type$”, this can be formulated as a rule
Thus, the type formers have rules saying which universe they belong to, such as:
With universes a la Russell, we can also omit the judgment “$A type$” and replace it everywhere by a judgment that A is a term of some universe. This is the approach taken by the HoTT book and by Coq?.
Russell universes have some issues; see for instance these notes.
A universe a la Tarski is a type together with an “interpretation” operation allowing us to regard its terms as types (or “codes for types”). Thus we have a rule such as
We usually also have operations on the universe corresponding to (but not identical to) type formers, such as
with an equality $El(pi(A,B))=\Pi \, El(A)\, El(B)$. Usually this latter equality (and those for other type formers) is a judgmental equality. If it is only a propositional equality?,we may speak of a weakly a la Tarski universe.
Universes defined internally via induction-recursion are (strongly) a la Tarski. Weakly a la Tarski universes are easier to obtain in semantics; see model of type theory in an (infinity,1)-topos. They are somewhat more annoying to use, but probably suffice for most purposes.
Universe polymorphism means that you don’t have to do things separately for each universe level; you can do it once “parametrized” over universes and then instantiate it to any particular universe.
Typical ambiguity means you don’t have to explicitly say what universe level you’re working at; you just say something like “Type” and the system (or the reader) guesses it.
They are discussed further in this blog post.
Both Russell and Tarski style universes can be polymorphic or not, and typically ambiguous or not.
A tower of universes is cumulative if $A:U_i$ implies $A:U_{i+1}$ (rather than, say, $Lift(A):U_{i+1}$).
Coq? uses cumulative Russell style universes with typical ambiguity. It used to have a sort of “fake” universe polymorphism, but recent versions of Coq have real universe polymorphism (thanks to Mathieu Sozeau). It also appears to have cumulativity, but apparently this is actually implemented internally via liftings that are simply invisible to the user (a sort of “cumulative ambiguity”).
Agda uses non-cumulative Russell style universes with universe polymorphism but without typical ambiguity: you always have to explicitly indicate the universe level.
The HoTT Book (first edition) uses cumulative Russell style universes with universe polymorphism and (except for a few places) typical ambiguity.
Revision on June 3, 2014 at 08:31:59 by Mike Shulman. See the history of this page for a list of all contributions to it.