Read this chapter directly, or use the interactive contents and dependency graph to choose another route.

Interactive contents · Dependency graph

This book develops classical set theory inside constructive Cubical type theory. Keeping the ambient foundation constructive makes the boundary of classical reasoning visible: definitions and proofs that do not need excluded middle remain constructive, while a theorem that does need it receives it as an explicit parameter. If classical logic were built into the ambient theory from the outset, the statements themselves would no longer reveal that distinction.

Besides marking the point at which the development becomes classical, excluded middle resolves the two smallness questions left open in the preceding chapter:

Excluded middle

Excluded middle supplies a decision for every proposition. Since propositions inhabit different universes, this principle must be stated one level at a time.

Definition (LEM) We write LEM ℓ for excluded middle at level ℓ, and define it as the dependent function below. For each P : hProp ℓ, it returns a decision Dec ⟨ P ⟩: yes carries a proof of P, while no carries a refutation. Because the function ranges over the whole proposition universe hProp ℓ, LEM ℓ inhabits Type (ℓ-suc ℓ). Its level index therefore records exactly which propositions the classical assumption can decide.

LEM : ∀ ℓ → Type (ℓ-suc ℓ)
LEM ℓ = (P : hProp ℓ) → Dec ⟨ P ⟩

Fact (isPropLEM) At every level ℓ, excluded middle LEM ℓ is itself a proposition.

isPropLEM : ∀ {ℓ} → isProp (LEM ℓ)

Proof For each P : hProp ℓ, isPropDec makes Dec ⟨ P ⟩ a proposition. The closure of propositions under dependent functions, isPropΠ, then proves the claim pointwise.

isPropLEM {ℓ} = isPropΠ λ P → isPropDec ⟨ P ⟩isProp

Lemma (lowerLEM) Excluded middle at a successor level implies excluded middle at the level immediately below. Repeating the lemma descends through further successor levels.

lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ

Proof Let lem : LEM (ℓ-suc ℓ) be given, and fix P : hProp ℓ. The hypothesis cannot decide P directly because it expects a proposition at level ℓ-suc ℓ. We therefore form the higher-level proposition whose underlying type is Lift ⟨ P ⟩; its propositionhood certificate is isOfHLevelLift 1 ⟨ P ⟩isProp. Applying lem to this pair decides the lifted copy of P.

The two panels below show how to turn that decision into Dec ⟨ P ⟩. The positive branch uses lower; the negative branch assumes a proof of P and refutes its lifted image. The function mapDec assembles these conversions.

lowerLEM {ℓ} lem P =
  mapDec lower (λ np p → np (lift p))
    (lem (Lift ⟨ P ⟩ , isOfHLevelLift 1 ⟨ P ⟩isProp))
$$\operatorname{yes}\,\hat x$$
$\operatorname{Lift}\langle P\rangle$ $\hat x$ $\operatorname{lower}$ $\langle P\rangle$ $\operatorname{lower}\,\hat x$
$$\operatorname{yes}\,(\operatorname{lower}\,\hat x)$$
$$\operatorname{no}\,\mathit{np}$$
$\operatorname{Lift}\langle P\rangle$ $\operatorname{lift}\,p$ $\operatorname{lift}$ $\langle P\rangle$ $p$
$$\mathit{np}\,(\operatorname{lift}\,p):\bot_0$$

A positive decision sends its proof downward by lower. A negative decision refutes a hypothetical p : ⟨ P ⟩ by sending it upward with lift and applying np

Ω-resizing from excluded middle

Once every proposition at the source level can be decided, each can be represented by one of two Boolean labels. For arbitrary levels ℓ₁ and ℓ₂, ΩResizing ℓ₁ ℓ₂ asks for one type in Type ℓ₂ equivalent to the entire type hProp ℓ₁. This chapter constructs such a classifier from excluded middle at ℓ₁. The general theorem ΩResizing→Resizing then turns this small presentation of the proposition universe into Resizing ℓ₁ ℓ₂: every source-level proposition receives an equivalent representative at the target level.

The classifier uses the previously introduced type Bool, whose two constructors true and false serve as its labels.

The labels are codes, not themselves propositions in hProp ℓ₁. Since Bool lies in Type ℓ-zero, the code type is lifted to Lift {ℓ-zero} {ℓ₂} Bool in the target universe Type ℓ₂. Its two labels will represent ⊤ and ⊥, both available in hProp ℓ₁ at every level. Constructing an equivalence between this target-level code type and the proposition universe will therefore give the required Ω-resizing.

The construction has two stages. First we define encoding from an explicit decision Dec ⟨ P ⟩, then decoding, and finally the two round-trip laws. We collect these four auxiliary results in the private module BooleanCodes; none uses excluded middle. The public theorem then invokes excluded middle to supply a decision for every P and assembles the four results into the equivalence.

private module BooleanCodes where

Lemma (encodeB) There is an encoding operation that takes a proposition P together with its decision and returns a code in Lift {ℓ-zero} {ℓ₂} Bool.

encodeB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) → Dec ⟨ P ⟩ → Lift {ℓ-zero} {ℓ₂} Bool

Proof Inspect the supplied decision. The yes branch returns lift true, while the no branch returns lift false. Both branches discard the particular proof or refutation and retain only which outcome holds. Because the decision is supplied explicitly, encoding uses no excluded middle.

encodeB P (yes _) = lift true
encodeB P (no _)  = lift false

Lemma (decodeB) There is a decoding operation that takes a code in Lift {ℓ-zero} {ℓ₂} Bool and returns a proposition in hProp ℓ₁.

decodeB : ∀ {ℓ₁ ℓ₂} → Lift {ℓ-zero} {ℓ₂} Bool → hProp ℓ₁

Proof Inspect the supplied code. The lift true branch returns ⊤, while the lift false branch returns ⊥. Both branches discard the label and retain only the proposition it represents. Because the two cases are handled directly, decoding also uses no excluded middle.

decodeB (lift true)  = ⊤
decodeB (lift false) = ⊥

Lemma (secB) For every proposition P and decision d, encoding with encodeB and then decoding with decodeB recovers P in hProp: decodeB (encodeB P d) ≡ P.

secB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) (d : Dec ⟨ P ⟩)
     → decodeB {ℓ₁} {ℓ₂} (encodeB {ℓ₁} {ℓ₂} P d) ≡ P

Proof Split on d. If d = yes p, encoding selects lift true and decoding returns ⊤, so the goal becomes ⊤ ≡ P. Propositional extensionality ⇔toPath constructs this path from the map returning p and the map returning tt*. If d = no np, encoding selects lift false and decoding returns ⊥, so the goal becomes ⊥ ≡ P. Its two maps are the absurd function λ () and the refutation np followed by elimination from ⊥₀. Thus decoding after encoding recovers a proposition equal to P in both cases.

secB {ℓ₁} {ℓ₂} P (yes p) = ⇔toPath (λ _ → p) (λ _ → tt*)
secB {ℓ₁} {ℓ₂} P (no np) = ⇔toPath (λ ()) (λ p → ⊥₀-rec (np p))

Lemma (retrB) For every code b̂ and decision d of the proposition it decodes to, decoding with decodeB and then encoding with encodeB recovers b̂: encodeB (decodeB b̂) d ≡ b̂.

retrB : ∀ {ℓ₁ ℓ₂} (b̂ : Lift {ℓ-zero} {ℓ₂} Bool)
        (d : Dec ⟨ decodeB {ℓ₁} {ℓ₂} b̂ ⟩)
      → encodeB {ℓ₁} {ℓ₂} (decodeB {ℓ₁} {ℓ₂} b̂) d ≡ b̂

Proof Split on b̂ and then on d, giving four cases. If b̂ = lift true, decoding returns ⊤. A proof selects lift true again, so the equality is refl; a refutation is impossible because applying it to tt* produces an element of ⊥₀. If b̂ = lift false, decoding returns ⊥. A proof is impossible by the empty pattern (); a refutation selects lift false again, so the equality is refl. Thus encoding after decoding recovers the original code in every possible case.

retrB {ℓ₁} {ℓ₂} (lift true)  (yes _)  = refl
retrB {ℓ₁} {ℓ₂} (lift true)  (no n⊤) = ⊥₀-rec (n⊤ tt*)
retrB {ℓ₁} {ℓ₂} (lift false) (yes ())
retrB {ℓ₁} {ℓ₂} (lift false) (no _)  = refl

The two round-trip laws show that encoding and decoding become mutually inverse once a decision is supplied uniformly for every proposition. The resulting classifier will therefore be a genuine type equivalence, not merely a surjective labelling of propositions by two truth values.

The candidate witness is the pair (Lift Bool , ...). Its first component lies in Type ℓ₂, and its second will be an equivalence hProp ℓ₁ ≃ Lift Bool. No ordering between ℓ₁ and ℓ₂ is required. The downward instance used later takes ℓ₁ = ℓ-suc ℓ and ℓ₂ = ℓ, but equal or higher target levels are allowed as well. Excluded middle has only one remaining role: it supplies the decisions used by the encoder uniformly; all four private results above are constructive.

Theorem (LEM→ΩResizing) For arbitrary levels ℓ₁ and ℓ₂, excluded middle at the source level ℓ₁ implies Ω-resizing from ℓ₁ to ℓ₂.

LEM→ΩResizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → ΩResizing ℓ₁ ℓ₂

Proof Choose Lift Bool as the first component. For the second, use isoToEquiv to turn the following isomorphism into an equivalence. Its forward map sends P to encodeB P (lem P), and its backward map is decodeB. The round-trip laws are retrB and secB, each instantiated with the decision supplied by lem. These two components form the required witness of ΩResizing ℓ₁ ℓ₂.

LEM→ΩResizing lem = Lift Bool , isoToEquiv (iso
  (λ P → encodeB P (lem P)) decodeB
  (λ b → retrB {ℓ₁ = _} b (lem (decodeB b)))
  (λ P → secB {ℓ₂ = _} P (lem P)))
  where open BooleanCodes

The two round-trip laws close the two triangles in the figure below. Fix lem : LEM ℓ₁, abbreviate the code type Lift {ℓ-zero} {ℓ₂} Bool by $B$, and write $E(P) := \operatorname{encodeB}\,P\,(\operatorname{lem}\,P)$ and $D := \operatorname{decodeB}$. Each round trip returns a point connected to its starting point by the indicated path.

$B$ $E(P)$ $\operatorname{hProp}\,\ell_1$ $P$ $D(E(P))$ $E$ $D$ $\operatorname{secB}$
$\operatorname{hProp}\,\ell_1$ $D(b)$ $B$ $b$ $E(D(b))$ $D$ $E$ $\operatorname{retrB}$

Encoding and decoding are inverse up to paths. Excluded middle supplies the decisions in $E$; with explicit decisions, encoding, decoding and both round-trip laws are constructive

Corollary (LEM→Resizing) For arbitrary levels ℓ₁ and ℓ₂, excluded middle at the source level ℓ₁ implies propositional resizing from ℓ₁ to ℓ₂.

Proof Apply LEM→ΩResizing, then convert the resulting proposition-universe resizing with the general theorem ΩResizing→Resizing.

LEM→Resizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → Resizing ℓ₁ ℓ₂
LEM→Resizing lem = ΩResizing→Resizing (LEM→ΩResizing lem)

Recap

This chapter stated excluded middle level by level as LEM ℓ, proved that it is itself a proposition, and used lowerLEM to obtain the instance immediately below a successor level. From LEM ℓ₁, LEM→ΩResizing constructs ΩResizing ℓ₁ ℓ₂ at any target level ℓ₂; composing this result with ΩResizing→Resizing gives Resizing ℓ₁ ℓ₂. Thus one source-level assumption of excluded middle resolves both size questions posed at the beginning of the chapter.