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.

{-# 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.

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.

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.

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.

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.

lowerSetChoice : ∀ {ℓ} → SetChoice (ℓ-suc ℓ) → SetChoice ℓ
lowerSetChoice sc X setX B inh =
  PT.map (λ f x → lower (f (lift x)))
         (sc (Lift X) (isOfHLevelLift  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.

             (λ 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.

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.

  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.

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

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

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

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

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

  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.

  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.

  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.

  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.

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

    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.

      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.

  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.