Separation and replacement, bounded

Bounded separation asks for more than a host-level subtype of a constructible set a. It asks for an element of the constructible model whose members are exactly those x ∈ a satisfying a given Δ₀ formula. Bounded replacement asks for the corresponding set of values of a functional Δ₀ relation. The proof of both statements will move the relevant data into one ordinal stage, form a definable subset there, and compare that stage calculation with satisfaction in the whole constructible model.

{-# OPTIONS --cubical --safe --guardedness #-}

Two kinds of logic must remain separate from the outset. Formulas and their quantifiers belong to the object language interpreted by the model. The statement that a truth value is decidable belongs to the host theory. We assume excluded middle at the successor universe level; it enters through the operation that assigns a constructible set its least containing stage. This assumption is neither an axiom asserted inside L nor a choice principle.

open import Base.Prelude
open import Base.Classical using ( LEM )

We therefore fix a universe level ℓ and a host-level hypothesis lem : LEM (ℓ-suc ℓ). This parameter remains explicit in the type of every resulting theorem. The fixed-stage argument itself will use definability, transitivity, and Δ₀ absoluteness constructively; the classical dependency appears when arbitrary constants, the source set, or selected image values are assigned canonical least stage indices.

module L.Axioms.Separation {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The object language makes the first notion of boundedness precise. A formula φ : Formula S n may contain constants from the model carrier S and has n free-variable slots. A certificate Δ₀ φ says that every quantifier occurring in φ is bounded by a term. Membership atoms are Δ₀, conjunction preserves the property, and bounded existential quantification preserves it. These three closure facts make the separation and image formulas Δ₀.

open import FOL.ZFStructure using ( Transitive; module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∃∈ )

A different notion of boundedness controls constants. BoundedTm P t and BoundedFo P φ say that every constant occurring in a term or formula satisfies the host-level predicate P. They say nothing about whether the formula's quantifiers are bounded, so mkBoundedFo applies even to formulas that are not Δ₀. Relabelling uses such a certificate to replace each constant by an index in a chosen stage, and the mapping lemmas compare satisfaction before and after that syntactic change.

open import FOL.Manipulation.ConstantBounding
  using ( BoundedTm; BoundedFo; BoundedTm-mono; BoundedFo-mono; module Relabel )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Semantics

Why move constants into one stage? A stage Lset σ has a small presentation, so formulas defining its subsets use indices from that presentation as their constants. The original formula instead uses arbitrary elements of S as constants. Once those constants have been relabelled, DefOf (Lset σ) can form the subset selected by the formula inside the ambient cumulative hierarchy; the constructibility results can then package that subset as an element of the model. The remaining task is to prove that this stage-defined subset has the same members as the original formula specifies in L.

import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Constructible {ℓ}

The hierarchy supplies two scales of ordinal bounds. bound2 puts two stage indices inside a common ordinal, while boundingOrd does the same for a family indexed by a small type. Monotonicity then moves stage membership to the common bound. The operation stage assigns each constructible set the least stage index whose layer contains it; only this least-stage operation in this construction uses lem. At the other end, uniqueL uses the model's set extensionality to prove uniqueness from a pointwise membership specification.

  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans; Lset-mono
        ; 𝒟ₒ; 𝒟ₒ-intro; Lset→isL )
open import L.Ordinal {ℓ} using ( ∅-ord; boundingOrd; bound2 )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS; 𝒟ₒ→isL; uniqueL )

Several kinds of equality have different roles here. ⇔toPath applies proposition extensionality to turn two implications into a path between proposition-valued truth values. Σ≡Prop lifts equality of underlying sets to equality of model elements because constructibility certificates form a proposition. Set extensionality enters separately through uniqueL. Finally, propositional truncation records that a witness exists without retaining a chosen witness; its eliminator is used only when the target is again a proposition.

open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )

Small presentations connect model membership with the small index types needed by ordinal bounding and stage definability. For a cumulative-hierarchy set A, the type ⟪ A ⟫ indexes its represented members and ⟪ A ⟫↪ returns the set named by an index. Conversely, ∈-asFiber turns a membership proof x ∈ A into an index together with a path from its represented set to x. The construction uses that untruncated fibre data locally; no representative is extracted from propositional truncation.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

The proposition-valued structure on L has carrier S. An element x : S is a dependent pair consisting of an ambient set fst x and a proof snd x that this set is constructible. Thus S is the carrier type of the model, not a set called L; its equality and membership are read from the underlying sets and take values in hProp.

open hPropStructure 𝒮ʟ

The axioms ultimately ask this carrier to realize a host-level class Q : S → hProp (ℓ-suc ℓ). The type SetOf Q pairs a model element b with, for every x : S, a path (x ∈ˢ b) ≡ Q x. In separation, Q x will combine membership in the source with an object-language satisfaction judgment. For example, if the formula says that x belongs to a constant c, the desired extension is the intersection of a and c. The proof realizes this class by a set in L; it does not identify the class itself with an object-language formula or assume that the host theory's subtype already belongs to L.

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

The same object-language formula can now be read in two structures. The notation γ ⊨v φ denotes satisfaction in the ambient cumulative hierarchy at an environment of raw sets, while γ ⊨ φ denotes satisfaction in the structure whose carrier is S. Keeping these judgments distinct is essential: the fixed-stage construction first proves a statement about an ambiently defined subset, then uses absoluteness to recover the intended satisfaction judgment in the constructible model.

module SemV = FOL.Semantics 𝒮ᵥ
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )

The constructible class is transitive: a member of a constructible set is constructible. This is exactly enough for bounded quantifiers. An ambient witness lying in the interpretation of a constructible bounding term can be repackaged as an element of S, and an inner witness can be projected back to its underlying set. Induction on a Δ₀ formula therefore gives abs₀, a path between its ambient and inner truth values. This is Δ₀ absoluteness, not a claim that L or any stage is elementary for arbitrary formulas.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL using ( abs₀ ) renaming ( _⊨ᵐ_ to _⊨_ )

The replacement image

For replacement, first state the image as a host-level predicate. The truth value ReplImage a φ z says that there merely exists an x : S such that x ∈ˢ a and the object-language formula φ is satisfied at the environment x ∷ z ∷ []. Here the source occupies slot zero and the candidate value slot one. The indexed host-level existential uses propositional truncation, so it forgets which source produced z; it is distinct from the object-language bounded existential ∃̇∈ that defines the same image by a unary formula. Nothing in this definition requires φ to be Δ₀ or the relation to be functional.

ReplImage : (a : S) (φ : Formula S ) → S → hProp (ℓ-suc ℓ)
ReplImage a φ z = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((x ∷ z ∷ []) ⊨ φ)

Bounding a functional image

The extra problem in replacement is to find one stage containing every possible value. FunctionalImage treats an arbitrary host-level relation R and assumes that for each x ∈ˢ a the fibre Σ[ y ∈ S ] ⟨ R x y ⟩ is contractible. Thus the fibre contains a specified centre and every other related pair is equal to it. This hypothesis supplies existence and uniqueness as data at each source; projecting its centres is ordinary dependent-function application and uses no host-level or object-theoretic choice axiom.

module FunctionalImage (a : S) (R : S → S → hProp (ℓ-suc ℓ))
                       (fc : (x : S) → ⟨ x ∈ˢ a ⟩
                           → isContr (Σ[ y ∈ S ] ⟨ R x y ⟩)) where

The type Mem packages a source element together with evidence that it belongs to a. This evidence is part of the input expected by the contractible-fibre hypothesis, so a bare x : S would not suffice. Since S already lives at the successor universe level, Mem is too large to serve directly as the small index type required by boundingOrd. The canonical small presentation of the underlying set fst a provides a small way to enumerate the source members needed for the bound.

  Mem : Type (ℓ-suc ℓ)
  Mem = Σ[ x ∈ S ] ⟨ x ∈ˢ a ⟩

For p : Mem, the contractible fibre fc (p .fst) (p .snd) already contains its centre. The function img projects the value component of that centre, giving a definite model element for each certified source member. Although this looks like choosing values pointwise, no truncated existence is being eliminated: the centres are explicit components of the supplied dependent function fc.

  img : Mem → S
  img p = fc (p .fst) (p .snd) .fst .fst

The centre contains more than the chosen value. Its second component proves that R (p .fst) (img p) holds, and img-sat names this fact. The distinction matters: img supplies an element whose stage can be bounded, whereas img-sat certifies that this selected element is genuinely a value of the relation at the given source.

  img-sat : (p : Mem) → ⟨ R (p .fst) (img p) ⟩
  img-sat p = fc (p .fst) (p .snd) .fst .snd

Contractibility also identifies the chosen centre with every competing related pair (y , h). Applying congruence to the first projection yields img p ≡ y, an equality of complete model elements, including their constructibility certificates. Placing img p in the common stage and transporting that membership along this equality then covers an arbitrary y satisfying R (p .fst) y. Functionality is used source by source; it does not say that values arising from different sources are distinct.

  img-uniq : (p : Mem) (y : S) → ⟨ R (p .fst) y ⟩ → img p ≡ y
  img-uniq p y h = cong fst (fc (p .fst) (p .snd) .snd (y , h))

To obtain a small indexing family, memS starts with an index m : ⟪ fst a ⟫. Its represented set is known to belong to fst a. Since a is constructible and the constructible class is transitive, that represented set is constructible as well, so it can be paired with its certificate to form an element of S. Together with the original membership proof this gives an element of Mem, to which img and the fibre hypothesis may be applied.

  private
    memS : ⟪ fst a ⟫ → Mem
    memS m = (⟪ fst a ⟫↪ m
             , isL-trans fm∈fa (a .snd)) , fm∈fa
      where

The local proof fm∈fa supplies the membership component of memS. The canonical presentation states membership first in its small relation, and ∈∈ₛ converts that fact to the proposition-valued membership of the cumulative hierarchy. Applying transitivity to fm∈fa and the certificate a .snd gives the constructibility component of memS. Thus the same membership fact both locates the represented set inside the source and permits it to be packaged as a constructible model element.

      fm∈fa : ⟨ ⟪ fst a ⟫↪ m ∈ fst a ⟩
      fm∈fa = ∈∈ₛ {a = ⟪ fst a ⟫↪ m} {b = fst a} .snd (∈ₛ⟪ fst a ⟫↪ m)

The source can now be traversed through the small type ⟪ fst a ⟫. For each index m, take the least stage index containing the selected value img (memS m) and supply its ordinality by stage-ord. The constructive operation boundingOrd returns one ordinal strictly above all these indices. The common-bound argument uses stage-ord and stage-mem; minimality is not needed for the common-bound argument, although it is also provided by the canonical stage assignment. If a is empty, the index family is empty and boundingOrd still returns an ordinal bound, without asserting that the image is inhabited.

    bImg = boundingOrd ⟪ fst a ⟫
      (λ m → stage (fst (img (memS m))) (img (memS m) .snd))
      (λ m → stage-ord (fst (img (memS m))) (img (memS m) .snd))

The first projection of this bounding result is named βimg. It is an ordinal stage index, not the stage itself. The corresponding stage is the cumulative hierarchy set Lset βimg; range∈βimg states that the underlying set of every related value belongs to this stage. Packaging Lset βimg as a model element is a separate operation and requires an ordinality certificate.

  βimg : V ℓ
  βimg = bImg .fst

The second projection of bImg certifies both parts of the bound. Its first part, exposed here as βimg-ord, proves that βimg is an ordinal; this permits Lset βimg to be packaged as a model element. The remaining part gives, for every small source index m, membership of the selected value's stage index in βimg. Combining that comparison with stage-mem places each selected image in Lset βimg. Transport from the represented source to an arbitrary source member, followed by img-uniq, extends the conclusion to every value related to that member. Ordinality and range containment are therefore distinct claims extracted from the same bounding construction.

  βimg-ord : IsOrd βimg
  βimg-ord = bImg .snd .fst

To bound every value of the relation, fix x ∈ˢ a, a candidate y, and a proof of R x y. The source membership identifies x with a member from the canonical small presentation of a. Functionality then identifies y with the chosen value at that presented member. That chosen value belongs to its canonical stage, whose index lies strictly below βimg; Lset-mono therefore places it in Lset βimg. Transport along the value equality gives the required membership for y. Thus the single stage Lset βimg contains every value related to a member of a. The canonical stages used earlier depend on lem; this final comparison and upward transport introduce no further classical principle.

  range∈βimg : (x : S) → ⟨ x ∈ˢ a ⟩ → (y : S) → ⟨ R x y ⟩
              → ⟨ fst y ∈ Lset βimg ⟩
  range∈βimg x x∈a y h = subst (λ w → ⟨ fst w ∈ Lset βimg ⟩) image≡y
    (Lset-mono {α = βimg} {β = stage (fst (img (memS m))) (img (memS m) .snd)}
      (bImg .snd .snd m) (stage-mem (fst (img (memS m))) (img (memS m) .snd)))

The membership fibre supplies both data needed to compare the arbitrary source with the small presentation. Its first projection is an index m of the presentation of fst a; this is data already contained in membership, rather than a choice from a merely inhabited collection. Its second projection is an equality between the set presented by m and fst x. The lemma Σ≡Prop lifts that equality to memS m .fst ≡ x, because the second component isL of a model element is proposition-valued and hence cannot distinguish two packages with the same underlying set.

    where
    m = ∈-asFiber {a = fst x} {b = fst a} x∈a .fst
    q : memS m .fst ≡ x
    q = Σ≡Prop (λ z → snd (isL z))
      (∈-asFiber {a = fst x} {b = fst a} x∈a .snd)

The relation proof originally has source x. Transporting it along the inverse of q makes it a proof of R (memS m .fst) y, so it lies in the same value fibre as the centre selected by fc at memS m. Since that fibre is contractible, img-uniq equates its centre img (memS m) with y. This is the precise use of functionality: it compares two values for one fixed source. It does not assert that different source members have different values.

    image≡y : img (memS m) ≡ y
    image≡y = img-uniq (memS m) y (subst (λ z → ⟨ R z y ⟩) (sym q) h)

At a fixed stage

The fixed-stage argument begins with an ordinal index σ and its certificate oσ. The construction DefC = DefOf (Lset σ) treats the members of Lset σ through their canonical small presentation. It supplies formulas whose constants are such presentation indices and the subset defSet cut out by each unary formula. The remaining task is to compare that stage-based definition with satisfaction in the constructible model.

module AtStage (σ : V ℓ) (oσ : IsOrd σ) where
  module DefC = DefOf (Lset σ)

Bounded-formula absoluteness requires the class under consideration to be transitive. Here DefC.M is the class of members of Lset σ, and layer-trans (Lset-layer σ) proves exactly that a member of one of its members is again in the stage. Notice that this proof does not use the ordinality certificate oσ: transitivity follows from Lset-layer σ itself. This closure is what keeps witnesses of bounded quantifiers inside the restricted world.

  Atrans : Transitive 𝒮ᵥ DefC.M
  Atrans = layer-trans (Lset-layer σ)

Supplying Atrans to DefC.Refine makes the bounded-formula comparison available. The renamed notation _⊨σ_ denotes the refinement's ambient V-valued reading: stage indices are interpreted by the members they present, and the resulting formula is evaluated in the surrounding hierarchy. In particular, RefC.abs-defSet will identify membership in a definable subset with this ambient reading for a Δ₀ formula. That fact provides the first half of the semantic bridge below.

  module RefC = DefC.Refine Atrans
  open RefC.Abs using () renaming ( _⊨ᵛ_ to _⊨σ_ )

The predicate Below c says only that the underlying set fst c belongs to Lset σ. Its role is to certify the constants occurring in a term or formula: BoundedFo Below φ contains one such certificate for every constant of φ. It says nothing about free-variable assignments or quantified witnesses. The separate cover hypothesis of carveAt will later control which satisfying values lie in the stage.

  Below : S → Type (ℓ-suc ℓ)
  Below c = ⟨ fst c ∈ Lset σ ⟩

The relabelling RL turns each model constant satisfying Below into an index of the small presentation ⟪ Lset σ ⟫. Its semantic maps are fst, from model elements to underlying sets, and ⟪ Lset σ ⟫↪, from presentation indices to the sets they name. For a proof that fst c ∈ Lset σ, ∈-asFiber returns both the required index and the equality saying that this index names fst c. These two projections establish the commuting triangle needed for correct relabelling.

  module RL = Relabel {K = S} {K' = ⟪ Lset σ ⟫} {W = V ℓ}
                fst ⟪ Lset σ ⟫↪ Below
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .fst)
                (λ c p → ∈-asFiber {a = fst c} {b = Lset σ} p .snd)

The bridge compares two satisfaction propositions for the same mathematical assignment. On the left, every constant of φ has first been relabelled to a presentation index by RL.liftFo; mapFo DefC.ι then interprets that index as the member it presents, and _⊨σ_ evaluates the result in the ambient hierarchy at ⟪ Lset σ ⟫↪ m. On the right, the original formula is evaluated inside the constructible model at the packaged element (⟪ Lset σ ⟫↪ m , xL). The constant bound h, the Δ₀ proof dφ, and the constructibility proof xL justify the three changes of viewpoint.

  satBridge : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ((⟪ Lset σ ⟫↪ m ∷ []) ⊨σ (mapFo DefC.ι (RL.liftFo φ h)))
              ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  satBridge φ h dφ m xL =

The first three paths normalize the two successive constant interpretations. The first ⊨-map expands the interpretation DefC.ι of the stage constants. The symmetric second application expresses the same reading through the presentation map ⟪ Lset σ ⟫↪. The path RL.liftFo-correct, placed under satisfaction by cong, then replaces "relabel to an index and name it again" with direct interpretation by fst. This last step is a syntactic formula equality derived from the commuting triangle in RL.

      ⊨-map 𝒮ᵥ DefC.ι fst (RL.liftFo φ h)
        (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (⊨-map 𝒮ᵥ ⟪ Lset σ ⟫↪ id (RL.liftFo φ h)
             (⟪ Lset σ ⟫↪ m ∷ []))
    ∙ cong (λ ψ → (⟪ Lset σ ⟫↪ m ∷ []) ⊨v ψ) (RL.liftFo-correct φ h)

The fourth path, another ⊨-map, moves from ambient satisfaction with the constants and environment read through fst to the corresponding formula over model elements. At that point both the original formula and the packaged one-element environment are in place. The final path uses abs₀ in the symmetric direction: Δ₀ absoluteness carries ambient truth at the underlying sets back to truth inside the constructible model. Since the result is an equality of hProps, later arguments may transport evidence in either direction.

    ∙ ⊨-map 𝒮ᵥ fst id φ (⟪ Lset σ ⟫↪ m ∷ [])
    ∙ sym (abs₀ dφ ((⟪ Lset σ ⟫↪ m , xL) ∷ []))

The desired membership specification can now be stated directly. For a presented stage member m, together with a proof xL that its represented set is constructible, membership in the definable subset cut out by the lifted formula equals satisfaction of the original formula in L. The left side uses the small presentation of Lset σ; the right side packages the same represented set as a model element. The equality therefore connects the stage construction to the predicate that separation must realize.

  carveSat : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
           → (⟪ Lset σ ⟫↪ m ∈ DefC.defSet (RL.liftFo φ h))
             ≡ (((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ)
  carveSat φ h dφ m xL =

The proof is the composite of two semantic equalities. First, RefC.abs-defSet uses transitivity and the lifted Δ₀ certificate to identify membership in DefC.defSet (RL.liftFo φ h) with ambient satisfaction of mapFo DefC.ι (RL.liftFo φ h) at the presented member. Then satBridge identifies that ambient proposition with satisfaction of the original formula inside the constructible model. The order matters: definability reaches the ambient hierarchy first, and model absoluteness supplies the final link.

    RefC.abs-defSet (RL.liftFo φ h) (RL.Δ₀-liftFo h dφ) m ∙ satBridge φ h dφ m xL

The operation carve is exactly DefC.defSet, now given a stable name for the rest of the construction. Declaring it opaque changes no set and adds no existence principle; it only prevents automatic unfolding. Mathematically, carve ψ remains the subset of Lset σ selected by the unary formula ψ over the stage's presentation. The following lemmas expose the membership and constructibility facts needed to use that subset.

  opaque
    carve : Formula ⟪ Lset σ ⟫  → V ℓ
    carve ψ = DefC.defSet ψ

The formula ψ itself witnesses that carve ψ is a definable subset of Lset σ. The constructor 𝒟ₒ-intro expects merely the existence of such a formula and an extensional equality with its defSet, so the explicit pair (ψ , refl) is inserted into propositional truncation as ∣ ψ , refl ∣₁. Consequently the particular defining formula is not retained by the membership proposition carve ψ ∈ 𝒟ₒ (Lset σ). This lemma supplies the premise from which 𝒟ₒ→isL will later derive constructibility. This line introduces the truncation; it does not eliminate it or recover a formula from it.

  opaque
    unfolding carve
    carve∈𝒟ₒ : (ψ : Formula ⟪ Lset σ ⟫ ) → ⟨ carve ψ ∈ 𝒟ₒ (Lset σ) ⟩
    carve∈𝒟ₒ ψ = 𝒟ₒ-intro (Lset σ) (DefC.defSet ψ) ∣ ψ , refl ∣₁

Every definable subset produced by DefC.defSet is contained in its ambient set Lset σ. The lemma carve⊆ records this inclusion for the opaque name: from y ∈ carve ψ it obtains y ∈ Lset σ by DefC.defSet⊆A. This containment is independent of whether y satisfies any formula in the constructible model; it follows from the way defSet ranges only over the stage's presented members.

    carve⊆ : (ψ : Formula ⟪ Lset σ ⟫ ) (y : V ℓ) → ⟨ y ∈ carve ψ ⟩
           → ⟨ y ∈ Lset σ ⟩
    carve⊆ ψ y mem = DefC.defSet⊆A ψ y mem

The forward reading of carveSat turns carved membership into model satisfaction. Given a presented member in carve (RL.liftFo φ h), substitution along the hProp equality carveSat produces a proof that the corresponding model element satisfies φ. No new logical implication is proved here: subst simply transports an inhabitant from the left endpoint of the established equality to the right endpoint.

    imageOut : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
               (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
             → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
             → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
    imageOut φ h dφ m xL mem = subst ⟨_⟩ (carveSat φ h dφ m xL) mem

The reverse reading follows the same equality in the opposite direction. Satisfaction of φ by the packaged presented member transports along sym (carveSat ...) to membership in the carved set. Together imageOut and imageIn give both directions of the pointwise correspondence, but only for members represented in the fixed stage. The later cover argument is what allows an arbitrary satisfying model element to be represented there.

    imageIn : (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
              (m : ⟪ Lset σ ⟫) (xL : ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩)
            → ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ φ ⟩
            → ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo φ h) ⟩
    imageIn φ h dφ m xL sat = subst ⟨_⟩ (sym (carveSat φ h dφ m xL)) sat

Satisfaction is insensitive to the proof component carried by a model element. An equality fst u ≡ fst v of underlying sets lifts through Σ≡Prop to an equality u ≡ v, because isL x is a proposition for every x; satisfaction then transports along the resulting equality of one-element environments. The argument does not inspect dφ, so this transport is mathematically valid for an arbitrary formula. The Δ₀ parameter remains in the statement although the proof does not use it, and no use of excluded middle occurs in the proof.

  opaque
    ⊨-transport : (φ : Formula S ) (dφ : Δ₀ φ) (u v : S) → fst u ≡ fst v
                → ⟨ (u ∷ []) ⊨ φ ⟩ → ⟨ (v ∷ []) ⊨ φ ⟩
    ⊨-transport φ dφ u v p =
      subst (λ z → ⟨ (z ∷ []) ⊨ φ ⟩) (Σ≡Prop (λ x → snd (isL x)) p)

Separation at a stage

Every index m : ⟪ Lset σ ⟫ presents an actual member of the stage. The canonical small-membership proof ∈ₛ⟪ Lset σ ⟫↪ m is converted by the second direction of ∈∈ₛ into the ambient proposition ⟪ Lset σ ⟫↪ m ∈ Lset σ. Since σ is ordinal, Lset→isL σ oσ turns this stage membership into the constructibility certificate needed to package the presented set as an element of S. This is the point in the fixed-stage construction where oσ is used.

  private
    memberIsL : (m : ⟪ Lset σ ⟫) → ⟨ isL (⟪ Lset σ ⟫↪ m) ⟩
    memberIsL m = Lset→isL σ oσ (⟪ Lset σ ⟫↪ m)
      (∈∈ₛ {a = ⟪ Lset σ ⟫↪ m} {b = Lset σ} .snd (∈ₛ⟪ Lset σ ⟫↪ m))

The general fixed-stage construction accepts a unary formula χ, a proof that all its constants satisfy Below, a Δ₀ certificate, and a cover saying that every model element satisfying χ has its underlying set in Lset σ. It must produce a contractible type of realizers for the satisfaction predicate. uniqueL reduces this goal to one explicit model element with a pointwise membership specification: propositional extensionality turns the two implications at each z into a path of truth values, and set extensionality then gives uniqueness of the realizing set.

  carveAt : (χ : Formula S ) (hχ : BoundedFo Below χ) (dχ : Δ₀ χ)
            (cover : (z : S) → ⟨ (z ∷ []) ⊨ χ ⟩ → ⟨ fst z ∈ Lset σ ⟩)
          → isContr (SetOf (λ z → (z ∷ []) ⊨ χ))
  carveAt χ hχ dχ cover = uniqueL (λ z → (z ∷ []) ⊨ χ) (replElt , spec)
    where

The chosen realizer has underlying set carve (RL.liftFo χ hχ). The bound hχ makes the relabelling of every constant into the stage legitimate, while carve∈𝒟ₒ proves that the resulting defSet belongs to the definable powerset of Lset σ. Applying 𝒟ₒ→isL σ oσ to that membership supplies the second component of the model element. Thus definability gives existence of a constructible realizer; its exact extension is established separately by spec.

    replElt : S
    replElt = carve (RL.liftFo χ hχ)
            , 𝒟ₒ→isL σ oσ (carve (RL.liftFo χ hχ)) (carve∈𝒟ₒ (RL.liftFo χ hχ))

The specification is a path between membership in replElt and satisfaction of χ, for every model element z. The forward implication starts with z ∈ˢ replElt. Since the underlying set of replElt is the carved set, carve⊆ places fst z in Lset σ; the canonical presentation then supplies an index m naming that set. After transporting carved membership to the presented representative, imageOut yields satisfaction there, and ⊨-transport moves it along the underlying-set equality back to z. The cover hypothesis is unnecessary in this direction because carved membership already provides the required stage bound.

    spec : (z : S) → (z ∈ˢ replElt) ≡ ((z ∷ []) ⊨ χ)
    spec z = ⇔toPath fwd bwd
      where
      fwd : ⟨ z ∈ˢ replElt ⟩ → ⟨ ((z ∷ []) ⊨ χ) ⟩
      fwd z∈ = ⊨-transport χ dχ (⟪ Lset σ ⟫↪ m , xL) z q (imageOut χ hχ dχ m xL m∈)

The local data make the passage to the canonical presentation explicit. First fz∈Lσ follows from containment of the carved set. Applying ∈-asFiber to this membership gives an index m : ⟪ Lset σ ⟫ and a path q : ⟪ Lset σ ⟫↪ m ≡ fst z. These are the two projections of one membership fibre, so no choice principle is involved. The path q will be used in opposite directions: first to move carved membership to the presented set, and then to move satisfaction from the packaged representative back to z.

        where
        fz∈Lσ = carve⊆ (RL.liftFo χ hχ) (fst z) z∈
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst
        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd

The forward direction of the specification ends with two steps. The represented member of the layer is packaged into a model element, its constructibility coming from the stage itself; and the membership in the carved set, proved for that represented member, is carried along the naming equation to the original element. The direction is complete: a member of the carved set satisfies the formula, in the model, at itself.

        xL = memberIsL m
        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) (sym q) z∈

The backward direction begins with the covering hypothesis, and this is the one place where the covering hypothesis is used: every element satisfying the formula is assumed to lie in the stage. Applying this hypothesis to the given satisfaction proof. The fibre of the stage membership then recovers the index of a canonical representative.

      bwd : ⟨ ((z ∷ []) ⊨ χ) ⟩ → ⟨ z ∈ˢ replElt ⟩
      bwd qz = subst (λ w → ⟨ w ∈ carve (RL.liftFo χ hχ) ⟩) q m∈
        where
        fz∈Lσ = cover z qz
        m = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .fst

The representative is named by an equation, and the satisfaction is moved to it. Since satisfaction depends only on the underlying set, the equation between underlying sets suffices; the representative is packaged as a model element with its own constructibility, and the formula now holds of the representative instead of the original.

        q : ⟪ Lset σ ⟫↪ m ≡ fst z
        q = ∈-asFiber {a = fst z} {b = Lset σ} fz∈Lσ .snd
        xL = memberIsL m
        satz : ⟨ ((⟪ Lset σ ⟫↪ m , xL) ∷ []) ⊨ χ ⟩
        satz = ⊨-transport χ dχ z (⟪ Lset σ ⟫↪ m , xL) (sym q) qz

The definability implication now applies: the representative satisfies the formula, so the representative belongs to the carved set; and the naming equation carries the membership back to the original element. Both directions are complete, and the specification is, at every element, an equality of two propositions: belonging to the carved realization, and satisfying the formula in the model.

        m∈ : ⟨ ⟪ Lset σ ⟫↪ m ∈ carve (RL.liftFo χ hχ) ⟩
        m∈ = imageIn χ hχ dχ m xL satz

Separation at a stage specializes the preceding construction to subsets. Its hypothesis is that the source set already lies in the stage; its formula is the conjunction of membership in the source with the given formula, which is bounded because a membership atom is bounded and conjunctions preserve boundedness, and its constants are bounded because the source was supplied below the stage and the formula's constants came certified. The fixed-stage theorem then returns exactly the contractible realization that the model field's separation asks for.

  separateAt : (a : S) (fa∈σ : ⟨ fst a ∈ Lset σ ⟩)
               (φ : Formula S ) (h : BoundedFo Below φ) (dφ : Δ₀ φ)
             → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
  separateAt a fa∈σ φ h dφ =
    carveAt ((var zero ∈̇ con a) ∧̇ φ) ((tt* , fa∈σ) , h) (δ-∧ δ-∈ dφ)

The covering hypothesis of the fixed-stage theorem is discharged by the first conjunct alone. An element satisfying the conjunction satisfies membership in the source, the source lies in the stage, and the stage is transitive, so the element lies in the stage as well. This is the mathematical reason the membership conjunct of the separation predicate is not decoration: it is what brings every candidate under the stage within which the subset is being carved.

      (λ z q → layer-trans (Lset-layer σ) {x = fst a} {y = fst z} (q .fst) fa∈σ)

Finding the stage

To compare bounds chosen independently, the stage condition is parameterized by its ordinal index. The predicate has the same mathematical content as before: an element's underlying set belongs to the layer named by the index. A single chosen stage therefore becomes a variable stage over which the subsequent search may quantify.

Below′ : V ℓ → S → Type (ℓ-suc ℓ)
Below′ σ c = ⟨ fst c ∈ Lset σ ⟩

The first lifting lemma moves a term's boundedness along the indices. If one stage index precedes another, then every constant lying under the first lies under the second, by the strict growth of the tower; and the boundedness certificate of a term is carried to the larger index by applying this pointwise at each constant. The term itself is unchanged; only the proof of boundedness is transported.

liftTmTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (t : Term S n)
         → BoundedTm (Below′ σ) t → BoundedTm (Below′ β) t
liftTmTo {σ} {β} σ∈β t h =
  BoundedTm-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') t h

The second lifting lemma does the same for formulas: a formula whose constants all lie under one stage index keeps that property under any later index. The proof applies the term lemma at every constant position of the formula. With the two lifting lemmas, a boundedness proof obtained at one stage can be transported to any later stage chosen for the remaining data.

liftFoTo : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → ∀ {n} (φ : Formula S n)
         → BoundedFo (Below′ σ) φ → BoundedFo (Below′ β) φ
liftFoTo {σ} {β} σ∈β φ h =
  BoundedFo-mono {P = Below′ σ} {Q = Below′ β}
    (λ (c : S) h' → Lset-mono {α = β} {β = σ} σ∈β {x = fst c} h') φ h

The search for a constant bound starts at terms, and the two cases could hardly be more different. A constant is bounded by its own earliest stage, with the ordinality of that index and the membership of the constant in its layer. A variable contains no constants, so the empty stage is returned with a vacuous proof; there is no constant to bound, and the result makes no claim that a variable's value belongs to the empty set.

mkBoundedTm : ∀ {n} (t : Term S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedTm (Below′ σ) t)
mkBoundedTm (con c) = stage (fst c) (c .snd)
                    , (stage-ord (fst c) (c .snd) , stage-mem (fst c) (c .snd))
mkBoundedTm (var i) = ∅ , (∅-ord , _)

The merger of two search results is stated once, generically, for any two kinds of certificates that can be lifted along the indices. Its input is a pair of results, each an ordinal index with its ordinality and a certificate; its output is one result at a common index, with both certificates carried there. The two lifting operations are parameters, so the same construction applies to two terms, two formulas, or a term and a formula.

private
  mkBounded : ∀ {ℓc ℓd} {C : V ℓ → Type ℓc} {D : V ℓ → Type ℓd}
            → (liftC : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → C σ → C β)
            → (liftD : {σ β : V ℓ} → ⟨ σ ∈ β ⟩ → D σ → D β)
            → (r₁ : Σ[ σ ∈ V ℓ ] (IsOrd σ × C σ))

The common-bound construction has three steps. It takes the bound of the two indices, which is an ordinal above both; it records that the first index precedes the bound and the second does too; and it applies the two lifting operations along these inclusions, so both certificates describe the common index. No property of the certificates is used beyond their liftable shape.

            → (r₂ : Σ[ σ ∈ V ℓ ] (IsOrd σ × D σ))
            → Σ[ σ ∈ V ℓ ] (IsOrd σ × (C σ × D σ))
  mkBounded liftC liftD r₁ r₂ = b .fst , (b .snd .fst ,
      ( liftC (b .snd .snd .fst) (r₁ .snd .snd)
      , liftD (b .snd .snd .snd) (r₂ .snd .snd) ))

The bound itself is the ordinal chapter's merge of two ordinals: an ordinal that each of the two precedes. This is the only ordinal-theoretic fact needed by this recursion, and it is constructive; the classical parameter does not enter here, but only earlier, where each constant's earliest stage was named.

    where
    b  = bound2 (r₁ .fst) (r₂ .fst) (r₁ .snd .fst) (r₂ .snd .fst)

The search over formulas recurses on the syntax. The two atomic forms merge the bounds of their two terms. Each propositional connective merges the bounds of its two subformulas. In every case the merger just described does the work, and the boundedness proofs are transported to the common index.

mkBoundedFo : ∀ {n} (φ : Formula S n) → Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ)
mkBoundedFo (t ∈̇ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (t ≐ u) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftTmTo σ∈β u) (mkBoundedTm t) (mkBoundedTm u)
mkBoundedFo (φ ∧̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo (φ ∨̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)

The remaining cases are instructive in their asymmetry. The false formula has no constants, so the empty stage is a bound. An unbounded quantifier has the same constant bound as its body: the quantifier itself introduces no constant, so the recursion passes underneath it untouched. A bounded quantifier also contains its bounding term: its bounding term names a constant, so the term's bound and the body's bound are merged.

mkBoundedFo (φ ⇒̇ ψ) = mkBounded (λ σ∈β → liftFoTo σ∈β φ) (λ σ∈β → liftFoTo σ∈β ψ) (mkBoundedFo φ) (mkBoundedFo ψ)
mkBoundedFo ⊥̇        = ∅ , (∅-ord , _)
mkBoundedFo (∃̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇ φ)    = mkBoundedFo φ
mkBoundedFo (∀̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)

The bounded existential behaves like the bounded universal: the bound of the bounding term is merged with the bound of the body. One property of the whole search deserves emphasis, because it separates two independent notions: the recursion inspects only constants, so it succeeds on formulas with unbounded quantifiers as well. A certificate produced here therefore says nothing about whether a formula is bounded; the two notions, constants-under-a-stage and bounded-quantifiers, remain separate throughout.

mkBoundedFo (∃̇∈ t φ) = mkBounded (λ σ∈β → liftTmTo σ∈β t) (λ σ∈β → liftFoTo σ∈β φ) (mkBoundedTm t) (mkBoundedFo φ)

Δ₀ separation

Bounded separation is now stated in full. For a source set and any unary formula all of whose quantifiers are bounded, the predicate "member of the source and satisfying the formula" has a contractible realization by a model element. The proof is one application of the fixed-stage separation theorem, after the stage has been computed.

separateΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
           → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
separateΔ₀ a φ dφ = AtStage.separateAt σ oσ a fa∈σ φ h dφ
  where
  rφ = mkBoundedFo φ

The stage is computed from two bounds. The search just constructed bounds the constants of the formula, while the established stage assignment gives the earliest stage containing the source set. The two indices are merged, and the formula's certificate is lifted to the merge. At the resulting common stage, both the formula's constants and the source lie below the chosen bound.

  sa = stage (fst a) (a .snd)
  bb = bound2 (rφ .fst) sa (rφ .snd .fst) (stage-ord (fst a) (a .snd))
  σ  = bb .fst
  oσ = bb .snd .fst
  h  = liftFoTo {σ = rφ .fst} {β = σ} (bb .snd .snd .fst) φ (rφ .snd .snd)

The source's own placement is recorded separately: it lies in its earliest layer, and the merge's recorded inclusion lifts that membership to the common stage. This supplies the covering hypothesis of the fixed-stage theorem. It follows directly from the monotonicity of the tower and the certificate supplied by the stage assignment.

  fa∈σ : ⟨ fst a ∈ Lset σ ⟩
  fa∈σ = Lset-mono {α = σ} {β = sa} (bb .snd .snd .snd) (stage-mem (fst a) (a .snd))

Δ₀ replacement

Bounded replacement is stated with its functionality hypothesis explicit. For a source, a binary formula all of whose quantifiers are bounded, and the assumption that each member's fibre of related values is contractible, the image predicate has a contractible realization by a model element. The proof transports realizability along an equality of predicates. Functionality is used to bound the related values; once that bound is known, ordinary separation collects the image.

replaceΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
          → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (x ∷ y ∷ []) ⊨ φ ⟩))
          → isContr (SetOf (ReplImage a φ))
replaceΔ₀ a φ dφ fc =
  subst (λ Q → isContr (SetOf Q)) (sym Q≡)

The functional-image bound is applied with the source in the first slot of the relation. It gives the common image stage with its ordinality and its covering fact. Full bounded separation is then applied at that stage, packaged as a model element, to the unary image formula; the formula's boundedness evidence is the bounded existential case, since the only quantifier added is bounded by the source.

    (separateΔ₀ (LsetS βimg βimg-ord) imageFo (δ-∃∈ dφ))
  where
  module I = FunctionalImage a (λ x y → (x ∷ y ∷ []) ⊨ φ) fc
  open I using ( βimg; βimg-ord; range∈βimg )

The unary image formula has the following semantics. It says, in the object language, that some member of the source relates to the outer candidate, and the bounded existential pushes that member into the first environment slot. The bounded existential here is the object language's own quantifier; the outer existence of the image predicate is the host level's truncated existence. The two agree in meaning through the semantics, but they are not the same syntactic object, and distinguishing them makes the next equality precise.

  imageFo : Formula S 
  imageFo = ∃̇∈ (con a) φ

The guarded predicate collects what the construction can verify: the candidate lies in the packaged common image stage, and it satisfies the unary image formula. The stage-membership conjunct provides a bound for Separation. The other conjunct describes the actual image, so the stage condition can later be removed using the covering theorem.

  BoundedImage : S → hProp (ℓ-suc ℓ)
  BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)

The equality of the two predicates is pointwise, and its two directions differ in effort. Forward: from the truncated source witness into the guarded predicate. The elimination is legitimate because the guarded predicate is a proposition, the covering fact supplies the stage membership, and the same source is placed back inside the truncation with its satisfaction in the slot order the formula expects. Backward: nothing is needed, for the satisfaction of the image formula at a candidate is, by its semantics, exactly the image predicate at that candidate; the stage conjunct is dropped and the second conjunct stands as the claim. Because the source occupies the first slot: no transposition of variables is needed anywhere.

  Q≡ : ReplImage a φ ≡ BoundedImage
  Q≡ = funExt (λ y → ⇔toPath (into y) (λ p → p .snd))
    where
    into : (y : S) → ⟨ ReplImage a φ y ⟩ → ⟨ BoundedImage y ⟩
    into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) →

For a candidate y in ReplImage a φ, the source x, its membership proof x∈a, and the satisfaction proof h are available under propositional truncation. Since BoundedImage y is a proposition, PT.rec may use these data while constructing its two conjuncts. The first component follows from range∈βimg: functionality implies that every value related to a member of a lies in Lset βimg. For the second component, the same x, x∈a, and h are placed back under propositional truncation. By the semantics of imageFo = ∃̇∈ (con a) φ, this is exactly the proof that y satisfies imageFo. Thus no source is returned as untruncated data.

This completes the implication from ReplImage a φ y to BoundedImage y. Together with the reverse implication, which discards the stage-membership component, it yields Q≡; transport along sym Q≡ then proves replaceΔ₀. Precisely, under the assumption lem : LEM (ℓ-suc ℓ), a Δ₀ witness for φ, and contractibility of the value fibre for every x ∈ˢ a, the result is isContr (SetOf (ReplImage a φ)). This is the stated Δ₀ replacement theorem. The branch introduces no additional classical principle, although the construction of the common stage used by range∈βimg depends on lem.

      range∈βimg x x∈a y h , ∣ x , (x∈a , h) ∣₁ }

Recap

Bounded separation and bounded replacement follow the same pattern. First place the source, the formula's constants, and, for replacement, all related values below one ordinal stage. Definability forms the required subset inside that stage, while relabelling and Δ₀ absoluteness identify its membership relation with satisfaction in the constructible model. Thus separateΔ₀ and replaceΔ₀ are obtained under the single host-level assumption lem : LEM (ℓ-suc ℓ).