First import the set quotient and binary-relation tools used below. Given a type `A` and a relation `R`, the quotient `A / R` has points `[ a ]`; a proof of `R a b` gives a path `[ a ] ≡ [ b ]`, and `squash/` ensures that the result is an h-set. `BinaryRelation` supplies the vocabulary for the relation laws we will verify. The imported isomorphism theorem `isEquivRel→effectiveIso` says that, when `R` is a proposition-valued equivalence relation, paths `[ a ] ≡ [ b ]` in the quotient are isomorphic to proofs of `R a b`. This lets us read equality of quotient points through the original relation. ```agda open import Cubical.HITs.SetQuotients using ( _/_; [_]; squash/; []surjective; isEquivRel→effectiveIso ) open import Cubical.Relation.Binary.Base using ( module BinaryRelation ) ``` **Construction** (`_~_`) On `Bool`, define a relation whose diagonal entries are always inhabited and whose off-diagonal entries are `⟨ P ⟩`. Thus `P` controls whether the two different booleans are related. ```agda _~_ : Bool → Bool → Type ℓ true ~ true = ⊤* false ~ false = ⊤* _ ~ _ = ⟨ P ⟩ ``` **Construction** (`Glued`) Take the quotient by this relation. We want to characterize paths between its distinguished points `[ true ]` and `[ false ]` by proofs of `P`. The isomorphism theorem applies once we verify that `_~_` is a proposition-valued equivalence relation. ```agda Glued : Type ℓ Glued = Bool / _~_ ``` **Lemma** (`~-prop`) For the quotient just constructed, the isomorphism theorem requires a proposition-valued equivalence relation. The checks use only the definition of `_~_`. Each diagonal entry is the proposition `⊤*`; each off-diagonal entry is the proposition packaged in `P`. ```agda ~-prop : BinaryRelation.isPropValued _~_ ~-prop true true = isProp⊤* ~-prop false false = isProp⊤* ~-prop true false = ⟨ P ⟩isProp ~-prop false true = ⟨ P ⟩isProp ``` **Lemma** (`~-refl`) The diagonal entries have the inhabitant `tt*`, which proves reflexivity. ```agda ~-refl : (a : Bool) → a ~ a ~-refl true = tt* ~-refl false = tt* ``` **Lemma** (`~-sym`) Swapping the inputs leaves the entry type unchanged. On the diagonal we return `tt*`; off the diagonal we reuse the given proof of `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 ``` **Lemma** (`~-trans`) For transitivity, first compare the endpoints `a` and `c`. If they agree, `tt*` proves `a ~ c`. ```agda ~-trans : (a b c : Bool) → a ~ b → b ~ c → a ~ c ~-trans true _ true _ _ = tt* ~-trans false _ false _ _ = tt* ``` If the endpoints differ, the middle boolean equals one of them, so one of the two premises is already a proof of `P`. Return that proof. ```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 ``` **Lemma** (`~-equivRel`) The three laws form the equivalence-relation record required by the isomorphism theorem. ```agda ~-equivRel : BinaryRelation.isEquivRel _~_ ~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans ``` **Lemma** (`quotientPath≃P`) The verified laws let us apply the isomorphism theorem. It identifies the path type between `[ true ]` and `[ false ]` with `true ~ false`, which is defined to be `⟨ P ⟩`. Applying `isoToEquiv` to this isomorphism yields the following type equivalence. ```agda quotientPath≃P : ([ true ] ≡ [ false ]) ≃ ⟨ P ⟩ quotientPath≃P = isoToEquiv (isEquivRel→effectiveIso ~-prop ~-equivRel true false) ``` In the figure, write $e$ for `quotientPath≃P`: its forward map sends a path to a proof of `P`, and its inverse sends a proof to a path. The following panels show the consequences of a proof or a refutation of `P`, without presuming that either has already been obtained.

$$([\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}]$

On the left, the inverse of $e$ supplies a path. On the right, $e$ would turn any connecting path into a proof contradicted by `n`

**Construction** (`Pick`) It remains to make equality in `Glued` decidable. A representative of `x : Glued` consists of a boolean `b` and a path `[ b ] ≡ x`. Their dependent pair type `Pick x` is precisely the fibre of the quotient map `[_] : Bool → Glued` over `x`. Its second component certifies that the boolean represents this particular class. ```agda Pick : Glued → Type ℓ Pick x = Σ[ b ∶ Bool ] ([ b ] ≡ x) ``` **Lemma** (`pickIsSet`) The family `Pick` is set-valued. Apply `isSetClass` to the h-set `Bool`: for each boolean, the second component is a path in the h-set `Glued`, hence a proposition. ```agda pickIsSet : (x : Glued) → isSet (Pick x) pickIsSet x = isSetClass isSetBool (λ b → squash/ [ b ] x) where open import Cubical.Data.Bool.Properties using ( isSetBool ) ``` **Lemma** (`pickable`) Every quotient point merely has a representative, as `[]surjective` states. ```agda pickable : (x : Glued) → ∥ Pick x ∥₁ pickable = []surjective ``` **Lemma** (`merePicker`) Apply `sc` with index type `Glued`, its h-set certificate `squash/`, the family `Pick`, and its pointwise h-set certificate `pickIsSet`. This is the only application of choice within the argument for `P`. It yields the mere existence of a function that chooses a representative at every quotient point. ```agda merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁ merePicker sc = sc Glued squash/ Pick pickIsSet pickable ``` For the next two auxiliary maps, temporarily suppose an actual `g : (x : Glued) → Pick x` is given, rather than only its mere existence. The inner parameterized submodule holds `g` fixed; `_` means the module itself needs no name. Its private definitions still require `g` when used outside the submodule, so no global choice function has been assumed. We will later eliminate the truncation to obtain a decision without this temporary supposition.

```agda private module _ (g : (x : Glued) → Pick x) where ```

**Construction** (`b₀` `b₁`) - `b₀` is the boolean selected by `g` at `[ true ]`. - `b₁` is the boolean selected by `g` at `[ false ]`. ```agda b₀ : Bool b₀ = g [ true ] .fst b₁ : Bool b₁ = g [ false ] .fst ``` **Construction** (`agree→P` `P→agree`) - `agree→P` If `q : b₀ ≡ b₁`, the certificates stored in `g` connect this agreement back to the quotient. Write $s_0$ and $s_1$ in the figure for `g [ true ] .snd` and `g [ false ] .snd`. The first certificate points from `[ b₀ ]` to `[ true ]`, so the composite must use `sym` there. - `P→agree` Conversely, a proof `p : ⟨ P ⟩` gives the path `invEq quotientPath≃P p`, written $e^{-1}(p)$ in the figure. The ordinary function `λ x → g x .fst` sends that path to `b₀ ≡ b₁`. Taking the first component makes the codomain the fixed type `Bool`, so `cong` suffices. ```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$

On the left, $e$ sends the composite path to a proof of `P`. On the right, the selected boolean varies along $e^{-1}(p)$, giving agreement

**Construction** (`decide`) Given `g : (x : Glued) → Pick x`, we now decide equality of the selected booleans, using `_≟_`. The two private auxiliary maps just proved convert its outcomes as follows: | Boolean comparison | Decision of `P` | | --- | --- | | `yes q` | `yes (agree→P g q)` | | `no ne` | `no (λ p → ne (P→agree g p))` | : Each Boolean comparison outcome yields the corresponding decision of the proposition In the second row, a proof of `P` would force the very equality that `ne` refutes. This is the negative map supplied to `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 ( _≟_ ) ```

Separate existence at each point

One function on the quotient