--- title: "The internal stage-order relation" module: L.Choice.InternalWellOrder lang: en site: "Bedrock" description: "The internal canonical well-order" stage: "The canonical well-order and Choice" reading_order: 83 canonical: https://bedrock.institute/en/L.Choice.InternalWellOrder.html html: L.Choice.InternalWellOrder.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/InternalWellOrder.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.OrderTable, L.Choice.StageOrderAdequacy, L.Choice.NameComparisonAdequacy, L.Choice.EarliestDisagreement, L.Coding.HierarchySequence, L.Coding.DefinablePowerSet, L.Coding.Model, L.Coding.CodeSet, L.Hierarchy, L.WellOrder.Base, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/zh/L.Choice.InternalWellOrder.md, https://bedrock.institute/ja/L.Choice.InternalWellOrder.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The internal stage-order relation At each constructible stage, `orderAt` already gives a host-level strict well-order of its members. The task here is to make the underlying comparison available to formulas interpreted in `L`: for each ordinal stage, we obtain a relation set whose ordered-pair members correspond in both directions to `relOf (orderAt α oα)`. This constructs no new well-order and proves no object-language formula saying that the relation is a well-order. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` The distinction between the two levels will guide the chapter. The well-order is a mathematical structure in the host theory, whereas its representative inside `L` must be a set that the first-order language can mention. ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` The construction is carried out at an arbitrary universe level and assumes excluded middle only at the displayed successor level. All later relation sets inherit precisely this standing hypothesis. ```agda module L.Choice.InternalWellOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` To describe one comparison step internally, it suffices to combine variables and constants with membership, equality, conjunction, and existential quantification. The six existential binders introduced below are repeated uses of this one logical constructor. ```agda open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} ``` The relation will be indexed by an ordinal stage. Its witnesses must therefore be recognized as constructible sets, and successor-stage membership must be related to definability over the preceding stage. ```agda using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; Lset-suc ) open import L.Choice.FirstIntersectionStage {ℓ} lem using ( stageBound ) ``` The semantic target has two distinct levels. `orderAt δ od` is the host-level strict well-order on the members of `Lset δ`. For the equal-birth step used in its recursive description, `Under δ (stepOrder δ od) u v` records that `u` and `v` belong to `Lset (sucV δ)` and that the resulting members are related by `stepOrder δ od`. Least names over `Lset δ` connect this host-level step to the formula constructed below. ```agda open import L.Choice.StageOrders {ℓ} lem using ( Mem; New; relOf; carry; orderAt; Under ; stepAt-fill; stepAt-read; IsLeastName; leastNameOf ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming ) open import L.Choice.NameComparison {ℓ} lem using ( StepAt ) ``` The recursive order table already knows how to turn an adequate step description into a relation set. What remains is to give one concrete formula and prove its two semantic directions, so that the table no longer depends on an abstract step parameter. ```agda open import L.Choice.OrderTable {ℓ} lem using ( IsRel; ixRel-fill; ixRel-rep ) open import L.Choice.StageOrderAdequacy {ℓ} lem using ( CodesAt; CodesAt-in; CodesAt-out; stepOrder; module Ordered ; towerS; towerS-fst; powS; powS-fst; sh2; sh3; StpOut; StpIn ) open import L.Choice.NameComparisonAdequacy {ℓ} lem using ( module At ) ``` That formula must recognize four moving objects: the stage tower, its definable subsets, the table value at the stage, and the codes over the tower. These recognition clauses let an arbitrary satisfying assignment be converted back into the intended mathematical data. ```agda open import L.Choice.EarliestDisagreement {ℓ} lem using ( codeOrder; codeOrder-fill; codeOrder-rep ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) ``` Two further witnesses are fixed constants: the comparison relation on codes and the code set for the empty alphabet. Together with the moving relation value from the table, they supply the auxiliary relations and domains used when least names are compared. ```agda open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) ``` Satisfaction is interpreted in the propositional structure of constructible sets. Consequently, each existential clause yields a propositionally truncated dependent pair: a witness may support the proof while remaining unavailable as chosen data outside the proposition. ```agda import FOL.Absoluteness open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) ``` The comparison takes place among members of a successor stage. Presenting a stage by a small type lets the host well-order act on its members, while `sucV` records the successor ordinal used to locate the two compared objects. ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV ) ``` From this point on, formulas are evaluated in the first-order structure carried by `L`. Thus an element used in a slot contains both its underlying set and the proposition that the set is constructible. ```agda open hPropStructure 𝒮ʟ ``` We write `γ ⊨ φ` for this interpretation. Absoluteness permits the recognition formulas to be read as concrete facts about the underlying sets, which is what makes the later unpacking possible. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## The elements the description binds The six-slot shift moves every variable past the six existential witnesses of the step formula. ```agda private sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i))))) ``` After all six witnesses have been bound, `StepAt` directly refers to five of them: the tower `tw`, the table relation `rl`, the code set `cs`, the code order `ro`, and the empty-alphabet code set `c0`. The definable-power-set witness `pw` is used by the surrounding membership clauses rather than passed to `StepAt`. ```agda iTow iRel iCod iOrd iNil : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) iTow = suc (suc (suc (suc (suc zero)))) iRel = suc (suc (suc zero)) iCod = suc (suc zero) ``` The two nearest indices select `ro` and `c0`. They do not introduce further binders; they only record where these already bound witnesses occur in the fully extended environment. ```agda iOrd = suc zero iNil = zero ``` ## The description The six witnesses of `Stp d f u v` are introduced in dependency order. First comes a tower recognized at stage `d`; next comes its definable power set, whose membership clauses will certify that the objects at `u` and `v` are available for the successor-stage comparison. ```agda opaque Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n Stp d f u v = ∃̇ ( LsetGraphAt zero (suc d) ∧̇ ∃̇ ( DefAt zero (suc zero) ``` The third witness is a value `rl` recorded by the table at the stage, and the fourth is the code set over the tower. The last two witnesses are variables constrained by object equality to be the canonical code order and the code set for the empty alphabet. ```agda ∧̇ ( (var (sh2 u) ∈̇ var zero) ∧̇ ( (var (sh2 v) ∈̇ var zero) ∧̇ ∃̇ ( appAt (sh3 f) (sh3 d) zero ∧̇ ∃̇ ( CodesAt zero (sh3 zero) ∧̇ ∃̇ ( (var zero ≐ con codeOrder) ``` At the innermost point, `StepAt` sees seven semantic slots: the five auxiliary witnesses selected above and the two original objects shifted past all six binders. It asserts the comparison of their least names; it does not assert that the represented relation satisfies a well-order formula inside `L`. ```agda ∧̇ ∃̇ ( (var zero ≐ con (AllCodes ∅ʟ)) ∧̇ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ) ) ) ) ) ) ) ) ``` ## The six binders, layer by layer The reading module fixes the four slots, the environment, and the ordinalness of the decoded stage, since the host order needs that ordinalness. ```agda module Reading {n : ℕ} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) where private δ : V ℓ δ = fst (lookup d γ) ``` The host order is carried onto the presentation of the stage: the strict order of the members is available on the small index type. ```agda ordW : SWO ⟪ Lset δ ⟫ ordW = carry (Lset δ) (orderAt δ od) ``` A name for a set in `Lset (sucV δ)` is formed over `Lset δ` and becomes distinguished as least only relative to the carried order `ordW` on that preceding stage. The predicate `IsLeastName` records both that the name denotes the given set and that no competing name is smaller. This is the precise bridge between sets in the successor stage and the name comparison used by `StepAt`. ```agda module NM = Naming (Lset δ) ordW ``` The semantic goal is the propositionally truncated `Under` statement. It contains both successor-stage memberships and the step comparison, but reading the existential formula establishes only that such evidence exists; it does not choose names or any of the six bound objects as data. ```agda Goal : Type (ℓ-suc ℓ) Goal = ∥ Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ ``` After all six witnesses have extended the environment, `StepHolds tw pw rl cs ro c0` is exactly the satisfaction of the innermost `StepAt` formula. It is the final semantic condition inside the six existential layers. The surrounding binders, rather than `StepHolds` itself, place the successive witnesses under propositional truncation. ```agda opaque StepHolds : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) StepHolds tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ⟩ ``` The innermost payload contains the equation fixing `c0` and the step satisfaction itself. These are ordinary conjunctive evidence inside the payload; the propositional truncation is introduced by the surrounding existential layer. ```agda Six : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) Six tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con (AllCodes ∅ʟ)) ⟩ × StepHolds tw pw rl cs ro c0 ``` One layer outward, `ro` is fixed to the canonical code order, while the existence of a suitable `c0` is propositionally truncated. Equality determines the intended underlying set, but the proof does not expose a selected existential witness. ```agda Five : (tw pw rl cs ro : S) → Type (ℓ-suc ℓ) Five tw pw rl cs ro = ⟨ (ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con codeOrder) ⟩ × ∥ (Σ[ c0 ∈ S ] Six tw pw rl cs ro c0) ∥₁ ``` The code-set clause characterizes `cs` over the bound tower. When the formula is read, its adequacy and the earlier identification of the tower determine the underlying set of `cs`; the remaining inner witnesses still stay under propositional truncation. ```agda Four : (tw pw rl cs : S) → Type (ℓ-suc ℓ) Four tw pw rl cs = ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ × ∥ (Σ[ ro ∈ S ] Five tw pw rl cs ro) ∥₁ ``` The table-application clause says that `rl` is some value recorded at the decoded stage. In the reading direction `rl` is arbitrary among such recorded values, a fact that later forces the relation hypothesis to quantify over every value there; in the filling direction a particular supplied `rl` is used. ```agda Three : (tw pw rl : S) → Type (ℓ-suc ℓ) Three tw pw rl = ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ × ∥ (Σ[ cs ∈ S ] Four tw pw rl cs) ∥₁ ``` The definable-power-set clause identifies `pw`, and the next two conjuncts place both compared objects in it. Once `tw` and `pw` have been identified, these memberships become membership in `Lset (sucV δ)`, supplying the two domain components required by `Under`. ```agda Two : (tw pw : S) → Type (ℓ-suc ℓ) Two tw pw = ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ( ⟨ fst (lookup u γ) ∈ fst pw ⟩ × ( ⟨ fst (lookup v γ) ∈ fst pw ⟩ ``` After those memberships, the remaining payload begins with the truncated existence of the table value `rl`. The eventual target `Goal` is itself a proposition, so the proof may eliminate each truncation into that target without extracting a reusable choice of witness. ```agda × ∥ (Σ[ rl ∈ S ] Three tw pw rl) ∥₁ ) ) ``` The outermost payload starts with a witness `tw` satisfying the stage graph. Ordinality makes that description unique at the level of underlying sets, so an arbitrary satisfying `tw` can be identified with `Lset δ`; the nested existence of all later witnesses remains propositionally truncated. ```agda One : (tw : S) → Type (ℓ-suc ℓ) One tw = ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ × ∥ (Σ[ pw ∈ S ] Two tw pw) ∥₁ ``` ## The step adequacy at a stage Only five of the six bound elements enter `StepAt`; `pw` serves the two surrounding membership clauses. Accordingly, `Slots` identifies the tower and code set with their intended values, assumes that `rl` has the pairwise representation property `IsRel δ rl`, and fixes `ro` and `c0` to the two required constants. These facts are exactly what the earlier name-comparison adequacy theorem needs. ```agda module Slots (tw pw rl cs ro c0 : S) (qtw : fst tw ≡ Lset δ) (hrel : IsRel δ rl) (qcs : fst cs ≡ fst (AllCodes (LsetS δ od))) (qro : fst ro ≡ fst codeOrder) ``` Inside the alignment, the naming adequacy is instantiated at the stage, and its local step comparison is opened with the code order and the relation value, both directions of whose representation are supplied. ```agda (qc0 : fst c0 ≡ fst (AllCodes ∅ʟ)) where private module A6 = At (Lset δ) (snd (LsetS δ od)) ordW module L6 = A6.Least codeOrder rl codeOrder-rep codeOrder-fill (ixRel-rep δ od rl hrel) (ixRel-fill δ od rl hrel) ``` With those certifications, the name-comparison theorem is instantiated in the fully extended environment. Its seven semantic slots are the two compared objects together with the five auxiliary witnesses selected by `iTow`, `iRel`, `iCod`, `iOrd`, and `iNil`. ```agda module St = L6.Step iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) qro refl (Σ≡Prop (λ x → snd (isL x)) qtw) qcs qc0 ``` For the first object, `LeastFst t` is the local form of the assertion that `t` is its least name. Its denotation equation is oriented oppositely from the corresponding equation in `IsLeastName`; the conversion lemmas below reverse that equation while preserving the same minimality claim. ```agda LeastFst : NM.Name → Type (ℓ-suc ℓ) LeastFst = St.LeastOf (sh6 u) ``` `LeastSnd` gives the same bridge for the second object. Keeping the two predicates parallel matters because `StepAt` compares one least name with the other rather than merely asserting that least names exist. ```agda LeastSnd : NM.Name → Type (ℓ-suc ℓ) LeastSnd = St.LeastOf (sh6 v) ``` The exported predicate `IsLeastName` and the adequacy theorem state the interpreting equation in opposite directions. Path symmetry converts the first object's equation, and the minimality clause is transported by reversing each competing equation in the same way. ```agda leastFst-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup u γ)) → LeastFst t leastFst-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` The second object's conversion is identical in form. It changes only the orientation of equality and preserves the mathematical content of leastness. ```agda leastSnd-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup v γ)) → LeastSnd t leastSnd-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` In the reading direction, the same symmetry recovers `IsLeastName` for the first object. Since reversing a path twice restores its original orientation, this conversion loses no information. ```agda leastFst-out : (t : NM.Name) → LeastFst t → IsLeastName δ ordW t (fst (lookup u γ)) leastFst-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` The second least-name predicate is read back in the same way, leaving two ordinary least-name facts ready for the host-level step lemma. ```agda leastSnd-out : (t : NM.Name) → LeastSnd t → IsLeastName δ ordW t (fst (lookup v γ)) leastSnd-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` The two semantic directions for the innermost formula are deliberately asymmetric. Given two particular least names and their comparison, `holds-in` proves `StepHolds`. From `StepHolds`, `holds-out` returns only the propositionally truncated existence of two suitable least names and their comparison, so no chosen pair escapes the formula. ```agda opaque unfolding StepHolds ``` In the inward direction, the local least-name facts for `t₁` and `t₂`, together with `t₁ ≺ₙ t₂`, supply all the semantic content of the innermost formula. The name-comparison adequacy theorem turns precisely these three facts into `StepHolds`. ```agda holds-in : (t₁ t₂ : NM.Name) → LeastFst t₁ → LeastSnd t₂ → NM._≺ₙ_ t₁ t₂ → StepHolds tw pw rl cs ro c0 holds-in = St.StepAt-fill ``` Conversely, reading the innermost satisfaction yields, under propositional truncation, two least names and their name comparison. The truncation is essential: the result asserts the existence of suitable names without exporting a chosen pair. ```agda holds-out : StepHolds tw pw rl cs ro c0 → ∥ Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] (LeastFst t₁ × (LeastSnd t₂ × NM._≺ₙ_ t₁ t₂)) ∥₁ holds-out = St.StepAt-read ``` ## Unpacking The total reading must work for whatever six witnesses a satisfying assignment provides. Its first hypotheses say that `tw` satisfies the graph description of the decoded stage, that `pw` satisfies the definable-power-set description over it, and that the first compared object belongs to `pw`; later uniqueness and adequacy results will turn these into facts about the concrete stage. ```agda private atAll : (tw pw rl cs ro c0 : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ ``` The next hypotheses supply the second membership, the table application, and the code-set description. Crucially, the relation premise ranges over every `r` recorded by the table at `δ`, because in the reading direction the existential formula may have bound any such `rl`; the final equation shown here fixes `ro` to the canonical code order. ```agda → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → fst ro ≡ fst codeOrder ``` The outward argument has now reached the innermost condition. Once the six existential witnesses have been identified, `atAll` reads satisfaction of `StepAt` into the merely existing data of two least names and their name comparison. Mapping the next argument over that propositional truncation will turn the name comparison into the required host-side `Under` comparison without choosing names outside the truncation. ```agda → fst c0 ≡ fst (AllCodes ∅ʟ) → StepHolds tw pw rl cs ro c0 → Goal atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep = PT.map atNames (K.holds-out hstep) where ``` The tower identification equation says the tower bound in the formula equals the constructible stage at the argument ordinal, read out through the layer-adequacy lemma. ```agda qtw : fst tw ≡ Lset δ qtw = Lset-only zero (suc d) (tw ∷ γ) hg od ``` The definable-subset identification says the bound set is the definable power set of the stage, transported along the tower equation. ```agda qpw : fst pw ≡ 𝒟ₒ (Lset δ) qpw = subst ⟨_⟩ (DefAt-stage δ od zero (suc zero) (pw ∷ tw ∷ γ) qtw) hdef ``` Membership in the successor stage is recovered by two transports: the first identifies the definable power set with the successor stage via the successor identity of the constructible layer, and the second rewrites along the identification of the bound set with that definable power set. Together they place the compared object inside `Lset (sucV δ)`. ```agda inSuc : (x : V ℓ) → ⟨ x ∈ fst pw ⟩ → ⟨ x ∈ Lset (sucV δ) ⟩ inSuc x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (Lset-suc δ)) (subst (λ z → ⟨ x ∈ z ⟩) qpw h) ``` The first comparison candidate is the underlying set at slot `u`, presented as a member of the successor stage by the recovery lemma. ```agda a : New δ a = fst (lookup u γ) , inSuc (fst (lookup u γ)) hu ``` The second comparison candidate is the underlying set at slot `v`, similarly presented. ```agda b : New δ b = fst (lookup v γ) , inSuc (fst (lookup v γ)) hv ``` Satisfaction of the application formula says that `rl` is a value recorded by the table at `δ`. The outward hypothesis `vals` deliberately applies to every such recorded value, so it supplies `IsRel δ rl` for the particular witness chosen inside `Stp`. This is a soundness condition on all possible table witnesses, not a uniqueness claim about the table value. ```agda hrel : IsRel δ rl hrel = vals rl (subst ⟨_⟩ (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ pw ∷ tw ∷ γ)) happ) ``` The outward reading of the code-set description identifies `cs` with `AllCodes (LsetS δ od)`, the code set over the current stage `Lset δ`. The compared objects live in the successor stage, but their names are formed relative to the preceding stage, so this code set is indexed by `δ`, not by `sucV δ`. ```agda qcs : fst cs ≡ fst (AllCodes (LsetS δ od)) qcs = cong fst (CodesAt-out (LsetS δ od) zero (sh3 zero) (cs ∷ rl ∷ pw ∷ tw ∷ γ) qtw hcs) ``` With the tower, stage relation, code set, and two fixed code objects now identified, `Slots` connects the six witnesses to the previously proved adequacy theorem for name comparison. This shared instance lets the remaining argument speak interchangeably about the innermost formula and the corresponding least-name data. ```agda module K = Slots tw pw rl cs ro c0 qtw hrel qcs qro qc0 ``` Inside the propositional truncation returned by the name adequacy theorem, suppose `t₁` and `t₂` are least names for the two compared sets and `t₁ ≺ₙ t₂`. The target `Under` contains more than the final comparison: it also records that both sets belong to `Lset (sucV δ)`. Those two membership components have already been established by `a` and `b`. ```agda atNames : Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] ( K.LeastFst t₁ × ( K.LeastSnd t₂ × NM._≺ₙ_ t₁ t₂ ) ) → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) atNames (t₁ , (t₂ , (l₁ , (l₂ , lt)))) = a .snd ``` The two outward least-name readings translate the local predicates back to `IsLeastName`. The theorem `stepAt-fill` then says that comparison of these least names entails the relation of `stepOrder δ od` between the represented new elements. Together with the memberships from the preceding group, this completes `Under`. ```agda , ( b .snd , stepAt-fill δ ordW a b t₁ t₂ (K.leastFst-out t₁ l₁) (K.leastSnd-out t₂ l₂) lt ) ``` ## Packing For the converse direction, fix one actual table value `rl`, evidence that the table records it at `δ`, and evidence that it represents the required stage relation. Also fix the two successor-stage memberships carried by an `Under` comparison. Unlike the outward direction, this construction has a particular local table value available and can use it as the third existential witness of `Stp`. ```agda module Pack (rl : S) (hpr : ⟨ pr δ (fst rl) ∈ fst (lookup f γ) ⟩) (hrel : IsRel δ rl) (hx : ⟨ fst (lookup u γ) ∈ Lset (sucV δ) ⟩) (hy : ⟨ fst (lookup v γ) ∈ Lset (sucV δ) ⟩) where ``` The packing argument uses the six witnesses in the order prescribed by `Stp`: `towerS δ od`, `powS δ od`, the supplied table value `rl`, `AllCodes (LsetS δ od)`, `codeOrder`, and `AllCodes ∅ʟ`. In particular, the fourth witness is the code set over the current stage `Lset δ`; only the two objects being compared belong to its successor stage. ```agda private module K = Slots (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) (towerS-fst δ od) hrel refl refl refl ``` The first comparison candidate is presented by its membership in the successor stage. ```agda a : New δ a = fst (lookup u γ) , hx ``` The second comparison candidate is similarly presented. ```agda b : New δ b = fst (lookup v γ) , hy ``` Every new element has a least name relative to the fixed host-side well-order `ordW`, so the first candidate supplies a pair consisting of a name and its `IsLeastName` proof. This is an explicit local witness used to fill the formula; it does not assert that `Stp` uniquely determines a name. ```agda n₁ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup u γ)) n₁ = leastNameOf δ ordW a ``` The same theorem supplies a least name for the second candidate. These two locally chosen names are compared and then passed to the inward adequacy theorem for `StepAt`. Its existential semantics, followed by the six outer existential binders of `Stp`, hides the names again; this construction exports no chosen pair of names. ```agda n₂ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup v γ)) n₂ = leastNameOf δ ordW b ``` The first witness is `towerS δ od`. Its defining theorem proves that it satisfies `LsetGraphAt` in the extended environment and therefore has underlying set `Lset δ`, as required by the first binder. ```agda hg : ⟨ (towerS δ od ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ hg = Lset-defines zero (suc d) (towerS δ od ∷ γ) od (towerS-fst δ od) ``` The second witness is `powS δ od`, whose underlying set is the definable-subset set `𝒟ₒ (Lset δ)`. The equation supplied by `DefAt-stage` characterizes satisfaction of `DefAt`; transporting `powS-fst` across that characterization proves the required satisfaction statement. This is the definable-subset set of the stage, not its full power set. ```agda hdef : ⟨ (powS δ od ∷ towerS δ od ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hdef = subst ⟨_⟩ (sym (DefAt-stage δ od zero (suc zero) (powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od))) (powS-fst δ od) ``` To fill the two membership conjuncts of `Stp`, the direction needed here is from the successor stage into the chosen definable-subset object. The identity `Lset-suc δ` rewrites membership in `Lset (sucV δ)` as membership in `𝒟ₒ (Lset δ)`, and `powS-fst` then rewrites that set as the underlying set of `powS δ od`. ```agda inPow : (x : V ℓ) → ⟨ x ∈ Lset (sucV δ) ⟩ → ⟨ x ∈ fst (powS δ od) ⟩ inPow x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (powS-fst δ od)) (subst (λ z → ⟨ x ∈ z ⟩) (Lset-suc δ) h) ``` The application satisfaction is transported from the table-entry proof along the adequacy of the application coding. ```agda happ : ⟨ (rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ powS δ od ∷ towerS δ od ∷ γ))) hpr ``` For the fourth witness, the inward reading of `CodesAt` proves that `AllCodes (LsetS δ od)` satisfies the code-set description over the tower `Lset δ`. No code set at the successor stage is needed. ```agda hcs : ⟨ (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ hcs = CodesAt-in (LsetS δ od) zero (sh3 zero) (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od) refl ``` Assume the host-side `stepOrder` comparison. The two least names already chosen satisfy the local least-name predicates after the inward equality adjustments. It remains only to turn the host comparison into the name comparison required by the innermost `StepAt` formula. ```agda hstep : relOf (stepOrder δ od) a b → StepHolds (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) hstep cmp = K.holds-in (n₁ .fst) (n₂ .fst) (K.leastFst-in (n₁ .fst) (n₁ .snd)) (K.leastSnd-in (n₂ .fst) (n₂ .snd)) ``` The theorem `stepAt-read` performs exactly that conversion, using the leastness proofs for `n₁` and `n₂`. Feeding the resulting name comparison to `holds-in` proves the innermost satisfaction statement. The argument uses the already existing host-side `stepOrder`; it does not construct a new well-order. ```agda (stepAt-read δ ordW a b (n₁ .fst) (n₂ .fst) (n₁ .snd) (n₂ .snd) cmp) ``` The six object-language existentials are interpreted as six nested propositionally truncated dependent pairs. `packAll` starts the nesting with `towerS δ od` and its `LsetGraphAt` proof. Although this proof constructs a concrete witness locally, the outermost existential boundary immediately retains only its propositional truncation. ```agda packAll : relOf (stepOrder δ od) a b → ∥ (Σ[ tw ∈ S ] One tw) ∥₁ packAll cmp = ∣ towerS δ od , ( hg , ∣ powS δ od ``` The second witness is `powS δ od`, accompanied by its `DefAt` satisfaction and by the two memberships transported from the successor stage. The third witness is the supplied table value `rl`; its recorded-pair proof yields the required satisfaction of `appAt`. Thus the filling direction uses a particular relation value already provided by the caller rather than choosing one from the table. ```agda , ( hdef , ( inPow (fst (lookup u γ)) hx , ( inPow (fst (lookup v γ)) hy , ∣ rl , ( happ ``` The code set satisfaction is followed by the code-order element and its identification equation, then by the empty-alphabet code set. ```agda , ∣ AllCodes (LsetS δ od) , ( hcs , ∣ codeOrder , ( refl , ∣ AllCodes ∅ʟ ``` The final wrappers insert the empty-alphabet code set, its identifying equality, and the satisfaction of the innermost step formula. Closing all six truncations proves `Stp` while exposing none of the chosen tower, relation, code, or name witnesses to later users. ```agda , ( refl , hstep cmp ) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ ) ) ) ∣₁ ) ∣₁ ``` ## The two readings The two readings now give the exact interface required by the recursive table, and their types record the essential asymmetry. The outward direction must accept every relation value recorded at the stage and returns only `∥ Under ... ∥₁`. The inward direction receives one specified recorded value with its `IsRel` proof and an untruncated `Under` comparison, from which it constructs satisfaction of `Stp`. ```agda opaque unfolding Stp StepHolds ``` For the outward reading, assume every value recorded by the table at `δ` represents the required stage relation. Satisfaction of `Stp` supplies only propositionally truncated existential witnesses, so `read` eliminates the six truncations one at a time into `Goal`, which is itself propositionally truncated. ```agda read : ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → ⟨ γ ⊨ Stp d f u v ⟩ → Goal read vals = PT.rec PT.squash₁ (λ { (tw , (hg , hpw)) → PT.rec PT.squash₁ (λ { (pw , (hdef , (hu , (hv , hrl)))) → PT.rec PT.squash₁ ``` The eliminations follow the binder order: tower, definable-subset set, table value, code set, code order, and empty-alphabet code set. At each level the witness remains available only inside the continuation for the next truncation; the construction never returns a selected six-tuple. ```agda (λ { (rl , (happ , hcs)) → PT.rec PT.squash₁ (λ { (cs , (hcs , hro)) → PT.rec PT.squash₁ (λ { (ro , (qro , hc0)) → PT.rec PT.squash₁ (λ { (c0 , (qc0 , hstep)) → atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep }) ``` Once all six witnesses and their conditions are locally available, `atAll` produces the propositionally truncated `Under` comparison. The nested eliminators then close in the reverse syntactic order, preserving the truncation boundary required by the object-language existentials. ```agda hc0 }) hro }) hcs }) hrl }) hpw }) ``` The inward reading consumes a specific table value with its membership and relation proof, together with the two membership proofs and the host-side comparison, and packs everything into the six-layer existential. ```agda fill : (r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ fill r hpr hrel (hx , (hy , cmp)) = Pack.packAll r hpr hrel hx hy cmp ``` The outward reading of the step formula is exported as the first adequacy direction: satisfaction implies a truncated step comparison. ```agda stp-out : StpOut Stp stp-out = Reading.read ``` ## The frame opened The inward reading of the step formula is exported as the second adequacy direction: a specific table entry with the correct relation and a host-side comparison together imply the formula satisfaction. ```agda stp-in : StpIn Stp stp-in = Reading.fill ``` Supplying `Stp` and these two readings completes the abstract construction of the stage-order table. In particular, it yields for every ordinal stage an internal set `relL` together with `relL-fill` and `relL-rep`, which convert pairwise between the host relation of `orderAt` and membership of the corresponding ordered pair in `relL`. This is a representation of the relation graph; no object-language assertion that `relL` satisfies a well-order formula is proved here. ```agda open Ordered Stp stp-out stp-in public ``` ## The order at the bounding ordinal For a constructible set `a`, `stageBound` chooses an ordinal above both `ω` and the first stage at which `a` appears. Consequently `Lset boundOrd` is high enough to contain the members of `a` and the members of those members, which is the local domain needed by the later transversal argument. The chosen bound is sufficient for that use; it is not asserted to be the least or a uniquely determined bound for `a`. ```agda module Bound (a : V ℓ) (p : ⟨ isL a ⟩) where boundOrd : V ℓ boundOrd = stageBound a p .fst ``` The same bounding result also certifies that `boundOrd` is an ordinal. This proof is what permits the already constructed host-side family `orderAt` to be specialized to the stage `Lset boundOrd`. ```agda boundOrd-ord : IsOrd boundOrd boundOrd-ord = stageBound a p .snd .fst ``` To obtain an internal relation object at this index, the table construction also needs the index itself to be constructible. An ordinal belongs to its own successor stage, so `boundOrd ∈ Lset (sucV boundOrd)` gives precisely the witness from which `Lset→isL` proves `isL boundOrd`. ```agda boundOrd-isL : ⟨ isL boundOrd ⟩ boundOrd-isL = Lset→isL (sucV boundOrd) (suc-ord boundOrd-ord) boundOrd (ord∈Lset-suc boundOrd boundOrd-ord) ``` The relation to be represented is the pre-existing host-side strict well-order `orderAt boundOrd boundOrd-ord` on `Mem (Lset boundOrd)`. Its well-order structure belongs to this `SWO` value; the following lines only realize its binary relation as a set inside `L`. ```agda boundOrder : SWO (Mem (Lset boundOrd)) boundOrder = orderAt boundOrd boundOrd-ord ``` The table supplies that internal set as `relL` at the chosen ordinal. Thus `orderL` is an element of the model whose members are intended to be ordered pairs from the relation graph. It is not a new well-order construction and is not itself accompanied here by an internal satisfaction proof of the well-order axioms. ```agda orderL : S orderL = relL boundOrd boundOrd-isL boundOrd-ord ``` The forward representation lemma takes a host-side comparison `relOf boundOrder x y` and inserts the encoded ordered pair `pr (fst x) (fst y)` into `orderL`. It establishes one direction of the pairwise correspondence between the existing `SWO` relation and its internal graph. ```agda orderL-fill : (x y : Mem (Lset boundOrd)) → relOf boundOrder x y → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ orderL-fill = relL-fill boundOrd boundOrd-isL boundOrd-ord ``` Conversely, membership of the encoded pair in `orderL` recovers the host-side comparison. Together, `orderL-fill` and `orderL-rep` say exactly which ordered pairs occur in the internal relation graph. They neither assert uniqueness of the set representing that graph nor prove within the object language that it is a well-order. ```agda orderL-rep : (x y : Mem (Lset boundOrd)) → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ → relOf boundOrder x y orderL-rep = relL-rep boundOrd boundOrd-isL boundOrd-ord ``` ## Recap The strict well-order remains the host-level structure `orderAt α oα` on `Mem (Lset α)`. The set `relL α hα oα` is an element of `L` that represents its binary relation as a graph, and `relL-fill` and `relL-rep` prove the two directions of that representation for each pair. The six-binder formula and its adequacy readings make this graph available to later object-language formulas, while proving neither a new well-order nor an object-language well-order assertion.