Choice

经典边界还有第二个接口。经典数学除排中律外还依靠选择运转，本章陈述本书采用的形式，逐层级、与 LEM 同款的接口风格。集合层选择说：在 h-集索引之上，截断与乘积交换：若每根纤维都仅仅有元，则仅仅地，全体纤维一齐有元。这是「非空集族有选择函数」的类型论读法，而索引上的 h-集限制正是它诚实的关键，因为对任意类型这条原理干脆为假。与排中律一样，选择从不全局假设：需要它的章节以参数领取，而第一个领取者是第三部之巅。

两个接口并非平级，本章当场证明这一点：选择证明排中律。这个观察出自 Diaconescu，类型论形式归于 Goodman 与 Myhill；它意味着在每个层级上，选择接口都悄悄把整条经典边界背在身上。

{-# 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 )
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
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 )
open import Cubical.Relation.Binary.Base using ( module BinaryRelation )

原理

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

与排中律一样，选择沿层级向下通行：把索引集与纤维抬高一层宇宙，在那里选择，再把选择函数降回来。于是较高层级上的单个实例覆盖其下诸层。

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)))
             (λ x → PT.map lift (inh (lower x))))

Diaconescu 定理

定理说：给定集合层选择，任何命题 P 都可判定，即或证明或反驳。乍看这很荒谬，因为判定程序无从下手：任意的 P 没有可分情形的把手。证明的想法是让几何来下手。造一个形状依赖于 P 的小空间：P 成立时它只有一个点，不成立时有两个点。然后向选择原理问一个关于这个空间的问题；答案不可能不泄露形状，而形状就是 P。

具体地，固定 P；以下一切都住在以定理作者命名的模块里。取两个布尔值，恰当 P 成立时把它们粘起来。「粘合」指集合商：点仍是 true 与 false，但凡粘合关系点头，两点之间就添一条路径，最后把结果截断为 h-集。粘合关系最好用一张四格表给出：对角线上平凡成立，混色的两格就是 P 本身，于是「这两点相关」与「P 成立」按定义是同一个命题。最后这一款是全部戏法所在，下文将两次兑付。

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

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

  Glued : Type ℓ
  Glued = Bool / _~_

关系是表，它的证书也就是表：逐格皆命题，对角线自反，表格对称故关系对称，传递性则读出幸存的那个混色格。证书不是记账：它们是库的有效性定理的入场券。该定理说，按命题值等价关系取商，粘合是诚实的：两点最终连通，只可能因为关系确实关联过它们，绝无误伤。换句话说，商里的路径可以倒着读，读回引起它的那份关系。

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

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

  ~-sym : (a b : Bool) → a ~ b → b ~ a
  ~-sym true  true  _ = tt*
  ~-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*
  ~-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

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

构造的心脏是一部两行的词典：商的两个点重合，当且仅当 P 成立。一个方向：若 P 成立，表格便判 true 与 false 相关，商随之把两个等价类等同起来，空间坍缩为一个点。另一个方向：若两个类重合，粘合的诚实性说明关系必定关联过 true 与 false，而按表格那份关系就是 P，故 P 成立。这正是混色格第一次付账之处，还一次付了两笔：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

现在选择原理进场，我们只问它一个问题：给粘合空间的每个点发一个布尔代表元。某点处的一次选取，是一个布尔值，连同「其等价类就是该点」的保证。每个点单独看必有选取，但只是仅仅有：商记得自己的点各有来处，却不记得来处是谁。把「每点仅仅有代表元」变成一个一举在处处选取的函数，正是集合层选择的本领，而它适用是因为粘合空间按构造是 h-集。留意这个函数做不到的事：它的构造完全接触不到 P，故无论 P 成立与否它都同样作答；它只是盲目地选取。

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

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

这个问题值得单独立为引理，好让类型原样展示选择交付的东西：仅仅地，一整个选取函数。

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

于是假设选取函数 g 已经在手。把它作用在两个特殊的点上，即 true 的类与 false 的类，给选出的两个布尔代表元起名 b₀ 与 b₁。这两个布尔值就是泄密者。每个方向一条引理把它们与 P 绑在一起。若代表元一致，就沿保证走一遍：true 的类接到 b₀ 的类，即 b₁ 的类，再接到 false 的类；于是两点重合，词典的反向条目把这次重合翻译成 P 的证明。若 P 成立，则两点本是同一个点，而函数作用在同一个点上只能给出同一个答案，b₀ 与 b₁ 被迫是同一个布尔值。(形式化地：把 g 沿粘合路径投影，投影的两端都是普通布尔值，连搬运都不需要。)

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

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

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

    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 不同，它们可以被检视：两个布尔值要么相等要么不等，机械可判。若 b₀ 与 b₁ 一致，第一条引理证出 P。若二者相异，P 必不成立，因为它若成立，第二条引理将迫使二者一致。无论哪边 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)
      fromDec (no ne) = Sum.inr (λ p → ne (P→agree p))

最后一道缺口，定理即合拢。选择从不真正交出选取函数，只交出它的仅仅存在。但目标「P 或非 P」自身是命题：两侧互斥，任何两个判定之间无可区分。对这样的目标，仅仅存在可以当作真实存在来消去，证明就此闭合。

  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 是本书的选择接口，逐层级陈述，与 LEM 同款形状；而经 choice→lem，它是两者中更强的那个：经由粘合布尔值、glue/unglue 词典与一次代表元比较，选择判定其层级的每个命题。排中律不回此礼，所以两个接口依然分立。模型章将把选择花在选择集上，并在收尾处兑现本章定理：高一层宇宙上的一份选择，就能付清全部经典账单。