Universes: Why Sort u?

What is the type of Sort 0?

A proposition variable appears in the type theory as an assumption $P : \Sort{0}$. It can occur in two places: in a context, as in the left judgment below, or bound by $\lambda$ or $\Pi$, as in the right one:

The left judgment proves $P \to P$ for one fixed $P$ supplied from outside. The right one is a single closed term that proves it for every $P$, and it can be applied later to any particular proposition; this is what the $\forall$ rows of Figure 4.1 need.

Both forms require $\Sort{0}$ to be a type. C-Ext, which adds $P : \Sort{0}$ to a context, and T-Lam and T-Pi, which bind $P : \Sort{0}$, all have the premise $\Gamma \vdash A : \Sort{u}$ for the type $A$ of the new variable. With $A = \Sort{0}$, this premise reads $\Gamma \vdash \Sort{0} : \Sort{u}$ for some $u$: the universe of propositions must itself have a type. The question is which.

Type is not a type

Suppose we replace all universes by a single universe $\mathsf{Type}$ that contains itself:

Translate $\forall P.\,\varphi$ as $\tPi{P}{\mathsf{Type}}{\varphi^\ast}$. Then $P$ ranges over a collection that contains $\mathsf{Type}$ itself and every type built from it. Such a collection is the type-theoretic analogue of the set of all sets, and naive set theory shows that such collections lead to contradictions. The best-known example is Russell's paradox: for $R = \{\, x \mid x \notin x \,\}$, both $R \in R$ and $R \notin R$ lead to a contradiction.

Type theory has no membership test like $x \notin x$, so Russell's argument does not carry over word for word. Girard instead adapted a related paradox about the collection of all well-orderings, due to Burali-Forti [Girard 1972], and Hurkens simplified the resulting term [Hurkens 1995]. The result is a closed term $t_{\mathrm{H}}$ with

so the system is inconsistent: $\bot$ has no proof, yet $\bot^\ast$ has a term, and a kernel built on these rules accepts a proof of every statement. The essential ingredient is a type $U$ that quantifies over all of $\mathsf{Type}$ while being a member of $\mathsf{Type}$, which lets $U$ contain a copy of its own double power set, something no set can do. Appendix C gives $t_{\mathrm{H}}$ in full, explains how it works, and shows how to reproduce the result by changing one line of the kernel.

The damage reaches the algorithm as well. Subject reduction still holds, so if $t_{\mathrm{H}}$ had a normal form, it would be a normal closed term of type $\tPi{p}{\mathsf{Type}}{p}$. The part of the consistency proof in Appendix D that analyses normal terms does not use strong normalization and carries over to $\mathsf{Type} : \mathsf{Type}$; it shows that no such normal term exists. Hence $t_{\mathrm{H}}$ has no normal form, strong normalization fails, and $\Normalize$ runs forever on it. A kernel with $\mathsf{Type} : \mathsf{Type}$ is not only unsound but also, on some inputs, non-terminating.

A hierarchy with an impredicative bottom

The second answer is that $\Sort{0}$ lives in a larger universe, which lives in a larger one still:

No universe contains itself. A $\Pi$-type takes an argument from one universe and returns a type in another, so T-Pi must also say which universe the $\Pi$-type itself belongs to. Lean's answer uses the function $\imax$:

The case split in $\imax$ makes a $\Pi$-type impredicative when its body is a proposition, and predicative otherwise. Pick the universes of $A$ and $B$ below and watch where the $\Pi$-type lands.

Propositions are impredicative. If the body $B$ is a proposition ($v = 0$), the whole $\Pi$ is a proposition, whatever it quantifies over. In particular $(\forall P.\,\varphi)^\ast = \tPi{P}{\Sort{0}}{\varphi^\ast}$ is in $\Sort{0}$, although it quantifies over all of $\Sort{0}$. A universe that contains types quantifying over itself is called impredicative. Because every translated formula lies in $\Sort{0}$, the premise $\psi^\ast : \Sort{0}$ of $\forall$-elim always holds, so a universal statement can be instantiated with any proposition, even with itself. For example, with $\mathit{id} = \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$,

so $\mathit{id}\;(\tPi{P}{\Sort{0}}{P \to P})\;\mathit{id}$ is well typed, with type $\tPi{P}{\Sort{0}}{P \to P}$. The same case makes $\forall n : \Nat,\, n + 0 = n$ a proposition, even though $\Nat$ lives in $\Sort{1}$; Chapter 7 relied on this for induction.

# "Every proposition implies itself" is itself a proposition,
# so it can be instantiated with itself.
def id : forall (P : Sort 0), P -> P := fun (P : Sort 0) => fun (h : P) => h
def self : forall (P : Sort 0), P -> P := id (forall (P : Sort 0), P -> P) id

# The analogous statement one level up is NOT its own instance:
# forall (A : Sort 1), A -> A lives in Sort 2, not Sort 1.
def idT : forall (A : Sort 1), A -> A := fun (A : Sort 1) => fun (a : A) => a
def selfT : forall (A : Sort 1), A -> A := idT (forall (A : Sort 1), A -> A) idT

Types are predicative. If the body is not a proposition ($v \ge 1$), the $\Pi$ lives in the larger of the two universes. A type that quantifies over $\Sort{u}$ then lives in $\Sort{(\max(u+1, v))}$, which is never $\Sort{u}$:

This property is called predicativity. For example, the identity on types $\tLam{A}{\Sort{1}}{\tLam{a}{A}{a}}$ has type $\tPi{A}{\Sort{1}}{A \to A}$, which lives in $\Sort{2}$, so it cannot be applied to its own type; a copy at $\Sort{2}$ can. Each level holds the level beneath it, and in practice a few levels suffice; higher levels appear when one quantifies over large collections, such as the category of all small categories.

Why this is safe. Impredicativity looks like the self-reference that the previous section warned against, but it is confined: $\Sort{0}$ contains types that quantify over $\Sort{0}$, yet $\Sort{0}$ is not a member of itself. Coquand showed that one impredicative universe at the bottom is consistent [Coquand 1988], whereas Girard's paradox can already be derived once two levels are impredicative [Hurkens 1995]. With these rules the system is consistent and strongly normalizing (Chapter 14).

Comparison with Lean

In Lean [de Moura and Ullrich 2021], $\Sort{0}$ is Prop, $\Sort{(u+1)}$ is Type u, and $\Pi$-types are assigned universes with $\imax$ as above. Two differences remain.

First, Prop in Lean has definitional proof irrelevance: any two proofs of the same proposition are definitionally equal. Our conversion does not identify proofs; adding this would make conversion depend on types, so the simple "normalize and compare" check of Chapter 12 would no longer suffice.

Second, Lean has universe polymorphism, so definitions can be stated once for all levels $u$, and $\imax$ then matters for level variables as well, with constraints such as $\imax(u, v) \le w$ solved symbolically. In our system every level is a concrete number.

The table summarizes the design space.

Exercises