The classical boundary

多数读者熟悉的集合论是经典的：排中律如空气般无处不在。然而宿主是构造性的，本书把两者之间的边界作为法条保持可见。纲领定下的规则是：经典原理一律作为显式参数进入，绝不作为全局假设。凡经典论证的章节都在自己的接口上言明，类型检查器守卫这条边界，全书没有一个 postulate。本章陈述后文一切经典论证所诉诸的那唯一原理，并存入它的两笔基本红利：上一章的非直谓性诸接口，在此赎回。

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

module Base.Classical where

open import Base.Prelude
open import Base.Truth
open import Base.Impredicativity
  using ( isSmall; Resizing; HPropSmallness; Impredicativity )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool using ( Bool; true; false )
open import Cubical.Data.Unit using ( tt* )
open import Cubical.Foundations.Equiv using ( propBiimpl→Equiv )
open import Cubical.Foundations.Isomorphism using ( iso; isoToEquiv )
open import Cubical.Functions.Logic using ( ⇔toPath )

陈述

LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)

LEM ℓ 说的是：层级 ℓ 上的每个命题要么真要么假。为什么取这个形式？在 univalent 基础中，类型层的全局选择或排中律与 univalence 不相容；能够一致地假设的恰是这个对 hProp 量化的命题形式。是基础本身逼出了这个诚实的措辞。

经典论证的章节在模块参数表中取 (lem : ∀ {ℓ} → LEM ℓ)，并在导入其他经典章节时把它传递下去。这带来一个值得停下体会的后果：一条定理是否用了排中律，是编译期事实。经典债务是章节类型的一部分，在每个导入处可见，而不是一条看不见的全局公理；又因为无一处 postulate，全书佩戴 Agda 的 --safe 印章。

红利之前先备一条传递引理。排中律沿层级向下通行：要判定一个小命题，把其底层类型抬高一层宇宙，在那里判定，再把裁决降回来。于是较高层级上的单个 LEM 实例默默覆盖其下每一层，本章结尾就要花掉这个事实。

lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ
lowerLEM {ℓ} lem P = fromLifted (lem lifted)
  where
  lifted : hProp (ℓ-suc ℓ)
  lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y))
  fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
  fromLifted (inl p)  = inl (lower p)
  fromLifted (inr np) = inr (λ p → np (lift p))

第一笔红利：小分类器

经典地看，命题只有两个可能的值，而这句不起眼的话在宇宙层级上有实实在在的后果。先看分类器：上一章命名的 HPropSmallness ℓ，索要一个与 hProp ℓ 等价的小类型。经典地看它就是 Lift Bool，在每一个层级 ℓ 上皆然。构造被刻意安排为：全部实际工作都是构造性的，下面四个助手把命题的判定 (一个证明，或一个反驳) 当作普通参数接收；排中律只在最后的总装处出场，负责供应这些判定。

本章先兑现作用域纪律的承诺：打开典范实例，恰取其中的 ⊤ 与 ⊥。自此这两个符号就是 hProp 代数的真值，且由定义性透明，这个 ⊥ 就是 (⊥* , isProp⊥*) 这个对本身。然后做解码方向，从布尔值到命题：decodeB 把 true 送到 ⊤、false 送到 ⊥。定义域取 Lift {ℓ-zero} {ℓ} Bool 而非裸 Bool，因为 Bool 住在最底层而命题住在 ℓ 层：正是这份提升的副本，让即将登场的等价两端住进同一个宇宙。

open module Canonical {ℓ : Level} = TruthAlgebra (hPropAlgebra ℓ) using ( ⊤; ⊥ )

private
  decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ
  decodeB (lift true)  = ⊤
  decodeB (lift false) = ⊥

编码方向藏着一处不对称。它「本该」有签名 hProp ℓ → Lift Bool，即 decodeB 的严格逆向，但这样的函数定义不出来：与 lift true、lift false 不同，任意命题 P 不是可供模式匹配的东西，写不出「若 P 成立、否则如何」的分支。所以 encodeB 多收一个参数，即 P 的判定 d，转而对它做匹配：有证明就是 true，有反驳就是 false。形状与 decodeB 相仿，但被检视的对象是递来的判定，从来不是命题本身。这里没有排中律；判定是输入。

  encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool
  encodeB P (inl _) = lift true
  encodeB P (inr _) = lift false

第一趟往返：把 P 编码再解码，得回 P 自身。工具是 ⇔toPath，即库的命题外延性：命题之间，两个方向的映射就足以给出一条路径 (在本书中，这条原理是定理而非公理)。若判定是证明 p，目标为 ⊤ ≡ P，两个方向都平凡：从 ⊤ 到 P，答案 p 已在手上；反向则一切送到 ⊤ 的居民 tt*。若判定是反驳 np，目标为 ⊥ ≡ P：从 ⊥* 出发无话可说，荒谬模式 λ () 说的正是这个；而任何声称的 P 之证明 p 都被 np 击碎，Empty.rec 消去随之而来的荒谬。

  secB : ∀ {ℓ} (P : hProp ℓ) (d : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥))
       → decodeB (encodeB P d) ≡ P
  secB P (inl p)  = ⇔toPath (λ _ → p) (λ _ → tt*)
  secB P (inr np) = ⇔toPath (λ ()) (λ p → Empty.rec (np p))

另一趟往返：把布尔值 b 解码再编码，得回 b。有一处细微值得注意：总装时来判定 decodeB b 的将是排中律，而它递来哪个判定无从许诺。所以 retrB 对每一个判定 d 证明该等式，分四种情形。true 配证明：refl。true 配所谓反驳 n⊤：不可能，因为 ⊤ 明明成立，n⊤ tt* 即是荒谬。false 配所谓证明：该证明是 ⊥* 的项，荒谬模式 () 在欠下任何等式之前就了结此案。false 配反驳：refl。

  retrB : ∀ {ℓ} (b : Lift {ℓ-zero} {ℓ} Bool)
          (d : ⟨ decodeB b ⟩ ⊎ (⟨ decodeB b ⟩ → Empty.⊥))
        → encodeB (decodeB b) d ≡ b
  retrB (lift true)  (inl _)  = refl
  retrB (lift true)  (inr n⊤) = Empty.rec (n⊤ tt*)
  retrB (lift false) (inl ())
  retrB (lift false) (inr _)  = refl

总装。iso 把四件套打包 (解码；先判定、再编码；两趟往返)，isoToEquiv 把同构升级为等价。数一数 lem 的出场：三次，且三次干的是同一件事，为构造性助手供应它们当作输入索要的判定。这就是排中律在这笔红利中的全部足迹。

lem→hPropSmallness : ∀ {ℓ} → LEM ℓ → HPropSmallness ℓ
lem→hPropSmallness lem = Lift Bool , isoToEquiv (iso decodeB
  (λ P → encodeB P (lem P))
  (λ P → secB P (lem P))
  (λ b → retrB b (lem (decodeB b))))

第二笔红利：命题降层

第二笔，Resizing：高一层的每个命题都是小的。经典地做：判定该命题，若成立则等价于 ⊤，若不成立则等价于 ⊥，而两者都是小的。

与之前一样，工作从递来的判定做起，其中直接用到 P .snd (命题性证明，正如序章预告的那样)。若 P 成立，小替身取 ℓ 层的 ⊤：命题之间，两个方向的映射就足以构成底层类型的等价，这正是 propBiimpl→Equiv 从两侧的命题性证明与两个映射装配出的东西；从 P 到 ⊤ 一切送到 tt*，反向则 p 已在手上。若 P 不成立，替身取 ⊥，两手荒谬招式与 secB 相同。留意与第一笔红利的差别：那里产出的是命题之间的路径 (⇔toPath)，这里产出的是底层类型之间的等价，于是同样的一对映射改喂给 propBiimpl→Equiv。

private
  resizeDec : ∀ {ℓ} (P : hProp (ℓ-suc ℓ)) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
            → isSmall P
  resizeDec P (inl p)  = ⊤ , propBiimpl→Equiv (P .snd) (⊤ .snd) (λ _ → tt*) (λ _ → p)
  resizeDec P (inr np) = ⊥ , propBiimpl→Equiv (P .snd) (⊥ .snd)
                               (λ p → Empty.rec (np p)) (λ ())

总装只有一行：用排中律判定 P，把判定递过去。签名就是强度记账：这笔红利在较高层级 ℓ-suc ℓ 上消费排中律，一次，仅此而已。

lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ
lem→resizing lem P = resizeDec P (lem P)

赎回打包

上一章把两件器具打包为 Impredicativity，依据是共同消费而非相互蕴含：谁也推不出谁。唯有排中律能一次赎回两件，而且只需较高层级上的单个实例：降层原样消费它，lowerLEM 把它的低层副本递给分类器。第三部将用这份打包开出自己的准确价格。

lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ
lem→impredicativity lem = record
  { resizing       = lem→resizing lem
  ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) }

小结

排中律以接口 LEM 的形式陈述，由章节作为参数领取，绝不全局假设；构造与经典数学的边界因此成为编译期事实。上一章的两个接口作为红利入账：小分类器经 lem→hPropSmallness，命题降层经 lem→resizing；打包 Impredicativity 整份赎回 (lem→impredicativity)。第三部将恰好花掉这份打包：它为累积层级 V 给全分离与幂集背后的小性假设标价。