# Contents

## Idea

In type theory, a type of (small) types – usually written $Type$ – is a type whose terms are themselves types. Thus, it is a universe of (small) types, a universe in type theory.

One also speaks of $Type$ 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 of types a judgement of the form

$\vdash A : Type$

says that $A$ is a term of type $Type$, hence is a (small) type itself. More generally, a hypothetical judgement of the form

$x : X \vdash A(x) : Type$

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

In homotopy type theory the type of types $Type$ 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 type of 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 of types, with $Type_0 : Type_1$ and $Type_1 : Type_2$, etc.

## Formalizations

### Type Universe à la Russell

A 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:U}{A \;type}$

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

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

With universes à 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 textbook and by Coq.

### Type Universe à la Tarski

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:U}{El(A)\;type}$

saying that for each term $A$ of the type universe $U$ there is an actual type $El(A)$. (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:U\quad B:A\to U}{\pi(A, B) : 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 à la Tarski universe (Gallozzi 14, p. 49-50).

We can give a slightly different definition of weakly à la Tarski universe using propositional equality and a larger universe. More precisely, we can consider two (or many) universes $U$ and $U'$ with the usual rules for the relative reflection $el(a):U'$ for any $a:U$, a choice of weakly or strongly a la Tarski computational rules for the reflections $El$ and $El'$, and a computation rule for the relative reflection el of $U$ inside $U'$ based on propositional equality, which gives us canonical elements of the identity types $Id_{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.

Universes defined internally via induction-recursion? are (strongly) à la Tarski. Weakly à la Tarski universes are easier to obtain in semantics (see below): they are somewhat more annoying to use, but probably suffice for most purposes.

## Properties

### Universe enlargement

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

### Categorical semantics

Univalent type universes à la Russell 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 à la 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.

## References

Some of the text above is adapted from the entry universe at the homotopy type theory web.

Type universes in Martin-Löf type theory originate around

• Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)

Basic discussion of the syntax of type universes is in

Definition of type universes weakly à la Tarski is in

Detailed discussion of the type of types in Coq is in

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, C. Sattler, The universe $\mathcal{U}_n$ is not an $n$-type May 2013 (pdf)

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