まず、以下で使う集合商と二項関係の道具を導入する。型 `A` と関係 `R` に対し、商 `A / R` は点 `[ a ]` をもち、`R a b` の証明からパス `[ a ] ≡ [ b ]` が得られる。`squash/` はその結果が h-集合であることを保証する。`BinaryRelation` は、これから検証する関係の法則を記述するために使う。ここで導入する同型定理 `isEquivRel→effectiveIso` は、`R` が命題値の同値関係ならば、商におけるパス `[ a ] ≡ [ b ]` と `R a b` の証明が同型になることを述べる。これにより、商の点の等しさを元の関係から理解できる。
```agda
open import Cubical.HITs.SetQuotients
using ( _/_; [_]; squash/; []surjective; isEquivRel→effectiveIso )
open import Cubical.Relation.Binary.Base using ( module BinaryRelation )
```
**構成** (`_~_`) `Bool` 上の関係を、対角成分は常に要素をもち、非対角成分は `⟨ P ⟩` となるように定める。異なる二つのブール値が関係をもつかどうかを `P` が決める。
```agda
_~_ : Bool → Bool → Type ℓ
true ~ true = ⊤*
false ~ false = ⊤*
_ ~ _ = ⟨ P ⟩
```
**構成** (`Glued`) この関係による商を取る。二つの点 `[ true ]` と `[ false ]` の間のパスを、`P` の証明によって特徴付けたい。`_~_` が命題値の同値関係であることを確かめれば、同型定理を適用できる。
```agda
Glued : Type ℓ
Glued = Bool / _~_
```
**補題** (`~-prop`) いま構成した商に同型定理を使うには、関係が命題値で同値律を満たす必要がある。検証には `_~_` の定義だけを使う。対角成分は命題 `⊤*` であり、非対角成分は `P` に含まれる命題である。
```agda
~-prop : BinaryRelation.isPropValued _~_
~-prop true true = isProp⊤*
~-prop false false = isProp⊤*
~-prop true false = ⟨ P ⟩isProp
~-prop false true = ⟨ P ⟩isProp
```
**補題** (`~-refl`) 対角成分の要素 `tt*` が反射性を証明する。
```agda
~-refl : (a : Bool) → a ~ a
~-refl true = tt*
~-refl false = tt*
```
**補題** (`~-sym`) 入力を交換しても成分の型は変わらない。対角では `tt*` を返し、非対角では与えられた `P` の証明を再利用する。
```agda
~-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` を証明する。
```agda
~-trans : (a b c : Bool) → a ~ b → b ~ c → a ~ c
~-trans true _ true _ _ = tt*
~-trans false _ false _ _ = tt*
```
両端が異なるなら、中間のブール値はどちらか一方に等しいため、二つの前提の一方がすでに `P` の証明である。それを返せばよい。
```agda
~-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`) 三つの法則を、同型定理が要求する同値関係のレコードにまとめる。
```agda
~-equivRel : BinaryRelation.isEquivRel _~_
~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans
```
**補題** (`quotientPath≃P`) これらの法則を確認すると、同型定理を適用できる。これは `[ true ]` と `[ false ]` の間のパス型と `true ~ false` の同型を与える。後者は定義上 `⟨ P ⟩` である。この同型を `isoToEquiv` で次の型同値に変換する。
```agda
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}]$
**構成** (`Pick`) 次に `Glued` の等しさを判定できるようにする。点 `x : Glued` の代表元は、ブール値 `b` とパス `[ b ] ≡ x` の組である。その依存対型 `Pick x` は、商写像 `[_] : Bool → Glued` の `x` 上のファイバーにほかならない。第二成分は、そのブール値が指定した商類を代表することを保証する。
```agda
Pick : Glued → Type ℓ
Pick x = Σ[ b ∶ Bool ] ([ b ] ≡ x)
```
**補題** (`pickIsSet`) 族 `Pick` は h-集合値である。h-集合 `Bool` に `isSetClass` を適用する。ブール値を固定した第二成分は h-集合 `Glued` のパスなので、命題である。
```agda
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` によって、商の各点には代表元が単に存在する。
```agda
pickable : (x : Glued) → ∥ Pick x ∥₁
pickable = []surjective
```
**補題** (`merePicker`) 添字型を `Glued`、その h-集合性の証明を `squash/`、族を `Pick`、各値の h-集合性の証明を `pickIsSet` として `sc` を適用する。`P` についての議論で選択を使うのはここだけである。各商点で代表元を選ぶ関数の単なる存在が得られる。
```agda
merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁
merePicker sc = sc Glued squash/ Pick pickIsSet pickable
```
次の二つの補助写像を作る間、単なる存在ではなく、実際の関数 `g : (x : Glued) → Pick x` が与えられたと仮定する。内側の引数付き部分モジュールは `g` を固定し、`_` はモジュール自体に名前が不要であることを表す。外で非公開の補助定義を使うときには、なお `g` を渡すので、大域的な選択関数を仮定したわけではない。後で切り詰めを除去し、この一時的な仮定なしに判定を得る。
```agda
private module _ (g : (x : Glued) → Pick x) where
```
**構成** (`b₀` `b₁`)
- `b₀` は `[ true ]` で `g` が選ぶブール値である。
- `b₁` は `[ false ]` で `g` が選ぶブール値である。
```agda
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` で十分である。
```agda
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` に渡す否定側の写像である。
```agda
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 ( _≟_ )
```