nLab type universe

Idea

In type theory, a type universe – usually written $\mathcal{U}$ or $Type$ – is a type whose terms are either themselves types (Russell universes), or representations of types in an internal model of the type theory (Tarski universes). Either way, it is a universe of (small) types, a universe in type theory, and sometimes called a type of types.

One also speaks of $\mathcal{U}$ as being a reflection of the type system in itself (e.g. MartinLöf 74, p. 6, Palmgren, pp. 2-3, Rathjen, p. 1, Luo 11, section 2.5, Luo 12, p. 2, Stanf. Enc. Phil.), following the reflection principle in set theory.

In homotopy type theory a type of (small) types is what in higher categorical semantics is interpreted as a (small) object classifier. Thus, the type of types is a refinement of the type of propositions which only contains the (-1)-truncated/h-level-1 types (and is semantically a subobject classifier).

In the presence of a type universe a judgement of the form

$$\vdash A : \mathcal{U}$$

says that $A$ is a term of type $\mathcal{U}$, hence is either a (small) type itself (for Russell universes), or a representation of types in an internal model of the type theory (for Tarski universes).

More generally, in Russell universes a hypothetical judgement of the form

$$x : X \vdash A(x) : \mathcal{U}$$

says that $A$ is an $X$-dependent type.

In Tarski universes the corresponding hypothetical judgment would be of the form

$$x : X \vdash El(A)(x)\; type$$

In homotopy type theory the type universe $\mathcal{U}$ is often assumed to satisfy the univalence axiom. This is a reflection of the fact that in its categorical semantics as an object classifier is part of an internal (∞,1)-category in the ambient (∞,1)-topos: the one that as an indexed category is the small codomain fibration.

Per Martin-Lof‘s original type theory contained a Russell universe which contained all types, which therefore in particular contained itself, i.e. one had $Type : Type$. But it was pointed out by Jean-Yves Girard that this was inconsistent; see Girard's paradox. Thus, modern type theories generally contain a hierarchy of types universes, with

$$n:\mathbb{N} \vdash \mathcal{U}(n) : \mathcal{U}(n + 1)$$

for Russell universes, and

$$n:\mathbb{N} \vdash \mathcal{U}(n)\; type$$

$$n:\mathbb{N} \vdash \mathcal{U}^{'}(n) : \mathcal{U}(n + 1)$$

$$n:\mathbb{N} \vdash El_{n+1}(\mathcal{U}^{'}(n)) \equiv Type(n)$$

$$n:\mathbb{N} \vdash El_{n,n+1}:\mathcal{U}(n) \to \mathcal{U}(n + 1)$$

$$n:\mathbb{N} \vdash p:is1Monic(El_{n,n+1})$$

for Tarski universes.

Formalizations

Russell universe

A Russell universe or universe à la Russell is a type whose terms are types. In the presence of a separate judgment “$A \;type$”, this can be formulated as a deduction rule of the form

$$\frac{A:\mathcal{U}}{A \;type}$$

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

$$\frac{A:\mathcal{U}\quad B:A\to \mathcal{U}}{\Pi\, A\, B : \mathcal{U}}$$

With Russell universes, 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 in UFP13.

Tarski universes

A Tarski universe or a universe à la Tarski (Hofmann, section 2.1.6, Luo 12, Gallozzi 14, p. 40) is a type $U$ together with an “interpretation” operation allowing us to regard its terms as codes or names for actual types. Thus we have a rule such as

$$\frac{A:\mathcal{U}}{El(A)\;type}$$

saying that for each term $A$ of the type universe $U$ there is an actual type $El(A)$. This is the approach taken by Egbert Rijke‘s Introduction to Homotopy Type Theory.

Conversely, with notation as used at object classifier in an (infinity,1)-topos, one might write $A = 'El(A)'$ to indicate that $A$ is the name of the type $El(A)$ in the type universe.

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

$$\frac{A:\mathcal{U}\quad B:A\to \mathcal{U}}{\pi(A, B) : \mathcal{U}}$$

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 an equivalence (i.e. we have a rule which gives us a canonical term of the equivalence type), we may speak of a weakly Tarski universe (Gallozzi 14, p. 49-50).

We can give a slightly different definition of weakly Tarski universe using propositional equality and a larger universe. More precisely, we can consider two (or many) universes $\mathcal{U}$ and $\mathcal{U}'$ with the usual rules for the relative reflection $el(a):\mathcal{U}'$ for any $a:U$, a choice of weakly or strongly Tarski computation rules for the reflections $El$ and $El'$, and a computation rule for the relative reflection el of $\mathcal{U}$ inside $\mathcal{U}'$ based on propositional equality, which gives us canonical elements of the identity types $Id_{\mathcal{U}'}(\pi'(el(a),el(b)),el(\pi(a,b)))$ and similarly for the other type formers.

If the containing universe is univalent the two definitions turn out to coincide.

The three notions of Tarski universe can be ordered by generality: Every Tarski universe is weakly Tarski by equivalences, because both definitional equality of types $A \equiv B$ and the identity types between two types $A = B$ imply that the two types of equivalent $A \simeq_\mathcal{U} B$. Similarly, every strict Tarski universe is weakly Tarski by the identity type, because definitional equality of types $A \equiv B$ implies that two types are identified $A = B$.

Since each type former is independent of each other, one could also have mixed versions of Tarski universes, where some of the type formers are strictly Tarski and some are weakly Tarski. This leads to $2^n$ possible Tarski universes, where $n$ is the number of type formers in a type theory, and the $2^n$ type theories are only partially ordered by generality. Internally in an ambient universe, that number becomes $3^n$.

Universes defined internally via induction-recursion are stricty Tarski. Weakly Tarski universes are easier to obtain in semantics (see below): they are somewhat more annoying to use, but probably suffice for most purposes. In objective type theory, there is no definitional equality, so every Tarski universe is weakly Tarski.

Properties

Universe enlargement

Both Coq and Agda support universe polymorphism to deal with the issue of universe enlargement. Moreover, Coq supports typical ambiguity.

Cumulativity

A tower of universes is cumulative if $A:\mathcal{U}_i$ implies $A:\mathcal{U}_{i+1}$ (rather than, say, $Lift(A):\mathcal{U}_{i+1}$).

Cumulative Russell universes have some issues; see for instance Luo 12.

• Coq uses Russell style universes. For practical purposes, it also has cumulativity, although there is some question (perhaps mainly semantic) of whether this is true internally or whether it uses casts that are simply hidden from the user.

• Agda uses non-cumulative Russell style universes.

• UFP13 (first edition) uses cumulative Russell style universes.

Categorical semantics

UnivalentRussell universes have been shown to be interpreted in type-theoretic model categories presenting the base (∞,1)-topos ∞Grpd

(Kapulkin-Lumsdaine-Voevodsky 12) and more generally presenting (∞,1)-toposes of (∞,1)-presheaves over elegant Reedy categories (Shulman 13).

Discussion for general (∞,1)-toposes (of (∞,1)-sheaves) that should have implementation weakly Tarski (Gallozzi 14, p. 49-50) is in (Gepner-Kock 12).

For more on this see the respective sections at relation between type theory and category theory.

Related concepts

• resizing axiom

• universe polymorphism

• univalence

• Prop, the type of propositions

  • subobject classifier

• object classifier

• type of classes

• parametric polymorphism

• Girard's paradox

• Awodey's conjecture

• univalent type theory

References

Type universes in Martin-Löf type theory originate in un-stratified and hence inconsistent form with

• Per Martin-Löf, §2.7.1 in: A Theory of Types, unpublished note (1971) [pdf, pdf]

and then in stratified and consistent form in

• Per Martin-Löf, §1.10 in: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80, Elsevier (1975) 73-118 [doi:10.1016/S0049-237X(08)71945-1, CiteSeer]

elaborated on in

• Per Martin-Löf (notes by Giovanni Sambin): Universes, pp. 47 in: Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) [pdf, pdf]

which also introduces (p. 48) the distinction into notions of Russell universes and Tarski universes.

Further discussion in

• Martin Hofmann, Universes, section 2.3.5 in: Syntax and semantics of dependent types, Chapter 2 in: Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [ECS-LFCS-95-327, pdf, doi:10.1007/978-1-4471-0963-1]

Review and further discussion:

• Erik Palmgren, On Universes in Type Theory, in Twenty-Five Years of Constructive Type Theory, Oxford University Press (1998) 191–204 [pdf, doi:10.1093/oso/9780198501275.003.0012]

Introduction with an eye towards homotopy type theory:

• Univalent Foundations Project, §1.3 in Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

Definition of weakly Tarski universes:

• Martin Hofmann, section 2.1.6 of Syntax and semantics of dependent types (web)

• Zhaohui Luo, Notes on Universes in Type Theory, 2012 (pdf)

• Cesare Gallozzi, Constructive Set Theory from a Weak Tarski Universe, MSc thesis (2014) (arXiv:1411.5591)

Detailed discussion of the type of types in Coq is in

• Adam Chlipala, Certified programming with dependent types – Library Universes

See also around slide 8 of the survey

• Frade, Calculus of inductive constructions (2008/2009) (pdf)

A formal proof in homotopy type theory that the type of homotopy n-types is not itself a homotopy $n$-type (it is an $(n+1)$-type) is in

• Nicolai Kraus, Christian Sattler, The universe $\mathcal{U}_n$ is not an $n$-type May 2013 (pdf)

(∞,1)-Categorical semantics for univalent type universes is discussed in

• Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky, The Simplicial Model of Univalent Foundations (arXiv:1211.2851)

• Michael Shulman, The univalence axiom for elegant Reedy presheaves (arXiv:1307.6248)

• David Gepner, Joachim Kock, Univalence in locally cartesian closed ∞-categories (arXiv:1208.1749)

Relation to injective types:

• Martín Escardó, Injectives types in univalent mathematics (arXiv:1903.01211)

See also

• Michael Rathjen, The strength of Martin-Löf type theory with superuniverse. Part I pdf

• Stanford Encyclopedia of Philosophy, Type theory – Extensions of type systems, Polymorphism, Paradoxes

• Zhaohui Luo, Contextual analysis of word meanings in type-theoretical semantics, in Pogodalla, Prost (eds.) Logical Aspects of Computational Linguistics, 2011 (pdf)