基础词汇

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

学习集合论时，我们谈论集合及其元素，也谈论集合之间的关系和函数。定义告诉我们所讨论的对象是什么，定理陈述这些对象具有怎样的性质，证明则说明这些性质为何成立。本书以集合论为对象理论，以立方类型论为元理论：我们在立方类型论中构造集合论的模型，解释集合论的语句，并证明这些模型满足相应的公理与定理。

这些构造和证明使用 Agda 证明助手书写并检查。Agda 提供形式语言和检查机制，立方类型论为这套形式化提供数学基础，Cubical 库则汇集了在此基础上建立的定义与定理。本书把承载对象理论形式化的这套 Cubical Agda 环境简称为宿主。因此，后文所说的「宿主中的类型」「宿主中的函数」或「宿主层的构造」，都属于元理论一侧，而不是集合论模型内部的对象。

要读懂这些内容，我们先要熟悉宿主中的基础词汇。

本章就从这套语言的基础概念开始。我们将逐个认识它们，既了解其含义，也看看它们如何用于数学陈述与证明。不必急于一次记住所有符号；随着这些概念在后续章节中反复出现，它们的用法会逐渐变得熟悉。需要时，也可以回到本章，重新查阅某个概念的含义。

词汇可溯源

为了便于这样的查阅，我们先说明这些基础概念从何而来，以及如何找到它们的定义。

阅读后续章节时，你会在章首看到一些包含 import 的语句。它们标明本章从哪些模块引入了哪些名称，相当于说明接下来的论证会用到哪些已有概念和结果。遇到不熟悉的名称时，可以先从这些语句确认它的来源，再点击名称查看具体定义。

本章集中引入的基础词汇是这项约定的一个例外。它们在全书中使用得十分频繁，因此统一收集在 Base.Prelude 中，供后续章节整体引入，不再逐个列出。我们会在这里列出所选用的 Cubical 库定义，并说明阅读本书所需的含义与用法，但不逐一展开库内部的构造和证明。希望进一步了解时，可以沿名称链接查阅原始定义，也可以结合 Cubical 库的文档及立方类型论的学习资料继续阅读。

在正式引入这些词汇之前，还有两行简短的代码需要说明：

第一行指定 Agda 检查本章时使用的选项。
展开选项说明
- --cubical 启用立方类型论的语言支持。
- --safe 启用安全模式，禁止直接宣告未经证明的公理，以及绕过终止性检查等做法；需要额外假设的定理仍可以书写，但这些假设必须明确出现在其参数或前提中。
- --guardedness 启用与余递归定义有关的检查。这类定义可以描述不断产生后续内容的对象，例如无限序列；检查的作用是约束递归的方式，使所需的内容能够逐步产生。初读本章时，只需知道这是 Agda 检查此类定义的一项设置，暂时不必掌握其中的技术细节。
第二行为本章对应的模块命名。这里的 Base.Prelude 就是前面提到的基础词汇模块。后续章节通过这个名称引入本章汇集的词汇，而 where 之后的内容构成模块的正文。

{-# OPTIONS --cubical --safe --guardedness #-}
module Base.Prelude where

至此，两行代码的作用和模块正文的位置都已明确，下面开始逐个认识这些概念。

宇宙层级

类型论必须区分类型的大小。若一个类型能够无条件地量化所有类型，它就会包含自身；因此，宿主把类型分入宇宙 Type ℓ，每个层级 ℓ : Level 对应一个宇宙。从代数上看，宇宙层级形成一个带后继算子的有底并半格：ℓ-zero 是底元，ℓ-suc 是后继算子，ℓ-max 是二元并运算。每个宇宙本身也是类型：

Type ℓ : Type (ℓ-suc ℓ)

本书凡检视「所有集合」或「所有命题」这样的总体，陈述所附的层级就记录了该总体被当作多大。

open import Cubical.Foundations.Prelude public
  using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max )

Π 类型

本书后面的许多构造都需要为每个对象给出一项依赖于它的数据。Π 类型正是表达这种关系的基本形式。

给定一个类型 A，以及对每个 x : A 指定的类型 B x，我们可以构造 Π 类型：

(x : A) → B x

Π 类型的元素称为依值函数。给定一个依值函数 f，它为每个 x : A 给出一个属于 B x 的元素 f x。由于结果所在的类型取决于输入 x，只有确定输入以后，才能确定相应输出应当属于哪个类型。

当 B 不依赖 x 时，所有输出都属于同一个类型，依值函数便特化为普通函数：

A → B

普通函数为每个输入给出同一类型中的输出；Π 类型则为每个 x 给出属于相应类型 B x 的数据。

Σ 类型

本书后面的许多构造都需要把某个对象与一项依赖于它的数据放在一起。Σ 类型正是表达这种关系的基本形式。

给定一个类型 A，以及对每个 x : A 指定的类型 B x，我们可以构造 Σ 类型：

Σ (x : A) B x

Σ 类型的元素称为依值对。它先给出一个 a : A，再给出一个属于 B a 的元素 b，所得的对写作 (a , b)。我们把 a 称为第一分量，把 b 称为第二分量。由于第二分量的类型取决于 a，只有确定第一分量以后，才能确定第二分量应当属于哪个类型。

当 B 不依赖 x 时，所有第二分量都属于同一个类型，依值对便特化为普通的积：

A × B := Σ (_ : A) B

普通的积把两个彼此独立的元素放在一起；Σ 类型则把某个 a 与属于相应类型 B a 的数据放在一起。依值对用 _,_ 构造，用 fst 取出第一分量，用 snd 取出第二分量。

Π 类型处理的是「对每个 x，给出依赖于 x 的数据」；Σ 类型处理的是「选定某个 x，并将依赖于它的数据与它放在一起」。

第二分量也可以是关于第一分量的性质证明。本书把这种随对象一同携带、使后续论证能够使用相应性质的证明称为证书。证书仍然是普通的 Agda 证明；这个名称强调的是它在依值对中所起的作用。

open import Cubical.Data.Sigma public
  using ( Σ; Σ-syntax; _×_; _,_; fst; snd )

记录类型

记录类型可以看作多重嵌套的 Σ 类型的语法糖。例如，要把一个元素 a : A、一个依赖于 a 的元素 b : B a，以及一个依赖于前两者的证明 c : C a b 放在一起，可以使用类型：

Σ (a : A) Σ (b : B a) C a b

其中的元素具有如下嵌套形状：

(a , (b , c))

在 Agda 中，关键字 record 开始一个记录类型的声明，随后为其中的各个分量指定字段名。要构造这个记录类型的元素，就必须为各个字段提供相应的值。记录声明还可以用关键字 constructor 为这种构造方式命名；这个名字称为记录类型的构造子。构造子按照字段之间的依赖关系接收各字段的值，再把它们组装成一个记录。例如，若三个字段依次对应 a、b 和 c，构造子 mkR 便可以把构造过程展平地写成：

mkR a b c

这与嵌套 Σ 类型的 (a , (b , c)) 表示同样的数据，只是省去了层层嵌套。字段名则充当投影，可以直接从记录中取出相应分量。因此，使用者不必记忆每个分量位于第几层，也不必反复组合 fst 与 snd。记录类型既保留了多重 Σ 类型的依赖结构，又通过具名字段和构造子提供了更清楚的平面接口。关于记录的声明、构造和投影，可进一步参阅 Agda 的记录类型文档。

宇宙层级之间的搬移

我们使用的 Agda 类型宇宙不是累积的。Type ℓ 的元素并不自动成为 Type (ℓ-suc ℓ) 的元素；在层级之间搬移类型需要显式运算 Lift。

Lift ℓ A 本身是一个记录类型。它只有一个字段 lower : A，用来保存原类型 A 的元素；它的构造子是 lift。给定 a : A，构造子产生 lift a : Lift ℓ A；反过来，给定 b : Lift ℓ A，字段投影 lower b 取出其中保存的 A 的元素。

lift 与 lower 在 A 和 Lift ℓ A 之间互为逆函数。这由两条等式分别表达：

lower (lift a) ≡ a

lift (lower b) ≡ b

第一条等式说，一个元素被装入 Lift 后立即取出，仍是原来的元素。第二条等式说，从 Lift 中取出元素再重新装入，仍得到原来的记录。因此，Lift 改变的是类型所在的宇宙以及元素的表示方式，不会增添或丢失数学信息。

具体来说，若 A 位于 Type ℓ₁，那么 Lift ℓ₂ A 位于 Type (ℓ-max ℓ₁ ℓ₂)。如果两个宇宙层级中已经有一个较高，ℓ-max 就保留那个层级；否则，它给出足以同时容纳二者的公共宇宙层级。因此，Lift 并不是把类型固定抬高若干层，而是把它放入当前所需的足够大的宇宙。

类型总能以这种方式向上复制，但一般不能向下搬移。

open import Cubical.Foundations.Prelude public
  using ( Lift; lift; lower )

相等与路径

在通常的数学语言中，x = y 是一个关于两个对象相等的命题。在类型论中，命题由类型表示，因此相等也由类型表示：对 A 中的两个元素 x 和 y，x ≡ y 是「x 与 y 相等」这一命题所对应的类型，它的元素就是相等的证明。

在立方类型论中，这种相等证明称为从 x 到 y 的路径，而 x ≡ y 称为路径类型。因此，路径并不是相等之外的另一种关系：路径就是本书所使用的相等证明，路径类型就是本书表示相等的方式。路径有起点和终点，因而可以反转方向，也可以首尾相接；下面的基本操作正是从这一结构产生的。

refl 是从一个元素到自身的路径，给出相等的自反性。
sym 反转路径的方向；从 x 到 y 的路径由此变成从 y 到 x 的路径。
_∙_ 把首尾相接的路径复合起来；从 x 到 y，再从 y 到 z，便得到从 x 到 z 的路径。
cong 说明函数保持相等：函数把相等的输入送到相等的输出。cong₂ 是相应的二元版本。
funExt 从逐点相等得到函数相等：如果 f x ≡ g x 对每个 x 都成立，那么 f ≡ g。
transport 沿类型之间的路径搬移元素；subst 则沿 x ≡ y，把依赖于 x 的数据搬移为依赖于 y 的数据。

例如，给定函数 f : A → B，cong 的作用可以概括为：

cong f : x ≡ y → f x ≡ f y

这表示函数 f 可以作用于一条相等路径，把输入之间的相等变成输出之间的相等。

路径本身也是类型中的元素，所以两条路径之间还可以形成新的相等。相等结构由此可以继续向更高层延伸：不仅可以问两个元素是否相等，还可以问它们的相等证明彼此是否相等。下一节将引入一套层次分类，用来衡量一个类型保留了多少层这样的相等结构。

关于 Cubical Agda 中的路径类型，可以参阅 Agda 2.8.0 手册中的 Cubical 章节。本节只使用理解后续构造所需的基本性质。

open import Cubical.Foundations.Prelude public
  using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; funExt )

同伦层级

路径本身也是类型中的元素，所以路径之间还可以形成新的路径。同伦层级按照这些相等证明还能保留多少可区分的结构，对类型进行分类。这里衡量的不是类型的大小；类型的大小由宇宙层级处理，同伦层级关心的是元素及其相等证明如何彼此区分。

isContr A：A 是可缩的。 这要求在 A 中选定一个中心，并为每个 x : A 给出一条从中心到 x 的路径。因此，A 不仅必须有元素，而且所有元素都与选定的中心相等，彼此之间也就无法通过相等加以区分。本书把 isContr 携带的这组数据读作唯一存在：中心给出存在性，所有元素都等于中心则给出唯一性。
isProp A：A 是命题。 这要求 A 中任意两个元素都相等。它不要求预先选定中心，甚至不要求 A 一定有元素；它只说明，一旦 A 有证明，这些证明之间便没有可区分的差别。因此，一个命题可以没有证明，也可以有证明，但不能有两个彼此不同的证明。
isSet A：A 是 h-集合。 前缀标明这是宿主层的概念：h-集合指满足 isSet 的类型，而不是所建模的集合论中的集合。这不要求 A 中任意两个元素都相等，而是要求任意两个元素之间的路径类型本身为命题。换言之，A 的元素可以彼此不同，也可以存在连接某些元素的路径；但给定相同的起点和终点以后，两条这样的路径必定相等。元素层面仍可保留差别，相等证明之间则不再保留可区分的更高结构。
isProp→isSet：命题都是 h-集合。 如果 A 满足 isProp，那么它也满足 isSet。这可以看成一次同伦层级的向上搬移：我们不改变 A，而是从较强的条件「任意两个元素相等」推出较弱的条件「任意两条相等路径彼此相等」。它与 Lift 所做的宇宙层级搬移有一点相似：二者都使同一个数学对象满足较高层级的要求。不过，两者作用于不同的层级轴。Lift 改变类型所在的宇宙，并产生一个与原类型等价的记录副本；isProp→isSet 不改变类型，也不改变它所在的宇宙，只是从已有的相等性质推出另一个相等性质。

open import Cubical.Foundations.Prelude public
  using ( isProp; isSet; isContr; isProp→isSet )

命题宇宙

在立方类型论中，命题是满足 isProp 的类型。这个条件保证该类型的任意两个元素都相等，因此其中只保留「是否存在证明」这一逻辑信息，不再区分不同的证明。类型具有元素时，相应命题成立；无法构造元素时，则尚未得到该命题的证明。

为了把一个命题连同它具有命题性这一事实放在一起，Cubical 库使用 hProp ℓ。它是宇宙层级 ℓ 上所有命题组成的类型；换言之，hProp ℓ 就是该层级上的命题宇宙。一个 P : hProp ℓ 包含两个分量：

第一分量是命题的底层类型，也就是表达命题的类型，即命题的表述本身；
第二分量是该类型确实满足 isProp 的证书。

因此，P : hProp ℓ 表示一个命题，却不表示这个命题已经得到证明。它携带的证书只说明第一分量具有命题性，并不说明第一分量中存在元素。

关于命题宇宙，后文会反复使用两项基本性质：

isSetHProp 表明 hProp ℓ 本身是 h-集合。不同命题仍然可以彼此区分，但命题之间的相等证明不再含有可区分的更高结构。
isPropΠ 表明命题对 Π 类型封闭。若每个 B x 都是命题，那么 (x : A) → B x 也是命题。因此，对一族命题作全称量化，所得结果仍然是命题。

open import Cubical.Foundations.HLevels public
  using ( hProp; isSetHProp; isPropΠ )

投影 ⟨_⟩ 用来取出命题的表述。对于 P : hProp ℓ，⟨ P ⟩ 就是它的第一分量；若要证明 P 所表达的命题成立，则须构造 ⟨ P ⟩ 的元素。命题性证书仍保存在第二分量 P .snd 中。

P 把命题的表述与命题性证书收在同一个对象中，因此可以整体作为函数的参数、返回值或记录的字段使用。需要陈述或证明这个命题时，再通过 ⟨ P ⟩ 取出相应的类型。

open import Cubical.Foundations.Structure public
  using ( ⟨_⟩ )

逻辑运算

命题宇宙对通常的逻辑运算封闭。两个逻辑常量分别是真与假。真命题 ⊤ 始终具有元素，库把它定义为可用于任意宇宙层级的命题。

open import Cubical.Functions.Logic public using ( ⊤ )

假命题由一个表示不可能性的类型构成。空类型 ⊥* 没有元素，也没有构造子。如果某个论证分支中仍然得到 x : ⊥*，该分支的前提便不可能成立，因而可以把 x 消去到任意类型：

⊥* → A

这条原则并非从实际数据中计算出 A 的元素，而是说根本没有需要处理的构造分支。isProp⊥* 证明空类型是命题，理由相同：其中不存在两个需要证明为相等的元素。

open import Cubical.Data.Empty public
  using ( ⊥*; isProp⊥* )

空类型与假命题表达的是同一种不可能性，只是所处的结构层次不同。空类型是 ⊥ 的底层类型；把 ⊥* 与它的命题性证书 isProp⊥* 配成一对，便得到所需宇宙层级上的假命题。

⊥ : ∀ {ℓ} → hProp ℓ
⊥ = ⊥* , isProp⊥*

对命题 P 与 Q，P ⊓ Q 表示二者的合取。它的证书同时包含 P 与 Q 的证明，所在宇宙层级取两个输入层级的最大值。

open import Cubical.Functions.Logic public using ( _⊓_ )

P ⊔ Q 表示析取。和类型会保留证明来自哪一侧的信息，因此库对它作命题截断，只保留两侧至少有一侧成立的信息。

open import Cubical.Functions.Logic public using ( _⊔_ )

P ⇒ Q 表示蕴涵。它的证书是一个函数，把 P 的任意证明变成 Q 的证明；由于 Q 是命题，这个函数类型也具有命题性。

open import Cubical.Functions.Logic public using ( _⇒_ )

¬ P 表示否定：它断言 P 的证明会导出假命题 ⊥，因此其含义由蕴涵与假共同构成。与一般的二元蕴涵不同，否定仍位于 P 所在的宇宙层级。

open import Cubical.Functions.Logic public using ( ¬_ )

对命题族 P : A → hProp ℓ'，∀[ x ∶ A ] P x 表示全称量化：它的证书为每个 x : A 给出 P x 的证明。把类型写在 ∶ 之后，使量词的论域直接呈现在表达式中。

open import Cubical.Functions.Logic public using ( ∀[]-syntax; ∀[∶]-syntax )

∃[ x ] P x 表示存在量化。依值对会同时保留见证 x : A 及其满足 P x 的证明；命题截断忘去具体选择了哪个见证，只保留某个见证确实存在的信息。

open import Cubical.Functions.Logic public using ( ∃[]-syntax; ∃[∶]-syntax )

下一节讨论随对象变化的命题。

类与成员关系

这里的「类」是集合论中的 class，不是类型论中的 type。本书以后约定：类专指 class，类型专指 type。二者在形式化中关系密切，但不是同一个概念。类型规定哪些项可以作为它的元素；类则在已经给定的一批对象中，用一个性质挑出满足它的对象。

类所考察的这批对象称为它的论域。写作 A 时，论域就是一个类型 A，它的元素是当前接受分类的全部对象。称 A 为论域，只说明变量 x : A 可以在这些对象中取值，并不表示 A 已经具有成员关系、运算或其他结构。后文构造集合论模型时，我们会在 A 上加入集合论的成员关系；此时，A 也将成为该模型的载体，它的元素则充当模型中的集合。

论域 A 上的类由一个函数表示：

M : A → hProp ℓ

对于每个 x : A，命题 M x 表示「x 具有类 M 所规定的性质」。因此，M 并不是把 x 送到另一个被收集起来的对象，而是为每个 x 给出一个关于它的命题。满足这个命题的对象，正是属于该类的对象。

这也解释了为什么我们还没有引入集合，就已经可以讨论类。此处的类是在元理论中定义的谓词，只需要一个论域和命题宇宙，并不需要先在对象理论中定义集合，也不声称这个类本身是一个集合。等到后文在这个论域上加入集合论结构以后，我们便可以用这种类描述模型中满足某项性质的集合。

类的成员关系写作 x ∈ᶜ M，读作「x 属于类 M」。它的含义就是 M 为 x 指定的命题：

x ∈ᶜ M := ⟨ M x ⟩

因此，证明 x ∈ᶜ M，就是构造命题 ⟨ M x ⟩ 的证明。上标 ᶜ 表明这里使用的是类的成员关系。它将这个宿主层谓词与后文在集合论模型中解释的集合成员关系区分开来：前者说明一个对象是否满足某项性质，后者则是对象理论语言中的关系。

open import Cubical.Foundations.Powerset public
  using () renaming ( _∈_ to _∈ᶜ_ )

自然数

自然数 ℕ 是由两个构造子生成的归纳类型。构造子 zero 是 ℕ 的元素；构造子 suc 把任意 n : ℕ 变为另一个元素 suc n : ℕ。构造规则为

$$\frac{}{\mathsf{zero}:\mathbb{N}}\qquad\frac{n:\mathbb{N}}{\mathsf{suc}\,n:\mathbb{N}}.$$

ℕ 的每个元素都由这两个构造子生成。相应的归纳原理包含 zero 情形，以及从 n 过渡到 suc n 的归纳步骤。

因此，要递归定义从 ℕ 出发的函数，只需给出函数在 zero 处的值，并说明如何由已经得到的 n 处之值构造 suc n 处之值。

open import Cubical.Data.Nat public
  using ( ℕ; zero; suc )

有限数

Fin 是以自然数为索引的一族类型。Fin zero 没有构造子；当索引为 suc n 时，构造子 zero 直接给出一个元素，而 suc 把 Fin n 的每个元素变为 Fin (suc n) 的元素。构造规则为

$$\frac{}{\mathsf{zero}:\operatorname{Fin}(\operatorname{suc}\,n)}\qquad\frac{i:\operatorname{Fin}(n)}{\mathsf{suc}\,i:\operatorname{Fin}(\operatorname{suc}\,n)}.$$

因此，Fin n 恰有 n 个元素：索引为 zero 时没有元素；索引由 n 变为 suc n 时，新增一个元素，并保留由 Fin n 的每个元素经 suc 构造出的元素。

open import Cubical.Data.FinData public
  using ( Fin; zero; suc )

向量

向量 Vec A n 是由 A 的元素组成、且长度写入类型的列表。它的两个构造规则可以写成

$$\frac{}{[]:\operatorname{Vec}(A,0)}\qquad\frac{a:A\quad v:\operatorname{Vec}(A,n)}{a∷v:\operatorname{Vec}(A,\operatorname{suc}\,n)}.$$

构造子 [] 给出 Vec A zero 的元素。给定 a : A 和 v : Vec A n，构造子 _∷_ 给出 a ∷ v : Vec A (suc n)。自然数索引由此与向量一同确定。函数 lookup 的类型是 Fin n → Vec A n → A；两个参数共享同一个索引 n。

open import Cubical.Data.Vec public
  using ( Vec; []; _∷_; lookup )

恒等函数

恒等函数 id 接受一个元素，并原样返回这个元素。它的类型为：

id : ∀ {ℓ} {A : Type ℓ} → A → A

其中，ℓ 是任意宇宙层级，A 是该层级中的任意类型。由于类型签名没有对 A 增加其他条件，id 可以作用于任何类型的元素。

id x = x

输入 x 本身已经具有结果类型 A，所以可以直接作为结果返回。这个定义既不改变 x，也不需要分析 x 的构造方式。

小结

本章介绍了书中反复使用的宿主层基础词汇：

Type 与 Level 描述类型宇宙及其层级；
Π 类型表示依值函数，Σ 类型表示依值对；
记录类型以具名字段和构造子展平多重嵌套的 Σ 类型；
Lift 在宇宙层级之间搬移类型；
路径类型表示相等，同伦层级描述类型所保留的相等结构；
hProp 是命题宇宙，⟨_⟩ 取出命题的表述；
真与假、合取与析取、蕴涵与否定、全称量化与存在量化，构成命题宇宙上的逻辑运算；
类是取值于命题宇宙的谓词，_∈ᶜ_ 表示类的成员关系；
ℕ、Fin 与 Vec 分别是归纳类型和以自然数为索引的类型族；
⊥* 是空类型，id 是恒等函数。

这些概念共同组成了本书所采用的基本形式语言。