Bedrock

为 𝑉 的形而上学奠基

以 Cubical Agda 形式化构建集合论的三语交互式教科书。在排中律假设下，证明可构造宇宙 L 满足 ZFC 与 GCH。

原点连接本书的开篇与收尾：先说明这段探索为何而来，再汇集各条证明路线最终抵达的成果。

前言

Bedrock 在 Cubical Agda 中形式化构建集合论，并以机器检验其证明，为关于集合宇宙的探问提供基础。首个已经完成的目标是：可构造宇宙满足 ZFC 与 GCH。全书逐步建立抵达这些成果所需的语言、模型与证明；下面的里程碑则让我们在出发前先看见终点。

这项工作的基本选择，是尽可能用宿主语言表达数学，只在公式本身成为研究对象时使用深嵌入的一阶语言。立方类型论还允许我们把累积层级构造为高阶归纳类型。这是一种数学基础的选择，并不声称元理论比所研究的理论更弱。

越过首个目标，还有关于力迫、内模型和 𝑉 的结构的问题。它们是项目的动力，而不是本书已经宣告的成果。我们的目的，是为这些探问提供经过验证的根基。

里程碑

定理0 SetChoice 蕴含 LEM，而 LEM 蕴含 ΩResizing。

open import Base.Choice public using ( SetChoice→LEM )
open import Base.Classical public using ( LEM→ΩResizing )

定理1 假设 ΩResizing，HIT 累积层级 V 是 ZF 的模型。

open import V.Model public using ( V⊨ZF )

定理2 假设 SetChoice，HIT 累积层级 V 是 ZFC 的模型。

open import V.Model public using ( V⊨ZFC )

定理3 假设 LEM，可构造宇宙 L 是 ZFC 的模型。

open import L.Model public using ( L⊨ZFC )

定理4 假设 LEM，可构造宇宙 L 在内部满足广义连续统假设。

open import L.GCH.Theorem public using ( L⊨GCH )

按主题阅读、并排比较路线，或从已完成的先修继续。

交互式目录 · 依赖图

依赖图

选项与说明

120 个章节的依赖从上向下展开。A → B 表示 B 导入 A。各布局展示同一份先修偏序；没有依赖路径的主题可以穿插学习。悬停追踪先修关系，点击固定。

骨架 (传递约简) 全部直接边

包含原点的引用边

颜色图例

拖动或滑动平移，双指捏合缩放。触摸板滚动平移，Ctrl + 滚轮缩放。方向键平移，+ / − 缩放，0 适合全图，Escape 退出全屏。

图中省略广泛使用的 Base.Prelude 导入边，章节详情仍保留它们。骨架保留可达关系，并不展示每一次直接使用；省略一条边不表示可以删除对应导入。学习阶段不要求把所有章节依次通读；进入汇合章节前，应完成图中所列先修。原点连接开篇与收尾，在此作为终点置于底部。

100%

术语表

术语按它们在全书中的首次出现顺序排列。选择术语即可回到首次引入的位置。

对象理论: 在元理论中得到表示和研究的理论；在本书中指集合论。
元理论: 用来表示和研究对象理论的理论；在本书中指立方类型论。
宿主: 承载对象理论形式化的 Cubical Agda 环境。
宇宙层级: 类型宇宙 Type ℓ 的大小指标 ℓ；它不同于同伦层级，也不同于可构造层级中的一层。
Π 类型: 结果类型可以随输入变化的依值函数类型。
依值函数: Π 类型的元素：它为每个输入给出相应类型中的一个元素。
Σ 类型: 第二分量的类型可以依赖第一分量的依值对类型。
依值对: Σ 类型的元素：选定的第一分量，连同属于相应类型的数据。
第一分量: 依值对中先给出的那个元素，用 fst 取出。
第二分量: 依值对中类型可以依赖第一分量的那个元素，用 snd 取出。
证书: 随对象一同携带的证明，使后续论证可以使用它所确立的性质。
优先级: 省去括号时决定运算符如何分组的规则；它不改变哪些表达式可以构成。
和类型: 归纳类型 A ⊎ B；其元素保留来自 A 或 B 的哪一侧，以及该侧给出的元素。
归纳类型: 由指定构造子生成的类型；相应的归纳原理用于分析它的元素。
构造子: 直接生成归纳类型或记录类型元素的基本操作。
记录类型: 用具名字段组合数据的类型；后面字段的类型可以依赖前面的字段。
字段: 记录类型中具名的分量，可用同名投影取出。
投影: 从对中取出某个分量、或从记录中取出某个字段的运算。
路径: 类型中两个元素之间的相等证明，它有起点与终点，可以反转，也可以首尾相接。
判断相等: 类型系统依据定义与计算规则认定的相等，本书写作 =；它是一个判断，而不是路径类型。
同伦层级: 按照元素及其相等证明中还保留多少可区分结构而形成的类型分类。
可缩: 带有选定中心、且每个元素都有路径与中心相连的类型。
唯一存在: 存在性与唯一性合在一起；本书以可缩类型表示，类型的中心给出所需的见证。
命题: 任意两个元素都相等的类型，因此只保留是否存在证明这一信息。
h-集合: 相等类型都是命题的类型：元素之间可以有差别，但同一对元素的任意两个相等证明彼此相等。
类型等价: 类型等价 A ≃ B 是每束纤维可缩的映射；逆向映射与两条往返路径可由这个条件导出。
纤维: 映射 f : A → B 在 b : B 上的纤维是依值对类型 Σ (a : A) (f a ≡ b)；它的元素由原像及其确实映到 b 的路径组成。
同构: 同构显式给出正向映射、逆向映射以及两条往返律。
往返律: 表达先去再回后在路径意义下恢复输入的规律。对 f : A → B 与 g : B → A，两条往返律分别为对所有输入成立的 g (f a) ≡ a 与 f (g b) ≡ b。
底层类型: 忘掉与一个类型一同打包的性质或结构后所得的类型；对于 P : hProp ℓ，它就是第一分量 ⟨ P ⟩。
命题截断: 把一个类型变成命题的运算：它保留该类型是否有元素的信息，却忘去具体是哪一个元素。
高阶归纳类型 (HIT): 除点构造子外，还允许以路径乃至更高路径作为构造子的归纳类型。
仅仅存在: 用命题截断表达的存在：∥ A ∥₁ 只说 A 有元素而不指定哪一个；对谓词 P，∥ Σ[ x ∶ A ] P x ∥₁ 说满足 P 的见证仅仅存在。
空类型: 没有任何构造子的类型；因为它没有元素，可以从它消去到任意类型。
逻辑等价: 逻辑等价给出两个方向的蕴含；对于命题，isProp 可将这两个映射提升为类型等价。
类: 给定论域上的谓词；本书将它表示为从该论域到命题宇宙的函数。
论域: 变量在其中取值的类型；称它为论域，并不为它添加关系、运算或其他结构。
载体: 承载一个结构的对象，并供该结构的关系与运算在其上定义的底层类型。
命题换级: 命题换级为每个命题在指定宇宙层级选取一个类型等价的代表。
命题宇宙换级: 命题宇宙换级用指定宇宙层级中的一个类型呈现整个命题宇宙。
集合值族的选择: 对 h-集合 X 和取值于 h-集合的族 B，逐点的仅仅有元蕴含一个在每个 B x 中选取元素的依值函数的仅仅存在。SetChoice 同时要求 X 和每个 B x 是 h-集合。
集合商: A / R 具有点 [ a ]、由 R a b 诱导的路径，以及保证其为 h-集合的构造子。若 R 是命题值等价关系，商类间的路径也能反向给出原关系。
对象语言: 用词项和公式写出集合论陈述的形式语言；这些写法的含义另行给出。
词项: 指代单个对象的写法；在这里由常元名或变元位置构成。
常元名: 从 K 中选取、用来构造词项的符号；语法本身并未指定它所指的对象。
常元域: 构造词项或公式时可用的常元名所组成的类型 K；它不必是模型的载体。
语境: 表达式当前可用的变元位置的有限序列，其长度为 n。
变元位置: 当前语境中一个可用的编号槽位，由 Fin n 的元素表示。
公式: 由原子比较、联结词和量词组成的书面陈述；语法本身不判断它是否成立。
原子公式: 直接用成员关系或相等比较两个词项而形成的公式，尚未加入联结词或量词。
量词: 表达「对每一个」或「存在某个」的语法形式，其公式体新增一个变元位置。
约束变元: 由外层量词提供所指对象的变元出现。
自由变元: 不由当前讨论的量词提供所指对象的变元出现；其值来自外层语境。
de Bruijn 索引: 用变元出现处到其约束者之间的层数来表示变元，而不保存变元名。
有界量词: 只在某个词项所描述的集合的元素中量化，而非遍及所有对象的量词。
句子: 没有自由变元的公式；它仍可以含有常元名。
无参: 不含常元名的公式，在这里把常元域取为空类型；它仍可以有自由变元。
环境: 为每个可用变元位置指定载体元素的向量；其长度与词项或公式的语境长度一致。
常元解释: 函数 ι : K → S 为每个常元名指定载体元素；量词扩展变元环境时，这些取值保持不变。
词项求值: 求出词项的载体值 ⟦ t ⟧ γ：常元通过 ι 取值，变元通过 γ 中的位置取值。
满足关系: 固定结构与常元解释后，γ ⊨ φ 是公式 φ 在环境 γ 下成立的命题；赋予这一含义本身并不判定真假。
结构同构: 载体之间保持并反映结构关系的双射；此处的关系是成员关系。

原点

前言

里程碑

选择章节以追踪先修关系

术语表