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.

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

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.

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.

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 ℓ).

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.

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.

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.

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.

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.

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

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.

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.

  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.

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.

  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.

  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.

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.

  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.

      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.

  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.

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.

  ϕₛ : 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.

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

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.

  Δ₀-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.

    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.

    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.

open Δ₀Small id
open SemanticsV.At S id using ( _⊨_ )

separateΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
           → Σ[ 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.

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

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.

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.

  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.

  ⊨ᵐ-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 ℓ).

  ⊨ᵐ-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.

  ⊨ᵐ-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.

    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.

      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.