Universe (Lean)

Definition

Universe (Lean)

In Lean, Type u is a universe of types at level u. Types themselves have types:

Nat    : Type 0
Type 0 : Type 1
Type 1 : Type 2

Type abbreviates Type 0. The declaration universe u introduces a level parameter, allowing definitions to work at different levels.

Why types need types

To quantify over something, Lean needs its type:

∀ (x : M), ...       -- range over elements of M
∀ (M : Type 0), ...  -- range over types serving as domains

The second line allows M = Nat, because Nat : Type 0. But suppose the domain’s elements should themselves be types, and we choose M = Type 0. This requires M : Type 1, since:

Type 0 : Type 1      -- not Type 0 : Type 0

An unrestricted type containing all types, including itself, would permit logical paradoxes. Lean instead separates the levels: the universe containing a type is not that type itself.

Levels are not cardinalities: Nat and Real both live in Type 0, despite one being countable and the other uncountable.

Why use a level parameter?

Rather than write separate definitions for domains in Type 0, Type 1, and so on, write:

universe u

A definition using M : Type u can then be instantiated at different levels. For each chosen u, ∀ (M : Type u), ... ranges over domains at that level—not over all levels simultaneously.

Example

Validity in every nonempty structure

import Mathlib.ModelTheory.Semantics
open FirstOrder
 
universe u
 
def Valid (L : Language) (τ : L.Sentence) : Prop :=
  ∀ (M : Type u) [Nonempty M] [L.Structure M], M ⊨ τ

Here M is the structure’s domain, whereas u is Lean’s level for its type:

x : M       -- an element of the domain
M : Type u  -- the domain's type level

The bracketed instance parameters supply nonemptiness and interpretations of the language’s symbols. M ⊨ τ says that the resulting structure satisfies τ.

We could replace Type u with Type for an initial version of K23. Using u adds generality; it does not change the proof by reducts and expansions.