Universes and Prop

Plain-language version: Why there is no type of all types

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

In Lean every type is itself a term, so every type has a type. The types of types are called universes or sorts. They form a hierarchy: Sort 0, Sort 1, Sort 2 and so on, each a member of the next, with no top. The bottom level, Sort 0, is Prop, the universe of propositions, and it obeys different rules from the levels above it. This page sets out the hierarchy, the rule that assigns a universe to a function type, the operation $\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}$ that rule needs, universe polymorphism, and the paradox that makes a hierarchy necessary.

Sorts and their names

Each universe has a level, and Sort u is the universe at level u. Two abbreviations name the cases that matter in practice: Prop is Sort 0, and Type u is Sort (u + 1), with Type alone meaning Type 0, that is, Sort 1.

#check Prop
#check Type
#check Type 3
#check Sort 0
example : Sort 0 = Prop := rfl
example : Sort 1 = Type := rfl
example : Sort (3 + 1) = Type 3 := rfl

Lean prints Prop : Type, Type : Type 1, Type 3 : Type 4 and Prop : Type, and accepts the three equations by rfl: the names are notation for the same terms. The typing rule behind the first four lines is the sort rule of Terms, types and judgments,

$\frac{}{\Gamma ⊢\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}(u+1)}$

and nothing else gives a universe a type. In particular no universe is a member of itself:

example : Type := Type

Lean 4.34.1 rejects it:

Type mismatch
  Type
has type
  Type 1
of sort `Type 2` but is expected to have type
  Type
of sort `Type 1`

Lean's universes are also not cumulative: a type in Type 0 is not thereby in Type 1, and each type has exactly one universe. A type is moved up explicitly, by wrapping it:

example : Type 1 := Nat

fails with Type mismatch, reporting that Nat has type Type but is expected to have type Type 1. The standard wrapper is ULift, a structure with one field, down, whose universe parameter says how far to lift:

#check (ULift.{1} Nat)
example : Type 1 := ULift.{1} Nat

Lean prints ULift Nat : Type 1 and accepts the example. Coq, by contrast, has cumulative universes; Carneiro notes that cumulativity breaks the unique-typing theorem his analysis of Lean relies on.

The universe of a function type

A dependent function type (x : A) → B is a type, so it lives in some universe. The formation rule decides which:

$\frac{\Gamma ⊢A:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u\Gamma ,x:A⊢B:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}v}{\Gamma ⊢(x:A)\to B:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}(\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}uv)}$

where

$\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}uv=\{\begin{array}{cc}0& \text{if }v=0\\ max(u,v)& \text{otherwise.}\end{array}$

There are two cases.

• The codomain is data ($v\ge 1$). The function type lives in the larger of the two universes. A type in Type u may only quantify over types in universes no larger than its own; this is predicativity.
• The codomain is a proposition ($v=0$). The function type is a proposition, whatever the domain. A proposition may quantify over all propositions, or over all types at any level, and still be a proposition; this is impredicativity.

#check ∀ (p : Prop), p → p
#check (α : Type) → α → α
#check (α : Type 2) → Prop
#check (n : Nat) → n = n

The output is

∀ (p : Prop), p → p : Prop
(α : Type) → α → α : Type 1
Type 2 → Prop : Type 3
∀ (n : Nat), n = n : Prop

The first statement quantifies over every proposition, including itself, and is a proposition. The second, the type of the polymorphic identity function on Type, quantifies over Type and so lands one level up, in Type 1. The third is a function type into Prop, not a function type whose values are proofs, so it is data: its codomain Prop lives in Sort 1, and the result is in $\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}(max(4,1))=$ Type 3.

Why imax

The two cases could be stated as two rules. A single operation on levels is needed because of universe polymorphism. A definition may be stated for an arbitrary level variable v, and the rule must give the function type a universe without knowing whether v will later be 0. With $max$ alone that is impossible. The obvious candidate, $maxuv$, goes wrong when v is set to 0: a proposition that quantifies over a type in Sort u would land in $\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}(max(u,0))=\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u$ instead of in Prop, and Prop would not be impredicative. No other expression built from $max$ and successor does better: one that mentions u is never below u, so it is not 0 when v is 0 and u is not, and one that does not mention u cannot equal $max(u,v)$ for every u. $\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}$ is the level expression that reduces to the right case once v is known.

Level expressions are built from numerals, variables, successor, $max$ and $\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}$, and two levels are equal when they denote the same number under every assignment of numbers to their variables. Lean will not treat $\mathrm{i}\mathrm{m}\mathrm{a}\mathrm{x}uv$ as $maxuv$, because the two differ when v is 0:

universe u v

def Fn (α : Sort u) (β : Sort v) : Sort (imax u v) := α → β

#check Fn.{1, 0}
#check Fn.{1, 1}
#check Fn.{0, 2}

The three instances print as Fn : Type → Prop → Prop, Fn : Type → Type → Type and Fn : Prop → Type 1 → Type 1: the same definition gives a proposition-valued result in the first case and data in the other two. Stating the result universe as Sort (max u v) instead is rejected:

universe u v

def Fn2 (α : Sort u) (β : Sort v) : Sort (max u v) := α → β

Type mismatch
  α → β
has type
  Sort (imax u v)
of sort `Type (imax u v)` but is expected to have type
  Sort (max u v)
of sort `Type (max u v)`

Universe polymorphism

A definition may take universe parameters, written after its name as .{u, v}. It is then a schema: each use instantiates the parameters with level expressions, and instantiations at different levels need not be definitionally equal.

set_option pp.universes true in
#check @id
#check @id.{0}
#check List.{0}

Lean prints @id.{u_1} : {α : Sort u_1} → α → α, then @id : ∀ {α : Prop}, α → α for the instance at level 0, where the identity function on proofs is itself a proof of a proposition, and List : Type → Type. This is what lets one identity function, one list type and one equality serve at every level. Without it each would have to be defined once per universe.

Prop

Prop is the universe of propositions. Besides impredicativity, it has properties that the levels above it lack:

• Definitional proof irrelevance: any two proofs of the same proposition are definitionally equal.
• Run-time irrelevance: proofs are erased from compiled code.
• Restricted elimination: except for a class of propositions with at most one proof, a proof cannot be used to produce data, only other proofs.
• Extensionality: logically equivalent propositions are equal, by the axiom propext.

An impredicative universe of propositions is a feature of the Calculus of Constructions of Coquand and Huet, and the theory implemented by Lean's kernel is a version of that calculus. Its strength is real: Carneiro observes that impredicativity corresponds, in a set-theoretic model, to having full power sets. The restriction on elimination is how the rules ensure that no computation can tell which proof of a proposition it has received, as proof irrelevance requires; it is treated on Proof irrelevance and subsingleton elimination.

Why there is a hierarchy

The simplest design would be a single universe containing every type, itself included: Type : Type. That design is inconsistent. In 1972 Girard derived a contradiction in a type system called System U, by formalising a paradox in the style of Burali-Forti's paradox of the largest ordinal. The same argument shows that the first version of Martin-Löf's type theory, which had Type : Type, proves falsity; in type theory the argument is known as Girard's paradox. The Homotopy Type Theory book makes the same point for a universe that contains itself: every type, including the empty one, becomes inhabited.

Hurkens's paper locates the problem precisely. Higher-order logic, in which propositions may quantify over all propositions, is consistent. Adding a single rule, which lets a type be formed by quantifying over the sort of all types, gives the system called $\lambda U^{-}$, which Coquand had already shown inconsistent; Hurkens gives a short term in it whose type is falsity. Impredicativity for propositions alone is therefore consistent, and adding it for types as well is not. Lean's design follows the line exactly: Prop is impredicative, and every universe above it is predicative and contained in the next. The plain-language account is Why there is no type of all types.

How strong the resulting hierarchy is, measured against set theory, is the subject of Consistency and the metatheory.

Next

Inductive types and recursors shows how every type other than universes and function types is introduced, and how the universe rules constrain it.