The classical boundary

Set theory as most readers know it is classical: excluded middle is ambient air. The host, however, is constructive, and this book keeps the boundary between the two visible as a matter of law. The rule, fixed in the Charter, is that classical principles enter as explicit parameters, never as global assumptions: a chapter that reasons classically says so in its own interface, the type checker polices the boundary, and there is not a single postulate in this book. This chapter states the one classical principle everything later appeals to, and banks its two basic dividends: the impredicativity interfaces of the previous chapter, redeemed.

{-# OPTIONS --cubical --safe --guardedness #-}

module Base.Classical where

open import Base.Prelude
open import Base.Truth
open import Base.Impredicativity
  using ( isSmall; Resizing; HPropSmallness; Impredicativity )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Bool using ( Bool; true; false )
open import Cubical.Data.Unit using ( tt* )
open import Cubical.Foundations.Equiv using ( propBiimpl→Equiv )
open import Cubical.Foundations.Isomorphism using ( iso; isoToEquiv )
open import Cubical.Functions.Logic using ( ⇔toPath )

The statement

LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)

LEM ℓ says: every proposition at level ℓ is either true or false. Why this particular form? In univalent foundations a type-level global choice or excluded middle is inconsistent with univalence; what can consistently be assumed is exactly this propositional form, quantified over hProp. The foundation itself forces the honest phrasing.

A chapter that works classically takes (lem : ∀ {ℓ} → LEM ℓ) in its module telescope and passes it along when importing other classical chapters. The consequence is worth pausing on: whether a theorem uses excluded middle is a compile-time fact. The classical debt is part of a chapter's type, visible at every import site, instead of an invisible global axiom; and since nothing is postulated, the whole book carries Agda's --safe seal.

One transfer lemma before the dividends. Excluded middle passes downward through the levels: to decide a small proposition, lift its underlying type one universe up, decide there, and lower the verdict. So a single instance of

LEM at a higher level silently covers every level below it, a fact the end of this chapter spends.

lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ
lowerLEM {ℓ} lem P = fromLifted (lem lifted)
  where
  lifted : hProp (ℓ-suc ℓ)
  lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y))
  fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
  fromLifted (inl p)  = inl (lower p)
  fromLifted (inr np) = inr (λ p → np (lift p))

The first dividend: a small classifier

Classically a proposition has only two possible values, and that innocent remark has universe-level teeth. First the classifier: HPropSmallness ℓ, named in the previous chapter, asks for a small type equivalent to hProp ℓ. Classically it is Lift Bool, at every level ℓ. The construction is arranged so that all the real work is constructive: the four helpers below take a decision of a proposition (a proof, or a refutation) as an ordinary argument, and excluded middle enters only at the final assembly, to supply those decisions.

First the chapter cashes the promise of the scope discipline: it opens the canonical instance, taking exactly its ⊤ and ⊥. From here on the two symbols mean the hProp algebra's truth values, and by definitional transparency this ⊥ is the pair (⊥* , isProp⊥*) itself. Then the decoding direction, from Booleans to propositions: decodeB sends true to

⊤ and false to ⊥. The domain is

lives at the bottom level while the propositions live at ℓ: the lifted copy is what lets the two ends of the coming equivalence share a universe.

open module Canonical {ℓ : Level} = TruthAlgebra (hPropAlgebra ℓ) using ( ⊤; ⊥ )

private
  decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ
  decodeB (lift true)  = ⊤
  decodeB (lift false) = ⊥

The encoding direction hides an asymmetry. Its would-be signature is

hProp ℓ → Lift Bool, the exact inverse of decodeB, but no such function can be defined: unlike lift true and lift false, an arbitrary proposition P is not a pattern one can match on, so there is no case split "if P holds, otherwise" to write. encodeB therefore takes one extra argument, a decision d of P, and matches on that: a proof gives

true, a refutation gives false. The shape mirrors

decodeB, but the thing being inspected is the handed-over decision, never the proposition itself. No excluded middle here; the decision is an input.

  encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool
  encodeB P (inl _) = lift true
  encodeB P (inr _) = lift false

One round trip: decoding the encoding of P gives back P itself. The tool is

⇔toPath, the library's propositional extensionality: between propositions, maps in both directions already make a path (in this book that principle is a theorem, not an axiom). If the decision is a proof p, the goal is

⊤ ≡ P, and both directions are trivial: from ⊤ to P the answer p is already in hand, and back the other way everything maps to

tt*, the inhabitant of ⊤. If the decision is a refutation np, the goal is ⊥ ≡ P: out of ⊥* nothing needs saying, which is what the absurd pattern λ () says, and any alleged proof p of P is crushed by np, with Empty.rec eliminating the resulting absurdity.

  secB : ∀ {ℓ} (P : hProp ℓ) (d : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥))
       → decodeB (encodeB P d) ≡ P
  secB P (inl p)  = ⇔toPath (λ _ → p) (λ _ → tt*)
  secB P (inr np) = ⇔toPath (λ ()) (λ p → Empty.rec (np p))

The other round trip: encoding the decoding of a Boolean b gives back b. One subtlety deserves attention: at assembly time it is excluded middle that will decide

proves the equation for every decision d, by four cases. true with a proof: refl. true with an alleged refutation n⊤: impossible, since ⊤ does hold, and n⊤ tt* is the absurdity. false with an alleged proof: that proof is a term of ⊥*, and the absurd pattern () closes the case before any equation is owed. false with a refutation: refl.

  retrB : ∀ {ℓ} (b : Lift {ℓ-zero} {ℓ} Bool)
          (d : ⟨ decodeB b ⟩ ⊎ (⟨ decodeB b ⟩ → Empty.⊥))
        → encodeB (decodeB b) d ≡ b
  retrB (lift true)  (inl _)  = refl
  retrB (lift true)  (inr n⊤) = Empty.rec (n⊤ tt*)
  retrB (lift false) (inl ())
  retrB (lift false) (inr _)  = refl

The assembly. iso packages the four pieces (decode; decide, then encode; the two round trips), and isoToEquiv upgrades the isomorphism to an equivalence. Count the occurrences of lem: three, and all three do the same job, supplying the decisions the constructive helpers asked for as inputs. That is the entire footprint of excluded middle in this dividend.

lem→hPropSmallness : ∀ {ℓ} → LEM ℓ → HPropSmallness ℓ
lem→hPropSmallness lem = Lift Bool , isoToEquiv (iso decodeB
  (λ P → encodeB P (lem P))
  (λ P → secB P (lem P))
  (λ b → retrB b (lem (decodeB b))))

The second dividend: propositional resizing

Second, Resizing: every proposition one universe up is small. Classically, decide the proposition: if it holds it is equivalent to ⊤, if it fails to ⊥, and both are small.

As before, the work is done from a handed-over decision, and P .snd (the propositionality proof, as the Prelude promised) is used directly. If P holds, the small stand-in is the ⊤ of level ℓ: between two propositions, maps in both directions already form an equivalence of underlying types, which is what propBiimpl→Equiv builds from the two propositionality proofs and the two maps; from P to ⊤ everything goes to tt*, and back the other way p is in hand. If P fails, the stand-in is ⊥, with the same two absurdity moves as in secB. Note the shift against the first dividend: there the output was a path between propositions (⇔toPath), here it is an equivalence between their underlying types, so the same pair of maps is fed to

propBiimpl→Equiv instead.

private
  resizeDec : ∀ {ℓ} (P : hProp (ℓ-suc ℓ)) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
            → isSmall P
  resizeDec P (inl p)  = ⊤ , propBiimpl→Equiv (P .snd) (⊤ .snd) (λ _ → tt*) (λ _ → p)
  resizeDec P (inr np) = ⊥ , propBiimpl→Equiv (P .snd) (⊥ .snd)
                               (λ p → Empty.rec (np p)) (λ ())

The assembly is one line: decide P with excluded middle, hand the decision over. The signature is the strength bookkeeping: this dividend consumes excluded middle at the higher level ℓ-suc ℓ, once, and nothing more.

lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ
lem→resizing lem P = resizeDec P (lem P)

Redeeming the packing

The previous chapter packed the two instruments as Impredicativity, by co-consumption, not implication: neither derives the other. Only the excluded middle redeems both at once, and from a single instance at the higher level: resizing consumes it as is, and lowerLEM hands the classifier its lower copy. Part 3 will name its exact prices in this packing.

lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ
lem→impredicativity lem = record
  { resizing       = lem→resizing lem
  ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) }

Recap

Excluded middle is stated as the interface LEM, taken by chapters as a parameter and never assumed globally; the boundary between constructive and classical mathematics is therefore a compile-time fact. The previous chapter's two interfaces are banked as dividends, the small classifier by

lem→hPropSmallness and propositional resizing by

lem→resizing, and the packing Impredicativity is redeemed whole (lem→impredicativity). Part 3 will spend exactly this packing: it prices, for the cumulative hierarchy V, the smallness assumptions behind full separation and power set.