この章を読むか、対話型目次と依存グラフで別のルートを選べます。

型の族の各型に要素があることと、すべての型から要素を選ぶ一つの関数をもつことは異なる。命題的切り詰めはこの違いを正確に表す。∥ B x ∥₁ は個々の添字における存在を述べ、∥ ((x : X) → B x) ∥₁ は選択関数全体の存在を述べる。本章では、h-集合で添字付けられた h-集合値の族について選択原理を定式化し、一つ上の宇宙レベルでの選択原理が現在のレベルでの選択原理を含意することを示し、選択原理が排中律を含意することを証明する。

原理

族 B : X → Type ℓ に対し、三種類のデータを区別する。各 B x の要素がすでに x の関数として与えられているなら、その関数自体が選択関数である。追加の原理が扱うのは、切り詰められた、より弱い入力である。

主張	得られるもの
`(x : X) → B x`	値を計算できる選択関数
`(x : X) → ∥ B x ∥₁`	添字ごとの存在
`∥ ((x : X) → B x) ∥₁`	すべての添字を扱う一つの関数の存在

選択に関わる三種類のデータ。関数そのもの、各点での単なる存在、関数全体の単なる存在

定義 (SetChoice) レベル ℓ の集合値族に対する選択は、任意の h-集合 X : Type ℓ と、各値 B x が h-集合である族 B : X → Type ℓに対し、上の表の第二行から第三行が従うと主張する。

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

切り詰めは依存関数型の外へ移るが、消えるわけではない。したがって仮定 sc : SetChoice ℓ が与えるのは、選択関数の単なる存在である。この存在を rec₁ で使うには、目標が命題でなければならない。Type ℓ 全体を量化するので、原理自体は Type (ℓ-suc ℓ) に住む。

補題 (lowerSetChoice) 一つ上の宇宙レベルの選択は、一つ下のレベルの選択を含意する。

lowerSetChoice : ∀ {ℓ} → SetChoice (ℓ-suc ℓ) → SetChoice ℓ

証明 sc : SetChoice (ℓ-suc ℓ) が与えられたとする。SetChoice ℓ を示すには、任意に与えられた h-集合の添字型 X と h-集合値の族 B について、前提 inh : (x : X) → ∥ B x ∥₁ から ∥ ((x : X) → B x) ∥₁ を導けばよい。inh は inhabited の略であり、各点での単なる存在を与えるだけで、具体的な元は選ばない。sc は一つ上の宇宙レベルの族を扱うので、Lift でこの選択問題をそのレベルへ移す。下図は、元のレベルから上がり、選択原理を適用し、元のレベルへ戻る流れを示す。

$$\widehat B\,\hat x := \operatorname{Lift}(B(\operatorname{lower}\,\hat x))$$

$$(x:X)\to\|B\,x\|_1$$

$\operatorname{map}_1\,\operatorname{lift}$

$$(\hat x:\operatorname{Lift}X)\to\|\widehat B\,\hat x\|_1$$

$\operatorname{sc}$

$$\|(\hat x:\operatorname{Lift}X)\to\widehat B\,\hat x\|_1$$

$\operatorname{map}_1$

$$\|(x:X)\to B\,x\|_1$$

高いレベルの選択から元のレベルの選択を得る流れ。入力を持ち上げ、選択原理を適用し、結果を元のレベルへ戻す

一つ上のレベルで sc を適用するには、持ち上げた添字型と族の各値が h-集合であることも示す必要がある。次の表は、その証明を元のレベルで与えられた性質からどう得るかを中心に、他の引数との対応も示す。

レベル `ℓ`	レベル `ℓ-suc ℓ`
`X`	`Lift X`
`setX`	`isOfHLevelLift 2 setX`
`B x`	`Lift (B (lower x̂))`、ただし `x̂ : Lift X`
`setB x`	`isOfHLevelLift 2 (setB (lower x̂))`
`inh x`	`map₁ lift (inh (lower x̂))`

高いレベルの引数は、元のレベルですでに与えられたデータから構成される

下の Agda コードは図と表を一つにつなぐ。表の右列が中央の選択に必要な入力を与え、コードの入れ子構造が図の上昇、選択原理の適用、元のレベルへの帰還に対応する。式全体の型は図の下端に示した目標そのものである。

lowerSetChoice sc X setX B setB inh = map₁ (λ f x → lower (f (lift x)))
         (sc (Lift X) (isOfHLevelLift 2 setX)
             (λ x̂ → Lift (B (lower x̂)))
             (λ x̂ → isOfHLevelLift 2 (setB (lower x̂)))
             (λ x̂ → map₁ lift (inh (lower x̂))))

ディアコネスクの定理

代表元を選ぶことから、任意の命題をどう判定できるのだろうか。前章では判定を得てから命題をブール値で符号化した。ここでは順序が逆になる。命題を判定せずに商を構成し、選択によってブール値を得て、その比較から判定を導く。

非公開の部分モジュール Diaconescu で任意の P : hProp ℓ を固定し、対応する商と補助結果を構成する。最後の定理はそれらを用いて、選択から P の判定を得る。

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

まず、以下で使う集合商と二項関係の道具を導入する。型 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) この関係による商を取る。二つの点 [ true ] と [ false ] の間のパスを、P の証明によって特徴付けたい。_~_ が命題値の同値関係であることを確かめれば、同型定理を適用できる。

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 の証明または反証があるときの帰結を示すもので、どちらかがすでに得られているとは仮定しない。

$$([\mathsf{true}] \equiv [\mathsf{false}]) \simeq \langle P\rangle$$

$$p : \langle P\rangle$$

$\mathsf{Glued}$ $[\mathsf{true}]$ $[\mathsf{false}]$ $e^{-1}(p)$

$$n : \neg\langle P\rangle$$

$\mathsf{Glued}$ $[\mathsf{true}]$ $[\mathsf{false}]$

左図では $e$ の逆写像からパスを得る。右図にパスがあれば、$e$ がそれを n と矛盾する証明へ送る

構成 (Pick) 次に Glued の等しさを判定できるようにする。点 x : Glued の代表元は、ブール値 b とパス [ b ] ≡ x の組である。その依存対型 Pick x は、商写像 [_] : Bool → Glued の x 上のファイバーにほかならない。第二成分は、そのブール値が指定した商類を代表することを保証する。

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

補題 (pickIsSet) 族 Pick は h-集合値である。h-集合 Bool に isSetClass を適用する。ブール値を固定した第二成分は 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、その h-集合性の証明を squash/、族を Pick、各値の h-集合性の証明を pickIsSet として 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₀ b₁)

b₀ は [ true ] で g が選ぶブール値である。
b₁ は [ false ] で g が選ぶブール値である。

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

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

構成 (agree→P P→agree)

agree→P q : b₀ ≡ b₁ があれば、g に含まれる証明によって、この一致を商のパスへ結び付けられる。図中の $s_0$、$s_1$ は、それぞれ g [ true ] .snd と g [ false ] .snd の略記である。最初の証明は [ b₀ ] から [ true ] へ向かうため、合成には sym で逆にしたものを使う。
P→agree 逆に p : ⟨ P ⟩ からは、逆写像によってパス invEq quotientPath≃P p が得られる。図中の $e^{-1}(p)$ はこのパスを表す。通常の関数 λ x → g x .fst はこのパスを b₀ ≡ b₁ へ送る。第一成分を取れば終域は固定された型 Bool なので、cong で十分である。

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)

$$q:b_0\equiv b_1$$

$\mathsf{Glued}$ $[\mathsf{true}]$ $[b_0]$ $[b_1]$ $[\mathsf{false}]$ $\mathsf{sym}(s_0)$ $\mathsf{cong}\,[{-}]\,q$ $s_1$

$$p:\langle P\rangle$$

$\mathsf{Glued}$ $e^{-1}(p)$ $[\mathsf{true}]$ $[\mathsf{false}]$ $x\mapsto g(x).\mathsf{fst}$ $\mathsf{Bool}$ $b_0$ $b_1$

左図では $e$ が合成したパスを P の証明へ送る。右図では $e^{-1}(p)$ に沿って選んだブール値を読み、両者の等しさを得る

構成 (decide) g : (x : Glued) → Pick x が与えられたとき、_≟_ を使って選ばれた二つのブール値の等しさを判定する。証明した二つの非公開の補助写像によって、結果を次のように変換できる。

ブール値の比較	`P` の判定
`yes q`	`yes (agree→P g q)`
`no ne`	`no (λ p → ne (P→agree g p))`

ブール値の比較の二つの結果から、命題についての肯定または否定の判定が得られる

第二行では、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 ( _≟_ )

「基礎語彙」で見た、切り詰めを経由する分解の具体例がここに現れる。図中の $G$ は型 (x : Glued) → Pick x の略記である。decide は実際の関数を受け取る。isPropDec ⟨ P ⟩isProp が目標 Dec ⟨ P ⟩ の命題性を示すので、rec₁ (isPropDec ⟨ P ⟩isProp) decide は関数の単なる存在も受け取れる。

$G$ $\|G\|_1$ $\mathsf{Dec}\,\langle P\rangle$ $|{-}|_1$ $\mathsf{decide}$ $\mathsf{rec}_1\,\cdots$

選択が $\|G\|_1$ の要素を与え、右側の関数がそこから P の判定を返す

定理 (Diaconescu) (SetChoice→LEM) 集合値族に対する選択は、同じ宇宙レベルの排中律を含意する。

証明 rec₁ (isPropDec ⟨ P ⟩isProp) decide を merePicker sc に適用する。P は任意だったので、結果は LEM ℓ である。

SetChoice→LEM : ∀ {ℓ} → SetChoice ℓ → LEM ℓ
SetChoice→LEM sc P = rec₁ (isPropDec ⟨ P ⟩isProp) decide (merePicker sc)
  where open Diaconescu P

証明を終えたところで、一見簡単そうな方法を振り返ろう。[ true ] では true を、[ false ] では false を選ぶだけではなぜ足りないのか。次の図は、各点で別々に代表元を得るところから SetChoice を経て、商の上の一つの関数へ進む。P が成り立つと仮定し、同じ点の二つの表記を結ぶパスをたどってみよう。

$P$ が成り立つと、商にはパスがある $p:[\mathsf{true}]\equiv[\mathsf{false}]$

各点で別々に存在

$(x : \mathsf{Glued})\to\|\mathsf{Pick}\,x\|_1$

仮に代表元を別々に見つけても：

$[\mathsf{true}]$$\mathsf{true}$

$[\mathsf{false}]$$\mathsf{false}$

$P$ が成り立つと、二つの表記は同じ商点を指す。異なる代表元を別々に見つけても矛盾しないが、表記ごとに出力を指定すると同じ入力に true と false の両方を与えてしまい、商の上の関数にならない。

$\mathsf{SetChoice}$ 一つの関数が単に存在

商の上の一つの関数

$\|((x : \mathsf{Glued})\to\mathsf{Pick}\,x)\|_1$

残る外側の切り詰めの内側で、一つの関数 $g$ を見る：

$f:\mathsf{Glued}\to\mathsf{Bool}$$f(x)=(g\,x).\mathsf{fst}$

$[\mathsf{true}]$ $[\mathsf{false}]$ $p$ $f$ $f$ $b_0$ $b_1$ $\operatorname{cong}\,f\,p$

$b_0\equiv b_1\quad\Longleftrightarrow\quad P$

代表元の証明が逆向きの含意を与える。よって $b_0$ と $b_1$ の比較で $P$ を判定できる。

一つの関数が商点間のパスをブール出力間のパスへ送る。判定は命題なので、外側の切り詰めを除ける

まとめ

本章では、h-集合を添字とする h-集合値の族について SetChoice ℓ を定式化した。各添字で要素が単に存在することから、一つの選択関数が単に存在することが従う。lowerSetChoice は、SetChoice (ℓ-suc ℓ) が SetChoice ℓ を含意することを示す。SetChoice→LEM の証明では、命題 P を二つの商点の等しさに符号化し、選択で得たブール代表元を比較して P を判定する。Dec ⟨ P ⟩ は命題なので、rec₁ により切り詰めを消去できる。したがって SetChoice ℓ から LEM ℓ が従う。