Homotopy Type Theory
universe (Rev #7, changes)

Showing changes from revision #6 to #7: Added | Removed | Changed

There are several kinds of universes that one can consider in type theory.

Universes a la Russell

A universe a la Russell is a type whose terms are types. In the presence of a separate judgment?AtypeA type”, this can be formulated as a rule

A:UAtype\frac{A:U}{A type}

Thus, the type formers have rules saying which universe they belong to, such as:

A:UB:AUΠAB:U\frac{A:U\quad B:A\to U}{\Pi\, A\, B : U}

With universes a la Russell, we can also omit the judgment “AtypeA 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.

Universes a la Tarski

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

A:UEl(A)type\frac{A:U}{El(A) type}

We usually also have operations on the universe corresponding to (but not identical to) type formers, such as

A:UB:AUpi(A,B):U\frac{A:U\quad B:A\to U}{pi(A, B) : U}

with an equality El(pi(A,B))=ΠEl(A)El(B)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.

See also

Revision on May 14, 2014 at 00:27:52 by Alexis Hazell?. See the history of this page for a list of all contributions to it.