选择原理

经典数学并不只有排中律。给定一族非空集合，可以同时从每个集合中各取一个元素；对有限或显式描述的族，这是例行手续，而对以任意集合为指标的族，它是一条真正的原理，即选择公理。类型论把这里的「非空」严格化了。在基础理论中，纤维 B x 的元素藏在它的命题截断 ∥ B x ∥₁ 之后：截断记录纤维有元素，却忘去是哪个元素。截断只能向命题消去，所以从这种形状的假设取不出真实的元素。《基础词汇》指出过：要从截断的存在陈述取出一个真正的函数，需要一条选择原理。因此这条原理的假设只能是每根纤维都仅仅有元。结论同样保留截断：它断言的是一个同时在每根纤维中取值的函数的仅仅存在，而不是函数本身。陈述从一开始就含有一项限制：指标类型必须是 h-集合；Diaconescu 定理的证明正需要这一点。

集合层选择与 LEM 都逐层级陈述，因此两族具有相同的外层类型 ∀ ℓ → Type (ℓ-suc ℓ)。二者内部量化的对象不同：排中律遍历命题，选择则遍历 h-集合 X、其上的族 B，以及各纤维仅仅有元的证明。两项原理都不被全局假设；需要其中一项时，章节会把所需层级的实例作为显式参数。

本章围绕三个问题展开。选择原理在这里断言什么，在哪些层级上断言？高一层宇宙的一个假设能否覆盖其下的层级？这条原理又有多强？最后一个问题由 Diaconescu 定理回答：SetChoice ℓ 蕴含 LEM ℓ，即 choice→lem。因此在每个层级上，选择接口都已给出排中律，两个接口并不平级。模型章两度依赖这一点：choice→lem 从一个 SetChoice (ℓ-suc ℓ) 实例取得驱动 ZF 公理的排中律，lowerSetChoice 把同一实例降到所需层级，供选择集公理使用。

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

module Base.Choice where

open import Base.Prelude
open import Base.Classical using ( LEM )

open import Cubical.Foundations.Prelude using ( Path )

Diaconescu 定理的证明是一个有限论证，用到三份具体材料。布尔类型 Bool 连同 true 与 false 构成两点类型，其相等由 _≟_ 判定。单元类型 Unit* 有唯一元素 tt*，isPropUnit* 记录它为命题，论证由此随处可得一条平凡成立的陈述。两个布尔值的比较返回 Dec 的元素：要么 yes 连同相等，要么 no 连同反驳。

open import Cubical.Foundations.HLevels using ( isOfHLevelLift )
open import Cubical.Data.Bool using ( Bool; true; false; _≟_ )
open import Cubical.Data.Unit using ( Unit*; tt*; isPropUnit* )
open import Cubical.Relation.Nullary using ( Dec; yes; no )
import Cubical.Data.Sum as Sum

除此之外，证明还需要两个构造。第一个是命题截断 ∥_∥₁，《基础词汇》已经介绍：它恰好保留一个类型的有元性，忘去元素是哪一个，所以从 ∥ A ∥₁ 取不出 A 自身的元素。第二个是集合商，本书在此首次用到；它从类型与关系构造类所成的类型，Diaconescu 构造就将在一个集合商内部进行。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.SetQuotients
  using ( _/_; [_]; eq/; squash/; []surjective; effective )

任意关系都可以生成集合商。本章还要使用更强的 effectivity 定理，把商类的相等反向读成原关系；这条定理要求关系取值于命题并满足等价律。库以 record 表述这两项条件，粘合关系将分别证明它们。

open import Cubical.Relation.Binary.Base using ( module BinaryRelation )

原理

原理在固定的层级 ℓ 上比较一个关于每根纤维的假设与一个关于全体纤维的结论。数据是 Type ℓ 中的指标类型 X、X 是 h-集合的证明、X 上的纤维族 B，以及对每个 x 的假设 ∥ B x ∥₁。结论 ∥ ((x : X) → B x) ∥₁ 说的是，仅仅存在一个同时在每根纤维中取元的函数。截断出现在两侧，这正是原理的准确强度。假设给出的不超过仅仅有元，结论断言的也不超过仅仅存在；真实的选择函数恰是缺失的东西，把它造出来正是这条假设的全部内容。由于陈述量化了整个 Type ℓ，它居于高一层的 Type (ℓ-suc ℓ)，理由与 LEM 相同。

SetChoice : ∀ ℓ → Type (ℓ-suc ℓ)
SetChoice ℓ = (X : Type ℓ) → isSet X → (B : X → Type ℓ)
            → ((x : X) → ∥ B x ∥₁) → ∥ ((x : X) → B x) ∥₁

与排中律一样，应用中的选择往往只拿到一个高层实例，再由一条下降引理把它换到所需的层级。lowerSetChoice 的类型是 SetChoice (ℓ-suc ℓ) → SetChoice ℓ：假设高一层宇宙的选择，恢复层级 ℓ 的选择。与 lowerLEM 一样，这里使用的工具是 Lift，即《基础词汇》中把 Type ℓ 的类型放进 Type (ℓ-suc ℓ) 中呈现、再取回来的运算。

给定层级 ℓ 的数据，证明先把它搬到高一层，使假设 sc 得以适用。指标类型 X 变为 Lift X，其 h-集合性由 setX 经 isOfHLevelLift 得到，库中这条定理说明抬升不扰动同伦层级。纤维族变为 λ x → Lift (B (lower x))：抬升指标上的纤维就是底下原指标上纤维的抬升，所以移动后的族与原族包含完全相同的信息。

lowerSetChoice : ∀ {ℓ} → SetChoice (ℓ-suc ℓ) → SetChoice ℓ
lowerSetChoice sc X setX B inh =
  PT.map (λ f x → lower (f (lift x)))
         (sc (Lift X) (isOfHLevelLift  setX)
             (λ x → Lift (B (lower x)))

其余输入以同样的方式移动。每个抬升纤维都仅仅有元，因为把指标降下、再对所得截断映射 lift，就给出所需的元素；PT.map 在截断内部作用，所以假设恰以原理所要求的形式成立。当 sc 返回抬升选择函数 f 的仅仅存在时，再一次 PT.map 给出降低后函数的仅仅存在，其在 x 处的值为 lower (f (lift x))。最后一步之所以合法，是因为目标是截断内部的陈述：至于这个具体的 f，截断之外没有任何主张。

             (λ x → PT.map lift (inh (lower x))))

Diaconescu 定理

定理说的是：给定集合层选择，任何命题 P 都可判定，即或证明或反驳。从构造性的观点看，这个结论远非显然：任意的 P 不提供可供分情况处理的切入口，判定程序也没有可以直接检视的内容。证明转而从几何入手。它构造一个形状依赖于 P 的小空间：其中 true 的类与 false 的类恰在 P 成立时重合。把这个空间上的一个问题交给选择原理，形状便暴露出来，而形状就是 P。

具体地，固定命题 P : hProp ℓ，在一个专属于该定理的模块中工作。取两个布尔值，恰在 P 成立时把它们粘起来。粘合即集合商：点仍是 true 与 false，但凡粘合关系如此断言，就添一条路径，结果做成 h-集合。关系是一张四格表：对角格平凡成立，混色的两格就是 P 本身。由最后这一条，「跨两点相关」与 P 是同一个陈述，论证将两次用到它。

粘合关系 _~_ 由对两个布尔值的模式匹配定义，表中四格一目了然。两个输入一致时，关系以单元类型 Unit* 的唯一元素 tt* 成立。二者相异时，关系以 ⟨ P ⟩ 的一个证明成立，即 P 的底层陈述。此外别无他用：从表中读出混色两格，就已经证明了跨两点相关所说的恰是 P。

module Diaconescu {ℓ} (P : hProp ℓ) where

  _~_ : Bool → Bool → Type ℓ
  true  ~ true  = Unit*
  false ~ false = Unit*
  _     ~ _     = ⟨ P ⟩

空间本身 Glued 是集合商 Bool / _~_。类型按关系取商时，点被保留，而只要给出关系关联二者的证明，构造子 eq/ 就添加路径 [ b ] ≡ [ b' ]；构造子 squash/ 再把结果做成 h-集合。它的两个特殊点是类 [ true ] 与 [ false ]。P 成立时，商在两点间提供路径；P 不成立时，下面的倒读会把两类分开。

  Glued : Type ℓ
  Glued = Bool / _~_

此后的一切都系于集合商的一条定理，即库的有效性：对取值于命题且满足等价律的关系，类与类之间的路径之所以存在，只是因为关系确实关联了代表元。因此商中的路径可以倒读为关系成立的证明。表格逐格供应该定理所要求的各个条件，下面几段逐一验证。

第一个条件是命题值性：对每对输入，a ~ b 的证明类型必须是命题。对角线上该类型是 Unit*，由 isPropUnit* 知其为命题；混色两格中它就是 ⟨ P ⟩ 自身，其命题性恰是 P 的第二分量 P .snd。若证明可以彼此不同，商中的路径就无法确定一个良定义的陈述供倒读。

  ~-prop : BinaryRelation.isPropValued _~_
  ~-prop true  true  = isPropUnit*
  ~-prop false false = isPropUnit*
  ~-prop true  false = P .snd
  ~-prop false true  = P .snd

自反性是直接的：两条对角格无条件成立，于是每个布尔值都与自身相关，各情形的证明都是 tt*。

  ~-refl : (a : Bool) → a ~ a
  ~-refl true  = tt*
  ~-refl false = tt*

  ~-sym : (a b : Bool) → a ~ b → b ~ a
  ~-sym true  true  _ = tt*

对称性成立，因为表本身对称：交换输入把每格映到自身，a ~ b 的证明即可充当 b ~ a 的证明。对角线上两个方向的证明都是 tt*；混色两格中它是 P 的证明，两个方向说的是同一件事。

  ~-sym false false _ = tt*
  ~-sym true  false p = p
  ~-sym false true  p = p

  ~-trans : (a b c : Bool) → a ~ b → b ~ c → a ~ c
  ~-trans true  _     true  _ _ = tt*

传递性要多想一步，因为两个证明的组合原则上可能要求表中不存在的格。逐情形检查可知这不会发生：两端一致时，某条对角格使结论平凡成立；两端相异时，给定的两个证明中必有一个来自混色格，而另一个此时只涉及相等的布尔值，于是同一个 P 的证明就充当结论。六个分支覆盖所有情形，每个都复用某个输入。

  ~-trans false _     false _ _ = tt*
  ~-trans true  false false p _ = p
  ~-trans false true  true  p _ = p
  ~-trans true  true  false _ p = p
  ~-trans false false true  _ p = p

三条定律由构造子 BinaryRelation.equivRel 组装为记录 isEquivRel _~_。有了命题值性与等价律，Glued 便恰好满足有效性的全部假设，其路径的倒读对下面的引理可用。

  ~-equivRel : BinaryRelation.isEquivRel _~_
  ~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans

构造的核心是一个两行论断：两个特殊类重合，当且仅当 P 成立。若 P 成立，表关联 true 与 false，商便等同两个类。若两类重合，有效性报告说关系关联了 true 与 false，而按表，该关系就是 P。混色格在两个方向上工作：P 的证明直接交给路径构造子，有效性的输出本身已是 ⟨ P ⟩ 的证明，无需解码，也没有需要排除的不可能情形。

两个方向成为具名函数。正向的 glue 把 P 的证明交给路径构造子：混色格以证明 p 成立，按商的定义两个类相等。反向的 unglue 是在 true 与 false 处例示的有效性：两类之间的任何路径返回 true ~ false 的证明，按表即 ⟨ P ⟩ 的证明。无需对路径作任何分情形。二者合起来，构成 P 与两类相等之间的词典。

  glue : ⟨ P ⟩ → Path Glued [ true ] [ false ]
  glue p = eq/ true false p

  unglue : Path Glued [ true ] [ false ] → ⟨ P ⟩
  unglue = effective ~-prop ~-equivRel true false

现在用上选择原理，问题只有一个：为 Glued 的每个点选出一个布尔代表元。一点处的选取是一个布尔值连同「其类等于该点」的保证。每个点单独地必有一次选取，但只能证明其仅仅存在：商记得自己的点来自代表元，却不记得来自哪一个。把这种逐点的仅仅有元转化为一个处处同时选取的函数的仅仅存在，正是集合层选择所述的内容；它在此适用，因为 Glued 按构造是 h-集合。选取函数在整个空间上一致地起作用；最后的比较只在两个特殊类处读取它。

被选取的族是 Pick x，一个依赖对：布尔值 b 连同见证类 [ b ] 等于点 x 的路径。每个点都仅仅有选取，这不是额外假设而是关于商的定理：[]surjective 说商的每个元素都仅仅作为某个代表元的类出现，pickable 就是把这句话按 x 取遍 Glued 读出的形式。注意第二分量的用处：它记录选的是哪个代表元；后面论证要重建类与类之间的路径，靠的正是这份证书，而非单独的布尔值。

  Pick : Glued → Type ℓ
  Pick x = Σ[ b ∈ Bool ] ([ b ] ≡ x)

  pickable : (x : Glued) → ∥ Pick x ∥₁
  pickable = []surjective

这个问题值得单独立为引理，好让类型原样展示选择所给出之物：在整个 Glued 上定义的选取函数的仅仅存在。给定 sc : SetChoice ℓ，引理用至今备好的数据例示它：指标 Glued、其 h-集合证明 squash/、族 Pick、逐点的有元性 pickable。假设 sc 本身是函数；被截断的只是它的输出。于是选择给出的不是函数，只是「有一个」的陈述，这一限制将塑造定理的最后一步。

  merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁
  merePicker sc = sc Glued squash/ Pick pickable

设 picking 函数 g : (x : Glued) → Pick x 已经在手。在两个特殊点处求值得到两次选取，其第一分量是布尔值 b₀ 与 b₁，分别在 true 的类与 false 的类处选出。此后的推理只关乎这两个普通布尔值，正是这一点使 P 得以机械判定。两条引理按方向把这两个值与 P 相连：若代表元一致，它们的保证给出从 true 的类到 false 的类的路径，有效性把它读成 P；若 P 成立，两个特殊点相等，g 尊重这条相等，于是 b₀ 与 b₁ 一致。

  module _ (g : (x : Glued) → Pick x) where

    b₀ : Bool
    b₀ = g [ true ] .fst

    b₁ : Bool
    b₁ = g [ false ] .fst

第一条引理把相等 q : b₀ ≡ b₁ 倒读为 P。三条路径在 Glued 中复合：从 true 的类到 b₀ 的类 (g [ true ] 的保证)，再到 b₁ 的类 (q 经 cong [_] 诱导的类相等)，再到 false 的类 (g [ false ] 的保证)。复合路径从一个特殊类走到另一个，unglue 把它变成 ⟨ P ⟩ 的证明。第二条引理正向而行：给定 P 的证明 p，路径 glue p 等同两点，沿它应用 g 便得 b₀ ≡ b₁；两端都是普通布尔值，所以这只是 g 的直接投影，无需对族作任何搬运。

    agree→P : b₀ ≡ b₁ → ⟨ P ⟩
    agree→P q = unglue (sym (g [ true ] .snd) ∙ cong [_] q ∙ g [ false ] .snd)

    P→agree : ⟨ P ⟩ → b₀ ≡ b₁
    P→agree p i = g (glue p i) .fst

现在改由两个布尔值判定 P。与 P 不同，它们可以被检视：两个布尔值相等或不相等，机械可判。若二者一致，第一条引理证出 P。若二者相异，P 必不成立，因为它若成立，第二条引理将迫使二者一致。无论哪边 P 都被判定；分情形发生在选出的两个布尔值上，从未触及 P 自身。

可判定相等 _≟_ 比较 b₀ 与 b₁，返回 Dec (b₀ ≡ b₁) 的元素：要么是携带相等证明的 yes，要么是携带反驳的 no。辅助函数 fromDec 经词典转换每种结果。yes 情形中，相等 q 送入 agree→P，产出左侧和项，即 ⟨ P ⟩ 的证明。

    decide : ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥)
    decide = fromDec (b₀ ≟ b₁)
      where
      fromDec : Dec (b₀ ≡ b₁) → ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥)
      fromDec (yes q) = Sum.inl (agree→P q)

no 情形中，ne 证明两个布尔值不可能相等。若 P 成立，P→agree 会给出二者相等，与 ne 相抵；右侧和项因此是这样的函数：取任一 ⟨ P ⟩ 的证明，经正向引理得到 b₀ ≡ b₁，再交给 ne。两种情形合起来判定 P，分情形只在布尔数据上进行。

      fromDec (no ne) = Sum.inr (λ p → ne (P→agree p))

定理组装前还差一步。选择并未交出选取函数，只交出它的仅仅存在。但目标「P 或非 P」自身是命题：两侧互斥，任何两个判定之间无可区分。对这样的目标，仅仅存在可以当作真实存在来消去，证明就此闭合。

「目标是命题」这一点被显式证明：Sum.isProp⊎ 要求两侧各自的命题性，以及两侧不能同时有元的证明。第一侧是 ⟨ P ⟩，由 P .snd 得其命题性。第二侧是函数类型 ⟨ P ⟩ → Empty.⊥，isPropΠ 利用 Empty.isProp⊥ 逐点证明它是命题。最后，λ p np → np p 证明两侧不能同时有元。定理 choice→lem 的类型随之是 SetChoice ℓ → LEM ℓ。给定 sc 与命题 P，它在 P 处进入 Diaconescu 模块，用 merePicker sc 得到仅仅的选取函数，再以 PT.rec 把截断消去到已证为命题的目标中，返回 decide。想法的次序重要：decide 内部的分情形是真实数据，截断之所以能消去，只因目标无法区分其答案。

  decideIsProp : isProp (⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥))
  decideIsProp = Sum.isProp⊎ (P .snd) (isPropΠ (λ _ → Empty.isProp⊥)) (λ p np → np p)

choice→lem : ∀ {ℓ} → SetChoice ℓ → LEM ℓ
choice→lem sc P = PT.rec decideIsProp decide (merePicker sc)
  where open Diaconescu P

小结

在一个固定的层级上，SetChoice 说的是：在 h-集合指标之上，每根纤维的仅仅有元给出一个同时处处选取的函数的仅仅存在。于是高一层的一个实例覆盖其下的层级；而由 Diaconescu 定理，它还能判定其层级的每个命题。在本章所证的方向上，选择是更强的经典接口：SetChoice ℓ → LEM ℓ；其逆在此并未建立。模型章以两种方式使用同一个 SetChoice (ℓ-suc ℓ) 实例：choice→lem 为 ZF 公理给出排中律，lowerSetChoice 则在较低层级给出选择集公理。