--- title: "基础词汇" module: Base.Prelude lang: zh site: "Bedrock" description: "基础词汇" stage: "基础" reading_order: 2 canonical: https://bedrock.institute/zh/Base.Prelude.html html: Base.Prelude.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Prelude.lagda.md prerequisites: [] routes: [common-foundations] translations: [https://bedrock.institute/en/Base.Prelude.md, https://bedrock.institute/ja/Base.Prelude.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Prelude where ``` # 基础词汇 本书以集合论为**对象理论**，以立方类型论为**元理论**：在立方类型论中构造集合论的模型，解释其中的句子，并证明其性质。Agda 检查这些构造与证明，Cubical 库提供所需的基础词汇；我们把这套工作环境简称为**宿主**。因此，「宿主中的类型或函数」属于元理论，而不是集合论模型内部的对象。 本章从数学含义和实际用法两方面介绍这些词汇。不必一次记住所有符号：后续章节会从 `Base.Prelude` 统一引入它们，遇到不熟悉的概念时，再回到这里查阅即可。 ## 阅读指南 先读文字，再看紧随其后的代码；代码给出前文的精确表达。带有类型声明和定义等式的定义，在结束处会自动显示 ∎。 可以在[交互式目录](index.html#reading-explorer)中选择阅读路线，也可以用[依赖图](index.html#dependency-map)查看章节间的先修关系。每章顶部的学习路线列出直接先修和可选后续章节。 悬停在带标记的名称或表达式上，可以查看类型；弹窗里的名称也可以继续悬停查看。 关键字和语法符号附有简短解释及 Agda 官方文档链接，术语则链接到首次引入的位置。基础词汇先指向本章的讲解；若想进一步了解库中的定义，可以沿可见的 Cubical 导入代码进入原文。 有了这些线索，下面就从本模块汇集的数学概念读起。 ## 宇宙层级 类型论必须区分类型的大小。若一个类型能够无条件地量化所有类型，它就会包含自身；因此，宿主把类型分入宇宙 `Type ℓ`，每个层级 `ℓ : Level` 对应一个宇宙。从代数上看，宇宙层级形成一个带后继算子的有底并半格：`ℓ-zero` 是底元，`ℓ-suc` 是后继算子，`ℓ-max` 是二元并运算。源码写法 `ℓ-suc ℓ` 在本站紧凑显示为 `ℓ-suc ℓ`；悬停仍可查看原始代码。每个宇宙本身也是类型：
Type ℓ : Type (ℓ-suc ℓ)
本书凡检视「所有集合」或「所有命题」这样的总体，陈述所附的层级就记录了该总体被当作多大。 ```agda open import Cubical.Foundations.Prelude public using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max ) ``` 恒等函数 `id` 是一个在每个宇宙层级上都能统一使用的简单例子。给定任意层级 `ℓ` 以及该层级中的类型 `A : Type ℓ`，它接受 `A` 的一个元素，并原样返回这个元素： ```agda id : ∀ {ℓ} {A : Type ℓ} → A → A ``` 层级参数与类型参数都是隐式的，因此调用时通常只需给出元素。这个元素本身已经具有结果类型 `A`，所以定义等式直接返回它，无须分析它是如何构造出来的。 ```agda id x = x ``` ### 层级之间的搬移 我们使用的 Agda 类型宇宙不是累积的。`Type ℓ` 的元素并不自动成为 `Type (ℓ-suc ℓ)` 的元素；在层级之间搬移类型需要显式运算 `Lift`。 `Lift ℓ A` 是一个记录类型，把原类型 `A` 的一个元素包装起来。给定 `a : A`，函数 `lift` 产生 `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` 并不是把类型固定抬高若干层，而是把它放入当前所需的足够大的宇宙。 类型总能以这种方式向上复制，但一般不能向下搬移。 ```agda open import Cubical.Foundations.Prelude public using ( Lift; lift; lower ) ``` ## 基本类型 下面四种构造组织了全书反复使用的数据。借助它们，我们可以描述随输入而变化的输出、把相互依赖的数据装在一起、区分不同选择，或为较大数据包的各个分量命名。下文会依次给出每种构造的确切名称和形式。 ### Π 类型 本书后面的许多构造都需要为每个对象给出一项依赖于它的数据。Π 类型正是表达这种关系的基本形式。 给定一个类型 `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`，只有确定第一分量以后，才能确定第二分量应当属于哪个类型。 第二分量也可以是关于第一分量的性质证明。本书把这种随对象一同携带、使后续论证能够使用相应性质的证明称为**证书**。证书仍然是普通的 Agda 证明；这个名称强调的是它在依值对中所起的作用。 当 `B` 不依赖 `x` 时，所有第二分量都属于同一个类型，依值对便特化为普通的积：
`A × B = Σ[ _ ∶ A ] B`
普通的积把两个彼此独立的元素放在一起；Σ 类型则把某个 `a` 与属于相应类型 `B a` 的数据放在一起。依值对用 `_,_` 构造。给定依值对 `p`，用 `p .fst` 与 `p .snd` 分别取出它的第一分量和第二分量。对于单字母名称，页面将它们紧凑显示为 `p .fst` 与 `p .snd`；悬停即可查看原始 Agda 写法。 ```agda open import Cubical.Data.Sigma public using ( Σ; _×_; _,_; fst; snd ) ``` 下面的代码块定义了 Σ 类型的两种绑定写法：默认只露出优先级声明，感兴趣时可以展开阅读具体实现。`Σ[ x ∶ A ] B x` 明确给出第一分量的类型，`Σ[ x ] B x` 则让 Agda 推断；两者构造同一个依值对类型。 ```agda infix 2 Σ[]-syntax Σ[∶]-syntax Σ[]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ} → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ') Σ[]-syntax {A = A} B = Σ A B Σ[∶]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ} → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ') Σ[∶]-syntax = Σ[]-syntax syntax Σ[∶]-syntax {A = A} (λ x → B) = Σ[ x ∶ A ] B syntax Σ[]-syntax (λ x → B) = Σ[ x ] B ```
$$f : \prod_{x:A} B(x)$$ $$\begin{array}{rcl} x_1 : A & \longmapsto & f(x_1) : B(x_1) \\[8pt] x_2 : A & \longmapsto & f(x_2) : B(x_2) \\[4pt] \vdots & & \vdots \end{array}$$
$$(a,b) : \sum_{x:A} B(x)$$
$a : A$ $b : B(a)$ $(a,b)$
Π 类型处理的是「对每个 `x`，给出依赖于 `x` 的数据」；Σ 类型处理的是「选定某个 `x`，并将依赖于它的数据与它放在一起」
### 和类型 和类型 `A ⊎ B` 是一种归纳类型，其元素有两种构造方式。给定 `a : A`，可以构造 `inl a : A ⊎ B`；给定 `b : B`，可以构造 `inr b : A ⊎ B`。构造规则为 $$\frac{a:A}{\operatorname{inl}\,a:A\mathbin{\uplus}B}\qquad\frac{b:B}{\operatorname{inr}\,b:A\mathbin{\uplus}B}$$ 这里的 `inl` 与 `inr` 称为**构造子**。因此，和类型的元素同时记录选中了哪一侧，以及该侧所给出的元素；模式匹配可以恢复这两项信息。消去子 `⊎-rec` 分别处理两个构造子：一个分支接收 `A`，另一个分支接收 `B`，两个分支必须产生相同的目标类型。 $$\mathsf{\uplus\text{-}rec}:(A\to C)\to(B\to C)\to A\mathbin{\uplus}B\to C$$ $$\mathsf{\uplus\text{-}rec}\;f\;g\;x= \begin{cases} f(a), & x=\operatorname{inl}\,a,\\ g(b), & x=\operatorname{inr}\,b \end{cases}$$ ```agda open import Cubical.Data.Sum public using ( _⊎_; inl; inr ) renaming ( rec to ⊎-rec ) ``` ### 记录类型 记录类型可以看作多重嵌套的 Σ 类型的语法糖。例如，要把一个元素 `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 的记录类型文档](https://agda.readthedocs.io/en/v2.8.0/language/record-types.html)。 ## 相等与路径 在通常的数学中，$x = y$ 断言两个对象相等。本书把这个断言写作 `x ≡ y`：对 `A` 中的两个元素 `x` 和 `y`，它是一个类型，其中的元素就是二者相等的证明。 我们把 `=` 留给**判断相等** (judgmental equality)，即类型系统依据定义与计算规则把两个表达式认作相同，例如 `id x = x`。在给出定义时，这个 `=` 相当于通常写的 $\mathrel{:=}$；判断相等也包括计算所得到的相等。它是类型系统作出的判断，本身并不是一个需要我们提供证明的类型。相比之下，`x ≡ y` 是一个类型，`p : x ≡ y` 给出其中的相等证明，对应于通常数学中需要证明的 $x = y$。若 `x` 与 `y` 判断相等，下面介绍的常值路径 `refl` 就能证明 `x ≡ y`；反过来，二者之间有路径，一般并不意味着它们判断相等。 在立方类型论中，这种相等证明称为从 `x` 到 `y` 的**路径**，而 `x ≡ y` 称为路径类型。因此，路径并不是相等之外的另一种关系：路径就是本书所使用的相等证明，路径类型就是本书表示相等的方式。路径有起点和终点，因而可以反转方向，也可以首尾相接；下面的基本操作正是从这一结构产生的。
$\operatorname{refl}_x$ $x$
$$\begin{gathered}\operatorname{refl}_x : x\equiv x\end{gathered}$$
`refl` 是从一个元素到自身的路径，给出相等的自反性。
$x$ $y$ $p$ $y$ $x$ $\operatorname{sym}\,p$ $\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{sym}}}$
$$\begin{gathered}p:x\equiv y,\quad\operatorname{sym}\,p:y\equiv x\end{gathered}$$
`sym` 反转路径的方向；从 `x` 到 `y` 的路径由此变成从 `y` 到 `x` 的路径。
$x$ $y$ $z$ $p$ $q$ $p\mathbin{\cdot}q$
$$\begin{gathered}p:x\equiv y,\quad q:y\equiv z\\[3pt]p\mathbin{\cdot}q:x\equiv z\end{gathered}$$
`_∙_` 把首尾相接的路径复合起来；从 `x` 到 `y`，再从 `y` 到 `z`，便得到从 `x` 到 `z` 的路径。
路径的三种基本操作：自反、反转与复合
`cong` 把函数作用到路径上。给定函数 `f : A → B` 和输入之间的路径 `p : x ≡ y`，它构造输出之间的路径 `cong f p : f x ≡ f y`。因此，固定 `f` 后，得到的是一个把路径送到路径的函数：
`cong f : x ≡ y → f x ≡ f y`
这里的两个输出都属于同一个类型 `B`。图中，`f` 把端点 `x` 和 `y` 送到 `f x` 和 `f y`，而 `cong f` 把端点之间的路径送到像之间的路径。`cong₂` 是函数有两个输入时的相应操作。
$$f : A\to B,\qquad p:x\equiv y$$
$x:A$ $y:A$ $p$ $f$ $f$ $f(x):B$ $f(y):B$ $\operatorname{cong}\,f\,p$
`cong`：函数把路径送到端点的像之间的路径
`transport` 把类型之间的路径转为元素之间的函数。给定同一宇宙中的类型 `A`、`B` 和路径 `p : A ≡ B`，它构造从 `A` 到 `B` 的函数 `transport p`。因此，固定 `p` 后，得到的是一个把元素送到元素的函数：
`transport p : A → B`
这里的路径以类型本身为端点。图中，`transport` 把这条路径转为函数，再由这个函数把元素 `a : A` 送到 `transport p a : B`。路径 `p` 提供类型的相等，而 `transport p` 执行元素的搬移。
$$p : A\equiv B$$
$$a : A$$
$$\xmapsto{\;\operatorname{transport}\,p\;}$$
$$b : B$$
$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{transport}}}$$
$$A : \operatorname{Type}_{\ell}$$
$p$
$$B : \operatorname{Type}_{\ell}$$
$$b := \operatorname{transport}\,p\,a$$
`transport`：类型之间的路径给出搬移元素的函数
`subst` 把类型族输入之间的路径转为相应类型之间的函数。给定类型族 `B : A → Type ℓ` 和路径 `p : x ≡ y`，它构造从 `B x` 到 `B y` 的函数 `subst B p`。因此，固定 `B` 和 `p` 后，得到的是一个把元素送到元素的函数：
`subst B p : B x → B y`
这里的路径连接输入 `x` 和 `y`，而被搬移的元素属于 `B x` 和 `B y`。图中，`subst B p` 把 `u : B x` 送到 `subst B p u : B y`。`subst2` 是类型族有两个输入时的相应操作：分别给出两个输入上的路径，即可把数据搬移到新输入对所对应的类型中。
$$B : A \to \operatorname{Type}_{\ell}, \qquad p : x \equiv y$$
$$u : B(x)$$
$$\xmapsto{\;\operatorname{subst}\,B\,p\;}$$
$$v : B(y)$$
$$x : A$$
$p$
$$y : A$$
$$v := \operatorname{subst}\,B\,p\,u$$
`subst`：指标之间的路径给出相应类型之间的函数
这三种操作的联系可以画成下图。每个框表示一个类型，框顶标明类型，框内的点表示它的元素。框之间的箭头表示这些类型之间的函数。从 `x ≡ y` 到 `B x → B y`，可以直接应用 `subst B`，也可以先应用 `cong B`，再应用 `transport`。
$$B : A \to \operatorname{Type}_{\ell}, \qquad x,y:A$$
$x\equiv y$ $B(x)\equiv B(y)$ $B(x)\to B(y)$ $p$ $\operatorname{cong}\,B\,p$ $\operatorname{cong}\,B$ $\operatorname{subst}\,B$ $\operatorname{transport}$ $\operatorname{subst}\,B\,p$ $\operatorname{transport}\,(\operatorname{cong}\,B\,p)$
对每个输入 `p`，两条路线所得的函数都属于同一类型 `B x → B y`。蓝线表示这两个函数之间存在路径。此处省略证明
`funExt` 从逐点相等得到函数相等：如果 `f x ≡ g x` 对每个 `x` 都成立，那么 `f ≡ g`。
$$f,g : A\to B$$
$$h : \prod_{x:A}\bigl(f(x)\equiv g(x)\bigr)$$
$f(x_1)$
$h(x_1)$
$g(x_1)$ $f(x_2)$
$h(x_2)$
$g(x_2)$ $\vdots$
$\vdots$
$\xmapsto{\operatorname{funExt}}$ $\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{funExt}}}$
$f$ $g$ $\operatorname{funExt}\,h$
$$\operatorname{funExt}\,h : f\equiv g$$
`funExt`：每个输入处的路径共同给出函数之间的路径
路径本身也是类型中的元素，所以两条路径之间还可以形成新的相等。相等结构由此可以继续向更高层延伸：不仅可以问两个元素是否相等，还可以问它们的相等证明彼此是否相等。下一节将引入一套层次分类，用来衡量一个类型保留了多少层这样的相等结构。 关于 Cubical Agda 中的路径类型，可以参阅 [Agda 2.8.0 手册中的 Cubical 章节](https://agda.readthedocs.io/en/v2.8.0/language/cubical.html)。本节只使用理解后续构造所需的基本性质。 ```agda open import Cubical.Foundations.Prelude public using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; subst2; funExt ) ``` ## 同伦层级 路径本身也是类型中的元素，所以路径之间还可以形成新的路径。同伦层级按照这些相等证明还能保留多少可区分的结构，对类型进行分类。这里衡量的不是类型的大小；类型的大小由宇宙层级处理，同伦层级关心的是元素及其相等证明如何彼此区分。 - **`isContr A`：`A` 是可缩的。** 这要求在 `A` 中选定一个中心，并为每个 `x : A` 给出一条从中心到 `x` 的路径。因此，`A` 不仅必须有元素，而且所有元素都与选定的中心相等，彼此之间也就无法通过相等加以区分。本书把 `isContr` 携带的这组数据读作**唯一存在**：中心给出存在性，所有元素都等于中心则给出唯一性。 - **`isProp A`：`A` 是命题。** 这要求 `A` 中任意两个元素都相等。它不要求预先选定中心，甚至不要求 `A` 一定有元素；它只说明，一旦 `A` 有证明，这些证明之间便没有可区分的差别。因此，一个命题可以没有证明，也可以有证明，但不能有两个彼此不同的证明。 - **`isSet A`：`A` 是 h-集合。** 通常，h 取自 homotopy (同伦)。在本书中，也可以把它联想为 host (宿主)：h-集合是宿主中满足 `isSet` 的类型，而不是后文要介绍的集合论中的集合。这不要求 `A` 中任意两个元素都相等，而是要求任意两个元素之间的路径类型本身为命题。换言之，`A` 的元素可以彼此不同，也可以存在连接某些元素的路径；但给定相同的起点和终点以后，两条这样的路径必定相等。元素层面仍可保留差别，相等证明之间则不再保留可区分的更高结构。
$$\operatorname{isContr}(A)$$
$$c,x,y : A$$
$c$ $x$ $y$ $h(x)$ $h(y)$
$$c : A,\quad h : \prod_{x:A}(c\equiv x)$$

带有选定中心、且每个元素都有路径与中心相连的类型。

$\Longrightarrow$ $\Downarrow$
$$\operatorname{isProp}(A)$$
$$x,y : A$$
$x$ $y$ $h(x,y)$
$$h : \prod_{x,y:A}(x\equiv y)$$

因此，一个命题可以没有证明，也可以有证明，但不能有两个彼此不同的证明。

$\Longrightarrow$ $\Downarrow$
$$\operatorname{isSet}(A)$$
$$x,y : A,\quad p,q : x\equiv y$$
$x$ $y$ $p$ $q$ $p\equiv q$
$$h : \prod_{x,y:A}\operatorname{isProp}(x\equiv y)$$

相等类型都是命题的类型：元素之间可以有差别，但同一对元素的任意两个相等证明彼此相等。

选定中心、元素相等、路径相等：这三个条件依次减弱
**`isProp→isSet`：命题都是 h-集合。** 如果 `A` 满足 `isProp`，那么它也满足 `isSet`。这可以看成一次同伦层级的向上搬移：我们不改变 `A`，而是从较强的条件「任意两个元素相等」推出较弱的条件「任意两条相等路径彼此相等」。它与 `Lift` 所做的宇宙层级搬移有一点相似：二者都使同一个数学对象满足较高层级的要求。不过，两者作用于不同的层级轴。 ```agda open import Cubical.Foundations.Prelude public using ( isProp; isSet; isContr; isProp→isSet ) ```

宇宙层级

$$\operatorname{Lift}\,\ell_2\,A : \operatorname{Type}_{\ell\text{-max}(\ell_1,\ell_2)}$$
$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{Lift}\,\ell_2}}$$
$$A : \operatorname{Type}_{\ell_1}$$

同伦层级

$$\operatorname{isContr}(A)$$
$$\Longrightarrow$$
$$\operatorname{isProp}(A)$$
$$\Longrightarrow$$
$$\operatorname{isSet}(A)$$
`Lift` 改变类型所在的宇宙，并产生一个携带同样数据的记录副本；`isProp→isSet` 不改变类型，也不改变它所在的宇宙，只是从已有的相等性质推出另一个相等性质
图中的两条轴彼此独立：将类型抬升到另一个宇宙，会保留它的同伦层级。函数 `isOfHLevelLift` 把相应的证书转给 `Lift A`。它的第一个参数指定同伦层级：`0` 表示可缩，`1` 表示命题性，`2` 表示 h-集合性。因此，给定 `h : isProp A`，`isOfHLevelLift 1 h` 就证明 `isProp (Lift A)`；给定 `h : isSet A`，`isOfHLevelLift 2 h` 就证明 `isSet (Lift A)`。这个数字指定的是相等的性质，而非 `Lift` 的目标宇宙。 ```agda open import Cubical.Foundations.HLevels public using ( isOfHLevelLift ) ``` ## 类型等价 路径比较同一个类型中的元素。若要比较类型本身，而且允许它们位于不同的宇宙，我们使用 `A ≃ B`，表示一个映射保留了两边元素及路径中的信息。仅仅存在两个方向的函数还不够；来回映射还必须能够恢复出发时的信息，下面将给出精确定义。 对类型 `A` 与 `B`，`A ≃ B` 是一个依值对。它的第一分量是映射 `f : A → B`；第二分量是依赖于 `f` 的证书。要读懂这份证书，先看下面的定义。 对固定的 `b : B`，`f` 在 `b` 上的**纤维**是下面这个依值对类型：
`Σ[ a ∶ A ] (f a ≡ b)`
纤维的一个元素由两部分组成：第一分量是一个候选原像 `a : A`，第二分量是一条路径 `f a ≡ b`，证明这个 `a` 的确映到 `b`。纤维为空，表示 `b` 没有原像；纤维中若有彼此不能通过路径等同的元素，则表示从 `b` 返回 `A` 时存在实质不同的选择。 ```agda open import Cubical.Foundations.Equiv public using ( _≃_ ) ``` 下面的动画假设每束纤维可缩：存在一个中心，以及一族将纤维中每个依值对连接到中心的路径。
$$F_b=\sum_{a:A}\bigl(f(a)\equiv b\bigr)$$
$A$ $B$ $f$ $a_{00}$ $a_{01}$ $a_{02}$ $a_{03}$ $b_0$ $a_{10}$ $a_{11}$ $a_{12}$ $a_{13}$ $b_1$ $a_{20}$ $a_{21}$ $a_{22}$ $a_{23}$ $b_2$
点击闪烁的三束纤维收拢，再次点击展开。每束路径合并为连接 $f(a_i)$ 与 $b_i$ 的一条路径 $p_i$，原像候选则合并为 $a_i$。这里的重合表示路径意义下的相等。每束纤维可缩，正是 $f$ 成为等价的条件
这里的类型等价需要与同构区分：同构显式给出映射 `f : A → B`、`g : B → A` 和两条往返律：对每个 `a : A` 有路径 `g (f a) ≡ a`，对每个 `b : B` 有路径 `f (g b) ≡ b`。构造子的参数顺序是 `iso f g s r`，其中 `s : (b : B) → f (g b) ≡ b`，`r : (a : A) → g (f a) ≡ a`。二者的联系在于：`iso` 把这些数据打包成 `Iso A B`，`isoToEquiv` 再把所得同构转换为 `A ≃ B`。显式列出映射使同构便于构造具体例子，立方库则以类型等价作为搬运类型结构的统一接口。 ```agda open import Cubical.Foundations.Isomorphism public using ( Iso; iso; isoToEquiv ) ``` 给定 `e : A ≃ B`，便可沿两个方向使用这份等价。函数 `equivFun e : A → B` 就是它的第一分量；`invEq e : B → A` 则借助可缩性证书恢复原像。两个方向来回复合，都会在路径意义下返回输入。特别地，当 `A` 与 `B` 都是命题时，这两个函数把任意一边的证明转换为另一边的证明。 ```agda open import Cubical.Foundations.Equiv public using ( equivFun; invEq ) ``` 类型等价也保留元素之间的路径。记 `f = equivFun e`。对于 `x y : A`，`congEquiv e` 给出类型等价
`(x ≡ y) ≃ (f x ≡ f y)`
它的正向映射是 `cong f`，即把函数作用于路径；逆向映射 `invEq (congEquiv e)` 则从像之间的路径恢复原来元素之间的路径。因此，类型等价既能把路径送过去，也能将其恢复；一般函数的 `cong` 只提供正向操作。 ```agda open import Cubical.Foundations.Equiv.Properties public using ( congEquiv ) ``` 最后，类型等价与 `Lift` 一样保留同伦层级。若 `h : isProp A`，则 `isOfHLevelRespectEquiv 1 e h` 证明 `isProp B`；若 `h : isSet A`，则 `isOfHLevelRespectEquiv 2 e h` 证明 `isSet B`。参数 `0` 同样用于传递可缩性。这里，证书沿等价从 `A` 传到 `B`，即使两者的宇宙不同也成立。 ```agda open import Cubical.Foundations.HLevels public using ( isOfHLevelRespectEquiv ) ``` 因此，我们可以用 `Iso` 构造便于操作的呈现，经 `isoToEquiv` 转换，再用所得等价搬移元素、路径和同伦层级证书。 ## 命题 下面的构造把表达陈述的类型从一般数据类型中区分出来。我们先刻画命题性，再构成命题宇宙，用截断控制存在性信息，用逻辑运算组合命题，最后以命题值谓词描述类。 ### 命题性 在立方类型论中，命题是满足 `isProp` 的类型。这个条件保证该类型的任意两个元素都相等，因此其中只保留「是否存在证明」这一逻辑信息，不再区分不同的证明。类型具有元素时，相应命题成立；无法构造元素时，则尚未得到该命题的证明。 后文会反复使用命题性的四项封闭性质： - `isPropΠ` 表明命题对 Π 类型封闭。若每个 `B x` 都是命题，那么 `(x : A) → B x` 也是命题。因此，对一族命题作全称量化，所得结果仍然是命题。 - `isProp→` 是 `isPropΠ` 不带依赖时的特例。只要值域 `B` 是命题，函数类型 `A → B` 就是命题，而无须要求定义域 `A` 也是命题。 - `isPropΣ` 处理依值对。若 `A` 和每个 `B x` 都是命题，那么 `Σ[ x ∶ A ] B x` 仍是命题。 - `isProp×` 是 `isPropΣ` 不带依赖时的特例。若 `A` 与 `B` 都是命题，那么同时包含二者证明的对仍是命题：任意两个这样的对都逐分量相等。 ```agda open import Cubical.Foundations.HLevels public using ( isPropΠ; isProp→; isPropΣ; isProp× ) ``` 命题性也控制着携带证明的依值对如何相等。若每个可能的第二分量都是命题，`Σ≡Prop` 表明：两个依值对的第一分量相等，就足以推出它们整体相等。证书不携带可进一步区分的选择，所以底层对象相等便能确定整个资料包相等。 ```agda open import Cubical.Data.Sigma public using ( Σ≡Prop ) ``` ### 命题宇宙 为了把一个命题连同它具有命题性这一事实放在一起，Cubical 库使用 `hProp ℓ`。它是宇宙层级 `ℓ` 上所有命题组成的类型；换言之，`hProp ℓ` 就是该层级上的**命题宇宙**。一个 `P : hProp ℓ` 包含两个分量： - 第一分量是命题的底层类型，也就是表达命题的类型，即命题的表述本身； - 第二分量是该类型确实满足 `isProp` 的证书。 因此，`P : hProp ℓ` 表示一个命题，却不表示这个命题已经得到证明。它携带的证书只说明第一分量具有命题性，并不说明第一分量中存在元素。 命题宇宙本身是 h-集合。`isSetHProp` 允许不同命题彼此有别，同时保证命题之间的相等证明不再含有可区分的更高结构。 ```agda open import Cubical.Foundations.HLevels public using ( hProp; isSetHProp ) ``` 投影 `⟨_⟩` 用来取出命题的表述。对于 `P : hProp ℓ`，`⟨ P ⟩` 就是它的第一分量；若要证明 `P` 所表达的命题成立，则须构造 `⟨ P ⟩` 的元素。记号 `⟨ P ⟩isProp` 则取出该底层类型满足 `isProp` 的证书。 `P` 把命题的表述与命题性证书收在同一个对象中，因此可以整体作为函数的参数、返回值或记录的字段使用。需要陈述或证明这个命题时，再通过 `⟨ P ⟩` 取出相应的类型。下图分别示意底层类型为空与有元素的例子：二者都携带命题性证书。 ```agda open import Cubical.Foundations.Structure public using ( ⟨_⟩ ) ⟨_⟩isProp : ∀ {ℓ} (P : hProp ℓ) → isProp ⟨ P ⟩ ⟨ P ⟩isProp = P .snd ```
$$P=(\langle P\rangle,h_P):\operatorname{hProp}\,\ell$$
$$\langle P\rangle:\operatorname{Type}_{\ell}$$
(没有元素)
$$h_P:\operatorname{isProp}\langle P\rangle$$
$$Q=(\langle Q\rangle,h_Q):\operatorname{hProp}\,\ell$$
$$\langle Q\rangle:\operatorname{Type}_{\ell}$$
$p$ $q$ $h_Q\,p\,q$
$$h_Q:\operatorname{isProp}\langle Q\rangle$$
证书 $h_Q$ 为任意两个证明给出路径；右图的曲线表示它在 $p$、$q$ 上的值 $h_Q\,p\,q$
### 命题截断 一个类型所携带的信息可能多于命题应当保留的信息。命题截断 `∥ A ∥₁` 记录 `A` 具有元素，却有意忘去具体是哪一个元素。它是一种高阶归纳类型，简称 HIT：生成它的不仅有点，还有点之间的路径。点构造子 `∣_∣₁` 把每个 `a : A` 送到 `∣ a ∣₁ : ∥ A ∥₁`；路径构造子 `squash₁` 把截断中的任意两个元素认同起来。其定义规则为 $$\frac{a:A}{|a|_1:\|A\|_1}\qquad\frac{x,y:\|A\|_1}{\mathsf{squash}_1(x,y):x=y}$$ 因此，即使 `A` 携带可区分的资料，`∥ A ∥₁` 仍然总是命题。 本书说 `A` 的元素**仅仅存在**，意指 `∥ A ∥₁` 有元素，而没有指定 `A` 中的某个元素。同样，说满足 `P x` 的 `x : A` 仅仅存在，意指 `∥ Σ[ x ∶ A ] P x ∥₁` 有元素。当 `P x` 是命题时，这个截断类型就是后文引入的逻辑存在量化 `∃[ x ∶ A ] P x` 的底层类型。
$A$ $a$ $b$ $\lvert{-}\rvert_1$ $\|A\|_1$ $\lvert a\rvert_1$ $\lvert b\rvert_1$ $\operatorname{squash}_1\,\lvert a\rvert_1\,\lvert b\rvert_1$
给定 `a b : A`，它们在截断中的像由图示路径相连。这两个像未必判断相等；`squash₁` 给出它们之间的相等证明
使用截断值有两种标准方式。递归子 `rec₁` 只有在目标已经证明为命题时，才允许局部取出一个代表；这项限制防止隐藏的选择逸出为普通资料。
`rec₁ : isProp P → (A → P) → ∥ A ∥₁ → P`
$$h : \operatorname{isProp}(P), \qquad f : A \to P$$
$A$ $\|A\|_1$ $P$ $|{-}|_1$ $f$ $\operatorname{rec}_1\,h\,f$
$$\operatorname{rec}_1\,h\,f\,(|a|_1) = f(a) \qquad (a : A)$$
当 `P` 是命题时，`rec₁` 使 `f : A → P` 经由截断分解。对代表 `a`，两条路线都得到 `f a`
映射 `map₁` 在截断内部应用函数 `A → B`，再返回一个截断值。
`map₁ : (A → B) → ∥ A ∥₁ → ∥ B ∥₁`
```agda import Cubical.HITs.PropositionalTruncation as PT open PT public using ( ∥_∥₁; ∣_∣₁; squash₁ ) renaming ( rec to rec₁; map to map₁ ) ``` ### 逻辑运算 命题宇宙对通常的逻辑运算封闭。下面从已经引入的类型构造出发逐项说明这些运算，并解释其中哪些需要命题截断。 #### 真 单元类型表示平凡的证据。它位于 `Type₀` 的零层级形式记作 `⊤₀`，提升到任意宇宙层级 `ℓ` 后记作 `⊤* {ℓ}`；二者的唯一元素分别记作 `tt` 与 `tt*`。单元类型中的任意两个元素都相等，因此 `isProp⊤*` 证明 `⊤*` 是命题。 ```agda open import Cubical.Data.Unit public using ( tt; tt* ) renaming ( Unit to ⊤₀; Unit* to ⊤*; isPropUnit* to isProp⊤* ) ``` 真命题 `⊤` 与单元类型表达的是同一种平凡成立性，只是所处的结构层次不同。单元类型是 `⊤` 的底层类型；把 `⊤*` 与它的命题性证书 `isProp⊤*` 配成一对，便得到所需宇宙层级上的真命题。因此，真属于命题宇宙，因为它的底层单元类型具有元素，且所有元素都相等。 ```agda open import Cubical.Functions.Logic public using ( ⊤ ) ``` #### 假 空类型表示不可能性。它位于 `Type₀` 的零层级形式记作 `⊥₀`，提升到任意宇宙层级 `ℓ` 后记作 `⊥* {ℓ}`。二者都没有元素，也没有构造子。如果某个论证分支中仍然得到 `x : ⊥*`，该分支的前提便不可能成立，因而可以把 `x` 消去到任意类型：
`⊥₀-rec : ⊥₀ → A`
`⊥*-rec : ⊥* → A`
消去子 `⊥₀-rec` 与 `⊥*-rec` 并非从实际数据中计算出 `A` 的元素，而是说根本没有需要处理的构造分支。`isProp⊥` 证明 `⊥₀` 是命题，`isProp⊥*` 则证明 `⊥*` 是命题；理由相同：其中不存在两个需要证明为相等的元素。 ```agda open import Cubical.Data.Empty public using ( ⊥*; isProp⊥* ) renaming ( ⊥ to ⊥₀; rec to ⊥₀-rec; rec* to ⊥*-rec ) open import Cubical.Data.Empty.Properties public using ( isProp⊥ ) ``` 假命题 `⊥` 与空类型表达的是同一种不可能性，只是所处的结构层次不同。空类型是 `⊥` 的底层类型；把 `⊥*` 与它的命题性证书 `isProp⊥*` 配成一对，便得到所需宇宙层级上的假命题。因此，假属于命题宇宙，因为它的底层空类型没有元素，所以其中所有元素空虚地相等。 ```agda ⊥ : ∀ {ℓ} → hProp ℓ ⊥ = ⊥* , isProp⊥* ``` #### 全称量化 对命题族 `P : A → hProp ℓ'`，全称量化就是前文介绍的 Π 类型：它的证明是一个依值函数，为每个 `x : A` 给出 `P x` 的证明。写作 `∀[ x ] P x` 时由 Agda 推断 `x` 的类型；写作 `∀[ x ∶ A ] P x` 时则把这个类型明确列出。这里不需要命题截断。每个 `P x` 都是命题，所以任意两个依值函数逐点相等，再由函数外延性可知它们相等；这正是 `isPropΠ` 所表达的封闭性。 ```agda open import Cubical.Functions.Logic public using ( ∀[]-syntax; ∀[∶]-syntax ) ``` #### 蕴涵 `P ⇒ Q` 表示蕴涵。它的证据是一个函数，把 `P` 的每个证明变成 `Q` 的证明，因此蕴涵就是刚刚介绍的全称量化不带依赖时的特例。这里不需要命题截断：由于 `Q` 是命题，任意两个这样的函数在每个输入上都给出相等的结果，再由函数外延性可知两个函数相等。因此，无论 `P` 有多少证明，这个函数类型本身已经是命题。 ```agda open import Cubical.Functions.Logic public using ( _⇒_ ) ``` #### 否定 否定是从 `P` 到假命题底层空类型的特殊蕴涵，记作 `¬ P`：它断言 `P` 的任何证明都会导出不可能性。与一般的二元蕴涵不同，否定仍位于 `P` 所在的宇宙层级。它为何对命题封闭，可以直接由前文的两项证书看出。首先，`isProp⊥` 说明零层级空类型是命题；随后，`isProp→` 说明只要值域是命题，函数类型就是命题，而无须要求定义域也是命题。把 `isProp→` 用于 `isProp⊥`，便证明了 `¬ P` 的底层类型具有命题性。这里不需要命题截断。 ```agda open import Cubical.Functions.Logic public using ( ¬_ ) ``` #### 命题外延性 命题之间的双向蕴涵称为逻辑等价。命题外延性把它变成命题宇宙内部的相等。双向蕴涵把上文引入的蕴涵打包两次：一个函数从 `P` 到 `Q`，另一个函数从 `Q` 到 `P`。这个包是一个积，也就是 Σ 类型不带依赖时的特例。`⇔toPath` 把这两个函数变成路径 `P ≡ Q`。这里不需要命题截断：因为 `P` 与 `Q` 都是命题，各自的证明不携带可区分的资料，所以两向蕴涵已经表达了建立二者相等所需的全部信息。又因为 `hProp` 是集合，所得的路径类型本身也是命题。 ```agda open import Cubical.Functions.Logic public using ( ⇔toPath ) ``` #### 存在量化 存在量化从前文介绍的 Σ 类型出发，其依值对同时包含见证 `x : A` 与 `P x` 的证明。即使每个 `P x` 都是命题，`A` 中的见证仍可能彼此不同，所以这个 Σ 类型未必是命题。因此，这套记法还要加上命题截断：`∃[ x ] P x` 让 Agda 推断见证的类型，`∃[ x ∶ A ] P x` 则明确写出这个类型；二者都忘掉具体选中了哪个见证，只保留某个见证存在。因此，存在量化需要截断，因为未经截断的证据含有 `A` 中的任意元素；前面的全称量化与蕴涵则没有这种额外资料。 ```agda open import Cubical.Functions.Logic public using ( ∃[]-syntax; ∃[∶]-syntax ) ``` #### 合取 Σ 构造相应的不带依赖的特例是合取。对命题 `P` 与 `Q`，`P ⊓ Q` 的证明就是一对资料，分别包含 `P` 与 `Q` 的证明。与上面的存在量化不同，这里不需要命题截断。因为两个分量本来都是命题，任意两个第一分量彼此相等，任意两个第二分量也彼此相等，所以两对资料必定相等；这正是 `isProp×` 所表达的封闭性。因此，合取可以保留两边的证明而仍为命题，其宇宙层级取两个输入层级的最大值。 ```agda open import Cubical.Functions.Logic public using ( _⊓_ ) ``` #### 析取 另一个二元运算是析取 `P ⊔ Q`。在截断之前，它的证据就是前文介绍的和类型：`inl p` 记录 `P` 的证明 `p`，`inr q` 记录 `Q` 的证明 `q`。即使 `P` 与 `Q` 都是命题，这个和类型也未必是命题；当两边都成立时，左右两个构造子仍然记录着可区分的选择。因此，析取要对这个和类型作命题截断，忘掉所选构造子及其中携带的证明，只保留「至少一边成立」。正是这一步截断使析取仍然取值于命题。 ```agda open import Cubical.Functions.Logic public using ( _⊔_ ) ``` ### 类与成员关系 一个随对象变化的命题，可以从给定的一批对象中挑出恰好使它成立的对象。集合论把这种由性质划定的对象范围称为类。 这里的「类」是集合论中的 **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 ⟩` 的证明。上标 `ᶜ` 表明这里使用的是类的成员关系。它将这个宿主层谓词与后文在集合论模型中解释的集合成员关系区分开来：前者说明一个对象是否满足某项性质，后者则是对象理论语言中的关系。 ```agda open import Cubical.Foundations.Powerset public using () renaming ( _∈_ to _∈ᶜ_ ) ``` 类还确定了由其元素组成的宿主类型 `Σ[ x ∶ A ] (x ∈ᶜ M)`。其中的元素把对象 `x` 与它满足 `M` 的证据配成一对；这个类型不是对象理论中表示 `M` 的集合。若 `A` 是 h-集合，由于每个 `M x` 的底层类型都是命题，Cubical 的引理 `isSetΣSndProp` 保证这个 Σ 类型仍是 h-集合。本书将该引理公开为 `isSetClass`。 ```agda open import Cubical.Foundations.HLevels public using () renaming ( isSetΣSndProp to isSetClass ) ``` ## 更多归纳类型 余下的基础数据类型展示了几种归纳构造：判定为两个答案之一保存证据，布尔类型提供两个不携带数据的标签，自然数支持递归，而带索引的族 `Fin` 与 `Vec` 则把数值界限记录在类型中。 ### 可判定性 判定类型 `A`，就是给出足以确定 `A` 是否有元素的证据。肯定回答携带元素 `a : A`；否定回答携带反驳 `n : A → ⊥₀`，说明任何声称属于 `A` 的元素都会导出不可能性。归纳类型 `Dec A` 恰好把这两种回答作为两个构造子，其构造规则为 $$\frac{a:A}{\mathsf{yes}\,a:\operatorname{Dec}(A)}\qquad\frac{n:A\to\bot_{0}}{\mathsf{no}\,n:\operatorname{Dec}(A)}$$ 因此，`yes a` 记录肯定回答及其见证，`no n` 则记录否定回答及其反驳。与命题析取不同，`Dec A` 不作命题截断：程序可以检查返回了哪个构造子，并使用它携带的证据。对某项有限比较作出判定，完全可以是构造主义的。将在后面的章节中引入的经典原理则更强：它为指定宇宙层级上的每个命题一致地给出这种判定。 对任意类型 `A` 而言，`Dec A` 未必是命题：两项肯定判定可能携带 `A` 中可区分的元素。但若 `A` 是命题，`isPropDec` 便证明它的判定也是命题。此时，肯定答案所携带的见证彼此相等；否定答案因反驳具有命题性而彼此相等；一肯定一否定则不能并存。 ```agda open import Cubical.Relation.Nullary public using ( Dec; yes; no; isPropDec ) ``` 已有的判定也可以转换。要从 `Dec A` 得到 `Dec B`，需要用函数 `f : A → B` 处理肯定情形，并用函数 `g : (A → ⊥₀) → (B → ⊥₀)` 处理否定情形。于是 `mapDec f g` 完成转换：把 `yes a` 送到 `yes (f a)`，把 `no n` 送到 `no (g n)`。只有肯定方向的函数还不够，因为对 `A` 的反驳一般不能反驳 `B`。若另有函数 `r : B → A`，便可用 `λ n b → n (r b)` 补足否定方向。 ```agda open import Cubical.Relation.Nullary public using ( mapDec ) ``` ### 布尔类型 归纳类型 `Bool` 恰有两个构造子：`true` 与 `false`。与一般和类型的构造子不同，这两个构造子都不携带额外数据。其构造规则为 $$\frac{}{\mathsf{true}:\operatorname{Bool}}\qquad\frac{}{\mathsf{false}:\operatorname{Bool}}$$ 因此，要定义一个以 `Bool` 为输入的函数，只需分别给出输入为 `true` 和 `false` 时的结果。当计算需要返回两个可区分的标签之一时，例如有限测试或掩码，布尔值便很有用。它们不应与上文引入的真命题和假命题混淆：`true` 与 `false` 是普通数据类型 `Bool` 的两个值，而不是命题的证明。 ```agda open import Cubical.Data.Bool public using ( Bool; true; false ) ``` ### 自然数 自然数 `ℕ` 是归纳类型，它在 Agda 中的原始构造子为 `zero : ℕ` 与 `suc : ℕ → ℕ`。前者直接给出一个自然数；后者把 `n : ℕ` 变为 `suc n : ℕ`。构造规则为 $$\frac{}{\mathsf{zero}:\mathbb{N}}\qquad\frac{n:\mathbb{N}}{\mathsf{suc}\,n:\mathbb{N}}$$ `ℕ` 的每个元素都由这两个构造子生成。相应的归纳原理包含 `zero` 情形，以及从 `n` 过渡到 `suc n` 的归纳步骤。 对于类型为 `ℕ` 的闭合值，Agda 还允许把 `zero`、`suc zero`、`suc (suc zero)` 分别写成数字字面量 `0`、`1`、`2`。含变量时，原始写法 `suc (suc (suc n))` 在这里也可紧凑显示为 `suc (suc (suc n))`；悬停仍能看到未改动的 Agda 代码。 因此，要递归定义从 `ℕ` 出发的函数，只需给出函数在 `zero` 处的值，并说明如何由已经得到的 `n` 处之值构造 `suc n` 处之值。 加法 `_+_` 合并两个自然数大小；在后续句法章节中，扩张或拼接语境时可用它计算可用变元的数量。 $$\mathord{+}:\mathbb N\to\mathbb N\to\mathbb N$$ $$m+n= \begin{cases} n, & m=0,\\ \operatorname{suc}(m'+n), & m=\operatorname{suc}(m') \end{cases}$$ ```agda open import Cubical.Data.Nat public using ( ℕ; zero; suc; _+_ ) ``` ### 有限数 `Fin` 是以自然数为索引的一族归纳类型。Agda 支持构造子重载：`Fin` 的构造子与 `ℕ` 的构造子同名，都叫 `zero` 和 `suc`。`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` 构造出的元素。 对于类型为 `Fin 3` 的元素，原始表达式 `zero`、`suc zero`、`suc (suc zero)` 会分别紧凑显示为 `zero`、`suc zero`、`suc (suc zero)`。悬停可查看原始构造子表达式及显式标注的类型。 函数 `toℕ` 忘去界限，把有限索引读作自然数。这个遗忘映射保留索引的数值位置，但结果的类型不再记录原来的界限。 $$\operatorname{to\mathbb N}:\operatorname{Fin}(n)\to\mathbb N$$ $$\operatorname{to\mathbb N}(i)= \begin{cases} 0, & i=\mathsf{zero},\\ \operatorname{suc}(\operatorname{to\mathbb N}(j)), & i=\mathsf{suc}\,j \end{cases}$$ ```agda open import Cubical.Data.FinData public using ( Fin; zero; suc; toℕ ) ``` ### 向量 向量 `Vec A n` 是由 `A` 的元素组成、且长度写入类型的列表。两个参数均为单字母时，网页将这个类型简记为 `Vec A n`，读作「`A` 的 `n` 次幂」。这只是显示约定，悬停或轻触可查看原始 Agda 代码。它的两个构造规则可以写成 $$\frac{}{[]:A^{0}}\qquad\frac{a:A\quad v:A^{n}}{a∷v:A^{n^{+}}}$$ 构造子 `[]` 给出 `Vec A zero` 的元素。给定 `a : A` 和 `v : Vec A n`，构造子 `_∷_` 给出 `a ∷ v : Vec A (suc n)`。自然数索引由此与向量一同确定。函数 `lookup` 的类型是 `Fin n → Vec A n → A`；两个参数共享同一个索引 `n`。 对于逐项写出的短向量，网页把 `a ∷ b ∷ c ∷ []` 显示为 `a ∷ b ∷ c ∷ []`。悬停或轻触这个方括号记号，可以查看原始构造子写法和类型。`a ∷ v` 这样的表达式没有逐项写出尾部，仍保留原样。 这些索引使常用的向量操作自带有用的保证。`lookup` 的索引必须属于 `Fin n`，所以越界访问根本无法写出。 $$\operatorname{lookup}:\operatorname{Fin}(n)\to A^{n}\to A$$ $$\operatorname{lookup}(i,a\mathbin{∷}v)= \begin{cases} a, & i=\mathsf{zero},\\ \operatorname{lookup}(j,v), & i=\mathsf{suc}\,j \end{cases}$$ 下图用有限索引选取长度为三的向量中的位置。
$$v=a\mathbin{∷}b\mathbin{∷}c\mathbin{∷}[]:A^{3}$$
$a$$b$$c$
$$i\mapsto\operatorname{lookup}\,i\,v$$
$\operatorname{Fin}(3)$ $0$ $1$ $2$ $A$ $a$ $b$ $c$
每一列对齐向量中的一个位置、它的索引和查找结果。`Fin 3` 恰好提供三个合法索引；分量 `a`、`b`、`c` 本身可以相同
函数 `map` 对每个分量应用同一个函数而不改变长度。 $$\operatorname{map}:(A\to B)\to A^{n}\to B^{n}$$ $$\operatorname{map}(f,v)= \begin{cases} [], & v=[],\\ f(a)\mathbin{∷}\operatorname{map}(f,w), & v=a\mathbin{∷}w \end{cases}$$ ```agda open import Cubical.Data.Vec public using ( Vec; []; _∷_; lookup; map ) ``` ## 小结 本章介绍了书中反复使用的宿主层基础词汇： - `Type` 与 `Level` 描述类型宇宙及其层级； - Π 类型表示依值函数，Σ 类型表示依值对，和类型区分由两个输入类型中哪一侧构造出的元素； - 记录类型以具名字段和构造子展平多重嵌套的 Σ 类型； - `Lift` 在宇宙层级之间搬移类型； - 路径类型表示相等；`transport`、`subst` 及其双参数推广 `subst2` 沿路径搬移数据； - 同伦层级描述类型保留的相等结构；命题性对 Π 类型、Σ 类型和积封闭，`Σ≡Prop` 把携带证明的依值对相等归结为第一分量相等； - 类型等价 `A ≃ B` 表示一个映射的每束纤维可缩；`Iso` 通过显式映射与往返律构造它，所得等价在类型之间传递元素、路径与同伦层级； - `hProp` 是命题宇宙，`isSetHProp` 描述其相等结构，`⟨_⟩` 取出命题的表述； - 命题截断 `∥ A ∥₁` 保留 `A` 是否有元素，却忘去具体见证；`rec₁` 把它消去到命题，`map₁` 则把它映射到另一个截断； - 真与假、合取与析取、蕴涵与否定、全称量化与存在量化，构成命题宇宙上的逻辑运算；命题外延性把两个方向的蕴涵变成命题相等； - 类是取值于命题宇宙的谓词，`_∈ᶜ_` 表示类的成员关系； - `Dec A` 保留 `A` 的一个元素或一份反驳；若要为任意命题一致地给出这种判定，则还需要额外原理； - `Bool` 是二元素数据类型，其构造子 `true` 与 `false` 提供两个可区分的计算标签； - `ℕ` 提供自然数及其加法，`Fin n` 提供小于 `n` 的索引，`Vec A n` 提供带长度索引、不会越界查找且映射后长度不变的序列； 这些概念共同组成了本书所采用的基本形式语言。