--- title: "Choice" module: Base.Choice lang: en site: "Bedrock" description: "Choice" stage: "Foundations" reading_order: 5 canonical: https://bedrock.institute/en/Base.Choice.html html: Base.Choice.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Choice.lagda.md prerequisites: [Base.Prelude, Base.Classical] routes: [common-foundations] translations: [https://bedrock.institute/zh/Base.Choice.md, https://bedrock.institute/ja/Base.Choice.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Choice Classical mathematics does not rest on excluded middle alone. Given a family of nonempty sets, one may pick one element from each set simultaneously; for a finite or explicitly described family this is routine, but for a family indexed by an arbitrary set it is a genuine principle, the axiom of choice. Type theory sharpens what "nonempty" can mean here. In the base theory, the elements of a fiber `B x` hide behind its propositional truncation `∥ B x ∥₁`, which records that the fiber has an element and forgets which one. A truncation eliminates only into propositions, so no actual element can be extracted from a hypothesis of this shape. The Prelude noted that extracting a genuine function from a truncated existential requires a choice principle. The hypothesis of the principle is therefore that every fiber is *merely* inhabited. The conclusion keeps the truncation as well: it claims the mere existence of one function choosing in every fiber at once, never the function itself. The statement includes one restriction from the start: the index type must be an h-set, and the proof of Diaconescu's theorem will need exactly this. Set-level choice and `LEM` are both stated one level at a time, so their families have the same outer type `∀ ℓ → Type (ℓ-suc ℓ)`. Their internal quantifiers are different: excluded middle ranges over propositions, while choice ranges over an h-set `X`, a family `B` over it, and proofs that its fibers are merely inhabited. Neither principle is assumed globally; a chapter that needs one takes the instance at the required level as an explicit parameter. Three questions organize the chapter. What does choice assert here, and at which levels? Does one assumption at a higher universe cover the levels below? And how strong is the principle? Diaconescu's theorem answers the last one: `SetChoice ℓ` implies `LEM ℓ`, proved as `choice→lem`, so at each level the choice interface already yields excluded middle, and the two interfaces are not peers. The model chapter draws on this twice: `choice→lem` obtains from a single `SetChoice (ℓ-suc ℓ)` the excluded middle that drives its ZF axioms, and `lowerSetChoice` lowers the same instance for the choice-set axiom. ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Choice where open import Base.Prelude open import Base.Classical using ( LEM ) open import Cubical.Foundations.Prelude using ( Path ) ``` The proof of Diaconescu's theorem is a finite argument, and it uses three concrete pieces. The booleans `Bool` with `true` and `false` form a two-point type whose equality `_≟_` decides. The unit type `Unit*` holds the single element `tt*`, and `isPropUnit*` records it as a proposition, so the argument has a trivially true statement available wherever one is needed. A comparison of two booleans returns an element of `Dec`: either `yes` with the equality, or `no` with its refutation. ```agda open import Cubical.Foundations.HLevels using ( isOfHLevelLift ) open import Cubical.Data.Bool using ( Bool; true; false; _≟_ ) open import Cubical.Data.Unit using ( Unit*; tt*; isPropUnit* ) open import Cubical.Relation.Nullary using ( Dec; yes; no ) import Cubical.Data.Sum as Sum ``` Beyond these, the proof needs two constructions. The first is propositional truncation `∥_∥₁`, introduced in the Prelude: it keeps exactly the inhabitedness of a type and forgets which element was there, so from `∥ A ∥₁` one never extracts an inhabitant of `A` itself. The second is the set quotient, which appears in this book for the first time here; from a type and a relation it builds the type of classes, and the Diaconescu construction is carried out inside one. ```agda import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁ ) open import Cubical.HITs.SetQuotients using ( _/_; [_]; eq/; squash/; []surjective; effective ) ``` A set quotient can be formed from any relation. The stronger effectivity theorem used here, which reads equality of quotient classes back as the original relation, requires that relation to be proposition-valued and to satisfy the equivalence laws. The library expresses these two requirements as records, and the gluing relation will be proved to meet both. ```agda open import Cubical.Relation.Binary.Base using ( module BinaryRelation ) ``` ## The principle The principle compares, at one fixed level `ℓ`, a hypothesis about each fiber with a conclusion about all fibers at once. The data are an index type `X` in `Type ℓ`, the proof that `X` is an h-set, a family `B` of fibers over `X`, and the hypothesis `∥ B x ∥₁` for every `x`. The conclusion `∥ ((x : X) → B x) ∥₁` says that merely, one function chooses an inhabitant in every fiber simultaneously. The truncation appears on both sides, and this is the principle's exact strength. The hypothesis gives nothing beyond mere inhabitation, so the conclusion claims no more than the same; an actual choice function is exactly what is missing, and supplying it is the whole content of the assumption. Since the statement quantifies over all of `Type ℓ`, it lives one level up, at `Type (ℓ-suc ℓ)`, for the same reason as `LEM`. ```agda SetChoice : ∀ ℓ → Type (ℓ-suc ℓ) SetChoice ℓ = (X : Type ℓ) → isSet X → (B : X → Type ℓ) → ((x : X) → ∥ B x ∥₁) → ∥ ((x : X) → B x) ∥₁ ``` Like excluded middle, choice in an application is often handed only one higher-level instance, and a descent lemma brings it to the level at hand. `lowerSetChoice` has type `SetChoice (ℓ-suc ℓ) → SetChoice ℓ`: assume choice one universe up, recover it at level `ℓ`. As in `lowerLEM`, the tool is `Lift`, the Prelude's operation for presenting a type of `Type ℓ` inside `Type (ℓ-suc ℓ)` and taking it back. Given data at level `ℓ`, the proof first moves it one level up, where the hypothesis `sc` applies. The index type `X` becomes `Lift X`, and its h-set condition follows from `setX` by `isOfHLevelLift`, which records that lifting does not disturb homotopy level. The family becomes `λ x → Lift (B (lower x))`: a fiber over a lifted index is the lifted fiber over the index beneath it, so the moved family contains exactly the information of the original. ```agda lowerSetChoice : ∀ {ℓ} → SetChoice (ℓ-suc ℓ) → SetChoice ℓ lowerSetChoice sc X setX B inh = PT.map (λ f x → lower (f (lift x))) (sc (Lift X) (isOfHLevelLift 2 setX) (λ x → Lift (B (lower x))) ``` The remaining inputs are transferred in the same way. Each lifted fiber is merely inhabited, because lowering its index and mapping `lift` over the resulting truncation exhibits the required element; `PT.map` acts inside the truncation, so the hypothesis holds in exactly the form the principle demands. When `sc` returns the mere existence of a lifted choice function `f`, one further `PT.map` produces the mere existence of the lowered function, whose value at `x` is `lower (f (lift x))`. The final step is legitimate because the goal is a statement inside a truncation: about the particular `f`, nothing is ever claimed outside it. ```agda (λ x → PT.map lift (inh (lower x)))) ``` ## Diaconescu's theorem The theorem reads: given set-level choice, every proposition `P` can be decided, proved or refuted. From a constructive viewpoint this conclusion is far from evident, since an arbitrary `P` offers no case to split on; a decision procedure has nothing to inspect directly. The proof approaches the question geometrically instead. It builds a small space whose shape depends on `P`: in it, the classes of `true` and `false` coincide exactly when `P` holds. One question about this space, put to choice, forces the shape into the open, and the shape is `P`. Concretely, fix a proposition `P : hProp ℓ` and work in a module dedicated to the theorem. Take the two booleans and glue them together exactly when `P` holds. Gluing is a set quotient: the points are still `true` and `false`, a path is added between them whenever the gluing relation says so, and the result is made into an h-set. The relation is a table with four entries: trivially true on the diagonal, and literally `P` itself in the two mixed squares. By that last clause, being related across the two points is the same statement as `P`, and the argument uses it twice. The gluing relation `_~_` is defined by pattern matching on the two booleans, so the four entries of the table are visible at once. When the two inputs agree, the relation holds with the one element `tt*` of the unit type `Unit*`. When they differ, it holds with a proof of `⟨ P ⟩`, the statement underlying `P`. Nothing else is used: reading the mixed squares off the table is already the proof that being related across the two points says exactly `P`. ```agda module Diaconescu {ℓ} (P : hProp ℓ) where _~_ : Bool → Bool → Type ℓ true ~ true = Unit* false ~ false = Unit* _ ~ _ = ⟨ P ⟩ ``` The space itself, `Glued`, is the set quotient `Bool / _~_`. A set quotient of a type by a relation keeps the points and adds a path `[ b ] ≡ [ b' ]` whenever the relation is proved to relate them, by the constructor `eq/`; the further constructor `squash/` makes the result an h-set. Its two distinguished points are the classes `[ true ]` and `[ false ]`. When `P` holds, the quotient supplies the path between them; when `P` fails, the backward reading below shows the two classes apart. ```agda Glued : Type ℓ Glued = Bool / _~_ ``` Everything now rests on one theorem about set quotients, the library's effectivity: for a relation that is proposition-valued and satisfies the equivalence laws, a path between classes exists only because the relation related the representatives. A path in the quotient can therefore be read backwards, into a proof of the relation. The table provides each condition the theorem asks for, and the next paragraphs verify them entry by entry. The first condition is proposition-valuedness: for each pair of inputs, the type of proofs of `a ~ b` must be a proposition. On the diagonal that type is `Unit*`, a proposition by `isPropUnit*`; in the mixed squares it is `⟨ P ⟩` itself, and its propositionhood is exactly the second component `P .snd` of the pair `P`. Were proofs allowed to differ, a path in the quotient would not determine a well-defined statement to read back. ```agda ~-prop : BinaryRelation.isPropValued _~_ ~-prop true true = isPropUnit* ~-prop false false = isPropUnit* ~-prop true false = P .snd ~-prop false true = P .snd ``` Reflexivity is immediate: the two diagonal entries hold unconditionally, so every boolean is related to itself, with `tt*` as the proof in each case. ```agda ~-refl : (a : Bool) → a ~ a ~-refl true = tt* ~-refl false = tt* ~-sym : (a b : Bool) → a ~ b → b ~ a ~-sym true true _ = tt* ``` Symmetry holds because the table itself is symmetric: swapping the inputs carries each entry to itself, so a proof of `a ~ b` serves as a proof of `b ~ a`. On the diagonal the proof is `tt*` either way, and in the mixed squares it is a proof of `P`, the same thing in both directions. ```agda ~-sym false false _ = tt* ~-sym true false p = p ~-sym false true p = p ~-trans : (a b c : Bool) → a ~ b → b ~ c → a ~ c ~-trans true _ true _ _ = tt* ``` Transitivity asks for a little more care, since two proofs could in principle demand an entry the table does not contain. The cases show this cannot happen. Whenever the endpoints agree, a diagonal entry settles the result trivially; whenever they differ, one of the two given proofs comes from a mixed square, and the other then involves only equal booleans, so the same proof of `P` serves as the result. Six cases cover the possibilities, each reusing one of the inputs. ```agda ~-trans false _ false _ _ = tt* ~-trans true false false p _ = p ~-trans false true true p _ = p ~-trans true true false _ p = p ~-trans false false true _ p = p ``` The three laws assemble into the record `isEquivRel _~_` by the constructor `BinaryRelation.equivRel`. With proposition-valuedness and the equivalence laws in place, `Glued` meets exactly the hypotheses of effectivity, and the backward reading of its paths is available to the lemmas below. ```agda ~-equivRel : BinaryRelation.isEquivRel _~_ ~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans ``` The core of the construction is a two-line statement: the two distinguished classes coincide exactly when `P` holds. If `P` holds, the table relates `true` to `false`, and the quotient identifies their classes. If the classes coincide, effectivity reports that the relation related `true` to `false`, and by the table that relation is `P`. The mixed squares do the work in both directions: a proof of `P` feeds the path constructor directly, and the output of effectivity is already a proof of `⟨ P ⟩`, with no decoding and no impossible case to dismiss. The two directions become named functions. Forward, `glue` hands a proof of `P` to the path constructor: since the mixed entry holds with proof `p`, the two classes are equal by the definition of the quotient. Backward, `unglue` is effectivity instantiated at `true` and `false`: any path between the two classes returns a proof of `true ~ false`, and by the table that is a proof of `⟨ P ⟩`. No case analysis on the path is needed. Together they form a dictionary between `P` and the equality of the two classes. ```agda glue : ⟨ P ⟩ → Path Glued [ true ] [ false ] glue p = eq/ true false p unglue : Path Glued [ true ] [ false ] → ⟨ P ⟩ unglue = effective ~-prop ~-equivRel true false ``` Now the choice principle is put to use, with a single question: hand every point of `Glued` a boolean representative. A pick at a point is a boolean together with the guarantee that its class equals that point. Each point on its own is sure to have one, but only merely so: a quotient remembers that its points come from representatives without remembering which. Converting this pointwise mere inhabitation into the mere existence of one function choosing everywhere at once is exactly what set-level choice states, and it applies here because `Glued` is an h-set by construction. The chooser acts uniformly over the whole space; the final comparison will read it at the two distinguished classes only. The family to choose from is `Pick x`, a dependent pair: a boolean `b` together with the path witnessing that the class `[ b ]` equals the point `x`. That every point merely has a pick is not an extra assumption but a theorem about quotients: `[]surjective` says each element of a quotient arises, merely, as the class of some representative, and `pickable` is that statement with `x` ranging over `Glued`. Note what the second component is for: it records which representative was chosen, and it is this certificate, not the boolean alone, that lets the argument rebuild paths between classes. ```agda Pick : Glued → Type ℓ Pick x = Σ[ b ∈ Bool ] ([ b ] ≡ x) pickable : (x : Glued) → ∥ Pick x ∥₁ pickable = []surjective ``` The question deserves a lemma of its own, so that its type displays what choice delivers: the mere existence of a function picking on the whole of `Glued`. Given `sc : SetChoice ℓ`, the lemma instantiates it with the data assembled so far, the index `Glued`, its h-set proof `squash/`, the family `Pick`, and the pointwise inhabitation `pickable`. The hypothesis `sc` is itself a function; what is truncated is only its output. Choice thus returns no function, only the statement that one exists, and this limit shapes the final step of the theorem. ```agda merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁ merePicker sc = sc Glued squash/ Pick pickable ``` Suppose, then, that a picking function `g` of type `(x : Glued) → Pick x` is at hand. Evaluating it at the two distinguished points yields two picks, and their first components are the booleans `b₀` and `b₁`, chosen at the class of `true` and at the class of `false`. All further reasoning concerns these two ordinary booleans, which is what makes `P` mechanically decidable. Two lemmas connect the values to `P`, one for each direction: if the representatives agree, their guarantees give a path from the class of `true` to the class of `false`, and effectivity reads it into `P`; if `P` holds, the two distinguished points are equal, and `g` respects the equality, so `b₀` and `b₁` agree. ```agda module _ (g : (x : Glued) → Pick x) where b₀ : Bool b₀ = g [ true ] .fst b₁ : Bool b₁ = g [ false ] .fst ``` The first lemma reads an equality `q : b₀ ≡ b₁` backwards into `P`. Three paths compose in `Glued`: from the class of `true` to the class of `b₀` (the guarantee of `g [ true ]`), from there to the class of `b₁` (the equality of classes induced by `q` through `cong [_]`), and from there to the class of `false` (the guarantee of `g [ false ]`). The composite runs from one distinguished class to the other, and `unglue` turns it into a proof of `⟨ P ⟩`. The second lemma goes forward: given a proof `p` of `P`, the path `glue p` identifies the two points, and applying `g` along it gives `b₀ ≡ b₁`; since both endpoints are plain booleans, this is a direct projection of `g`, with no transport of the family. ```agda agree→P : b₀ ≡ b₁ → ⟨ P ⟩ agree→P q = unglue (sym (g [ true ] .snd) ∙ cong [_] q ∙ g [ false ] .snd) P→agree : ⟨ P ⟩ → b₀ ≡ b₁ P→agree p i = g (glue p i) .fst ``` Now decide `P` by inspecting the two booleans, which, unlike `P`, can be inspected: two booleans are equal or not, mechanically. If they agree, the first lemma proves `P`. If they differ, `P` must fail, for otherwise the second lemma would force them to agree. Either way `P` is decided, and the case split ran on the two chosen booleans, never on `P` itself. The decidable equality `_≟_` compares `b₀` with `b₁` and returns an element of `Dec (b₀ ≡ b₁)`: either `yes` with the equality proof, or `no` with its refutation. The helper `fromDec` converts each outcome through the dictionary. In the `yes` case the equality `q` feeds `agree→P` and yields the left summand, a proof of `⟨ P ⟩`. ```agda decide : ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥) decide = fromDec (b₀ ≟ b₁) where fromDec : Dec (b₀ ≡ b₁) → ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥) fromDec (yes q) = Sum.inl (agree→P q) ``` In the `no` case, `ne` proves that the two booleans cannot be equal. Were `P` to hold, `P→agree` would exhibit them as equal, against `ne`; the right summand is therefore the function that takes any proof of `⟨ P ⟩`, obtains `b₀ ≡ b₁` by the forward lemma, and hands it to `ne`. Together the two cases decide `P`, with the case split on boolean data alone. ```agda fromDec (no ne) = Sum.inr (λ p → ne (P→agree p)) ``` One gap remains before the theorem assembles. Choice delivers no picking function, only its mere existence. But the goal, `P` or not `P`, is itself a proposition: the two sides exclude each other, so between any two decisions there is nothing to distinguish. Into such a goal, mere existence eliminates as if it were actual, and the proof closes. That the goal is a proposition is proved explicitly: `Sum.isProp⊎` asks for the propositionhood of each side and for the impossibility of inhabiting both. The first side is `⟨ P ⟩`, propositional by `P .snd`. The second is the function type `⟨ P ⟩ → Empty.⊥`, whose propositionhood follows pointwise from `Empty.isProp⊥` by `isPropΠ`. Finally, `λ p np → np p` proves that the two sides cannot be inhabited at once. The theorem `choice→lem` then has type `SetChoice ℓ → LEM ℓ`. Given `sc` and a proposition `P`, it works inside the Diaconescu module at `P`, obtains the mere picker by `merePicker sc`, and eliminates the truncation with `PT.rec` into the now-certified propositional goal, returning `decide`. The order of ideas matters: the case split inside `decide` is genuine data, and the truncation is discharged only because the target cannot distinguish its answers. ```agda decideIsProp : isProp (⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥)) decideIsProp = Sum.isProp⊎ (P .snd) (isPropΠ (λ _ → Empty.isProp⊥)) (λ p np → np p) choice→lem : ∀ {ℓ} → SetChoice ℓ → LEM ℓ choice→lem sc P = PT.rec decideIsProp decide (merePicker sc) where open Diaconescu P ``` ## Recap At one fixed level, `SetChoice` says that over an h-set of indices, the mere inhabitation of every fiber yields the mere existence of one function choosing everywhere at once. One higher-level instance therefore covers the level below, and by Diaconescu's theorem it decides every proposition of its level. In the direction this chapter proves, choice is the stronger classical interface: `SetChoice ℓ → LEM ℓ`, and no converse is established here. The model chapter uses one `SetChoice (ℓ-suc ℓ)` instance in two ways: `choice→lem` supplies excluded middle for the ZF axioms, while `lowerSetChoice` supplies the choice-set axiom at the lower level.