---
title: "选择原理"
module: Base.Choice
lang: zh
site: "Bedrock"
description: "选择原理"
stage: "基础"
reading_order: 5
canonical: https://bedrock.institute/zh/Base.Choice.html
html: Base.Choice.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Choice.lagda.md
prerequisites: [Base.Prelude, Base.Classical]
routes: [common-foundations]
translations: [https://bedrock.institute/en/Base.Choice.md, https://bedrock.institute/ja/Base.Choice.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 选择原理

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

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

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

```agda
{-# 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` 连同反驳。

```agda
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 构造就将在一个集合商内部进行。

```agda
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 表述这两项条件，粘合关系将分别证明它们。

```agda
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` 相同。

```agda
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))`：抬升指标上的纤维就是底下原指标上纤维的抬升，所以移动后的族与原族包含完全相同的信息。

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

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

```agda
             (λ 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`。

```agda
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` 不成立时，下面的倒读会把两类分开。

```agda
  Glued : Type ℓ
  Glued = Bool / _~_
```

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

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

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

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

```agda
  ~-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` 的证明，两个方向说的是同一件事。

```agda
  ~-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` 的证明就充当结论。六个分支覆盖所有情形，每个都复用某个输入。

```agda
  ~-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` 便恰好满足有效性的全部假设，其路径的倒读对下面的引理可用。

```agda
  ~-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` 与两类相等之间的词典。

```agda
  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` 读出的形式。注意第二分量的用处：它记录选的是哪个代表元；后面论证要重建类与类之间的路径，靠的正是这份证书，而非单独的布尔值。

```agda
  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` 本身是函数；被截断的只是它的输出。于是选择给出的不是函数，只是「有一个」的陈述，这一限制将塑造定理的最后一步。

```agda
  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₁` 一致。

```agda
  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` 的直接投影，无需对族作任何搬运。

```agda
    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 ⟩` 的证明。

```agda
    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`，分情形只在布尔数据上进行。

```agda
      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` 内部的分情形是真实数据，截断之所以能消去，只因目标无法区分其答案。

```agda
  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` 则在较低层级给出选择集公理。