选择原理

先引入下文要用的集合商与二元关系工具。给定类型 A 与关系 R，商 A / R 中有点 [ a ]；R a b 的证明给出路径 [ a ] ≡ [ b ]，squash/ 则保证结果是 h-集合。BinaryRelation 提供随后验证关系定律所用的表述。这里引入的同构定理 isEquivRel→effectiveIso 说：若 R 是取值于命题的等价关系，则商中 [ a ] ≡ [ b ] 的路径与 R a b 的证明同构。由此可以通过原关系理解商中两点的相等。

open import Cubical.HITs.SetQuotients
  using ( _/_; [_]; squash/; []surjective; isEquivRel→effectiveIso )
open import Cubical.Relation.Binary.Base using ( module BinaryRelation )

构造 (_~_) 在 Bool 上定义关系，对角格始终有元素，非对角格则是 ⟨ P ⟩。这样，两个不同的布尔值是否相关就由 P 控制。

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

构造 (Glued) 按这个关系取商。我们希望用 P 的证明来刻画两个特殊点 [ true ] 与 [ false ] 之间的路径。只要验证 _~_ 是取值于命题的等价关系，就能应用同构定理。

Glued : Type ℓ
Glued = Bool / _~_

引理 (~-prop) 对于刚构造的商，同构定理要求关系取值于命题并满足等价律。验证只需查看 _~_ 的定义：对角格是命题 ⊤*，非对角格是 P 所打包的命题。

~-prop : BinaryRelation.isPropValued _~_
~-prop true  true  = isProp⊤*
~-prop false false = isProp⊤*
~-prop true  false = ⟨ P ⟩isProp
~-prop false true  = ⟨ P ⟩isProp

引理 (~-refl) 对角格有元素 tt*，这就证明了自反性。

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

引理 (~-sym) 交换输入不改变格中的类型。对角格返回 tt*，非对角格复用所给的 P 的证明。

~-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 与 c。两端相同时，tt* 证明 a ~ c。

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

两端不同时，中间的布尔值必等于其中一端，因而两个前提中已有一个是 P 的证明，返回它即可。

~-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) 三条定律组成同构定理所需的等价关系记录。

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

引理 (quotientPath≃P) 验证这些定律后，就能应用同构定理。它给出 [ true ] 与 [ false ] 之间的路径类型与 true ~ false 的同构，而后者按定义就是 ⟨ P ⟩。再用 isoToEquiv 将这个同构转为下面的类型等价。

quotientPath≃P : ([ true ] ≡ [ false ]) ≃ ⟨ P ⟩
quotientPath≃P = isoToEquiv
  (isEquivRel→effectiveIso ~-prop ~-equivRel true false)

图中的 $e$ 简记 quotientPath≃P：正向映射把路径变为 P 的证明，逆向映射把证明变为路径。下面分别展示有 P 的证明或反驳时的情形，并不预先断定我们已经取得了其中一种。

构造 (Pick) 接下来要使 Glued 中的相等变得可判定。点 x : Glued 的代表元由布尔值 b 与路径 [ b ] ≡ x 组成。它们的依值对类型 Pick x 恰是商映射 [_] : Bool → Glued 在 x 上的一束纤维。第二分量证明这个布尔值代表的是指定的商类。

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

引理 (pickIsSet) 族 Pick 取值于 h-集合。这里将 isSetClass 用于 h-集合 Bool：固定布尔值后的第二分量是 h-集合 Glued 中的路径，因而是命题。

pickIsSet : (x : Glued) → isSet (Pick x)
pickIsSet x = isSetClass isSetBool (λ b → squash/ [ b ] x)
  where
    open import Cubical.Data.Bool.Properties using ( isSetBool )

引理 (pickable) []surjective 保证每个商点都有代表元，其存在性以命题截断表达。

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

引理 (merePicker) 以 Glued 为指标类型，squash/ 为其 h-集合性证书，Pick 为所选的族，pickIsSet 为逐点的 h-集合性证书，应用 sc。这是针对 P 的论证中唯一一次使用选择；得到的是为每个商点选取代表元的函数的仅仅存在。

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

接下来暂设已取得实际函数 g : (x : Glued) → Pick x，而不只是知道它仅仅存在。里面的带参数子模块将 g 固定为共同参数；_ 表示模块本身无须命名。离开子模块后，使用这些私有辅助定义仍须传入 g，所以这里并未凭空假设全局选择函数。稍后再消去截断，去掉这个暂设而得到判定。

private 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 = equivFun quotientPath≃P
  (sym (g [ true ] .snd) ∙ cong [_] q ∙ g [ false ] .snd)

P→agree : ⟨ P ⟩ → b₀ ≡ b₁
P→agree p = cong (λ x → g x .fst) (invEq quotientPath≃P p)

构造 (decide) 给定 g : (x : Glued) → Pick x，现在用 _≟_ 判定选出的两个布尔值是否相等。刚证明的两个私有辅助映射把比较结果转换如下：

第二行中，P 的证明会迫使两个布尔值相等，而这正是 ne 所反驳的。因此得到传给 mapDec 的否定方向。

decide : ((x : Glued) → Pick x) → Dec ⟨ P ⟩
decide g = mapDec (agree→P g) (λ ne p → ne (P→agree g p)) (b₀ g ≟ b₁ g)
  where
    open import Cubical.Data.Bool using ( _≟_ )