# 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.

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) 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

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

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 a propositional equality,we may speak of a weakly à la Tarski universe.

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 have systems to manage universe sizes and universe enlargement automatically; Agda’s is more advanced (universe polymorphism), whereas Coq’s is good enough for many purposes but tends to produce “universe inconsistencies” when working with univalence.

### 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 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.

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

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)