1.7 Types and Universes

Lean is a dependently typed system. Every expression has a type, and types themselves are classified by universes. Understanding this hierarchy explains why definitions typecheck, how polymorphism works, and why some constructions require explicit universe control.

Problem

You want to understand what Type, Prop, and universe levels mean, how Lean prevents paradoxes, and how to write definitions that work uniformly across many types.

Solution

Use #check to inspect universe levels and observe how Lean assigns types to types.

#check Nat
#check Type
#check Type 1
#check Prop

Typical output:

Nat : Type
Type : Type 1
Type 1 : Type 2
Prop : Type

This reveals the key structure:

• Nat is a type
• Type is itself a type, but at a higher level
• universes form a hierarchy Type 0, Type 1, Type 2, …
• Prop is a special sort used for logical statements

Universe Hierarchy

Lean avoids logical inconsistencies by stratifying types into levels.

The hierarchy is:

Type 0 : Type 1 : Type 2 : Type 3 : ...

By convention:

• Type means Type 0
• Type 1 is the next universe
• and so on

You can check:

#check Type 0
#check Type 1
#check Type 2

Each level lives in the next.

This prevents self-referential definitions such as “the type of all types that do not contain themselves”.

Prop vs Type

Prop is the universe of logical propositions.

#check True
#check False
#check 1 = 1

Output:

True : Prop
False : Prop
1 = 1 : Prop

Key differences:

Proofs in Prop are not used for computation. Lean treats them as logically meaningful but computationally irrelevant.

Example:

def f (n : Nat) (h : n = n) : Nat :=
  n

The argument h is ignored at runtime.

Functions Between Types

A function type:

Nat -> Nat

means a function from Nat to Nat.

More generally:

α -> β

where α and β are types.

Dependent functions allow the result type to depend on the input:

(x : Nat) -> Fin (x + 1)

This expresses that the result type varies with x.

Polymorphism

Lean supports polymorphic definitions using type parameters.

def identity (α : Type) (x : α) : α :=
  x

Check:

#check identity

Result:

identity : (α : Type) -> α -> α

This function works for any type α.

Using implicit arguments:

def identity' {α : Type} (x : α) : α :=
  x

Now Lean infers α:

#check identity' 5
#check identity' true

Universe Polymorphism

A more general definition works across universe levels:

universe u

def id_univ {α : Type u} (x : α) : α :=
  x

Here:

• u is a universe variable
• α may live in any universe

Check:

#check id_univ

Result:

id_univ : {α : Type u} -> α -> α

Without universe polymorphism, definitions would be restricted to Type 0.

Example: Polymorphic Container

universe u

structure Box (α : Type u) where
  val : α

Check:

#check Box

Result:

Box : Type u -> Type u

This works uniformly for any universe level.

Dependent Types

Dependent types allow types to depend on values.

def vector (α : Type) (n : Nat) := Fin n -> α

Here the type depends on n.

Example usage:

#check vector Nat 3

Result:

vector Nat 3 : Type

Dependent types are central to encoding precise specifications.

Implicit Universe Inference

Lean usually infers universe levels automatically.

def const {α β : Type} (x : α) (y : β) : α :=
  x

Lean assigns universe variables behind the scenes.

Only introduce explicit universes when needed.

Common Pitfalls

If Lean reports a universe mismatch, the types live in incompatible universe levels.

If a definition works for Nat but not for general types, it may be missing polymorphism.

If implicit arguments fail, the universe parameter may need to be explicit.

If types become too large, inspect their universe levels with #check.

Minimal Working Example

universe u

def pair {α : Type u} (x y : α) : α × α :=
  (x, y)

#check pair 3 4

Expected:

pair 3 4 : Nat × Nat

Takeaway

Types in Lean are organized into a hierarchy of universes. Type classifies data, Prop classifies logical statements, and universe levels prevent inconsistencies. Polymorphism and dependent types allow definitions to work uniformly across many structures. Understanding this system is necessary for writing general, reusable, and correct Lean code.