--- title: "Separation and replacement, bounded" module: L.Axioms.Separation lang: en site: "Bedrock" description: "Separation and replacement, bounded" stage: "Constructible stages and the axioms" reading_order: 32 canonical: https://bedrock.institute/en/L.Axioms.Separation.html html: L.Axioms.Separation.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Separation.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantBounding, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Semantics, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, L.Definability, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Axioms.Separation.md, https://bedrock.institute/ja/L.Axioms.Separation.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 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. ```agda {-# 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. ```agda 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. ```agda 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 Δ₀. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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`. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda ReplImage : (a : S) (φ : Formula S 2) → 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda β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. ```agda β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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda satBridge : (φ : Formula S 1) (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`. ```agda ⊨-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. ```agda ∙ ⊨-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. ```agda carveSat : (φ : Formula S 1) (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. ```agda 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. ```agda opaque carve : Formula ⟪ Lset σ ⟫ 1 → 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. ```agda opaque unfolding carve carve∈𝒟ₒ : (ψ : Formula ⟪ Lset σ ⟫ 1) → ⟨ 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. ```agda carve⊆ : (ψ : Formula ⟪ Lset σ ⟫ 1) (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. ```agda imageOut : (φ : Formula S 1) (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. ```agda imageIn : (φ : Formula S 1) (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. ```agda opaque ⊨-transport : (φ : Formula S 1) (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. ```agda 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. ```agda carveAt : (χ : Formula S 1) (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`. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda separateAt : (a : S) (fa∈σ : ⟨ fst a ∈ Lset σ ⟩) (φ : Formula S 1) (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. ```agda (λ 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda → (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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ → 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. ```agda 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. ```agda 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. ```agda replaceΔ₀ : (a : S) (φ : Formula S 2) → Δ₀ φ → ((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. ```agda (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. ```agda imageFo : Formula S 1 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. ```agda 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. ```agda 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`. ```agda 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 ℓ)`.