--- title: "The classical boundary" module: Base.Classical lang: en site: "Bedrock" description: "The classical boundary" stage: "Foundations" reading_order: 4 canonical: https://bedrock.institute/en/Base.Classical.html html: Base.Classical.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Classical.lagda.md prerequisites: [Base.Prelude, Base.Impredicativity] routes: [common-foundations] translations: [https://bedrock.institute/zh/Base.Classical.md, https://bedrock.institute/ja/Base.Classical.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The classical boundary In a universe-leveled type theory, propositions raise two distinct smallness questions. First, fixing a proposition `P : hProp (ℓ-suc ℓ)`, can we find an equivalent proposition one level down? That is propositional resizing: it speaks proposition by proposition. Second, the type `hProp ℓ` of all level-`ℓ` propositions itself lives in `Type (ℓ-suc ℓ)`; can the whole totality be presented by one small type? That is the small classifier. The two claims have different shapes, and this chapter proves both from one explicit hypothesis. The hypothesis is excluded middle: every proposition of a given level is either true or false. Cubical type theory does not assume it, so each classical proof here receives it as an explicit parameter, and each result records exactly which level instance it uses. Constructive definitions and classical steps stay separate throughout: the constructions decide nothing on their own, and the hypothesis enters only where decisions are consumed. ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Classical where ``` The two smallness questions received their exact shapes in the Impredicativity chapter, and this chapter uses that vocabulary unchanged. For a single proposition, `isSmall P` consists of a lower-level proposition `Q : hProp ℓ` together with an equivalence of underlying types `⟨ P ⟩ ≃ ⟨ Q ⟩`. The uniform statements differ in what they quantify over: `Resizing ℓ` asks that every `P : hProp (ℓ-suc ℓ)` carry such data, while `HPropSmallness ℓ` asks for a single type `Ω' : Type ℓ` equivalent to the whole `hProp ℓ` at once. One is a family of per-proposition witnesses, the other one carrier for the totality; this chapter derives each from excluded middle and claims no implication between them. ```agda open import Base.Prelude open import Base.Impredicativity using ( isSmall; Resizing; HPropSmallness; Impredicativity ) ``` What it means to decide a proposition must be fixed before anything is proved. To decide `P` is to produce either a proof of `⟨ P ⟩`, or a map from `⟨ P ⟩` into the empty type, which refutes `P` by turning any proof into an absurdity. The coproduct `_⊎_` with its two constructors carries exactly this either-or, and the disjunction is genuine data: an element knows which side it came from, so a decision can be used in a case analysis. The booleans `Bool` with `true` and `false` will label the two outcomes, and `tt*` is the lone inhabitant of the unit type underlying the proposition true. ```agda 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* ) ``` Smallness compares propositions through sameness, and two forms of sameness appear below. Between two propositions, a pair of maps in both directions yields a path between the `hProp` values, by propositional extensionality `⇔toPath`; it also yields an equivalence of underlying types, by `propBiimpl→Equiv`. An isomorphism `iso` records two maps together with the two inverse laws, and `isoToEquiv` reads it as an equivalence. The classifier will identify propositions, so it builds paths of `hProp`; resizing must deliver equivalences of underlying types. ```agda 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 Before proving anything, the assumption must be stated with its universe level pinned down. The level index is not decoration: it says at which universe the uniform decision is demanded, and every later theorem can be read off for which classical instance it asks. For each universe level `ℓ`, `LEM ℓ` is a function taking a proposition `P : hProp ℓ` and returning either a proof of `⟨ P ⟩` or a refutation, that is, a map from `⟨ P ⟩` into the empty type. Because it quantifies over all propositions of `hProp ℓ`, its type lives one universe up, in `Type (ℓ-suc ℓ)`. The statement is therefore large, although each decision it delivers is one small piece of data, and `LEM ℓ` is asserted one level at a time rather than for all levels at once. Note the strength this shape provides: a decision is data, not a proposition, so a hypothesis of excluded middle permits case analysis between a proof and a refutation, rather than merely asserting that one of them exists. ```agda LEM : ∀ ℓ → Type (ℓ-suc ℓ) LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) ``` Applications need excluded middle at more than one level, yet a proof is usually handed only the higher instance `LEM (ℓ-suc ℓ)`. One descent lemma bridges the gap. It is a one-step result, exactly `LEM (ℓ-suc ℓ) → LEM ℓ`: to decide `P : hProp ℓ`, decide a lifted copy of `P` one universe up and bring the verdict back. Nothing here claims that decisions descend through arbitrarily many levels at once. Given `lem : LEM (ℓ-suc ℓ)` and a proposition `P : hProp ℓ`, the plan is to apply `lem` not to `P` itself but to a lifted copy of `P` living at level `ℓ-suc ℓ`, where the hypothesis applies. The verdict about the copy is then translated back into a verdict about `P`. ```agda lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ lowerLEM {ℓ} lem P = fromLifted (lem lifted) ``` The lifted proposition has underlying type `Lift ⟨ P ⟩`. Its elements are the elements of `⟨ P ⟩` in the higher universe, and it is a proposition: for elements `x` and `y`, lower both with `lower`, use the propositionhood `P .snd` of `P` to get a path between the lowerings, and apply `cong lift` to lift that path back up. So `lifted` is a legitimate input to `lem`. ```agda where lifted : hProp (ℓ-suc ℓ) lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y)) ``` Translating the verdict needs only `lift` and `lower`, and these travel in the right directions. A proof of `Lift ⟨ P ⟩` lowers with `lower` to a proof of `⟨ P ⟩`. A refutation of `Lift ⟨ P ⟩` composed with `lift` becomes a refutation of `⟨ P ⟩`, since it applies to any proof of `⟨ P ⟩` after lifting. Both cases are pure transport of the decision, with no classical reasoning of their own; the classical step was deciding the lifted proposition. ```agda fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) fromLifted (inl p) = inl (lower p) fromLifted (inr np) = inr (λ p → np (lift p)) ``` ## A small classifier from excluded middle Classically, every proposition at a fixed level is one of two things: true or false. That suggests a two-point classifier. The candidate small representative is `Lift Bool`, with `true` representing the proposition true and `false` representing the proposition false. Two warnings keep the picture honest. A Boolean is a label; the proposition it represents is a separate `hProp` value, and the classifier equates them only up to paths between `hProp` values, never by syntactic identity. And the two endpoints have different sizes: `Lift Bool` lives in `Type ℓ` while `hProp ℓ` lives in `Type (ℓ-suc ℓ)`; an equivalence is allowed to relate types at different levels, and that size gap is precisely the smallness being established. The construction splits cleanly. Decoding sends each Boolean to its representative proposition. Encoding needs to know, for a given `P`, which case holds, so it takes the decision of `P` as an explicit argument; the two inverse laws are then proved for that data. Excluded middle enters only at the end, to supply such decisions uniformly. The two representative propositions are the canonical top proposition `⊤` and bottom proposition `⊥` of the Prelude's logical operations. The latter is definitionally the pair `(⊥* , isProp⊥*)`, so its underlying type is the empty type `⊥*`. Both are available at every level `ℓ`, which is exactly what lets them serve as representatives inside `hProp ℓ`; the Boolean labels below will denote precisely these two. ```agda private decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ ``` Decoding reads a Boolean label and returns the proposition it represents: `lift true` yields `⊤` and `lift false` yields `⊥`. The domain is the lift `Lift {ℓ-zero} {ℓ} Bool` rather than `Bool` itself: `Bool` lives in `Type ℓ-zero`, and its lift is a type of `Type ℓ`, which is what the classifier's statement demands. Note that decoding alone is only a function assigning representatives; that the assignment is faithful in both directions is the content of the two inverse laws below. ```agda decodeB (lift true) = ⊤ decodeB (lift false) = ⊥ ``` Encoding is the converse assignment: given `P` and a decision of `P`, return the label of the winning case. The decision is an explicit argument, not something the encoder produces itself, so this step uses no excluded middle. Choosing a representative for `P` is thus a two-step affair in general: first decide `P`, then read off the label. The two inverse laws will show the round trips are the identity, one on propositions and one on labels. The match is on the decision, not on `P`: an inhabitant of the left summand yields `lift true`, one of the right yields `lift false`. The proof or refutation itself is discarded, because the label records only which case held, not a witness. The result type is `Lift {ℓ-zero} {ℓ} Bool`, matching `decodeB`'s domain exactly. ```agda encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool encodeB P (inl _) = lift true encodeB P (inr _) = lift false ``` The first inverse law says that the representative chosen through a decision has the same truth value as `P`. Concretely, `secB` proves `decodeB (encodeB P d) ≡ P`, a path between `hProp` values. The proof strategy in both cases is the same: give maps in both directions and let propositional extensionality `⇔toPath` assemble the path. If the decision was a proof `p`, the goal is `⊤ ≡ P`. The map from `⊤` to `⟨ P ⟩` is simply `p`, the decided witness; in the reverse direction every input goes to `tt*`, the lone inhabitant of `⊤`. If the decision was a refutation `np`, the goal is `⊥ ≡ P`. Out of `⊥*` there is no constructor to match, which the absurd pattern `λ ()` expresses, and each proof `p` of `⟨ P ⟩` is fed to `np` and eliminated by `Empty.rec`. In both branches the chosen representative is path-equal to `P`, so the encoding round trip loses no truth value. ```agda 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 second inverse law reads the representative back: `encodeB (decodeB b) d ≡ b`. Here one subtlety is essential. In the assembled classifier the decision `d` will be produced by excluded middle, and nothing guarantees how that decision computes. So `retrB` must hold for **every** decision `d`, not just the ones a particular proof would supply. The proof therefore splits into four cases: two compatible branches compute to `refl`, and two incompatible branches are eliminated as impossible, which also shows the two representatives cannot be confused: `⊤` is inhabited and `⊥` is empty. For `b = lift true`, decoding gives `⊤`. Encoding with a proof returns `lift true`, and the goal is definitionally `refl`. The alleged refutation branch cannot occur: applying it to `tt*`, the inhabitant of `⊤`, would give an element of the empty type, and `Empty.rec` concludes the case from that contradiction. ```agda 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*) ``` For `b = lift false`, decoding gives `⊥` with underlying type `⊥*`. An alleged proof of it would be a term of the empty type, so the absurd pattern `()` ends that branch at once; encoding with a refutation returns `lift false`, again by `refl`. Across all four cases, the label returned always equals the label we started from, whichever decision is supplied. ```agda retrB (lift false) (inl ()) retrB (lift false) (inr _) = refl ``` Now the pieces assemble into the classifier promised by `HPropSmallness ℓ`: a type in `Type ℓ` equivalent to `hProp ℓ`. The small type is `Lift Bool`; the equivalence comes from the isomorphism whose forward map is `decodeB` and whose backward map decides `P` and encodes. The two inverse laws are exactly `secB` and `retrB`, each instantiated with decisions from `lem`. This is where excluded middle does its work in this section: it supplies, uniformly, the decisions that the constructive parts take as inputs. The pair `(Lift Bool , ...)` witnesses `HPropSmallness ℓ`: its first component has type `Type ℓ` and its second is an equivalence `Lift Bool ≃ hProp ℓ`. The level placement is the point: `Lift Bool` : `Type ℓ` while `hProp ℓ` : `Type (ℓ-suc ℓ)`, so a type one universe up acquires a small representative. This is a size statement about levels, not a claim that both sides share a universe; and the equivalence itself rests on the two inverse laws, so a Boolean label and its proposition are identified only up to the paths that `secB` and `retrB` certify. ```agda 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)))) ``` ## Propositional resizing from excluded middle The second smallness question is per-proposition. Fix `P : hProp (ℓ-suc ℓ)`; resizing produces a proposition `Q : hProp ℓ` together with an equivalence of underlying types `⟨ P ⟩ ≃ ⟨ Q ⟩`. The same two representatives serve again: if `P` is true, take `⊤`; if false, take `⊥`, both at level `ℓ`. Note the shape of the result: it is an equivalence of the underlying types, not a path between the packaged propositions `P` and `Q`. The two constructions differ in what they assemble. The classifier identifies propositions, so its sameness was assembled as paths between `hProp` values, by propositional extensionality. Resizing must instead deliver an equivalence of underlying types, and `propBiimpl→Equiv` produces exactly that: fed the propositionhood proofs `P .snd` and `Q .snd` together with the two maps, it returns `⟨ P ⟩ ≃ ⟨ Q ⟩`. Given a decision of `P`, `resizeDec` returns the witness of `isSmall P`. In the true case the witness is `(⊤ , equivalence)`: the map from `⟨ P ⟩` to `⊤` sends every input to `tt*`, and the map back uses the decided proof `p`. Since both sides are propositions, `propBiimpl→Equiv`, fed the propositionality proofs `P .snd` and `⊤ .snd`, turns this pair of maps into an equivalence of underlying types. ```agda 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) ``` In the false case the witness is `(⊥ , equivalence)`, with the same absurd maps as in `secB`: the map from `⟨ P ⟩` kills each proof `p` with the refutation `np` via `Empty.rec`, and the reverse map is absurd on the spot because `⊥*` has no constructor. Both representatives `⊤` and `⊥` live at level `ℓ`, one below `P`, which is exactly the smallness being certified: `Q` is chosen inside `hProp ℓ` and the equivalence connects `⟨ P ⟩` with `⟨ Q ⟩`. ```agda (λ p → Empty.rec (np p)) (λ ()) ``` Resizing now follows from a single instance of excluded middle at level `ℓ-suc ℓ`, and the level is forced by the statement itself: `Resizing ℓ` quantifies over `hProp (ℓ-suc ℓ)`, so the decisions it consumes are precisely decisions of propositions one universe up. `lem→resizing` turns `LEM (ℓ-suc ℓ)` into `Resizing ℓ` in one line: for each `P : hProp (ℓ-suc ℓ)`, decide it with `lem` and hand the verdict to `resizeDec`. Everything lies in the direction of the levels: resizing at `ℓ` consumes a classical decision at `ℓ-suc ℓ`, because the propositions receiving lower-universe representatives are precisely those one universe up. ```agda lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ lem→resizing lem P = resizeDec P (lem P) ``` ## Combining the two consequences The two size controls now come from one hypothesis. A single instance of `LEM (ℓ-suc ℓ)` yields resizing directly, and by descending one step with `lowerLEM` it also yields the classifier. The two principles remain distinct statements: this chapter proves both from the same hypothesis and asserts nothing about whether either implies the other. The record `Impredicativity ℓ` introduced in "Impredicativity" has two fields, one per principle, and `lem→impredicativity` fills both from a single `lem`. The resizing field is `lem→resizing lem`, which uses the given instance at its own level. The classifier field is `lem→hPropSmallness (lowerLEM lem)`, which first descends to `LEM ℓ` and then builds `Lift Bool ≃ hProp ℓ`. The sharing is a fact about this derivation: both consequences were provable from the same higher-level instance, not a claim that the principles imply each other. ```agda lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ lem→impredicativity lem = record { resizing = lem→resizing lem ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) } ``` ## Recap Excluded middle here is one thing: the ability to decide every proposition at a stated level, carried always as an explicit hypothesis. One instance at `ℓ-suc ℓ` supplied the decisions for the whole chapter. It decided each lifted proposition for `lowerLEM`, decided each `P : hProp (ℓ-suc ℓ)` for resizing, and, after one step of descent, decided every `P : hProp ℓ` for the classifier. The two consequences remain distinct principles, and nothing here compares them; `lem→impredicativity` holds both because the same hypothesis happened to yield both. The cumulative-hierarchy chapters take this interface and use it where smallness is demanded, behind full separation and the power set of `V`.