先引入下文要用的集合商与二元关系工具。给定类型 `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`) 按这个关系取商。我们希望用 `P` 的证明来刻画两个特殊点 `[ true ]` 与 `[ false ]` 之间的路径。只要验证 `_~_` 是取值于命题的等价关系，就能应用同构定理。
```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-集合。这里将 `isSetClass` 用于 h-集合 `Bool`：固定布尔值后的第二分量是 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` 为指标类型，`squash/` 为其 h-集合性证书，`Pick` 为所选的族，`pickIsSet` 为逐点的 h-集合性证书，应用 `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₀` 是 `g` 在 `[ true ]` 处选出的布尔值。
- `b₁` 是 `g` 在 `[ false ]` 处选出的布尔值。
```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 ( _≟_ )
```