Choice

The classical boundary has a second interface. Alongside the excluded middle, classical mathematics runs on choice, and this chapter states the book's form of it, one level at a time, in the same interface style as LEM. Set-level choice says that over an h-set of indices, truncation commutes with the product: if every fiber is merely inhabited, then merely, every fiber is inhabited at once. This is the type-theoretic reading of "a family of nonempty sets has a choice function", and the h-set restriction on the index is what keeps it honest, since over arbitrary types the principle is simply false. Like the excluded middle, choice is never assumed globally: a chapter that needs it takes it as a parameter, and the first to do so is Part 3's summit.

The two interfaces are not peers, and this chapter proves it on the spot: choice proves the excluded middle. The observation is due to Diaconescu, with the type-theoretic form by Goodman and Myhill; it means that at each level the choice interface quietly carries the whole classical boundary with it.

{-# 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 )
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
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 )
open import Cubical.Relation.Binary.Base using ( module BinaryRelation )

The principle

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

Like the excluded middle, choice passes downward through the levels: lift the index set and the fibers one universe up, choose there, lower the choice function. A single higher instance therefore covers the levels below.

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)))
             (λ x → PT.map lift (inh (lower x))))

Diaconescu's theorem

The theorem: given set-level choice, any proposition P can be decided, proved or refuted. On its face this is absurd, since a decision procedure has nothing to inspect: an arbitrary P offers no case to split on. The proof's idea is to make geometry do the inspecting. Build a little space whose very shape depends on P: it has one point if P holds and two points if it fails. Ask choice a single question about that space; the answer cannot help but leak the shape, and the shape is P.

Concretely, fix P; everything below lives in a module named after the theorem's author. Take the two booleans and glue them together exactly when P holds. "Gluing" is a set quotient: the points are still true and false, but a path is added between them whenever the gluing relation says so, and the result is truncated to an h-set. The relation is best given as a four-entry table: trivially satisfied on the diagonal, and literally P itself in the two mixed squares, so that "the two points are related" and "P holds" are the same proposition by definition. That last clause is the whole trick, and it will pay twice below.

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

  _~_ : Bool → Bool → Type ℓ
  true  ~ true  = Unit*
  false ~ false = Unit*
  _     ~ _     = ⟨ P ⟩

  Glued : Type ℓ
  Glued = Bool / _~_

Because the relation is a table, its certificates are tables too: propositional in every square, reflexive on the diagonal, symmetric since the table is, and transitive by reading off whichever mixed square survives. The certificates are not bookkeeping: they are the ticket to the library's effectivity theorem, which says that a quotient by a propositional equivalence relation glues honestly: two points end up connected only if the relation actually related them, never by accident. In other words, a path in the quotient can be read backwards, recovering the relation that caused it.

  ~-prop : BinaryRelation.isPropValued _~_
  ~-prop true  true  = isPropUnit*
  ~-prop false false = isPropUnit*
  ~-prop true  false = P .snd
  ~-prop false true  = P .snd

  ~-refl : (a : Bool) → a ~ a
  ~-refl true  = tt*
  ~-refl false = tt*

  ~-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 b c : Bool) → a ~ b → b ~ c → a ~ c
  ~-trans true  _     true  _ _ = tt*
  ~-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

  ~-equivRel : BinaryRelation.isEquivRel _~_
  ~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans

The heart of the construction is a two-line dictionary: the two points of the quotient coincide exactly when P holds. One direction: if P holds, the table relates true to false, so the quotient identifies their classes; the space has collapsed to a single point. The other direction: if the two classes coincide, honesty of the gluing says the relation must have related true to false, and by the table that relation is P, so P holds. This is where the mixed square pays for the first time, twice over: a P-witness feeds the path constructor directly, and the effectivity theorem's output is already a proof of P, with no decoding and no impossible case to dismiss.

  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 enters, and here is the single question we ask it: hand every point of the glued space a boolean representative. A pick at a point is a boolean together with the guarantee that its class is that point. Each point separately is sure to have one, but only merely so: a quotient remembers that its points came from somewhere without remembering from where. Turning "each point merely has a representative" into one function choosing representatives everywhere at once is exactly what set-level choice does, and it applies because the glued space is an h-set by construction. Note what the function cannot do: it was built with no access to P, so it answers the same way whether or not P holds; it merely, blindly, picks.

  Pick : Glued → Type ℓ
  Pick x = Σ[ b ∈ Bool ] ([ b ] ≡ x)

  pickable : (x : Glued) → ∥ Pick x ∥₁
  pickable = []surjective

The question deserves to be a lemma of its own, so that its type displays exactly what choice delivers: merely, a picking function, whole.

  merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁
  merePicker sc = sc Glued squash/ Pick pickable

Suppose, then, that a picking function g is in hand. Apply it to the two distinguished points, the class of true and the class of false, and name the two boolean representatives it selects, b₀ and b₁. These two booleans are the leak. One lemma per direction ties them to P. If the representatives agree, walk the guarantees: the class of true connects to the class of b₀, which is the class of b₁, which connects to the class of false; so the two points coincide, and the dictionary's backward entry turns that coincidence into a proof of P. If P holds, the two points are one single point, and a function applied to one point yields one answer, so b₀ and b₁ are forced to be the same boolean. (Formally: project g along the gluing path; both endpoints of the projection are plain booleans, so no transport is even needed.)

  module _ (g : (x : Glued) → Pick x) where

    b₀ : Bool
    b₀ = g [ true ] .fst

    b₁ : Bool
    b₁ = g [ false ] .fst

    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 looking at the two booleans, which, unlike P, can be inspected: two booleans are equal or they are not, mechanically. If b₀ and b₁ agree, the first lemma proves P. If they differ, P must fail, for had it held, the second lemma would force them to agree. Either way P is decided, and note where the classical rabbit came out of the hat: the case split happened on finite data that the choice function was forced to commit to, not on P itself.

    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)
      fromDec (no ne) = Sum.inr (λ p → ne (P→agree p))

One last gap and the theorem assembles. Choice never hands over an actual 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.

  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

SetChoice is the book's choice interface, one level at a time, in the same shape as LEM; and by choice→lem it is the stronger of the two: choice decides every proposition of its level, through the glued booleans, the glue/unglue dictionary, and one comparison of chosen representatives. The excluded middle does not return the favour, so the two interfaces remain distinct. The model chapter spends choice on its choice set, and closes by cashing this chapter's theorem: one instance of choice, one universe up, funds the entire classical bill.