Read this chapter directly, or use the interactive contents and dependency graph to choose another route.

Knowing that each type in a family has an element is different from having one function that chooses an element of every type. Propositional truncation makes the distinction precise: ∥ B x ∥₁ asserts existence at an individual index, while ∥ ((x : X) → B x) ∥₁ asserts the existence of a whole choice function. We formulate this principle for h-set-indexed families of h-sets, show that choice at one universe level higher implies choice at the current level, and prove that choice implies excluded middle.

The principle

For a family B : X → Type ℓ, there are three kinds of data worth distinguishing. If an element of every B x is already given as a function of x, that function is the choice function itself. The additional principle concerns the weaker, truncated input.

Statement	What it supplies
`(x : X) → B x`	A choice function, which can be evaluated.
`(x : X) → ∥ B x ∥₁`	Existence separately at each index.
`∥ ((x : X) → B x) ∥₁`	Existence of one function on all indices.

Three forms of choice data, from a function to individual and whole-function mere existence

Definition (SetChoice) Choice for set-valued families at level ℓ asserts that the second row of the table above implies the third for every h-set X : Type ℓ and every family B : X → Type ℓ whose values B x are h-sets.

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

The truncation moves outside the dependent function type; it does not disappear. A hypothesis sc : SetChoice ℓ therefore gives the mere existence of a choice function. To use that existence with rec₁, we must have a proposition as our goal. Quantification over Type ℓ puts the whole principle in Type (ℓ-suc ℓ).

Lemma (lowerSetChoice) Choice one universe level higher implies choice at the level below.

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

Proof Let sc : SetChoice (ℓ-suc ℓ) be given. To prove SetChoice ℓ, we must show that, for any h-set of indices X and h-set-valued family B, the premise inh : (x : X) → ∥ B x ∥₁ yields ∥ ((x : X) → B x) ∥₁. The name inh abbreviates inhabited: it supplies mere existence at each index, without selecting an element. Because sc works one universe higher, we use Lift to present this choice problem at the level it accepts. The figure shows the route up, across, and back down.

$$\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$$

How higher-level choice yields choice at the original level: lift the input, apply the choice principle, then return the result to the original level

To apply sc one level higher, we must also supply h-set proofs for the lifted index type and every value of the lifted family. The table shows how those proofs, along with the other arguments, come from the data already given at the original level.

At level `ℓ`	At level `ℓ-suc ℓ`
`X`	`Lift X`
`setX`	`isOfHLevelLift 2 setX`
`B x`	`Lift (B (lower x̂))`, for `x̂ : Lift X`
`setB x`	`isOfHLevelLift 2 (setB (lower x̂))`
`inh x`	`map₁ lift (inh (lower x̂))`

The higher-level arguments are built from data already given at the original level

The Agda block brings the figure and table together. The table's right column supplies the central choice step, while the block's nested structure follows the figure's ascent, application of choice, and return to the original level. The complete expression has the type shown as the goal at the bottom of the figure.

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's theorem

How can choosing representatives decide an arbitrary proposition? The preceding chapter encoded a proposition by a boolean after obtaining a decision. Here the order is reversed: we construct a quotient from the proposition without deciding it, and choice will supply the booleans whose comparison gives the decision.

The private submodule Diaconescu fixes an arbitrary P : hProp ℓ and develops the quotient and auxiliary constructions for it. The final theorem uses them to turn choice into a decision of P.

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

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.

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.

_~_ : 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.

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.

~-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.

~-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.

~-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.

~-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.

~-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.

~-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.

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.

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.

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.

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.

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.

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 ].

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.

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.

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 ( _≟_ )

The factorization through truncation shown in the Prelude has a concrete instance here. In the figure, $G$ abbreviates the type (x : Glued) → Pick x. The map decide is defined on actual functions. Since isPropDec ⟨ P ⟩isProp shows that the target Dec ⟨ P ⟩ is a proposition, rec₁ (isPropDec ⟨ P ⟩isProp) decide also accepts their mere existence.

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

Choice supplies an element of $\|G\|_1$; the right-hand function returns a decision of P

Theorem (Diaconescu) (SetChoice→LEM) Choice for set-valued families implies excluded middle at the same universe level.

Proof Apply rec₁ (isPropDec ⟨ P ⟩isProp) decide to merePicker sc. Since P was arbitrary, the result is LEM ℓ.

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

Now that the proof is complete, consider a tempting shortcut: why not prescribe true at [ true ] and false at [ false ]? The diagram follows this question from separate pointwise witnesses through SetChoice to one function on the quotient. Suppose P holds and follow the path between the two names of the same point.

If $P$ holds, the quotient has a path $p:[\mathsf{true}]\equiv[\mathsf{false}]$

Separate existence at each point

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

Even if representatives were found separately:

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

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

When $P$ holds, the two names denote one point. Different representatives can be found separately, but prescribing them as outputs would give one input both true and false: not a function on the quotient.

$\mathsf{SetChoice}$ A single function exists, merely

One function on the quotient

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

Inside this remaining truncation, take one function $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$

The representative certificates give the reverse direction. Comparing $b_0$ and $b_1$ therefore decides $P$.

One function sends the path between quotient points to a path between its Boolean outputs; the resulting decision is a proposition, so it can leave the outer truncation

Recap

This chapter formulated SetChoice ℓ for h-set indices and h-set-valued families: pointwise mere existence of elements implies the mere existence of one choice function. lowerSetChoice shows that SetChoice (ℓ-suc ℓ) implies SetChoice ℓ. To prove SetChoice→LEM, we encoded a proposition P in the equality of two quotient points. Choice provided Boolean representatives whose comparison decides P; because Dec ⟨ P ⟩ is a proposition, rec₁ eliminates the truncation. Thus SetChoice ℓ implies LEM ℓ.