--- title: "Small truth values in the cumulative hierarchy" module: V.Smallness lang: en site: "Bedrock" description: "Small truth values in the cumulative hierarchy" stage: "The ambient hierarchy" reading_order: 21 canonical: https://bedrock.institute/en/V.Smallness.html html: V.Smallness.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Smallness.lagda.md prerequisites: [Base.Prelude, Base.Impredicativity, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy] routes: [ambient-model] translations: [https://bedrock.institute/zh/V.Smallness.md, https://bedrock.institute/ja/V.Smallness.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Small truth values in the cumulative hierarchy Work over the cumulative hierarchy `V ℓ` produces many statements of the form `x ∈ˢ a` or `a ≈ˢ b`: propositions packaged as elements of `hProp (ℓ-suc ℓ)`, one universe above the level `ℓ` at which the sets themselves are indexed. Such upper-universe propositions are inconvenient: constructions that expect data at level `ℓ`, among them the library's separation set, cannot accept them. A proposition `P : hProp (ℓ-suc ℓ)` is therefore called **small** when it is equivalent, as a type of proofs, to some proposition `Q : hProp ℓ` in the lower universe. Smallness is not a reduction of `P` itself; it is a certificate that another, lower proposition says exactly the same thing. This chapter lowers large truth values to small ones in stages. The atomic membership and equality relations of `V` are small outright, because each set comes with a small index type presenting its members. Smallness then propagates through every connective and through bounded quantifiers, whose range is exactly such an index type. For unbounded quantifiers, this chapter proves preservation when the range itself is essentially small, that is, equivalent to a type at level `ℓ`. The two payoffs are separation for Δ₀ formulas with no propositional resizing, and smallness of every formula's truth value inside a restricted structure whose carrier is essentially small. Everything in this chapter takes place at one fixed universe level `ℓ`, fixed once and for all by the module parameter. The ambient object is the cumulative hierarchy `V ℓ` from the chapter V.Hierarchy, whose sets are images of `Type ℓ`-indexed families. The one definition that organizes everything is `isSmall`: for `P : hProp (ℓ-suc ℓ)`, an inhabitant of `isSmall P` is a pair consisting of a lower-universe proposition `Q : hProp ℓ` and an equivalence of underlying types `⟨ P ⟩ ≃ ⟨ Q ⟩`. The chapter's task is to manufacture such pairs. Its setting is the `ZFStructure` record, which packages a carrier with truth-valued equality and membership relations; the restriction `_↾_` of such a record to a class is used in the final section. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module V.Smallness {ℓ : Level} where open import Base.Impredicativity using ( isSmall ) ``` The statements to be lowered live in a formal first-order language. Its relation symbols are `_∈̇_` and `_≐_` for membership and equality; its connectives combine formulas; and it has both bounded quantifiers `∀̇∈` and `∃̇∈` and unbounded quantifiers `∀̇` and `∃̇_`. The `Δ₀` fragment classifies formulas within the Lévy hierarchy. `Δ₀` is not a predicate on formulas but an inductive witness that a formula is built from atoms using connectives and bounded quantifiers only. Crucially there is no constructor for unbounded quantification: a formula containing `∀̇` or `∃̇_` simply cannot carry a Δ₀ witness, and the Δ₀ theorem of this chapter relies on exactly that absence. ```agda open import FOL.ZFStructure using ( ZFStructure; _↾_ ) open import FOL.Syntax using ( Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ) ``` A formula's meaning is given by the semantics module, instantiated here at the structure `𝒮ᵥ` from V.Hierarchy: the cumulative hierarchy equipped as a structure whose relations take values in `hProp (ℓ-suc ℓ)`. So the truth values this chapter studies are exactly propositions one universe up, the kind `isSmall` speaks about. The proofs all rest on a small toolkit for equivalences: the type `_≃_` with its evaluation `equivFun` and preimages `invEq`, `equivΠ` for lifting equivalences through function types, and `propBiimpl→Equiv`, which turns two proofs of propositionhood and a bi-implication into an equivalence. Since both sides of the equivalences below are propositions, this last constructor carries most of the weight. ```agda import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import Cubical.Foundations.Equiv using ( _≃_; equivFun; invEq; invEquiv; equivΠ; propBiimpl→Equiv ) import Cubical.Functions.Logic as Logic ``` Closing smallness under the connectives needs proposition operations at the lower level `ℓ`, the target universe of every compression. They remain under the qualified name `Logic`, so `Logic.⊓` and its siblings visibly act on `hProp ℓ`, while the unqualified operations used below act on `hProp (ℓ-suc ℓ)`. The remaining pieces support specific equivalence constructions: `Σ-cong-equiv` builds an equivalence of pair types from componentwise equivalences, `Sum.⊎-equiv` handles coproducts, `tt*` is the unit element, and the propositional truncation module `PT` provides a map operation that transports merely-exists statements along a function without ever choosing a witness. ```agda open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Data.Sigma using ( Σ-cong-equiv ) import Cubical.Data.Sum as Sum open import Cubical.Data.Unit using ( tt* ) import Cubical.HITs.PropositionalTruncation as PT ``` The hierarchy itself supplies the atomic data. Each set `a` comes with a monic presentation: a small index type `⟪ a ⟫` with an embedding `⟪ a ⟫↪` into `V ℓ`. Membership in a set therefore has a small twin `_∈ₛ_`, defined as the type of pairs `(m : ⟪ b ⟫, ⟪ b ⟫↪ m ∼ a)`, which lives in `hProp ℓ`; the conversion `∈∈ₛ` links the two memberships in both directions, and `identityPrinciple` identifies bisimilarity `∼` with actual paths. The operation `∈-asFiber` turns an (untruncated) membership into an actual fiber of the embedding. `SeparationSet` is the library's separation construction, which only accepts predicates already valued in the lower universe. The unqualified connectives `⊓ ⊔ ⇒ ¬ ⊤ ⊥` and quantifiers `∀[ x ] P x` and `∃[ x ] P x` act directly on `hProp (ℓ-suc ℓ)`. ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∼_; identityPrinciple; _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module SeparationSet ) ``` The structure record is instantiated at `𝒮ᵥ`, and from this point the names `S`, `_≈ˢ_` and `_∈ˢ_` refer to its carrier and relations. Concretely `S` is `V ℓ`. A statement about members of the structure is thus a proposition one universe up, which is precisely the kind of statement this chapter spends its effort on proving small. ```agda open ZFStructure 𝒮ᵥ ``` ## Being small A proposition `P : hProp (ℓ-suc ℓ)` is small, written `isSmall P`, when it comes with a lower-universe proposition `Q : hProp ℓ` and an equivalence `⟨ P ⟩ ≃ ⟨ Q ⟩`. The definition was introduced in `Base.Impredicativity`, where the resizing interface asserts smallness of every proposition at once. This chapter assumes no such interface. It earns smallness for individual propositions, beginning with the two atomic relations of the structure, and the rest of the chapter passes these witnesses through connectives and quantifiers. Why should the atoms be small at all? Because of how a set in `V ℓ` is built: as the image of a family indexed by some `⟪ a ⟫ : Type ℓ`. To say `x` is a member of `a` is to say some index presents a member equal to `x`, and that statement quantifies over a small type. Membership therefore has a small twin `a ∈ₛ b`, and `∈∈ₛ` converts between the two relations in both directions. Equality likewise compresses to bisimilarity `a ∼ b` via the identity principle. The first lemma packages the small membership relation as a smallness witness. To show `isSmall (a ∈ˢ b)` we must exhibit a lower-universe proposition with an equivalence to `⟨ a ∈ˢ b ⟩`; the witness is `a ∈ₛ b`, and since both underlying types are propositions, `propBiimpl→Equiv` builds the equivalence from the two directions of `∈∈ₛ` alone. No content about `a` or `b` is used: whatever the sets are, membership between them is small. Note what the lemma does not say: it does not identify the two relations by a path, and it does not make `∈ˢ` itself land in the lower universe; it supplies a compressed equivalent. ```agda small-∈ : (a b : S) → isSmall (a ∈ˢ b) small-∈ a b = (a ∈ₛ b) , propBiimpl→Equiv (snd (a ∈ˢ b)) (snd (a ∈ₛ b)) (∈∈ₛ {a = a} {b = b} .fst) (∈∈ₛ {a = a} {b = b} .snd) small-≡ : (a b : S) → isSmall (a ≈ˢ b) ``` The equality atom follows the same pattern with a different small twin. The structure's equality `a ≈ˢ b` is compressed to bisimilarity `a ∼ b`, the statement that the two sets have the same members; the library's identity principle is an equivalence between `⟨ a ∼ b ⟩` and the path type `a ≡ b`, and `invEquiv` orients it in the direction required by `isSmall`, from the large equality type `⟨ a ≈ˢ b ⟩` to the lower-universe bisimilarity proposition. Together with `small-∈` this exhausts the atomic cases of the language. ```agda small-≡ a b = (a ∼ b) , invEquiv identityPrinciple ``` ## The connectives preserve smallness With the atoms in hand, the next question is whether smallness survives logical combination. It does: each of the four connectives and the two constants passes smallness witnesses through, and once this section is done, any truth value built from small atoms by connectives is small again. This is what later lets an induction over Δ₀ witnesses close off all the connective cases at once. Each proof takes two smallness witnesses `(P' , eP)` and `(Q' , eQ)`, where `eP : ⟨ P ⟩ ≃ ⟨ P' ⟩` and `eQ : ⟨ Q ⟩ ≃ ⟨ Q' ⟩`, and returns a smallness witness for the compound. The lower-universe component is built from `P'` and `Q'` by the corresponding `Logic` operation at level `ℓ`, and the equivalence component transports proofs of the compound along `eP` and `eQ`. Conjunction is the simplest case because the underlying type of `P ⊓ Q` is a pair `⟨ P ⟩ × ⟨ Q ⟩`. Pairing the two compressed propositions with `Logic.⊓`, whose underlying type is likewise a product, the equivalence is obtained by `Σ-cong-equiv` applied to `eP` and `eQ`: map a pair of proofs to the pair of its compressions. Nothing about propositions is needed beyond that each factor compresses. ```agda small⊓ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊓ Q) small⊓ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⊓ Q') , Σ-cong-equiv eP (λ _ → eQ) small⊔ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊔ Q) small⊔ {P} {Q} (P' , eP) (Q' , eQ) = ``` Disjunction and implication need one idea each. For disjunction, `⟨ P ⊔ Q ⟩` is the propositional truncation of the coproduct, so the compressed proposition `P' Logic.⊔ Q'` is again a truncation, and `PT.propTrunc≃` lifts the coproduct equivalence `Sum.⊎-equiv eP eQ` to the truncations. This is where truncation discipline shows: the map merely relabels which side holds, never inspects which side was chosen, because truncation provides no chosen side. For implication, `⟨ P ⇒ Q ⟩` is the function type `⟨ P ⟩ → ⟨ Q ⟩`; the compressed proposition `P' Logic.⇒ Q'` has the same shape at level `ℓ`, and `equivΠ` transports the equivalence through the function space pointwise. ```agda (P' Logic.⊔ Q') , PT.propTrunc≃ (Sum.⊎-equiv eP eQ) small⇒ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⇒ Q) small⇒ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⇒ Q') , equivΠ eP (λ _ → eQ) small¬ : {P : hProp (ℓ-suc ℓ)} → isSmall P → isSmall (¬ P) ``` Negation is the one case where the compressed proposition alone does not determine the equivalence, because negation is contravariant: a proof of `¬ P` consumes a proof of `P`. The compressed proposition is `Logic.¬ P'`, whose underlying type sends `⟨ P' ⟩` to the empty type. Both sides are propositions, so `propBiimpl→Equiv` applies, and the two directions use `eP` in opposite orientations: to contradict `np : ¬ P` from a compressed refutation `p'`, apply `np` to the preimage `invEq eP p'`; conversely, feed the image `equivFun eP p` of `p : ⟨ P ⟩` to `np'`. The evaluation and inverse of the equivalence appear with opposite variance exactly as the logic of negation demands. ```agda small¬ {P} (P' , eP) = (Logic.¬ P') , propBiimpl→Equiv (snd (¬ P)) (snd (Logic.¬ P')) (λ np p' → np (invEq eP p')) (λ np' p → np' (equivFun eP p)) small⊤ : isSmall ⊤ ``` The two constants close the section. Truth is small because both sides are inhabited propositions: the compressed proposition is `Logic.⊤`, and in each direction the function discards its argument and returns the unit element `tt*`. Falsity begins slightly differently: the truth value `⊥` was defined as the hProp pair `(⊥* , isProp⊥*)`, so its underlying type is the empty type `⊥*` itself, and the compressed proposition is that same empty type packaged as an hProp. Both functions are then defined by absurdity: an argument of an empty type admits no cases. ```agda small⊤ = Logic.⊤ , propBiimpl→Equiv (⊤ .snd) (snd (Logic.⊤ {ℓ})) (λ _ → tt*) (λ _ → tt*) small⊥ : isSmall (⊥ {ℓ = ℓ-suc ℓ}) small⊥ = (⊥* , isProp⊥*) , ``` The absurd case analysis `(λ ())` in each direction is the whole content of the falsity proof: `⊥*` has no constructors, so a function out of it requires no defining clauses. This is the first appearance of a theme that returns with force in the Δ₀ section: absence of constructors does real logical work. ```agda propBiimpl→Equiv isProp⊥* isProp⊥* (λ ()) (λ ()) ``` ## Bounded quantifiers preserve smallness The connectives suffice only for quantifier-free truth values, and one bounded quantifier in a formula would already break the induction of the next section. This section removes that obstacle. A quantifier over all of `V ℓ` ranges over the large carrier `S : Type (ℓ-suc ℓ)`, so the constructions used here do not by themselves compress its truth value. A quantifier **bounded by a set `a`** ranges, semantically, only over the members of `a`, and those members are presented by a small index type: the monic presentation gives `a` as `sett ⟪ a ⟫ ⟪ a ⟫↪` with `⟪ a ⟫ : Type ℓ`. Quantifying over `⟪ a ⟫` instead therefore produces a truth value built from the small propositions `sm (⟪ a ⟫↪ m)` by a Π or a truncated Σ, and both compress. The bridge between the two quantifications is `∈-asFiber`: from an inhabitant of `x ∈ᵗ a` it returns an actual fiber of `⟪ a ⟫↪` over `x`, a pair of an index `m` with a path `⟪ a ⟫↪ m ≡ x`. The fiber is **untruncated**, because `⟪ a ⟫↪` is an embedding, so passing from a member of `a` back to an index of `⟪ a ⟫` is a function, not a choice. This is what lets the backward directions of both lemmas proceed without any selection. The universal bounded quantifier states: for every member `x` of `a`, the proposition `B x` holds. Its truth value is `∀[ x ] (x ∈ˢ a) ⇒ B x`, an implication indexed over the whole carrier, where the antecedent `x ∈ˢ a` restricts attention to members. The lemma assumes each `B x` small, with witness `sm x = (B' x , e x)`, and concludes the whole universal statement small. The compressed proposition replaces membership with its small twin and the carrier with `⟪ a ⟫`: it asserts that for every index `m : ⟪ a ⟫`, the proposition `B' (⟪ a ⟫↪ m)` holds. The bound `a` enters as an explicit parameter, while the family `B` stays implicit, fixed by the goal type. ```agda small-∀∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)} → (∀ x → isSmall (B x)) → isSmall (∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x) small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd where ``` The forward direction converts a proof of the original statement into a proof of the compressed one. Given `f` assigning to each `x` an implication from `x ∈ˢ a` to `B x`, we must produce, for each index `m`, a proof of `B' (⟪ a ⟫↪ m)`. First apply `f` at the member `⟪ a ⟫↪ m`; this needs the antecedent, namely a proof that `⟪ a ⟫↪ m` is a member of `a`, which the conversion `∈∈ₛ` produces from the canonical witness `∈ₛ⟪ a ⟫↪ m`, itself just the pair of the index with the reflexivity of `∼`. The resulting proof of `B (⟪ a ⟫↪ m)` is then pushed through the equivalence `e` to land in the compressed proposition. ```agda big = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x Qsm = ∀[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst fwd : ⟨ big ⟩ → ⟨ Qsm ⟩ fwd f m = equivFun (sm (⟪ a ⟫↪ m) .snd) (f (⟪ a ⟫↪ m) (∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m))) ``` The backward direction is where the embedding earns its keep. Given `g`, a function assigning to each index `m` a proof of `B' (⟪ a ⟫↪ m)`, we must produce, for each `x` with `x∈a : x ∈ᵗ a`, a proof of `B x`. The fiber `mf = ∈-asFiber x∈a` supplies an index `mf .fst` with a path `mf .snd : ⟪ a ⟫↪ (mf .fst) ≡ x`. Applying `g` at that index yields a proof of `B' (⟪ a ⟫↪ (mf .fst))`, which the inverse equivalence sends to `B (⟪ a ⟫↪ (mf .fst))`; the `subst` then transports it along `mf .snd` to `B x`. Note that the path, not an arbitrary choice among members, does the adjusting: had the fiber been truncated, this transport would be unavailable and the lemma would fail without extra assumptions. ```agda bwd : ⟨ Qsm ⟩ → ⟨ big ⟩ bwd g x x∈a = subst (λ v → ⟨ B v ⟩) (mf .snd) (invEq (sm (⟪ a ⟫↪ (mf .fst)) .snd) (g (mf .fst))) where mf = ∈-asFiber {a = x} {b = a} x∈a ``` The existential bounded quantifier states: some member `x` of `a` has `B x`. Its truth value is `∃[ x ] (x ∈ˢ a) ⊓ B x`, a truncated pairing of membership with `B`, and the compressed proposition asserts, merely, some index `m : ⟪ a ⟫` with `B' (⟪ a ⟫↪ m)`. The hypothesis and conclusion mirror the universal case, but the proofs differ in kind: because both sides are truncated existentials, neither direction returns a function; each maps truncations to truncations. ```agda small-∃∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)} → (∀ x → isSmall (B x)) → isSmall (∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x) small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd where ``` Forward: `PT.map` applies a pointwise construction inside the truncation, which is permitted because the target, the compressed proposition, is again a proposition. The pointwise step unpacks a truncated triple `(x , x∈a , bx)` of a member, its membership evidence, and a proof of `B x`; this unpacking is legitimate only because it happens under the truncation, where the choice of `x` need never be exported. The fiber of `x∈a` then yields an index, and the proof `bx` is transported along the fiber's path, in the direction `sym (mf .snd)`, before the equivalence compresses it. Compare this with the universal forward direction: there a function was in hand outright, here one merely knows that such data exists. ```agda big = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x Qsm = ∃[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst fwd : ⟨ big ⟩ → ⟨ Qsm ⟩ fwd = PT.map λ where (x , x∈a , bx) → ``` Backward: again under `PT.map`, a truncated pair `(m , q)` of an index and a proof of `B' (⟪ a ⟫↪ m)` is turned into a member of `a` with property `B`. The member is `⟪ a ⟫↪ m`, its membership evidence comes from `∈∈ₛ` applied to the canonical witness, and the property proof is the preimage `invEq (sm _ .snd) q`. Here no transport is needed at all: the index is given from the start, so nothing has to be recovered. The asymmetry between the two directions is exactly the asymmetry of data: one side holds an index outright, the other must manufacture one from a member, and only the embedding makes that manufacturing a function. ```agda let mf = ∈-asFiber {a = x} {b = a} x∈a in mf .fst , equivFun (sm (⟪ a ⟫↪ (mf .fst)) .snd) (subst (λ v → ⟨ B v ⟩) (sym (mf .snd)) bx) bwd : ⟨ Qsm ⟩ → ⟨ big ⟩ ``` With this pair of lemmas the bounded quantifier clauses of the semantics are covered, and the induction of the next section can pass through any formula whose quantifiers are all bounded. Worth noting is what was not used: no classical principle, no choice, and no resizing entered either proof. The only substantive facts were the monic presentation of membership and the property that `⟪ a ⟫↪` is an embedding. ```agda bwd = PT.map λ where (m , q) → ⟪ a ⟫↪ m , ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m) , invEq (sm (⟪ a ⟫↪ m) .snd) q ``` ## From smallness to separation This section is where smallness pays off. The library's separation construction `SeparationSet` builds, for a set `a` and a predicate `ϕ : V ℓ → hProp ℓ` valued in the **lower** universe, a set whose members are exactly the members of `a` satisfying `ϕ`. Such a construction is impossible for upper-universe predicates, since its internal index type would have to live at level `ℓ`. The lemma below is the adapter: given a predicate `P` on `S` with a smallness witness at every point, it produces a set `s` in the structure together with the membership specification `y ∈ˢ s` if and only if `y ∈ˢ a` and `P y`, stated as paths in the style of the model record's separation field. This is also where the pieces assemble into a plan. Whatever first supplies smallness of a predicate, whether the bounded quantifiers of the last section or the essentially small worlds of the last, this lemma converts the small predicate into a set, once and in the same way. The statement deserves a close reading. The result is a dependent pair: a set `s` of the structure, and for every `y` a **path** `(y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y)` in the type `hProp (ℓ-suc ℓ)`, not merely a bi-implication between the underlying propositions. This matches the shape of the separation field in the model record, so the construction can be transplanted into any structure that must verify the separation axiom. The proof applies the library construction to `a` and to the compressed predicate, and assembles the required paths from the two directions of the resulting specification. ```agda separateFromSmall : (a : S) (P : S → hProp (ℓ-suc ℓ)) → (∀ y → isSmall (P y)) → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y)) separateFromSmall a P sm = Sep.SEPAREE , λ y → ⇔toPath (fwd y) (bwd y) where ``` The compressed predicate is assembled first: `ϕₛ y` is by definition the lower-universe stand-in `sm y .fst` extracted from the pointwise smallness witness. The library module `Sep` is then instantiated at `a` and `ϕₛ`, and its resulting set is named `Sep.SEPAREE`. This is the only place in the chapter where the library's separation runs; anything else this part separates goes through this lemma. ```agda ϕₛ : S → hProp ℓ ϕₛ y = sm y .fst module Sep = SeparationSet a ϕₛ fwd : ∀ y → ⟨ y ∈ˢ Sep.SEPAREE ⟩ → ⟨ (y ∈ˢ a) ⊓ P y ⟩ fwd y y∈s = ∈∈ₛ {a = y} {b = a} .snd (Sep.separation-ax y .fst y∈ₛs .fst) ``` Both directions translate between the structure membership `y ∈ˢ Sep.SEPAREE` and the pair `y ∈ˢ a` plus `P y`. Forward: convert `y∈s` through `∈∈ₛ` into the small membership, feed it to the library's specification `separation-ax y` in its forward direction, and obtain the pair of `y ∈ₛ a` and the compressed property; the first component converts back to `y ∈ᵗ a` via `∈∈ₛ` in the other orientation, and the second is expanded through the inverse of the equivalence `e`. Backward is the mirror image: convert membership in `a` to its small form, compress the property proof with `equivFun`, and let `separation-ax y` in its backward direction produce membership in `Sep.SEPAREE`, converted once more through `∈∈ₛ`. The library specification does the set-theoretic work; the equivalences do the universe bookkeeping. ```agda , invEq (sm y .snd) (Sep.separation-ax y .fst y∈ₛs .snd) where y∈ₛs = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .fst y∈s bwd : ∀ y → ⟨ (y ∈ˢ a) ⊓ P y ⟩ → ⟨ y ∈ˢ Sep.SEPAREE ⟩ bwd y yp = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .snd (Sep.separation-ax y .snd (∈∈ₛ {a = y} {b = a} .fst (yp .fst) , equivFun (sm y .snd) (yp .snd))) ``` ## Δ₀ formulas evaluate small The previous sections built a stock of smallness witnesses: two atoms, four connectives, two constants, and two bounded quantifiers. This section converts the stock into a theorem by induction over the `Δ₀` witness itself. Recall from the chapter on the Lévy hierarchy that `Δ₀` is an inductive witness, one per formula, whose constructors certify that the formula is built from atoms by connectives and bounded quantifiers only. The theorem states that any formula carrying such a witness has a small truth value at every environment. Since the witness is defined inductively, the proof is an induction with one case per constructor, and each case is exactly one of the stock lemmas. The case analysis has an instructive omission: there are no cases for the unbounded quantifiers `∀̇` and `∃̇_`, because the witness type has no constructors for them. Absence of constructors is what makes the classification; a formula with an unbounded quantifier simply cannot carry a Δ₀ witness, so the induction never needs to face it. The Lévy hierarchy thus functions as an accounting of universe cost: Δ₀ is exactly the fragment whose truth values come without it. The setup instantiates the semantics once and for all: `SemanticsV` is the satisfaction relation over `𝒮ᵥ` with truth values in `hProp (ℓ-suc ℓ)`, so a formula's truth value is exactly a proposition of the kind the whole chapter has been compressing. The environment type `S ^ n` is the length-`n` vector notation. The module is parameterized by a constant interpretation `ι : K → S`, so the theorem holds for any choice of constants; the canonical case `ι` the identity is taken at the end of the chapter. Inside, `open SemanticsV.At K ι` brings the term evaluation `⟦_⟧` and satisfaction `_⊨_` into scope. The goal type deserves attention: `Δ₀-small` is a function from a Δ₀ witness to, for each environment `γ`, a smallness witness of `γ ⊨ φ`. The induction is over the witness, with the formula and environment universally quantified around it. ```agda module SemanticsV = FOL.Semantics 𝒮ᵥ open SemanticsV using ( _^_ ) module Δ₀Small {ℓc} {K : Type ℓc} (ι : K → S) where open SemanticsV.At K ι Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : S ^ n) → isSmall (γ ⊨ φ) ``` The atom cases invoke the first two stock lemmas directly, after evaluating the two terms in the environment `γ`: membership becomes `small-∈` applied to the values of `t` and `u`, equality becomes `small-≡`. The three binary connective cases are equally direct: the induction hypotheses `Δ₀-small c γ` and `Δ₀-small d γ` are smallness witnesses for the subformulas' truth values, and the closure lemma of the corresponding connective combines them. The explicit instantiation `{P = γ ⊨ φ}` merely records which propositions the witnesses compress; Agda could infer them, but writing them out documents the shape of the case. ```agda Δ₀-small (δ-∈ {t = t} {u}) γ = small-∈ (⟦ t ⟧ γ) (⟦ u ⟧ γ) Δ₀-small (δ-≐ {t = t} {u}) γ = small-≡ (⟦ t ⟧ γ) (⟦ u ⟧ γ) Δ₀-small (δ-∧ {φ = φ} {ψ} c d) γ = small⊓ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ) Δ₀-small (δ-∨ {φ = φ} {ψ} c d) γ = ``` The remaining connective-shaped case is falsity, and then the two bounded quantifiers. Falsity needs no environment at all: the witness `δ-⊥` carries no subformulas, and the case is just `small⊥`. The bounded quantifier cases are the interesting ones. For `δ-∀∈`, the formula is `∀̇∈ t φ`, whose truth value is `∀[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ φ)`; this is precisely the shape that `small-∀∈` consumes, with `a` the value of `t` and the family `B x` the truth value of the body at the extended environment `x ∷ γ`. The induction hypothesis is applied at the extended environment, which is legitimate because the witness `c` certifies the body `φ` itself. ```agda small⊔ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ) Δ₀-small (δ-⇒ {φ = φ} {ψ} c d) γ = small⇒ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ) Δ₀-small δ-⊥ γ = small⊥ Δ₀-small (δ-∀∈ {t = t} {φ = φ} c) γ = ``` The existential bounded case mirrors the universal one exactly, with `small-∃∈` in place of `small-∀∈` and the conjunction-shaped truth value `∃[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ)` matched against `small-∃∈`'s conclusion. This closes the induction: every constructor of the witness type has a case, every case is one stock lemma, and no case remains for the unbounded quantifiers. The theorem `Δ₀-small` is thus the point where the earlier sections stop being isolated facts and become a statement about the formal language. ```agda small-∀∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ)) Δ₀-small (δ-∃∈ {t = t} {φ = φ} c) γ = small-∃∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ)) ``` ## Δ₀ separation without resizing Compose the induction of the last section with the adapter of the section before it, and the chapter's central theorem appears. Take the canonical constant interpretation, in which the constants of the language are the sets of the structure themselves and `ι` is the identity. Then a Δ₀ formula `φ` with one free variable defines a pointwise-small predicate on `S`, and `separateFromSmall` turns it into a set. The result is a full instance of the separation axiom schema restricted to Δ₀ formulas, proved with no resizing principle, no classical axiom, and no choice: the smallness is supplied by the induction, and the library construction does the rest. The model chapter still owes the unrestricted separation axiom; this theorem shows that the Δ₀ tier of the Lévy hierarchy needs nothing beyond the representation of `V`. The two opening lines fix the canonical interpretation: `Δ₀Small id` instantiates the induction at the identity, and the satisfaction relation for one free variable is re-exported as `_⊨_`. The theorem's type is the separation specification with `φ` in place of an arbitrary predicate: a set `s` such that, for every `y`, membership in `s` is equal, as truth values, to membership in `a` conjoined with `y` satisfying `φ` at the one-point environment `y ∷ []`. The proof is a single application of `separateFromSmall`, passing the predicate `λ y → (y ∷ []) ⊨ φ` together with its pointwise smallness, which is `Δ₀-small c` applied at every one-point environment. Nothing else intervenes: the Δ₀ witness `c` is consumed exactly once, by the induction. ```agda open Δ₀Small id open SemanticsV.At S id using ( _⊨_ ) separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ))) separateΔ₀ a φ c = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → Δ₀-small c (y ∷ [])) ``` ## Essentially small worlds The Δ₀ theorem prices every quantifier as if it ranged over all of `V ℓ`. This final register of smallness removes even that cost, by changing where the quantifier ranges. Suppose a type `A` at the upper level is equipped with an equivalence `e : X ≃ A` from a small type `X : Type ℓ`. Then quantification over `A` can be replaced, step by step, by quantification over `X`: each statement about an element `a` of `A` is read at its preimage `equivFun e m`. The bounded-quantifier lemmas are a related but distinct phenomenon: there the range was an index type presenting a set, with membership as the filter; here no boundedness hypothesis remains. Smallness is then carried not by the shape of the formula but by the shape of the world it is spoken in. Note the direction of the hypothesis: it asserts that the equivalence `e` from `X` onto `A` exists; `A` itself still lives at the upper level. The universal version first. The statement `∀[ x ] P x B` quantifies over all of `A`; the compressed proposition quantifies instead over `X`, asserting that for every `m : X` the compressed proposition `sm (equivFun e m) .fst` holds. Since `e` is an equivalence, quantifying over `X` or over `A` gives equivalent dependent function types. The equivalence component transports a family of proofs `f : ∀ m → ⟨ sm (e m) ⟩` to `∀ a → ⟨ B a ⟩` by `equivΠ`, composed with each pointwise equivalence, and `invEquiv` orients the composite from the small Π to the large one, as the goal type demands. Note the contrast with `small-∀∈`: there the antecedent `x ∈ˢ a` did the filtering; here no antecedent exists, and the equivalence alone carries the reduction. ```agda small-∀ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)} → (∀ a → isSmall (B a)) → isSmall (∀[ a ∶ A ] B a) small-∀ {X = X} e sm = (∀[ m ∶ X ] sm (equivFun e m) .fst) , invEquiv (equivΠ e (λ m → invEquiv (sm (equivFun e m) .snd))) ``` The existential version follows the same plan with truncations in place of function types. The compressed proposition is the truncated Σ over `X` of the small witnesses; the equivalence is obtained from the truncated Σ over `A` of the large witnesses by `Σ-cong-equiv`, which changes the base of the pair from `A` to `X` along `e` and each fiber along the inverse pointwise equivalence, and `PT.propTrunc≃` then lifts the pair equivalence to the truncations. Again `invEquiv` supplies the required orientation. Together the two lemmas say: quantification over any essentially small type preserves smallness, and essentially small means, in the next block, equivalent to a type at level `ℓ`. ```agda small-∃ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)} → (∀ a → isSmall (B a)) → isSmall (∃[ a ∶ A ] B a) small-∃ {X = X} e sm = (∃[ m ∶ X ] sm (equivFun e m) .fst) , invEquiv (PT.propTrunc≃ (Σ-cong-equiv e (λ m → invEquiv (sm (equivFun e m) .snd)))) ``` The consequence: over an essentially small restricted structure, **every** formula evaluates small, no Δ₀ witness required. Fix a class `M` on the structure and suppose its restricted carrier is essentially small, in the precise form of an equivalence `e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))` with `X : Type ℓ`. Inside the structure `𝒮ᵥ ↾ M`, the quantifiers range over that restricted carrier, so the two lemmas of the last block apply to every quantifier, bounded or not, and the atoms reduce to `V`'s atomic smallness through the first projection. Boundedness is a syntactic restriction on a formula, whereas essential smallness is a property of the quantifier range. Once that hypothesis is available, the structural induction covers unbounded as well as bounded quantifiers. This smallness of inner satisfaction is what lets a definability step, such as the one the constructible hierarchy takes at each stage, operate with predicates at the lower universe. The module's parameters assemble the small world. `M` is a class on the carrier `S`, possibly proper: nothing restricts its size. The hypothesis is the pair of a small type `X : Type ℓ` and an equivalence from `X` onto the restricted carrier `Σ[ x ∈ S ] (x ∈ᶜ M)`; this is the exact sense in which the world is essentially small, and note that the burden rests on the equivalence existing, not on `M` being in any way bounded internally. The constants are interpreted in the restricted carrier by `ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)`, so every constant denotes a pair whose second component is evidence that its first component lies in `M`. ```agda module InnerSmall (M : S → hProp (ℓ-suc ℓ)) (X : Type ℓ) (e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))) {ℓc} {K : Type ℓc} (ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)) where SM : Type (ℓ-suc ℓ) ``` Two abbreviations fix notation. `SM` names the restricted carrier itself, and `𝒮M` is the structure restricted to `M`, built by `_↾_`: its carrier is `SM`, its h-set certificate is inherited, and its two relations pull back along the first projection, so equality and membership inside the world are decided by the underlying sets of `V`. The semantics module is instantiated at `𝒮M`, and the satisfaction and term-evaluation notations are renamed with a superscript to mark that formulas are being read **inside** the world. The renaming is exported public, so other chapters can read restricted satisfaction under these names. ```agda SM = Σ[ x ∈ S ] (x ∈ᶜ M) 𝒮M : ZFStructure (ℓ-suc ℓ) 𝒮M = 𝒮ᵥ ↾ M module SemanticsM = FOL.Semantics 𝒮M open SemanticsM.At K ι renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) public ``` The theorem's statement is deliberately parallel to `Δ₀-small`: for every formula `φ` of any arity `n` and every environment `δ : SM ^ n` of restricted elements, the truth value `δ ⊨ᵐ φ` is small. There is no inductive witness in sight, because none is needed: the induction here is on the formula itself, and the essential smallness of the carrier replaces the Δ₀ restriction. The two atom cases evaluate the terms inside the world, obtaining restricted elements, and apply the atomic smallness lemmas to their first projections: the world's membership `(fst xm) ∈ˢ (fst ym)` is exactly a proposition of the ambient structure, already known small. ```agda ⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : SM ^ n) → isSmall (δ ⊨ᵐ φ) ⊨ᵐ-small (t ∈̇ u) δ = small-∈ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) ⊨ᵐ-small (t ≐ u) δ = small-≡ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ)) ⊨ᵐ-small (φ ∧̇ ψ) δ = small⊓ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ) ``` The three binary connectives and falsity pass through exactly as before: the closure lemmas `small⊓`, `small⊔`, `small⇒` and the constant `small⊥` are level-generic in the propositions they consume, so they apply unchanged to truth values read inside the world. This reuse is the point of having isolated them in the earlier section: nothing about those proofs mentioned `V` specifically, only `hProp (ℓ-suc ℓ)`. ```agda ⊨ᵐ-small (φ ∨̇ ψ) δ = small⊔ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ) ⊨ᵐ-small (φ ⇒̇ ψ) δ = small⇒ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ) ⊨ᵐ-small ⊥̇ δ = small⊥ ``` Now the quantifiers, where the two world lemmas enter. The unbounded existential `∃̇ φ` has truth value `∃[ xm ] (xm ∷ δ) ⊨ᵐ φ` over the restricted carrier, and the induction hypothesis supplies smallness of each fiber `(xm ∷ δ) ⊨ᵐ φ`. This is precisely the shape of `small-∃`, with `A` the restricted carrier and `e` its smallness equivalence, so the case closes by direct application. The universal case is the mirror image with `small-∀`. Note how the quantification is genuinely over the restricted world: an element of `SM` is a pair, so the extended environment `xm ∷ δ` extends by whole restricted elements, and the body is read at them. ```agda ⊨ᵐ-small (∃̇ φ) δ = small-∃ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ)) ⊨ᵐ-small (∀̇ φ) δ = small-∀ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ)) ⊨ᵐ-small (∀̇∈ t φ) δ = ``` The bounded quantifiers combine the two sources of smallness in one case each. For `∀̇∈ t φ`, the truth value is an implication, bounded over the restricted carrier: `∀[ xm ] (fst xm ∈ˢ ⟦ t ⟧ᵐ δ) ⇒ ((xm ∷ δ) ⊨ᵐ φ)`. Smallness of the antecedent comes from the atomic lemma, smallness of the consequent from the induction hypothesis, and `small⇒` assembles the implication; the whole statement is then small by `small-∀` along `e`. The interesting detail is the first projection `fst xm`: boundedness is a statement about the underlying set of the restricted element, since the membership relation of the world is the pullback of `V`'s. ```agda small-∀ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⇒ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm → small⇒ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ} (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ))) ⊨ᵐ-small (∃̇∈ t φ) δ = small-∃ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⊓ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm → ``` The existential bounded case is the dual composition: the truth value pairs boundedness with the body under a truncated Σ, `small⊓` combines the two smallness witnesses, and `small-∃` moves the whole statement to the small index type. With this case the induction is complete, and the chapter's second headline result stands: inside an essentially small world, every formula, unbounded quantifiers included, has a small truth value. Where Δ₀-smallness was carried by the shape of the formula, essential smallness is carried by the range of the quantifiers; either way, once a small predicate is in hand, the separation of the previous section applies. ```agda small⊓ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ} (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ))) ``` ## Recap Smallness is equivalence to a proposition one universe down (`isSmall`). The atomic membership and equality of `V` compress through the library's monic presentation; the four connectives and two constants pass smallness witnesses through their corresponding lower-level operations; and the bounded quantifiers compress by quantifying over a set's small index type, using the untruncated fibers of the embedding. The adapter `separateFromSmall` converts any pointwise-small predicate into a set with the separation specification. The induction `Δ₀-small` then gives the Δ₀ tier of the Lévy hierarchy outright, and `separateΔ₀` turns it into Δ₀ separation with no propositional resizing, no classical axiom, and no choice. Formulas outside Δ₀ need more, and the model chapter supplies it under the name of propositional resizing. The final section added a second route: over a world whose carrier is essentially small, that is, equivalent to a type at level `ℓ`, every formula evaluates small, which is what lets a definability step work with lower-universe predicates.