可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

本书以构造主义的 Cubical 类型论为基础，在其中发展经典集合论。保留构造主义的基础，可以清楚划出经典推理的边界：不需要排中律的定义和证明仍然是构造主义的；真正需要排中律的定理，则把它作为显式参数。如果一开始就在基础理论中预设经典逻辑，定理的陈述本身就无法再显示这种区别。

排中律不仅标志着本书进入经典推理之处，还能解决上一章留下的两个命题大小问题：

排中律

排中律为每个命题给出真假的判定。命题分居不同的宇宙，因此这条原理需要逐层陈述。

定义 (LEM) 我们把「ℓ 层的排中律」记作 LEM ℓ，并将其定义为以下依值函数：对每个 P : hProp ℓ，它返回判定 Dec ⟨ P ⟩；yes 携带 P 的证明，no 则携带它的反驳。由于这个函数量化整个命题宇宙 hProp ℓ，LEM ℓ 位于 Type (ℓ-suc ℓ)。它的层级指标因而准确标明了这项经典假设可以判定哪些命题。

LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → Dec ⟨ P ⟩

事实 (isPropLEM) 对每个层级 ℓ，排中律 LEM ℓ 本身也是命题。

isPropLEM : ∀ {ℓ} → isProp (LEM ℓ)

证明 对每个 P : hProp ℓ，isPropDec 说明 Dec ⟨ P ⟩ 是命题。再由命题对依赖函数的封闭性 isPropΠ 逐点证明结论。

isPropLEM {ℓ} = isPropΠ λ P → isPropDec ⟨ P ⟩isProp

引理 (lowerLEM) 后继层级上的排中律蕴含紧邻低一层的排中律。反复应用该引理，即可继续逐层下降。

lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ

证明 给定 lem : LEM (ℓ-suc ℓ)，并固定 P : hProp ℓ。lem 要求输入 ℓ-suc ℓ 层的命题，因而不能直接判定 P。为此，构造一个高层命题：其底层类型是 Lift ⟨ P ⟩，命题性证书是 isOfHLevelLift 1 ⟨ P ⟩isProp。把这一对交给 lem，便得到 P 的抬升副本的判定。

下图的两个分支说明如何把这一判定转回 Dec ⟨ P ⟩：肯定分支使用 lower，否定分支则假设 P 的证明，并反驳其抬升后的像。函数 mapDec 把这两种转换合在一起。

lowerLEM {ℓ} lem P =
  mapDec lower (λ np p → np (lift p))
    (lem (Lift ⟨ P ⟩ , isOfHLevelLift 1 ⟨ P ⟩isProp))
$$\operatorname{yes}\,\hat x$$
$\operatorname{Lift}\langle P\rangle$ $\hat x$ $\operatorname{lower}$ $\langle P\rangle$ $\operatorname{lower}\,\hat x$
$$\operatorname{yes}\,(\operatorname{lower}\,\hat x)$$
$$\operatorname{no}\,\mathit{np}$$
$\operatorname{Lift}\langle P\rangle$ $\operatorname{lift}\,p$ $\operatorname{lift}$ $\langle P\rangle$ $p$
$$\mathit{np}\,(\operatorname{lift}\,p):\bot_0$$

肯定判定通过 lower 把证明向下搬移。否定判定则临时假设 p : ⟨ P ⟩，经 lift 向上搬移，再由 np 得到矛盾

由排中律得到命题宇宙换级

一旦源层的每个命题都可以判定，就能用两个布尔标签之一来代表它。对任意层级 ℓ₁ 与 ℓ₂，ΩResizing ℓ₁ ℓ₂ 要求 Type ℓ₂ 中有一个与整个 hProp ℓ₁ 类型等价的类型。本章从 ℓ₁ 层的排中律构造这样的分类器，再应用一般定理 ΩResizing→Resizing，把这个对命题宇宙的小表示转化为 Resizing ℓ₁ ℓ₂：源层的每个命题在目标层都有一个与之类型等价的代表。

分类器采用前文引入的类型 Bool，以它的两个构造子 true 与 false 作为标签。

这些标签只是编码，并非 hProp ℓ₁ 中的命题。Bool 位于 Type ℓ-zero，所以要把编码类型提升为目标宇宙 Type ℓ₂ 中的 Lift {ℓ-zero} {ℓ₂} Bool。它的两个标签将分别代表 hProp ℓ₁ 中的 ⊤ 与 ⊥，而这两个命题可用于任意层级。只要构造出这个目标层编码类型与命题宇宙之间的等价，就得到了所需的命题宇宙换级。

构造分为两步。第一步先根据显式判定 Dec ⟨ P ⟩ 定义编码，再定义解码，最后证明两条往返律。我们把这四项辅助结果放在私有子模块 BooleanCodes 中，它们都不使用排中律。第二步的公开定理才调用排中律，为每个 P 统一给出判定，并把这四项结果组装成所需的等价。

private module BooleanCodes where

引理 (encodeB) 存在一个编码操作，它以命题 P 及其判定为输入，返回 Lift {ℓ-zero} {ℓ₂} Bool 中的编码。

encodeB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) → Dec ⟨ P ⟩ → Lift {ℓ-zero} {ℓ₂} Bool

证明 考察给定的判定。yes 分支返回 lift true，no 分支返回 lift false。两个分支都舍去具体的证明或反驳，只保留哪一种结果成立。由于判定是显式给出的，编码过程不使用排中律。

encodeB P (yes _) = lift true
encodeB P (no _)  = lift false

引理 (decodeB) 存在一个解码操作，它以 Lift {ℓ-zero} {ℓ₂} Bool 中的编码为输入，返回 hProp ℓ₁ 中的命题。

decodeB : ∀ {ℓ₁ ℓ₂} → Lift {ℓ-zero} {ℓ₂} Bool → hProp ℓ₁

证明 考察给定的编码。lift true 分支返回 ⊤，lift false 分支返回 ⊥。两个分支都舍去标签，只保留它所代表的命题。由于两种情形都是直接给出的，解码过程同样不使用排中律。

decodeB (lift true)  = ⊤
decodeB (lift false) = ⊥

引理 (secB) 对任意命题 P 及其判定 d，先用 encodeB 编码，再用 decodeB 解码，会在 hProp 中恢复 P：decodeB (encodeB P d) ≡ P。

secB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) (d : Dec ⟨ P ⟩)
     → decodeB {ℓ₁} {ℓ₂} (encodeB {ℓ₁} {ℓ₂} P d) ≡ P

证明 对 d 分情形。若 d = yes p，编码选出 lift true，解码得到 ⊤，所以目标化为 ⊤ ≡ P。命题外延性 ⇔toPath 从两个方向的映射构造这条路径：一个映射返回 p，另一个映射返回 tt*。若 d = no np，编码选出 lift false，解码得到 ⊥，所以目标化为 ⊥ ≡ P。两个方向的映射分别是荒谬函数 λ ()，以及先应用反驳 np、再从 ⊥₀ 消去的函数。因此在两种情形下，先编码再解码都会恢复一个与 P 相等的命题。

secB {ℓ₁} {ℓ₂} P (yes p) = ⇔toPath (λ _ → p) (λ _ → tt*)
secB {ℓ₁} {ℓ₂} P (no np) = ⇔toPath (λ ()) (λ p → ⊥₀-rec (np p))

引理 (retrB) 对任意编码 b̂ 及其解码所得命题的判定 d，先用 decodeB 解码，再用 encodeB 编码，会恢复 b̂：encodeB (decodeB b̂) d ≡ b̂。

retrB : ∀ {ℓ₁ ℓ₂} (b̂ : Lift {ℓ-zero} {ℓ₂} Bool)
        (d : Dec ⟨ decodeB {ℓ₁} {ℓ₂} b̂ ⟩)
      → encodeB {ℓ₁} {ℓ₂} (decodeB {ℓ₁} {ℓ₂} b̂) d ≡ b̂

证明 先对 b̂ 分情形，再对 d 分情形，共有四种组合。若 b̂ = lift true，解码得到 ⊤。证明会再次选出 lift true，所以等式由 refl 成立；反驳则不可能存在，因为把它用于 tt* 就会得到 ⊥₀ 的元素。若 b̂ = lift false，解码得到 ⊥。证明因空模式 () 而不可能；反驳会再次选出 lift false，所以等式也由 refl 成立。因此在所有可能的情形下，先解码再编码都会恢复原编码。

retrB {ℓ₁} {ℓ₂} (lift true)  (yes _)  = refl
retrB {ℓ₁} {ℓ₂} (lift true)  (no n⊤) = ⊥₀-rec (n⊤ tt*)
retrB {ℓ₁} {ℓ₂} (lift false) (yes ())
retrB {ℓ₁} {ℓ₂} (lift false) (no _)  = refl

两条往返律共同表明：只要能为每个命题统一给出判定，编码与解码就互为逆映射。因此，所得分类器将给出真正的类型等价，而不只是用两个真值标签满射地覆盖命题。

候选见证是序对 (Lift Bool , ...)：第一分量位于 Type ℓ₂，第二分量将是类型等价 hProp ℓ₁ ≃ Lift Bool。这里不要求 ℓ₁ 与 ℓ₂ 具有任何大小关系。后文使用的向下实例取 ℓ₁ = ℓ-suc ℓ、ℓ₂ = ℓ，但目标层级也可以与源层级相同或更高。排中律只剩下一项作用：为编码器统一提供所需的判定；以上四项私有结果都是构造主义的。

定理 (LEM→ΩResizing) 对任意层级 ℓ₁ 与 ℓ₂，源层 ℓ₁ 的排中律蕴含从 ℓ₁ 到 ℓ₂ 的命题宇宙换级。

LEM→ΩResizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → ΩResizing ℓ₁ ℓ₂

证明 取 Lift Bool 为第一分量。第二分量使用 isoToEquiv，把下面的同构转化为类型等价。同构的正向映射把 P 送到 encodeB P (lem P)，逆向映射是 decodeB；两条往返律分别使用 retrB 与 secB，并以 lem 给出的判定将其具体化。这两个分量共同构成 ΩResizing ℓ₁ ℓ₂ 所需的见证。

LEM→ΩResizing lem = Lift Bool , isoToEquiv (iso
  (λ P → encodeB P (lem P)) decodeB
  (λ b → retrB {ℓ₁ = _} b (lem (decodeB b)))
  (λ P → secB {ℓ₂ = _} P (lem P)))
  where open BooleanCodes

下图中的两个三角形分别由两条往返律闭合。固定 lem : LEM ℓ₁，把编码类型 Lift {ℓ-zero} {ℓ₂} Bool 简写为 $B$，并记 $E(P) := \operatorname{encodeB}\,P\,(\operatorname{lem}\,P)$、$D := \operatorname{decodeB}$。每次往返所得的点，都由标出的路径与出发点相连。

$B$ $E(P)$ $\operatorname{hProp}\,\ell_1$ $P$ $D(E(P))$ $E$ $D$ $\operatorname{secB}$
$\operatorname{hProp}\,\ell_1$ $D(b)$ $B$ $b$ $E(D(b))$ $D$ $E$ $\operatorname{retrB}$

编码与解码在路径意义下互为逆映射。排中律为 $E$ 提供判定；给定显式判定后，编码、解码与两条往返律都是构造主义的

推论 (LEM→Resizing) 对任意层级 ℓ₁ 与 ℓ₂，源层 ℓ₁ 的排中律蕴含从 ℓ₁ 到 ℓ₂ 的命题换级。

证明 先应用 LEM→ΩResizing 得到命题宇宙换级，再用一般定理 ΩResizing→Resizing 将其转化为命题换级。

LEM→Resizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → Resizing ℓ₁ ℓ₂
LEM→Resizing lem = ΩResizing→Resizing (LEM→ΩResizing lem)

小结

本章把排中律逐层写成 LEM ℓ，证明它本身是命题，并用 lowerLEM 从后继层级的排中律得到紧邻低一层的实例。给定 LEM ℓ₁，LEM→ΩResizing 对任意目标层级 ℓ₂ 构造 ΩResizing ℓ₁ ℓ₂；再与 ΩResizing→Resizing 复合，便得到 Resizing ℓ₁ ℓ₂。因此，源层级上的同一个排中律假设解决了本章开头提出的两个大小问题。