--- title: "Adequacy of the stage-order description" module: L.Choice.StageOrderAdequacy lang: en site: "Bedrock" description: "Adequacy of the stage-order description" stage: "The canonical well-order and Choice" reading_order: 79 canonical: https://bedrock.institute/en/L.Choice.StageOrderAdequacy.html html: L.Choice.StageOrderAdequacy.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/StageOrderAdequacy.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Ordinal.Stages, L.Axioms.Basic, L.Stage, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.WellOrder.Base, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Coding.DefinablePowerSet, L.Coding.CodeSet, L.Hierarchy, L.Choice.OrderTable, V.Coding, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/zh/L.Choice.StageOrderAdequacy.md, https://bedrock.institute/ja/L.Choice.StageOrderAdequacy.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Adequacy of the stage-order description The metatheory already carries a strict well order at every constructible stage, but the object language of `L` can speak only through formulas. This chapter translates that order into formulas: it describes the birth stage of each set, the code set that travels with each carrier, and the comparison rule of the stage order, proving that the descriptions are faithful to their meta-language meanings. One piece is deliberately left as a parameter: the comparison inside a fixed birth stage. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` Classical reasoning enters through one explicit hypothesis, `lem`. It will be used when ordinal stages must be compared, while the formulas constructed in this chapter remain ordinary formulas of the object language. Thus a semantic argument may use excluded middle without inserting a new axiom into the language being interpreted. ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` Keep the two levels of discourse distinct from the outset. The previously constructed `orderAt` is a meta-language strict well order. The goal here is to build formulas whose satisfaction expresses its underlying comparison; no formula in this chapter reconstructs the `SWO` structure or reproves its well-foundedness. ```agda module L.Choice.StageOrderAdequacy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` The translation uses only the object language's ordinary atoms and connectives. Membership states that a proposed witness lies in a stage or code set, equality identifies two represented objects, and existential quantification hides the auxiliary sets needed by the description. Later proofs interpret these formulas in the constructible structure and compare the resulting propositions with their meta-language counterparts. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Model {ℓ} using ( ∈sucV-elim ) ``` The relevant geometry of the hierarchy is simple. Ordinals linearly order the stages, membership between ordinal indices makes the tower monotone, and the successor of an ordinal separates a stage from its next definable-power-set stage. These facts will let us identify a proposed birth ordinal by comparing its successor with the least stage at which the set appears. ```agda open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; IsOrd; isPropIsOrd; Lset-mono; Lset→isL; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord; mem-ord ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ ) ``` For a constructible set `x`, its least containing stage is a successor, and `birth x` is the ordinal immediately below it. Consequently `x` is absent from `Lset (birth x)` but present in `Lset (sucV (birth x))`, which is the definable power set of the former stage. The formula `BirthAt` will express these two membership facts; leastness itself remains a meta-language theorem. ```agda open import L.Axioms.Basic {ℓ} using ( Lset-suc; LsetS; 𝒟ₒS; extensionalL ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest ) open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj ) open import L.Choice.StageOrders {ℓ} lem using ( birth; birth-ord; birth-suc; birth-mem; birth-stage; birth-proof ``` The existing stage order compares two members lexicographically by birth. An earlier birth decides the comparison immediately; equal births defer to the local order on the new elements of that stage. The later formula mirrors precisely this one unfolding equation, so its adequacy concerns the relation already carried by `orderAt`, not the construction of that order. ```agda ; Mem; New; relOf; carry; Under; stepAt ; orderAt; orderAt-step; module Family ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate ) open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both ) ``` The same-stage comparison needs formulas over a carrier that varies with the common birth ordinal. Hence its syntax cannot be fixed once at a single stage. The code predicate used below ranges over every finite arity relative to a carrier held in a variable slot, allowing the carrier and its formula codes to move together. ```agda open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.CodeSet {ℓ} lem using ( arityNumAtL; arityNumAtL-in; arityNumAtL-out; hasWitnessAt ; witnessAt-in; witnessAt-out; keyS; codeS ``` The final target is a relation represented as a set of ordered pairs in `L`. A table below the ambient stage supplies local relation values, and the formula must agree with the meta-language comparison for every encoded pair. This agreement will require both correctness and existence of table entries, and it remains conditional on the two adequacy directions supplied for the local step formula. ```agda ; AllCodes; AllCodes-in; AllCodes-out; IsKeyOverAny ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.OrderTable {ℓ} lem using ( Ordering; strict; Related; IsRel; Values; Entries ; related-in; module Described ) ``` An element of the represented relation is read as a code `pr u v`. Adequacy therefore has two tasks: recover some compared members `u` and `v` from such a pair code, and prove that their stage-order comparison holds; conversely, a known comparison must put the corresponding pair code into the represented set. The existence involved here is propositionally truncated, so it does not select a canonical decomposition. ```agda open import V.Coding {ℓ} using ( pr ) ``` Several identifications in the proof transport relations along equal stage indices or equal pair codes. Because ordinality and constructibility evidence are propositions, changing such evidence does not change the mathematical object being represented. This proof irrelevance is what permits transport without turning certificates into additional choices. ```agda import FOL.Absoluteness open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Data.Sigma using ( Σ≡Prop ) ``` Existential satisfaction is propositionally truncated throughout. A proof may use a stage value, a definable-power-set value, a decoded formula, or a table entry only when its target is again a proposition. In particular, none of the eliminations below yields a canonical witness, a chosen decoder, or a choice function assigning local relation values. ```agda import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) ``` Two successor constructions play different roles. `sucV` advances an ordinal stage, whereas numerals encode finite arities inside the hierarchy. Keeping them distinct prevents the statement that a set enters at the successor of its birth from being confused with the arity component of a formula code. ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV; #_ ) ``` Formulas will be interpreted in the constructible structure `𝒮ʟ`. Their meanings are therefore proposition-valued: satisfaction records whether a described membership, equality, or existence holds inside `L`, while the proofs comparing those meanings live in the surrounding Cubical Agda metatheory. ```agda open hPropStructure 𝒮ʟ ``` We write `γ ⊨ φ` for satisfaction at an environment and `⟦ t ⟧ γ` for the value of a term. This notation is the bridge used in every adequacy statement: the left side reads object-language syntax, while the right side identifies the corresponding set, ordinal, or relation in the metatheory. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ; ⟦_⟧ᵐ to ⟦_⟧ ) ``` The first shift names the variable two slots outward, preparing the formulas that bind four objects. ```agda sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ``` The second shift moves variables three slots outward. ```agda sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n))) sh3 i = suc (suc (suc i)) ``` A private shift moves variables four slots outward, reserved for the four-object bindings of the next section. ```agda private sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = suc (suc (suc (suc i))) ``` The term shift moves a term past four new bindings: constants keep their values, and each variable is renamed by the same shift. ```agda tm4 : ∀ {n} → Term S n → Term S (suc (suc (suc (suc n)))) tm4 (con k) = con k tm4 (var i) = var (sh4 i) ``` The evaluation of the shifted term is unaffected by the four extra bindings: this definitional agreement is recorded once and reused silently. ```agda tm4-val : ∀ {n} (t : Term S n) (a b c d : S) (γ : S ^ n) → ⟦ tm4 t ⟧ (d ∷ c ∷ b ∷ a ∷ γ) ≡ ⟦ t ⟧ γ tm4-val (con k) a b c d γ = refl tm4-val (var i) a b c d γ = refl ``` To place `Lset β` in a formula environment, we package the stage together with its constructibility proof as an element of `S`. The ordinalness hypothesis supplies that proof. What matters mathematically is the first projection recorded below: the package still denotes exactly `Lset β`, so it can serve as the stage witness when `BirthAt` is read inward. ```agda opaque towerS : (β : V ℓ) → IsOrd β → S towerS β ob = LsetS β ob ``` The underlying set of the packaged stage is the stage itself, definitionally. ```agda towerS-fst : (β : V ℓ) (ob : IsOrd β) → fst (towerS β ob) ≡ Lset β towerS-fst β ob = refl ``` The second witness needed by `BirthAt` is the definable power set of that stage. We package `𝒟ₒ (Lset β)` in the same way; its constructibility follows from the stage facts available at the ordinal `β`, and its first projection is the set required by the formula. ```agda powS : (β : V ℓ) → IsOrd β → S powS β ob = 𝒟ₒS β ob ``` Its underlying set is the definable power set of the stage at the ordinal, definitionally. ```agda powS-fst : (β : V ℓ) (ob : IsOrd β) → fst (powS β ob) ≡ 𝒟ₒ (Lset β) powS-fst β ob = refl ``` ## The birth stage, said inside `BirthAt b x` binds two auxiliary sets. The first is required to be the tower stage `Lset β` described at the candidate slot `b`; `x` must not belong to it. The second is required to be the definable power set of the first, and `x` must belong to it. Thus the formula expresses the boundary between two consecutive stages. It neither asserts that `β` is an ordinal nor contains an internal minimality clause. ```agda BirthAt : ∀ {n} → Fin n → Fin n → Formula S n BirthAt b x = ∃̇ ( LsetGraphAt zero (suc b) ∧̇ ( ¬̇ (var (suc x) ∈̇ var zero) ∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ (var (sh2 x) ∈̇ var zero) ) ) ) ``` Fix an environment `γ`. The candidate ordinal is the underlying set at slot `b`, while the set whose birth is being tested is the element at slot `x`. All subsequent reasoning is relative to these two interpretations, so the theorem concerns arbitrary variable assignments rather than specially chosen constants. ```agda module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where private β : V ℓ β = fst (lookup b γ) ``` The element `z` carries both its underlying set and evidence that it belongs to `L`. The meta-language function `birth` uses that evidence to form an ordinal, but proof irrelevance ensures that the resulting ordinal does not encode a choice of constructibility proof. ```agda z : S z = lookup x γ ``` The inner record collects a definable power set value `d` over the candidate stage `c`, together with satisfaction of the power-set description and the membership of the parameter in `d`. ```agda Inner : S → Type (ℓ-suc ℓ) Inner c = Σ[ d ∈ S ] ( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ fst z ∈ fst d ⟩ ) ``` The outer record adds the satisfaction of the stage graph at the raised index, the refutation of the parameter's membership in the candidate stage, and the truncation of the inner record. Together they are exactly what the birth formula asserts. ```agda Outer : S → Type (ℓ-suc ℓ) Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ( (⟨ fst z ∈ fst c ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥) × ∥ Inner c ∥₁ ) ``` The key semantic lemma assumes that `β` is an ordinal and that `x` lies in `𝒟ₒ (Lset β)` but not in `Lset β`. From precisely these boundary facts it proves `β ≡ birth x`. Ordinality is an input to this reading; it is not recovered from satisfaction of `BirthAt`. ```agda decideBirth : IsOrd β → ⟨ fst z ∈ 𝒟ₒ (Lset β) ⟩ → (⟨ fst z ∈ Lset β ⟩ → Empty.⊥) → β ≡ birth (fst z) (snd z) decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob) (stage (fst z) (snd z)) ``` Using `Lset-suc`, membership in `𝒟ₒ (Lset β)` becomes membership in `Lset (sucV β)`. This says that the least stage containing `x` occurs no later than the successor of `β`; the proof must still rule out every earlier possibility. ```agda (stage-ord (fst z) (snd z))) where mem : ⟨ fst z ∈ Lset (sucV β) ⟩ mem = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (Lset-suc β)) hin ``` Suppose the least stage of `x` belonged to `sucV β`. Membership in a successor ordinal splits into two cases: that stage belongs to `β`, or it equals `β`. In either case, monotonicity or direct transport would put `x` in `Lset β`, contradicting the assumed nonmembership. ```agda early : ⟨ stage (fst z) (snd z) ∈ sucV β ⟩ → Empty.⊥ early h = Empty.rec* (∈sucV-elim {A = β} {x = stage (fst z) (snd z)} Empty.isProp⊥* h below same) where below : ⟨ stage (fst z) (snd z) ∈ β ⟩ → Empty.⊥* ``` If `stage x ∈ β`, monotonicity carries the known membership of `x` in `Lset (stage x)` into `Lset β`. If `stage x ≡ β`, transport along that equality gives the same conclusion directly. Both alternatives contradict the boundary assumption `x ∉ Lset β`. ```agda below k = Empty.rec (hout (Lset-mono {α = β} {β = stage (fst z) (snd z)} k {x = fst z} (stage-mem (fst z) (snd z)))) same : stage (fst z) (snd z) ≡ β → Empty.⊥* same e = Empty.rec (hout (subst (λ u → ⟨ fst z ∈ Lset u ⟩) e ``` In the equality case, `stage x ≡ β` transports the known membership `x ∈ Lset (stage x)` to `x ∈ Lset β`. This is the second contradiction needed to show that the least stage cannot occur at or below `β`. ```agda (stage-mem (fst z) (snd z)))) ``` Ordinal trichotomy now compares `sucV β` with `stage x`. If the successor were strictly earlier, `x ∈ Lset (sucV β)` would contradict the defining minimality of `stage x`. If `stage x` were earlier, the preceding argument would contradict `x ∉ Lset β`. Hence only equality can remain. ```agda go : ⟨ sucV β ∈ stage (fst z) (snd z) ⟩ ⊎ ((sucV β ≡ stage (fst z) (snd z)) ⊎ ⟨ stage (fst z) (snd z) ∈ sucV β ⟩) → β ≡ birth (fst z) (snd z) go (inl h) = Empty.rec (stage-earliest (fst z) (snd z) (sucV β) (suc-ord ob) mem h) ``` From `sucV β ≡ stage x` and the identity `stage x ≡ sucV (birth x)`, injectivity of ordinal successor gives `β ≡ birth x`. The conclusion is forced by exclusion of the two strict cases; the proof does not choose a birth witness from the formula. ```agda go (inr (inl e)) = ord-suc-inj β (birth (fst z) (snd z)) ob (e ∙ sym (birth-suc (fst z) (snd z))) go (inr (inr h)) = Empty.rec (early h) ``` The reading lemma carries the ordinalness hypothesis of the slot: the formula alone does not prove the slot to be an ordinal. The proof unwraps the truncated existential and reaches the outer record. ```agda BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (fst z) (snd z) BirthAt-out h ob = PT.rec (setIsSet β (birth (fst z) (snd z))) atCarrier h where atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ ``` At each candidate stage, the inner record supplies a definable power set value containing the parameter, and the refutation of the parameter's membership in the candidate stage; the decision lemma is applied to these three data. ```agda → (⟨ fst z ∈ fst c ⟩ → Empty.⊥) → Inner c → β ≡ birth (fst z) (snd z) atInner c hg hn (d , (hd , hm)) = decideBirth ob (subst (λ u → ⟨ fst z ∈ u ⟩) qd hm) (λ k → hn (subst (λ u → ⟨ fst z ∈ u ⟩) (sym qc) k)) ``` The stage graph at the raised index is identified with the stage at the candidate ordinal by the uniqueness of the hierarchy description, and the power-set value is identified with the definable power set of that stage by the stage equation of the description. ```agda where qc : fst c ≡ Lset β qc = Lset-only zero (suc b) (c ∷ γ) hg ob qd : fst d ≡ 𝒟ₒ (Lset β) qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd ``` The outer record is eliminated into the inner reading, and the inner reading feeds the decision lemma; the whole proof eliminates the truncation into an equality of ordinals, which is a proposition. ```agda atCarrier : Σ[ c ∈ S ] Outer c → β ≡ birth (fst z) (snd z) atCarrier (c , (hg , (hn , hi))) = PT.rec (setIsSet β (birth (fst z) (snd z))) (atInner c hg (λ k → lower (hn k))) hi ``` For the converse direction, assume that the ordinal in slot `b` equals the meta-language birth of `x`. The two existential witnesses are the packaged stage `Lset β` and its packaged definable power set. They are placed under propositional truncation as required by existential satisfaction, so this construction does not assert that the formula has uniquely determined witnesses. ```agda BirthAt-in : IsOrd β → β ≡ birth (fst z) (snd z) → ⟨ γ ⊨ BirthAt b x ⟩ BirthAt-in ob e = ∣ towerS β ob , (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁ where hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ ``` The stage graph at the raised index holds because the packaged stage is the stage at that index, by the defining equation of the presentation. ```agda hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob) ``` If `x` belonged to `Lset β`, then after replacing `β` by `birth x`, it would occur at a stage strictly below `stage x = sucV (birth x)`. This contradicts `stage-earliest`, and supplies the negative membership required by `BirthAt`. ```agda hn : ⟨ fst z ∈ fst (towerS β ob) ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥ hn k = lift (stage-earliest (fst z) (snd z) β ob (subst (λ u → ⟨ fst z ∈ u ⟩) (towerS-fst β ob) k) (subst (λ u → ⟨ u ∈ stage (fst z) (snd z) ⟩) (sym e) (birth-stage (fst z) (snd z)))) ``` The stage equation for `DefAt` identifies its satisfaction proposition with equality to `𝒟ₒ (Lset β)`. The projection equation for `powS β ob` supplies exactly that equality, so the packaged definable power set satisfies the required clause. ```agda hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hd = subst ⟨_⟩ (sym (DefAt-stage β ob zero (suc zero) (powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob))) (powS-fst β ob) ``` Finally, `birth-mem` places `x` in `Lset (sucV (birth x))`. Replacing the proposed ordinal by the birth ordinal, using `Lset-suc`, and then using the projection equation for the packaged power set transports this membership to the second witness. Together with the outward reading, this proves that `BirthAt` describes the birth ordinal exactly whenever the candidate slot is assumed ordinal; it adds neither internal ordinality nor canonical existential witnesses. ```agda hm : ⟨ fst z ∈ fst (powS β ob) ⟩ hm = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (powS-fst β ob)) (subst (λ u → ⟨ fst z ∈ u ⟩) (Lset-suc β) (subst (λ u → ⟨ fst z ∈ Lset (sucV u) ⟩) (sym e) (birth-mem (fst z) (snd z)))) ``` ## The codes at any arity, at a carrier held in a slot The per-code recognizer combines two clauses: the first reads an arity numeral from the code, and the second checks that the code witnesses a formula over the working alphabet. Together they say the code is a genuine formula code at some arity. ```agda isCodeAnyAt : ∀ {n} → Fin n → Fin n → Formula S n isCodeAnyAt c w = arityNumAtL c ∧̇ hasWitnessAt w c ``` The inward reading is stated for a working set `A`, two slots, an environment aligned with `A`, a formula of arity `k`, and the equation identifying the code slot with the key of that formula. It fills both conjuncts. ```agda module _ (A : S) where codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → (ψ : Formula ⟪ fst A ⟫ k) → fst (lookup c γ) ≡ fst (keyS A ψ) → ⟨ γ ⊨ isCodeAnyAt c w ⟩ ``` The two conjuncts are filled by their own inward readings: the arity reading names the natural number and the code, and the witness reading confirms the formula is over the aligned alphabet. ```agda codeAnyAt-in {k = k} c w γ qw ψ qc = arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc ``` The outward reading recovers the truncated code witness: some arity and some formula produce this key. The truncated data stays inside propositional truncation. ```agda codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A → ⟨ γ ⊨ isCodeAnyAt c w ⟩ → ⟨ IsKeyOverAny A (lookup c γ) ⟩ codeAnyAt-out c w γ qw (hk , hw) = ``` The proof eliminates the arity reading into a pair of a natural number and a code, then maps the witness reading into the code-level truncated existence. ```agda PT.rec squash₁ step (arityNumAtL-out c γ hk) where step : Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z)) → ⟨ IsKeyOverAny A (lookup c γ) ⟩ step (m , (z , qz)) = PT.map (λ { (ψ , q) → m , (ψ , q) }) ``` The witness-reading elimination recovers the formula and the code equation at the correct arity, completing the truncated existence. ```agda (witnessAt-out A w c γ qw hw m z qz) ``` ## The set, in one extension `CodesAt c w` does not construct a code set. Through `extAt`, it describes the set already occupying slot `c`: an element belongs to that set exactly when it is the key of some finite-arity formula over the carrier in slot `w`. This determines the slot value extensionally as `AllCodes A`, while every formula witness used in the membership reading remains propositionally truncated. ```agda CodesAt : ∀ {n} → Fin n → Fin n → Formula S n CodesAt c w = extAt c (isCodeAnyAt zero (suc w)) ``` The outward reading of the code set says that the slot holds exactly the code set of the working alphabet. The proof is by extensionality in two directions. ```agda module _ (A : S) {n : ℕ} (c w : Fin n) (γ : S ^ n) (qw : fst (lookup w γ) ≡ fst A) where CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A CodesAt-out h = extensionalL step where ``` For the first inclusion, `codeAnyAt-out` turns membership in the described slot into the propositionally truncated assertion that the element is a formula key. `AllCodes-in` turns precisely that assertion into membership in the fixed meta-language set `AllCodes A`; no particular decoding is selected. ```agda step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A) step x = ⇔toPath (λ hx → AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw (extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx))) ``` For the reverse inclusion, membership in `AllCodes A` gives only the propositional truncation of an arity and a formula whose key is the given element. Since satisfaction of the per-code formula is itself a proposition, the proof may eliminate that truncation there and apply `codeAnyAt-in`. No distinguished decoding is extracted. ```agda (λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x (PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , q)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q }) (AllCodes-out A x hx))) ``` Conversely, suppose the value in slot `c` is equal to `AllCodes A`. To prove `CodesAt`, it remains to establish the two membership implications required by the extension formula: a member of the slot satisfies the per-code predicate, and anything satisfying that predicate belongs to the slot. ```agda CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩ CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back where into : (x : S) → ⟨ fst x ∈ fst (lookup c γ) ⟩ → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩ ``` For the first implication, the equality of sets turns slot membership into membership in `AllCodes A`. The latter supplies a formula witness only under propositional truncation, which may be eliminated into the proposition expressing satisfaction of `isCodeAnyAt`. ```agda into x hx = PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w))) (λ { (k , (ψ , qk)) → codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk }) (AllCodes-out A x (subst (λ u → ⟨ fst x ∈ fst u ⟩) q hx)) ``` For the converse implication, `codeAnyAt-out` turns satisfaction into the truncated assertion that the candidate is some formula key. `AllCodes-in` uses precisely that assertion to prove membership in `AllCodes A`, and the set equality transports the result back to slot `c`. ```agda back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩ → ⟨ fst x ∈ fst (lookup c γ) ⟩ back x hx = subst (λ u → ⟨ fst x ∈ fst u ⟩) (sym q) (AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx)) ``` ## The order at a stage, unfolded once At an ordinal `δ`, the already constructed order `orderAt δ` compares members of `Lset δ`. Transporting that order to the small carrier expected by the naming construction lets `stepAt δ` build the local strict well-order `stepOrder δ` on `New δ`, the members of `Lset (sucV δ)`. ```agda stepOrder : (δ : V ℓ) → IsOrd δ → SWO (New δ) stepOrder δ oδ = stepAt δ (carry (Lset δ) (orderAt δ oδ)) ``` If `δ ≡ δ'`, an `Under` comparison at `δ` transports to one at `δ'`. The dependent pair path also reconciles the two proofs that the carrier is ordinal; this is valid because `IsOrd` is a proposition. Thus the transported comparison does not depend on a chosen ordinality certificate. ```agda stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ) → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y stepMoved δ δ' e o o' x y = subst (λ p → Under (fst p) (stepOrder (fst p) (snd p)) x y) (Σ≡Prop isPropIsOrd {u = δ , o} {v = δ' , o'} e) ``` Suppose the birth ordinal of a constructible set `x` belongs to an ordinal `α`. Then the successor of that birth is either a member of `α` or equal to `α`. Since `x` belongs to the level at that successor, either alternative places `x` in `Lset α`. ```agda bornIn : (α : V ℓ) → IsOrd α → (x : V ℓ) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ α ⟩ → ⟨ x ∈ Lset α ⟩ bornIn α oα x p h = reach (suc∈or≡ (birth x p) α (birth-ord x p) oα h) where reach : ⟨ sucV (birth x p) ∈ α ⟩ ⊎ (sucV (birth x p) ≡ α) → ⟨ x ∈ Lset α ⟩ ``` The two alternatives supplied by `suc∈or≡` finish the argument. If the successor birth belongs to `α`, monotonicity carries `birth-mem` up to `Lset α`; if it equals `α`, transport along the equality gives the same membership directly. ```agda reach (inl k) = Lset-mono {α = α} {β = sucV (birth x p)} k {x = x} (birth-mem x p) reach (inr e) = subst (λ w → ⟨ x ∈ Lset w ⟩) e (birth-mem x p) ``` Now fix an ambient ordinal `α`. Every member of `Lset α` has a birth ordinal below `α`, so the earlier-stage orders needed by the recursive equation for `orderAt α` are available at exactly the required indices. This lets us state the equation as a direct comparison of the two members' births. ```agda module _ (α : V ℓ) (oα : IsOrd α) where private module Fam = Family α (λ δ _ → orderAt δ) oα ``` Every layer member is constructible, by the layer's constructibility and transitivity along membership. ```agda memberL : (a : Mem (Lset α)) → ⟨ isL (fst a) ⟩ memberL a = Lset→isL α oα (fst a) (snd a) ``` Because every member `a` of `Lset α` is constructible, it has a birth ordinal. We write this ordinal as `bornOf a`; it will be the primary key when the order at `α` is unfolded. ```agda bornOf : (a : Mem (Lset α)) → V ℓ bornOf a = birth (fst a) (memberL a) ``` The fact `bornOf a ∈ α` has two roles. It confirms that the birth ordinal is available as an earlier index in the unfolding of `orderAt α`, and later it lets `bornIn` recover `a` as a member of the ambient stage from an object-language birth description. ```agda bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩ bornMem a = Fam.bornAt a .snd ``` The unfolding equation is the connection point of the chapter. It says: the order at `α` holds between `a` and `b` exactly when either the birth ordinal of `a` is strictly below that of `b`, or they share the same birth ordinal and the local step order at that birth ordinal places `a` below `b`. ```agda order-unfold : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b ≡ ( ⟨ bornOf a ∈ bornOf b ⟩ ⊎ ( (bornOf b ≡ bornOf a) × Under (bornOf a) (stepOrder (bornOf a) ``` The proof uses `orderAt-step` to expose one layer of the membership recursion and then applies congruence to its underlying relation. It therefore derives the two-case equation from the order constructed in the previous chapter; it does not construct or reprove that strict well-order here. ```agda (mem-ord {A = α} oα (bornOf a) (bornMem a))) (fst a) (fst b) ) ) order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α) ``` The member-to-carrier wrapper packages each layer member as a carrier element, so that the formula environment can hold it. ```agda opaque memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S memS α oα a = fst a , memberL α oα a ``` The first-projection equation confirms the packaging preserves the underlying set. ```agda memS-fst : (α : V ℓ) (oα : IsOrd α) (a : Mem (Lset α)) → fst (memS α oα a) ≡ fst a memS-fst α oα a = refl ``` The birth presentation packages the birth ordinal with the constructibility transported from the enclosing ordinal `α`. ```agda bornS : (α : V ℓ) (oα : IsOrd α) → ⟨ isL α ⟩ → Mem (Lset α) → S bornS α oα pα a = bornOf α oα a , isL-trans {x = α} {y = bornOf α oα a} (bornMem α oα a) pα ``` The first-projection equation confirms the packaging preserves the birth ordinal. ```agda bornS-fst : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ bornOf α oα a bornS-fst α oα pα a = refl ``` The birth equation confirms the packaged birth matches the computed birth of the packaged member. ```agda bornS-birth : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α)) → fst (bornS α oα pα a) ≡ birth (fst (memS α oα a)) (snd (memS α oα a)) bornS-birth α oα pα a = refl ``` ## The order described, with the step as a parameter The step-formula type is a four-slot formula family, parameterized by the carrier slot, the table slot, and the two comparison slots. ```agda StpFo : Type (ℓ-suc ℓ) StpFo = ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n ``` The outward adequacy reading is relative to an ordinal carrier `d`, a table `f`, and two compared objects. Its table hypothesis says that every value `r` recorded at `d` realizes the stage relation `IsRel d r`. From satisfaction of `Stp` it concludes only the propositional truncation of the corresponding `Under` comparison. ```agda StpOut StpIn : StpFo → Type (ℓ-suc ℓ) StpOut Stp = ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → ((r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r) → ⟨ γ ⊨ Stp d f u v ⟩ ``` The outward direction deliberately returns `∥ Under ... ∥₁`, so it supplies existence of a local comparison without selecting a canonical witness. The inward direction has different input: the caller provides one particular value `r`, evidence that the table records it at `d`, and a proof that `r` realizes the relation there. ```agda → ∥ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ StpIn Stp = ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) → (r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst (lookup d γ)) r ``` The inward reading produces the formula satisfaction from the specific table entry and the `Under` comparison. ```agda → Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ ``` The module `Ordered` assumes an abstract step formula together with these two readings. Everything that follows is therefore a conditional translation of the birth-first rule: it proves the adequacy of the whole stage comparison from the adequacy of the same-birth comparison, without claiming here that any concrete step formula satisfies the interface. ```agda module Ordered (Stp : StpFo) (stp-out : StpOut Stp) (stp-in : StpIn Stp) where ``` The four newly bound objects are the compared sets `u,v` and their candidate birth ordinals `du,dv`. The first two clauses assert `BirthAt du u` and `BirthAt dv v`; at this point those clauses identify births only when the later reading supplies ordinality of `du` and `dv`. ```agda OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n)))) OrdBody tb f = BirthAt (suc zero) (sh3 zero) ∧̇ ( BirthAt zero (sh2 zero) ∧̇ ( (var (suc zero) ∈̇ tm4 tb) ``` The next two clauses require both candidate births to belong to the stage denoted by `tb`. The final disjunction reproduces the birth-first rule: either `du ∈ dv`, or `dv ≡ du` and the supplied step formula compares `u` with `v` at that common carrier. No object-membership relation between `u` and `v` is asserted here. ```agda ∧̇ ( (var zero ∈̇ tm4 tb) ∧̇ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) ) ``` `CondCore` first existentially binds the two compared objects `u` and `v`. The pair formula requires the argument in slot `z` to be their ordered pair. Two further existential quantifiers bind their candidate births before `OrdBody` checks the birth-first comparison. All four witnesses occur under the satisfaction semantics of existential formulas and are therefore propositionally truncated. ```agda opaque CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n CondCore z tb f = ∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) ) ``` ## What the description says, both ways To read `CondCore`, fix the ordinal stage denoted by `tb` and a table over that stage. `Values` guarantees that every recorded value realizes the appropriate local relation, while `Entries` says merely that some value is recorded at every carrier below the stage. These are exactly the hypotheses later used in the two directions. ```agda module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : S ^ n) (oα : IsOrd (fst (⟦ tb ⟧ γ))) (vals : Values (lookup f γ) (fst (⟦ tb ⟧ γ))) (ents : Entries (lookup f γ) (fst (⟦ tb ⟧ γ))) where private ``` The stage ordinal is named for direct reference. ```agda α : V ℓ α = fst (⟦ tb ⟧ γ) ``` The shifting lemma confirms that the four-slot renaming preserves the denotation of the stage term. ```agda shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ shift u v du dv = tm4-val tb u v du dv γ ``` For a carrier `d` below `α`, `Entries` supplies only a propositionally truncated table value. The helper may eliminate that truncation into any proposition `P`: for each recovered `r`, `Values` proves `IsRel d r`, and the continuation uses the recorded pair together with that proof to establish `P`. ```agda value : (d : S) → ⟨ fst d ∈ α ⟩ → (P : hProp (ℓ-suc ℓ)) → ((r : S) → ⟨ pr (fst d) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst d) r → ⟨ P ⟩) → ⟨ P ⟩ value d hd P k = PT.rec (snd P) ``` Concretely, `ents d hd` gives the truncated pair consisting of a value `r` and its table entry. Propositional truncation is eliminated only because `P` is an `hProp`; `vals` then supplies the relation-realization proof required by the continuation. The construction does not select a table value outside that proposition. ```agda (λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd) ``` The deep satisfaction type reads the ordered body at the four-slot environment built from the two comparison objects and their birth ordinals. ```agda Deep : (u v du : S) → S → Type (ℓ-suc ℓ) Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩ ``` The two readings use the same defining equation of `CondCore` in opposite directions. Outward, the four existential bindings are decoded into a pair and two birth candidates; inward, an existing `Related` comparison supplies those bindings. The equal-birth branch is the only point where the assumed readings of `Stp` enter. ```agda opaque unfolding CondCore ``` The outward reading opens the four nested existential witnesses in order: the compared objects `u,v`, then their candidate births `du,dv`. Each witness is available only through propositional truncation, and each elimination targets `Related α ...`, which is a proposition. The innermost data is then passed to the mathematical comparison argument. ```agda CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α (fst (lookup z γ)) ⟩ CondCore-out = PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (u , hv) → PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (v , (hp , hdu)) → PT.rec (snd (Related α (fst (lookup z γ)))) (λ { (du , hdv) → PT.rec (snd (Related α (fst (lookup z γ)))) ``` The local name `Goal` records the proposition that the argument in slot `z` satisfies the meta-level predicate `Related α`. The pair equation and the satisfaction of `OrdBody` for the four recovered witnesses are the two ingredients passed to `atDeep`; the remaining proof will turn them into that relatedness proposition. ```agda (λ { (dv , hd) → atDeep u v du dv hp hd }) hdv }) hdu }) hv }) where Goal : Type (ℓ-suc ℓ) Goal = ⟨ Related α (fst (lookup z γ)) ⟩ ``` After the four existential witnesses have been opened into the proposition `Related`, the outward proof has two pieces of information: `hp` says that the argument is the coded pair of `u` and `v`, while the deep record says that `du,dv` are candidate births below the ambient stage and satisfy the birth-first comparison. The witnesses are used only inside this propositional target; the proof does not select a canonical pair or canonical birth data. ```agda atDeep : (u v du dv : S) → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ → Deep u v du dv → Goal atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) = subst (λ w → ⟨ Related α w ⟩) (sym qz) ``` Adequacy of the pairing formula identifies the set in slot `z` with `pr (fst u) (fst v)`. It is this equality, rather than an equality between `u` and `v`, that lets the proof change its target to `Related α` of the represented pair and analyze the birth comparison there. ```agda (PT.rec (snd (Related α (pr (fst u) (fst v)))) atCase hcmp) where qz : fst (lookup z γ) ≡ pr (fst u) (fst v) qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp ``` The membership of the first birth stage in the ordinal is transported along the shift of environments: the shifted and unshifted readings of the birth stage agree on the underlying set. ```agda hmu : ⟨ fst du ∈ α ⟩ hmu = subst (λ w → ⟨ fst du ∈ fst w ⟩) (shift u v du dv) hmu₀ ``` The second birth stage is transported by the same shift, so both birth stages are known to belong to the ordinal. ```agda hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (shift u v du dv) hmv₀ ``` The first birth stage is an ordinal: it belongs to the ordinal, and members of ordinals are ordinals. ```agda odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu ``` The second birth stage is an ordinal by the same argument. ```agda odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv ``` The reading lemma of the birth formula now applies to the first birth stage: with its ordinalness, the satisfaction of the birth formula identifies the recorded stage with the true birth ordinal of the first object. ```agda qu : fst du ≡ birth (fst u) (snd u) qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu ``` The same reading applies to the second birth stage and the second object. ```agda qv : fst dv ≡ birth (fst v) (snd v) qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv ``` The first object can now be regarded as a member of `Lset α`. Its constructibility evidence is already carried by `u`; the new fact is membership in the ambient level, obtained from `bornIn` because the identified birth ordinal belongs to `α`. ```agda a : Mem (Lset α) a = fst u , bornIn α oα (fst u) (snd u) (subst (λ w → ⟨ w ∈ α ⟩) qu hmu) ``` The second object is packaged identically. ```agda c : Mem (Lset α) c = fst v , bornIn α oα (fst v) (snd v) (subst (λ w → ⟨ w ∈ α ⟩) qv hmv) ``` The packaged member `a` carries the same underlying set as `u`, although its constructibility proof was obtained through stage membership. Proof irrelevance for that evidence, expressed by `birth-proof`, shows that its computed birth agrees with the birth computed from `u`; composing with `qu` identifies it with the recorded stage `du`. ```agda qa : bornOf α oα a ≡ fst du qa = birth-proof (fst u) (memberL α oα a) (snd u) ∙ sym qu ``` The birth ordinal of the packaged second object agrees with the recorded second birth stage. ```agda qc : bornOf α oα c ≡ fst dv qc = birth-proof (fst v) (memberL α oα c) (snd v) ∙ sym qv ``` It remains to prove the meta-language comparison `relOf (orderAt α oα) a c`. The order-table interface then maps that comparison to the proposition that the coded pair of the two underlying sets belongs to `Related α`. No object-language relation has yet been chosen at this step. ```agda fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (fst u) (fst v)) ⟩ fill = related-in α oα a c ``` The comparison encoded by `OrdBody` has exactly the two branches in the one-step unfolding of `orderAt`. If `du ∈ dv`, the identifications `qa` and `qc` turn this into the earlier-birth branch for `a` and `c`; transporting through `order-unfold` then gives their stage-order comparison. ```agda atCase : ⟨ fst du ∈ fst dv ⟩ ⊎ ( (fst dv ≡ fst du) × ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ ) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atCase (inl h) = fill (transport (sym (order-unfold α oα a c)) ``` In the equal-birth branch, `OrdBody` supplies satisfaction of the abstract formula `Stp`. Applying `stp-out` with the ordinality of the common birth and the `Values` hypothesis yields only a propositionally truncated `Under` comparison. That truncation may be eliminated into `Related`, which is a proposition; the argument neither inspects how `Stp` obtained a table value nor extracts such a value. ```agda (inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym qa) (sym qc) h))) atCase (inr (e , hs)) = PT.rec (snd (Related α (pr (fst u) (fst v)))) atUnder (stp-out (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) odu (λ r hr → vals du r hmu hr) hs) ``` Given an `Under` comparison at the recorded common birth, the proof must align it with the birth attached to the packaged member `a`. Once aligned, it supplies the equal-birth branch of `order-unfold`; the resulting `orderAt` comparison is then represented by `Related`. ```agda where atUnder : Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) → ⟨ Related α (pr (fst u) (fst v)) ⟩ atUnder und = fill (transport (sym (order-unfold α oα a c)) (inr (qc ∙ e ∙ sym qa ``` The alignment uses the equality `qa` between the two carrier ordinals. `stepMoved` transports the local comparison along this equality and reconciles the two ordinalness proofs by proof irrelevance. It does not use transitivity of the shared ordinal and does not create a new local order. ```agda , stepMoved (fst du) (bornOf α oα a) (sym qa) odu (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) (fst u) (fst v) und))) ``` For the inward direction, `Related α z` contains an ordinalness proof and, under propositional truncation, two members `a,c` of `Lset α`, an equation saying that `z` is their coded pair, and their `Ordering` comparison. `Pairs` names precisely this payload so that it can be eliminated only into the satisfaction proposition being constructed. ```agda private Pairs : IsOrd α → Type (ℓ-suc ℓ) Pairs o = Σ[ a ∈ Mem (Lset α) ] ∥ (Σ[ c ∈ Mem (Lset α) ] ( (fst (lookup z γ) ≡ pr (fst a) (fst c)) × ⟨ Ordering α o a c ⟩ )) ∥₁ ``` The inward reading eliminates the truncated contents of `Related` into satisfaction of `CondCore`. Once an ordinalness proof and a represented pair are available locally, `atRel` reconstructs the four existential witnesses and the birth-first comparison; no global choice of a represented pair is produced. ```agda CondCore-in : ⟨ Related α (fst (lookup z γ)) ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ CondCore-in = PT.rec (snd (γ ⊨ CondCore z tb f)) atOrd where atRel : (o : IsOrd α) (a c : Mem (Lset α)) → fst (lookup z γ) ≡ pr (fst a) (fst c) ``` The ambient ordinalness `oα` is already a hypothesis of the whole reading. Here the local proof instead extracts the constructibility component `pα` from the value of the stage term, then asks the table for a value at the first member's birth. Because the target is a satisfaction proposition, the merely existing table value can be eliminated into it. ```agda → ⟨ Ordering α o a c ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩ atRel o a c q hord = value (bornS α oα pα a) hmu (γ ⊨ CondCore z tb f) atValue where pα : ⟨ isL α ⟩ ``` Every term is interpreted in the structure `𝒮ʟ`, whose elements pair an underlying set with evidence of constructibility. Thus the second projection of `⟦ tb ⟧ γ` supplies `isL α`; this is part of the semantic value of the term, rather than a separate satisfaction assumption. ```agda pα = snd (⟦ tb ⟧ γ) ``` The witnesses for `CondCore` are now chosen locally: `u,v` package the two stage members as elements of `𝒮ʟ`, and `du,dv` package their actual birth ordinals. These are witnesses for this proof of a proposition, not canonical choices exported from `Related`. ```agda u v du dv : S u = memS α oα a v = memS α oα c du = bornS α oα pα a dv = bornS α oα pα c ``` For every member of `Lset α`, its true birth ordinal lies below `α`. Since the first projection of `bornS` is that ordinal, the same membership statement holds for the value placed in slot `du`; this is the form inspected by the object-language clause. ```agda hmu : ⟨ fst du ∈ α ⟩ hmu = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα a)) (bornMem α oα a) ``` The birth stage of the second member belongs to the ordinal by the same transport. ```agda hmv : ⟨ fst dv ∈ α ⟩ hmv = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα c)) (bornMem α oα c) ``` The first birth stage is an ordinal, since it lies inside the ordinal. ```agda odu : IsOrd (fst du) odu = mem-ord {A = α} oα (fst du) hmu ``` The second birth stage is an ordinal by the same reading. ```agda odv : IsOrd (fst dv) odv = mem-ord {A = α} oα (fst dv) hmv ``` Unfolding the already constructed stage order yields its two-branch lexicographic rule. Either `a` was born strictly before `c`, or their births agree and the local `stepOrder` at that common birth places the underlying set of `a` below that of `c`. ```agda cmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) ) ``` The comparison is obtained by transporting the strict reading along the identification of the two ordinalness proofs, since ordinalness is a proposition and the two proofs describe the same ordinal. ```agda cmp = transport (order-unfold α oα a c) (strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩) (isPropIsOrd α o oα) hord)) ``` The equation contained in `Related` identifies the argument with the ordered pair of the underlying sets of `a` and `c`. The first-projection equations for `memS` rewrite those endpoints as the values placed in slots `u` and `v`, giving exactly the pairing clause required by `CondCore`. ```agda hp : ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩ hp = subst ⟨_⟩ (sym (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ))) (q ∙ cong₂ pr (sym (memS-fst α oα a)) (sym (memS-fst α oα c))) ``` To fill the first `BirthAt` clause, the inward reading supplies both facts that its adequacy lemma requires: `du` is ordinal, and its underlying set is exactly the birth ordinal of `u`. The formula itself still does not assert ordinality or choose a least stage. ```agda hbu : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt (suc zero) (sh3 zero) ⟩ hbu = BirthAt-in (suc zero) (sh3 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu (bornS-birth α oα pα a) ``` The birth formula for the second birth stage is filled at the same deep environment. ```agda hbv : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt zero (sh2 zero) ⟩ hbv = BirthAt-in zero (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odv (bornS-birth α oα pα c) ``` In the equal-birth branch, `cmp` supplies an `Under` comparison on the actual birth carrier of `a` and on the underlying sets of `a,c`. The step formula, however, is read at the packaged values `du,u,v`, so the carrier and both endpoints must be transported to those representations. ```agda moved : Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) → Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v) moved und = subst2 (λ p r → Under (fst du) (stepOrder (fst du) odu) p r) ``` The endpoint transports use the exposed underlying-set equations for `memS`. The carrier transport uses `bornS-fst` and `stepMoved`, whose dependent path also identifies the two proofs of ordinality because `IsOrd` is a proposition. No transitivity argument is involved. ```agda (sym (memS-fst α oα a)) (sym (memS-fst α oα c)) (stepMoved (bornOf α oα a) (fst du) (sym (bornS-fst α oα pα a)) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) odu (fst a) (fst c) und) ``` `Entries` provides a merely existing table value `r` at the first birth, and `Values` proves that any such recorded value realizes `IsRel`. For each local payload, `atValue` constructs satisfaction of `CondCore` by inserting the two members and their two births. The table value is passed specifically to `stp-in` in the equal-birth branch; it is not made into a globally chosen value. ```agda atValue : (r : S) → ⟨ pr (fst du) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst du) r → ⟨ γ ⊨ CondCore z tb f ⟩ atValue r hr hrel = ∣ u , ∣ v , (hp , ∣ du , ∣ dv , (hbu , (hbv , (hmu₀ , (hmv₀ , side)))) ∣₁ ∣₁) ∣₁ ∣₁ where ``` Inside `OrdBody`, four new binders lie in front of the original environment, so the stage term appears as `tm4 tb`. The shift equation proves that this raised term still denotes `α`; it therefore transports the known membership of the first birth into the exact form required by the object-language clause. ```agda hmu₀ : ⟨ fst du ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmu₀ = subst (λ w → ⟨ fst du ∈ fst w ⟩) (sym (shift u v du dv)) hmu ``` The second birth stage is transported by the same shift equation. ```agda hmv₀ : ⟨ fst dv ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩ hmv₀ = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (sym (shift u v du dv)) hmv ``` The remaining clause must reproduce the same two branches obtained from `order-unfold`: earlier birth, or equal birth followed by the local step comparison. The helper keeps this case split inside the satisfaction proposition, where the witnesses and any truncated table entry may legitimately be used. ```agda atCmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩ ⊎ ( (bornOf α oα c ≡ bornOf α oα a) × Under (bornOf α oα a) (stepOrder (bornOf α oα a) (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))) (fst a) (fst c) ) ``` In the earlier-birth branch, the exposed equations for `bornS` rewrite the meta-language membership between the true births as membership between `du` and `dv`. The result is injected into the left side of the object-language disjunction, whose satisfaction is propositionally truncated. ```agda → ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ atCmp (inl h) = ∣ inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym (bornS-fst α oα pα a)) (sym (bornS-fst α oα pα c)) h) ∣₁ ``` In the equal-birth branch, the birth equality is rewritten to an equality between `dv` and `du`. The inward adequacy hypothesis `stp-in` then uses the particular recorded value `r`, its table membership, its `IsRel` proof, and the transported `Under` comparison to fill the local step formula. This is precisely the direction in which a concrete local table value is available. ```agda atCmp (inr (e , und)) = ∣ inr ( bornS-fst α oα pα c ∙ e ∙ sym (bornS-fst α oα pα a) , stp-in (suc zero) (sh4 f) (sh3 zero) (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu r hr hrel (moved und) ) ∣₁ ``` Applying this two-branch translation to `cmp` completes the comparison clause of `OrdBody`. Together with the two birth descriptions and the two bounds below `α`, it supplies the deep record required by `CondCore`; it adds no further choice or order-theoretic claim. ```agda side : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero) ∨̇ ( (var zero ≐ var (suc zero)) ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩ side = atCmp cmp ``` The pair-level assembly eliminates the truncated existence of the second member: for each candidate `c` related to `a`, the local assembly produces the satisfaction of the core clause. ```agda atPairs : (o : IsOrd α) → Pairs o → ⟨ γ ⊨ CondCore z tb f ⟩ atPairs o (a , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (λ { (c , (q , hord)) → atRel o a c q hord }) h ``` The outer payload of `Related` supplies an ordinalness proof `o` and only the propositional truncation of `Pairs o`. Since satisfaction of `CondCore` is a proposition, `atOrd` may eliminate this truncation and pass each represented pair to `atPairs`. Independence from the particular ordinalness proof is used earlier, when `o` is identified with the ambient proof `oα` through `isPropIsOrd`. ```agda atOrd : Σ[ o ∈ IsOrd α ] ∥ Pairs o ∥₁ → ⟨ γ ⊨ CondCore z tb f ⟩ atOrd (o , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (atPairs o) h ``` The specification identifies the satisfaction of the core clause with the relation of the coded pair, as paths of propositions in both directions. ```agda CondCore-spec : (γ ⊨ CondCore z tb f) ≡ Related α (fst (lookup z γ)) CondCore-spec = ⇔toPath CondCore-out CondCore-in ``` ## The frame's two hypotheses, discharged `Cond` is the form used when the stage and table already occupy variable slots in an ambient environment. The new zeroth slot is reserved for the coded pair being tested, while the old stage and table indices are raised past it. Thus `Cond` introduces no witness for the stage; it refers to the stage already supplied by the surrounding context. ```agda Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n) Cond b f = CondCore zero (var (suc b)) (suc f) ``` `Cond₀ B F` is the constant-stage form needed by separation. Its sole existential binder supplies a table value and the equality clause pins that value to the fixed constant `F`; the stage is already the constant term `B`. The remaining free slot holds the coded pair under test. The later specification proves that this form and `Cond` describe the same `Related` comparison, still relative to the supplied `StpOut` and `StpIn`; neither form constructs the stage order itself. ```agda Cond₀ : S → S → Formula S 1 Cond₀ B F = ∃̇ ( (var zero ≐ con F) ∧̇ CondCore (suc zero) (con B) zero ) ``` The variable form tests a possible ordered pair `z` while the stage and the table remain in the ambient environment. Assuming that the stage is ordinal and that the table has the stated value and entry readings, its adequacy equation identifies satisfaction of `Cond` with the host-side class `Related`. Thus this formula describes the already constructed stage comparison; it does not construct a new order. ```agda cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z) cond-spec b f γ ob vals ents z = ``` Prepending `z` moves every old environment slot one place to the right. Consequently the core reads `z` at slot zero, the stage through `var (suc b)`, and the table through `suc f`. With precisely these shifts, the general `CondCore` equation gives the desired variable-form equation directly. ```agda CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents ``` For separation, the ambient environment contains only the candidate `z`, so the constant form must bind the table it consults. A bound element `c` is suitable when its underlying set equals that of the fixed table `F` and the core comparison holds with `c` in the table slot. The auxiliary proposition `Held c` packages exactly these two facts; `c` is a table representative, not a formula code. ```agda module _ (B F : S) (oB : IsOrd (fst B)) (vals : Values F (fst B)) (ents : Entries F (fst B)) (z : S) where private Held : S → Type (ℓ-suc ℓ) Held c = (fst c ≡ fst F) ``` In the two-slot environment `c ∷ z ∷ []`, slot zero is the bound table representative and slot one is the possible ordered pair. The stage is supplied by the constant term `con B`. This arrangement lets the same core express the constant case; when it is read outward, the table readings for `F` must be transferred to the extensionally equal representative `c`. ```agda × ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩ ``` The outward direction starts from a propositionally truncated existential witness for the bound table. Since `Related` is itself a proposition, the truncation may be eliminated into that target. The helper `atHeld` reasons under a temporary representative `c` and its two `Held` facts; no representative escapes this proof, so the argument produces neither a canonical witness nor a choice function. ```agda cond₀-out : ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ → ⟨ Related (fst B) (fst z) ⟩ cond₀-out = PT.rec (snd (Related (fst B) (fst z))) atHeld where atHeld : Σ[ c ∈ S ] Held c → ⟨ Related (fst B) (fst z) ⟩ atHeld (c , (qc , hc)) = ``` The equality `qc` lets the two table readings cross between the bound representative and `F`, but in opposite directions. An entry assumed in `c` is transported to `F` before `vals` identifies its value as a realization of the stage relation. Conversely, `ents` supplies a propositionally truncated entry in `F`, and mapping under that truncation transports the entry back to `c`. ```agda CondCore-out (suc zero) (con B) zero (c ∷ z ∷ []) oB (λ x r hx hp → vals x r hx (subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) qc hp)) (λ x hx → PT.map (λ { (r , hr) → r , subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) (sym qc) hr }) ``` These transported readings are exactly the hypotheses required to read the core comparison outward. Applying them to `hc` yields the `Related` fact for `z`. The entry witness remains propositionally truncated throughout this passage, which is sufficient because both the core satisfaction and the resulting relation claim are propositions. ```agda (ents x hx)) hc ``` For the inward direction there is already a specified table `F`, so it can serve as the existential witness and its equality with the constant table is reflexive. The core inward reading then turns the given `Related` fact into satisfaction with `F` in the table slot. This constructs a witness inside propositional truncation; it does not extract one from truncated information or assert that table representatives are uniquely chosen. ```agda cond₀-in : ⟨ Related (fst B) (fst z) ⟩ → ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ cond₀-in h = ∣ F , (refl , CondCore-in (suc zero) (con B) zero (F ∷ z ∷ []) oB vals ents h) ∣₁ ``` The two implications give a path between the satisfaction proposition for `Cond₀ B F` and `Related (fst B) (fst z)`. Hence the constant formula has exactly the same mathematical reading as the variable form under the same ordinality, value, and entry hypotheses. This equality concerns proposition-valued meanings; it does not identify the two formulas syntactically or choose a distinguished presentation of the table. ```agda cond₀-spec : (B F : S) → IsOrd (fst B) → Values F (fst B) → Entries F (fst B) → (z : S) → ((z ∷ []) ⊨ Cond₀ B F) ≡ Related (fst B) (fst z) cond₀-spec B F oB vals ents z = ⇔toPath (cond₀-out B F oB vals ents z) (cond₀-in B F oB vals ents z) ``` The generic table construction can now use `Cond` when the stage and table occupy variable slots and `Cond₀` when they are fixed constants. Its resulting relation objects represent the comparison underlying the previously constructed strict well-order `orderAt`; no well-order is rebuilt here. Every result remains relative to `StpOut` and `StpIn` for the abstract step formula. `InternalWellOrder` later supplies those two readings for the concrete step and thereby removes this remaining parameter. ```agda open Described Cond Cond₀ cond-spec cond₀-spec public ``` ## Recap The chapter has described, in the object language, the relation underlying the previously constructed stage order. `BirthAt` identifies a birth ordinal only under an external ordinality hypothesis, `CodesAt` determines the moving code set only extensionally, and `CondCore` matches the birth-first comparison only relative to `StpOut`, `StpIn`, `Values`, and `Entries`. All existential, decoding, table-value, and `Under` witnesses remain within propositional truncation. The next chapter supplies the concrete step formula and its two readings.