阅读指南

选择一条阅读路线，查看先修关系，或集中回顾本书的里程碑与术语。

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

阅读指南 · 依赖地图

依赖地图

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

边：
颜色图例

选择章节以追踪先修关系

可向两个方向滚动图；也可切换为全图概览。

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

里程碑

本页汇集全书已经证明的最终成果，也为通往这些成果的阅读路线提供简明入口。每一项先用传统数学书的语言陈述定理，再直接导入证明它的 Agda 声明。

{-# OPTIONS --cubical --safe --guardedness #-}

module Milestones where

定理1 在排中律假设下，宿主层 V 是 ZF 的模型。

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

定理2 在宿主层选择公理的假设下，宿主层 V 是 ZFC 的模型。

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

定理3 在排中律假设下，可构造宇宙 L 是 ZFC 的模型。

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

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

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

术语表

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

对象理论
在元理论中得到表示和研究的理论；在本书中指集合论。
元理论
用来表示和研究对象理论的理论；在本书中指立方类型论。
宿主
承载对象理论形式化的 Cubical Agda 环境。
宇宙层级
类型宇宙 Type ℓ 的大小指标 ℓ；它不同于同伦层级，也不同于可构造层级中的一层。
Π 类型
结果类型可以随输入变化的依值函数类型。
依值函数
Π 类型的元素：它为每个输入给出相应类型中的一个元素。
Σ 类型
第二分量的类型可以依赖第一分量的依值对类型。
依值对
Σ 类型的元素：选定的第一分量，连同属于相应类型的数据。
第一分量
依值对中先给出的那个元素，用 fst 取出。
第二分量
依值对中类型可以依赖第一分量的那个元素，用 snd 取出。
证书
随对象一同携带的证明，使后续论证可以使用它所确立的性质。
字段
记录类型中具名的分量，可用同名投影取出。
构造子
直接生成归纳类型或记录类型元素的基本操作。
投影
从对中取出某个分量、或从记录中取出某个字段的运算。
路径
类型中两个元素之间的相等证明，它有起点与终点，可以反转，也可以首尾相接。
同伦层级
按照元素及其相等证明中还保留多少可区分结构而形成的类型分类。
可缩
带有选定中心、且每个元素都有路径与中心相连的类型。
唯一存在
存在性与唯一性合在一起；本书以可缩类型表示，类型的中心给出所需的见证。
命题
任意两个元素都相等的类型，因此只保留是否存在证明这一信息。
h-集合
相等类型都是命题的类型：元素之间可以有差别，但同一对元素的任意两个相等证明彼此相等。
底层类型
忘掉与一个类型一同打包的性质或结构后所得的类型；对于 P : hProp ℓ，它就是第一分量 ⟨ P ⟩。
空类型
没有任何构造子的类型；因为它没有元素，可以从它消去到任意类型。
命题截断
把一个类型变成命题的运算：它保留该类型是否有元素的信息，却忘去具体是哪一个元素。
类
给定论域上的谓词；本书将它表示为从该论域到命题宇宙的函数。
论域
变量在其中取值的类型；称它为论域，并不为它添加关系、运算或其他结构。
载体
承载一个结构的对象，并供该结构的关系与运算在其上定义的底层类型。
逻辑等价
逻辑等价给出两个方向的蕴含；对于命题，isProp 可将这两个映射提升为类型等价。
类型等价
类型等价 A ≃ B 是纤维皆可缩的映射；逆向映射与两条往返路径可由这个条件导出。
纤维
映射 f : A → B 在 b : B 上的纤维是依值对类型 Σ (a : A) (f a ≡ b)；它的元素由原像及其确实映到 b 的路径组成。
同构
同构显式给出正向映射、逆向映射以及两条逆律。