Lean 4 的类型系统里有一个经常被初学者忽视的维度：每个类型本身也有类型，类型的类型称为 universe（宇宙）。忽视这一维度，往往导致一类难以直觉理解的报错——类型不匹配、universe 不一致、无法做大消除。本篇聚焦 universe 层级的实际操作，包括 Prop 与 Type u 的区别、universe 多态定义、以及常见 universe 错误的诊断方法。

前置阅读：本系列 01 Lake 项目结构与依赖管理和 02 Term-mode 与 Tactic-mode 的切换心法；形式化方法系列准备 Lean 4 实验环境。

Universe 层级

Lean 4 的类型层级是一个无穷塔（infinite tower），用 Sort 统一表示：

1	`Sort 0 : Sort 1 : Sort 2 : Sort 3 : ...`

Prop 是 Sort 0 的别名，Type 是 Type 0 = Sort 1 的别名，Type 1 是 Sort 2，以此类推。

#check Prop      -- Prop : Type
#check Type      -- Type : Type 1
#check Type 1    -- Type 1 : Type 2
#check Sort 0    -- Sort 0 : Sort 1
#check Sort 1    -- Sort 1 : Sort 2

Prop : Type 这个输出乍看像循环，实际上是 Prop : Sort 1 的显示简写——Type 在这里就是 Type 0 = Sort 1，不是悖论。

整个塔的规则来自依值类型论（CIC，Calculus of Inductive Constructions）的 predicativity（直谓性）原则：一个 universe 不能包含自身。Type u 只能包含 Type v（v < u）中的类型，以防止 Girard 悖论。

`#check` 查看 universe

1
2
3

#check @List      -- List.{u_1} : Type u_1 → Type u_1
#check @Prod      -- Prod.{u_1, u_2} : Type u_1 → Type u_2 → Type (max u_1 u_2)
#check @Eq        -- Eq.{u_1} : {α : Sort u_1} → α → α → Prop

@ 前缀让 Lean 显示所有隐式参数，包括 universe 参数。Eq 活在 Prop，因为等式是逻辑命题；List 和 Prod 活在 Type，因为它们是数据结构。

`Prop` 与 `Type`：核心区别

证明无关性

Prop 中的类型具有证明无关性（proof irrelevance）：同一命题的任意两个证明在 Lean 的定义等价意义下相等。

1	`#check @proof_irrel -- proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂`

模式匹配无法从 Prop 的证明中提取内容——Prop 的值只有两个层面的意义：有证明（真）或无证明（假）。具体证明项是什么不影响任何计算。

Type 没有这条约束：Nat 的值 0 和 1 不同；true 和 false 是不同的 Bool 值。

大消除限制

大消除（large elimination）是指：对某个归纳类型做 match，根据不同分支返回类型本身（而不是类型的值）。Prop 中的类型不允许大消除，因为那会破坏证明无关性。

试图从 Or 的证明中提取数据：

-- 这段代码会报错
def getLeft (h : True ∨ False) : Bool :=
  match h with
  | Or.inl _ => true
  | Or.inr _ => false

Or 是 Prop 中的归纳类型。对它 match 然后返回 Bool（Type 中的类型）就是大消除，Lean 会拒绝：

1
2
3

error: type mismatch
  ...
  Or.rec can only eliminate into Prop

正确做法是在 Prop 层面推理，或换用 Decidable（Type 中的版本）：

-- 在 Prop 层推理（结论也是 Prop）
theorem or_true_implies_something (h : True ∨ False) : True := by
  cases h with
  | inl ht => exact ht
  | inr hf => exact hf.elim

-- 使用 Decidable（可计算版本）
def getLeft' (h : Decidable True) : Bool :=
  match h with
  | Decidable.isTrue _  => true
  | Decidable.isFalse _ => false

InfoView 目标状态（当执行 cases h，h : True ∨ False，目标是 Bool 时）：

case inl
h✝ : True
⊢ Bool
-- Lean 此时会报错：Or.rec 只能消除到 Prop，无法产生 Bool

`Prop` 与 `Type` 的归属原则

放在 `Prop`	放在 `Type`
逻辑命题（`P ∧ Q`、`∀ x, P x`、`a = b`）	数据类型（`Nat`、`List α`、`Bool`）
存在性断言（`∃ x, P x`，只关心存在，不关心见证）	带计算内容的存在（`Σ x, P x`，Sigma type）
定理（`theorem`）	函数、构造子、可执行值（`def`、`fun`）
不需要在运行时提取的证据	需要在运行时提取的数据

Universe 多态

`universe` 声明

当一个定义对任意 universe level 都成立，应声明为 universe 多态（universe-polymorphic），使其可在任何 universe 下实例化：

universe u v

structure Pair (α : Type u) (β : Type v) : Type (max u v) where
  fst : α
  snd : β

#check @Pair              -- Pair.{u, v} : Type u → Type v → Type (max u v)
#check Pair Nat Bool      -- Pair Nat Bool : Type
#check Pair (Type) (Type 1)  -- Pair Type (Type 1) : Type 2

max u v 是 universe level 算术：Pair 的 universe 是两个组件 universe 的最大值。Pair Nat Bool（两者都在 Type 0）得到 Type 0；Pair (Type) (Type 1) 得到 Type 2。

函数签名中的 universe 参数

universe u

-- 显式 universe 参数：α 和 β 约束在同一 universe
def swap {α : Type u} {β : Type u} (p : α × β) : β × α :=
  ⟨p.2, p.1⟩

-- Type* 自动引入独立 universe 变量，α 和 β 可以在不同 universe
def swap' {α : Type*} {β : Type*} (p : α × β) : β × α :=
  ⟨p.2, p.1⟩

#check @swap   -- swap.{u} : {α : Type u} → {β : Type u} → α × β → β × α
#check @swap'  -- swap'.{u_1, u_2} : {α : Type u_1} → {β : Type u_2} → α × β → β × α

Type* 等价于 Type _（underscore），让 Lean 自动引入一个新的 universe 变量。swap 约束 α 和 β 在同一个 universe；swap' 允许它们在不同 universe。

term-mode 与 tactic-mode 在 universe 多态函数中的写法对比：

-- term mode：直接构造配对
theorem pairSwap {α : Type*} {β : Type*} (p : α × β) : β × α :=
  ⟨p.2, p.1⟩

-- tactic mode：同样结论，用 exact 或展开为 constructor
theorem pairSwap' {α : Type*} {β : Type*} (p : α × β) : β × α := by
  exact ⟨p.2, p.1⟩
  -- 或者展开：
  -- constructor
  -- · exact p.2
  -- · exact p.1

Universe 约束推断

Lean 4 的 universe 推断是约束求解：每次使用一个多态定义，Lean 生成约束（等式或不等式），再用最小 universe 解满足所有约束。

def pairExample : Pair Nat String := ⟨42, "hello"⟩
-- Lean 推断 Pair.{0, 0}，因为 Nat 和 String 都在 Type 0

def mixedPair : Pair Nat (Type) := ⟨0, Bool⟩
-- Lean 推断 Pair.{0, 1}，因为 Nat : Type 0，Type : Type 1
#check mixedPair  -- mixedPair : Pair Nat Type

常见 Universe 错误诊断

把 `Type` 当 `Prop` 用

-- 报错：
-- def bad (α : Type) : Prop := α
-- error: type mismatch
--   α has type Type : Type 1
--   but is expected to have type Prop : Type

Type 不是 Prop，两者分属不同 universe（Sort 1 vs Sort 0）。要表达"某个类型非空"，用 Nonempty：

1 2	`def isNonempty (α : Type) : Prop := Nonempty α #check @Nonempty -- Nonempty.{u_1} : Sort u_1 → Prop`

Universe 不一致

1
2
3

-- 报错：
-- def AllTypes : Type := Type
-- error: "Type" has type "Type 1" which is not definitionally equal to "Type"

Type 0 不能包含 Type 0 自身，违反直谓性。要把 Type 作为值，需要更高一级：

1 2	`def TypeLevel1Example : Type 1 := Type #check TypeLevel1Example -- TypeLevel1Example : Type 1`

从 `Prop` 提取数据（大消除）

已在上节展示。两个诊断要点：

报错含 can only eliminate into Prop：对 Prop-valued 归纳类型做大消除
报错含 type mismatch，右侧是 Prop 而左侧是 Type：universe 混淆

`noncomputable` 与选择公理

从 Prop 的存在性证明中提取见证值需要选择公理，对应标记 noncomputable：

noncomputable def witness {α : Type} {p : α → Prop} (h : ∃ x, p x) : α :=
  Classical.choose h

#check @Classical.choose
-- Classical.choose : {α : Sort u_1} → (∃ x, p x) → α

noncomputable 不是 universe 错误，但经常因为同一类跨 Prop/Type 边界操作而触发。

速查表

概念	Lean 4 写法	说明
Prop（Sort 0）	`Prop`	命题，证明无关
Type（Sort 1）	`Type` 或 `Type 0`	普通数据类型
Type n（Sort n+1）	`Type n`	更高层 universe
统一表示	`Sort n`	n=0 是 Prop，n≥1 是 Type (n-1)
Universe 多态参数	`universe u` / `Type u` / `Type*`	允许在任意 universe 实例化
查看 universe 层级	`#check @Foo`	显示隐式 universe 参数
证明无关性	`proof_irrel`	Prop 中所有证明等价
大消除限制	`Or.rec can only eliminate into Prop`	Prop 不能产生 Type 数据
非构造性提取	`noncomputable` + `Classical.choose`	选择公理绕过大消除限制

练习

练习 1：用 #check 验证以下表达式的 universe 层级，并解释结果：

1
2
3

#check @And
#check @Sum
#check @Sigma

And 在 Prop，Sum 和 Sigma 应该在哪？用 universe 层级解释二者的区别。

练习 2：定义 universe 多态的三元组类型 Triple，使其满足：

1 2	`Triple Nat Bool String : Type Triple (Type) (Type 1) Nat : Type 2`

用 #check 验证。提示：需要 universe u v w 和 max u (max v w)。

练习 3：下面的定义合法，但可以改造成会触发 universe 错误的版本。找出一个真正会报错的变体，分析错误信息，给出修复方案：

1 2	`def ContainsNat (α : Type) : Prop := Nonempty (α → Nat)`

参考资料

Theorem Proving in Lean 4，Universes 章节：https://leanprover.github.io/theorem_proving_in_lean4/universes.html
Functional Programming in Lean，Polymorphism 章节：https://lean-lang.org/functional_programming_in_lean/
Lean 4 源码，Init/Prelude.lean：Prop、Sort、proof_irrel 的定义
Mathlib4 文档，Universe Polymorphism：https://leanprover-community.github.io/mathlib4_docs/
Lean Zulip，“universe polymorphism” 话题