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.

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

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.

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.

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.

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.

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.

  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.

  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.

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.

  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.

  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.

  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.

  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.

  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.

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.

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

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

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.

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.