--- title: "The limit-stage order inside L" module: L.Choice.LimitStageOrder lang: en site: "Bedrock" description: "The limit-stage order inside L" stage: "The canonical well-order and Choice" reading_order: 81 canonical: https://bedrock.institute/en/L.Choice.LimitStageOrder.html html: L.Choice.LimitStageOrder.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/LimitStageOrder.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Hierarchy, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/zh/L.Choice.LimitStageOrder.md, https://bedrock.institute/ja/L.Choice.LimitStageOrder.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # The limit-stage order inside L An external strict well-order on the members of `Lset ω` is already available. The question here is how its comparison can be used by formulas inside `L`. The answer will pass through three distinct forms: a meta-level comparison, an object-language description of that comparison, and, once the finite-stage description has been supplied, a constructible set realizing the described relation. ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` All constructions are relative to one explicit instance of excluded middle at level `ℓ-suc ℓ`. Earlier work used this hypothesis to obtain the least finite stage at which a limit-stage member appears, and the present chapter also passes it to the separation and bounding results it uses. This hypothesis decides propositions when those constructions require it; it does not provide a choice function for an arbitrary family. ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` Fix a universe level `ℓ` and the excluded-middle instance just described. The internal relation constructed later is still conditional at this point: it is defined inside the module `Described` after a formula for the finite-stage order and its two semantic directions have been supplied. The next chapter will provide that instance and expose `codeOrder` for subsequent use. ```agda module L.Choice.LimitStageOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` The object language must describe comparisons without confusing syntax with their meaning in the hierarchy. Its formulas use variables, constants, membership, connectives and quantifiers; because the constant domain is the constructible carrier, a constant already denotes a particular constructible set. The coding lemmas provide the two elementary tests needed later. An ordered-pair equality determines both components, and the numeral coding is injective, while `#mono` turns `k < m` into membership of `# k` in `# m`. Thus set-theoretic membership can faithfully carry the strict comparison of finite indices. ```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; pr-inj; #mono; #-inj′ ) ``` The intended structure is the constructible universe. An element of its carrier packages a set with evidence of constructibility, and transitivity supplies the same evidence for every member of such a set. This lets witnesses move from ordinary hierarchy membership into environments of the object language. In particular, `finiteStage n` is the stage `Lset (# n)`, whereas the limit stage is `Lset ω`; the numeral and ordinal facts keep these indices distinct from the stages they name. The packaged stages and the constant `ωʟ` then allow formulas to refer to this hierarchy from inside the structure. ```agda open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd ) open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; ω-ord ) open import L.Axioms.Basic {ℓ} using ( LsetS ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ ) ``` Three bridges turn a semantic comparison into a set of `L`. First, `smallDom` puts a small family inside one common constructible set, but does not claim that the bound is its exact image. Second, separation cuts from such a bound exactly the elements satisfying a one-variable formula. Third, the coding formulas for pairs, relation membership, and the hierarchy sequence come with adequacy laws that translate satisfaction into the corresponding facts about sets. Together these tools separate the problem of finding a common domain from the problem of stating the exact relation on that domain. ```agda open import L.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Recursion {ℓ} lem using ( smallDom ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; prAtL; prAtL-adequate; prʟ; prʟ-fst ) open import L.Coding.Expressions {ℓ} using ( numL ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) ``` The comparison to be represented is already defined externally. At a successor stage, `before (suc n)` compares two subsets of `finiteStage n` at their earliest disagreement, using `before n` below that point. A witness for `precedes R A x y` lies in `A`, belongs to `y` and not to `x`, and records agreement of `x` and `y` at every earlier point; its existence is propositionally truncated. The type `Limit` packages members of `Lset ω`, and their least appearance levels form the primary key of `limitOrder`; only equal levels invoke the corresponding `before` comparison. The two representation directions for the resulting relation set have exactly the form required by `Adequacy.Keys`. ```agda open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; level; level-in; levelData; limitOrder ; before; precedes; Agrees; Witness; finiteStage ) open import L.Choice.NameComparison {ℓ} lem using ( module Adequacy ) ``` The order `limitOrder` is available as an `SWO` bundle: besides its comparison it provides trichotomy, irreflexivity, transitivity and well-foundedness. The internalization argument does not reprove these laws. It uses the first three later for a specific purpose: when reading an object-language disjunction yields only a propositionally truncated strict comparison, trichotomy identifies the possible branch, while irreflexivity and transitivity refute the incompatible branches. ```agda open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt ) ``` The limit comparison has the lexicographic shape needed later. Its first alternative says that the first member has a smaller level. Its second says that the levels agree and compares the underlying sets by `before` at their common level. Natural-number trichotomy analyzes the first key, and `subst2` transports binary relations when equalities identify the coded levels or endpoints. The accompanying `Lift` and `lower` operations only reconcile universe levels; they do not remove propositional truncation. ```agda import FOL.Absoluteness open import Cubical.Data.Sum using ( _⊎_; inl; inr ) open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Data.Nat.Order using ( _<_; _≟_ ) import Cubical.Data.Nat.Order as NatOrder ``` Object-language existential quantification and disjunction are interpreted as propositionally truncated existence and choice of branch. Consequently, their witnesses may be used only when the target is a proposition, such as impossibility, equality of hierarchy sets, or another truncation. This does not mean that every existential type in the chapter is truncated: explicit data, including packaged carrier elements and bounds, remains visible when its type requires it. Recovering a strict comparison from a truncation is not a general elimination principle either; it relies specifically on the trichotomy and order laws of `limitOrder`. ```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 ``` To apply the bounding lemma, the members of `Lset ω` need a small index type. The fiber `⟪ Lset ω ⟫` provides such indices, and `∈-asFiber` turns a given membership proof into an index whose image is the original member. Taking a product of two such fibers therefore indexes all ordered pairs of limit-stage members. The later set `pairsBound` will contain every one of these pairs; exactness will come only after separation. ```agda using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_; ω ) ``` Three membership symbols now have separate roles. For carrier elements, `x ∈ˢ y` is the proposition-valued membership of the constructible structure; between underlying hierarchy sets, `fst x ∈ fst y` uses ambient membership; inside a formula, `_∈̇_` is only the syntactic membership atom. The satisfaction judgment introduced next is what turns the third form into the first two. Keeping these layers separate will prevent a formula that describes an order from being mistaken for a proof that its realizing set is internally well-ordered. ```agda open hPropStructure 𝒮ʟ ``` The judgment `_⊨_` is the inner satisfaction relation obtained by restricting the ambient hierarchy structure to the constructible class. Its carrier consists of sets equipped with constructibility evidence, so both constants and quantified values range over constructible objects. Atomic membership is interpreted through first projections, and transitivity ensures that a member of a constructible bound can again be packaged as a carrier element. Thus satisfaction supplies the precise bridge from an object-language formula to ordinary membership facts about its underlying sets. ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` Write `_≺ˡ_` for the comparison carried by `limitOrder`. It orders two limit-stage members first by their least appearance levels and, when those levels coincide, by earliest disagreement in the common finite stage. The remaining goal is conditional: given an object-language formula representing every finite-stage `before` relation on its intended domain, construct inside `Described` a set `codeOrder` such that the ordered pair of `u` and `v` belongs to it exactly when `u ≺ˡ v`. The next chapter supplies the required finite-stage formula and thereby obtains the usable instance. ```agda open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ ) ``` Bound variables are represented by de Bruijn positions. Opening two nested binders therefore moves every position from the surrounding environment past two new entries, and `sh2` records exactly this shift. It will be used when earliest disagreement binds a candidate point and then a point below it, and when the unequal-level branch binds the two level numerals. The shift changes only how an existing free variable is addressed; it does not change the set or relation denoted by that variable. ```agda private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ``` An environment contains elements of the constructible carrier rather than bare hierarchy sets. For a natural number `k`, `towerS k` therefore packages the stage `Lset (# k)` with its constructibility evidence. The definition is opaque so later proofs use its public projection equation instead of expanding the hierarchy construction. This opacity controls reduction only; no mathematical assumption is added. ```agda opaque towerS : ℕ → S towerS k = LsetS (# k) (numeral-ord k) ``` The equation `towerS-fst k` identifies the underlying set of this carrier element with `Lset (# k)`. It is the transport point between two views of the same stage: formulas receive the packaged element `towerS k`, while the external level lemmas state membership in the underlying hierarchy set. Later proofs cross this equation whenever they move a membership fact between those views. ```agda towerS-fst : (k : ℕ) → fst (towerS k) ≡ Lset (# k) towerS-fst k = refl ``` The index itself needs a separate carrier element. The value `numS k` packages the numeral `# k` with evidence that it is constructible. Keeping `numS k` distinct from `towerS k` prevents a common confusion: the former denotes the ordinal index, while the latter denotes the constructible stage indexed by it. `LevelAt` will relate these two objects through the hierarchy-sequence description. ```agda numS : ℕ → S numS k = # k , numL k ``` The projection equation `numS-fst k` recovers `# k` from the packaged numeral. Together with `towerS-fst k`, it lets the same natural number be used coherently in both roles: as a level value in an environment and as the index of the stage exhibited by a witness. These equations justify the transports between object-language values and external facts about numerals and stages. ```agda numS-fst : (k : ℕ) → fst (numS k) ≡ # k numS-fst k = refl ``` Suppose position `i` of an environment has underlying set `# j`. The lemma `towerGraph` places `towerS j` in the fresh position and proves that `LsetGraphAt` relates the two positions. Its content is exactly the hierarchy-sequence specification: the value associated with the numeral `# j` is the stage `Lset (# j)`. Thus the same lemma supplies a genuine tower witness both for existence at the true level and for testing minimality against that level. ```agda towerGraph : ∀ {n} (j : ℕ) (δ : S ^ n) (i : Fin n) → fst (lookup i δ) ≡ # j → ⟨ (towerS j ∷ δ) ⊨ LsetGraphAt zero (suc i) ⟩ towerGraph j δ i q = Lset-defines zero (suc i) (towerS j ∷ δ) (subst IsOrd (sym q) (numeral-ord j)) (towerS-fst j ∙ cong Lset (sym q)) ``` ## The level, said inside The formula `LevelAt b x` begins the first key. It first requires the value at `b` to belong to `ω`, so it can be decoded as a numeral. It then asks for a value described by `LsetGraphAt` at that numeral and requires the value at `x` to belong to the resulting stage. These clauses say that `b` is an appearance stage for `x`; the remaining clause will make it the least one. ```agda LevelAt : ∀ {n} → Fin n → Fin n → Formula S n LevelAt b x = (var b ∈̇ con ωʟ) ∧̇ ( ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ∧̇ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero) ``` Minimality is expressed over every member `u` of the candidate numeral `b`, not merely over its immediate predecessor. For every stage described at such a `u`, the value at `x` must fail to belong to that stage. Since the members of `# k` are precisely the smaller numerals, a candidate `b = # k` therefore excludes all stages `0, …, k-1`. The two nested binders account for the shifted occurrence of `x`. Semantically the universal clauses are function types; the nearby propositionally truncated decoding of numeral membership is used only with a propositional target and does not select a smaller index. ```agda ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ) ``` To prove the two readings of `LevelAt`, fix a genuine limit-stage member `a`, a natural number `k`, and an equation `qk : level a ≡ k` identifying `k` with its least appearance level. The positive component of `levelData a`, transported along `qk`, gives `aIn`: the underlying set of `a` belongs to `Lset (# k)`. The negative component says that membership in any `Lset (# m)` with `m < k` is impossible. These are exactly the existence and minimality facts needed to show that the formula recognizes the true level, and later to prove that any level recognized by the formula equals `# k`. ```agda module Level (a : Limit) (k : ℕ) (qk : level a ≡ k) where private aIn : ⟨ fst a ∈ Lset (# k) ⟩ aIn = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) qk (level-in a) ``` The second projection of `levelData a` supplies the minimality needed throughout the argument. If the underlying set of `a` already belongs to `Lset (# m)` and `m < k`, the equation `qk` turns this last inequality into `m < level a`, contradicting that minimality. The comparison expected by `levelData` lives one universe higher, so it is wrapped with `lift`. This is only a universe-level adjustment; no propositional truncation is involved. ```agda aMin : (m : ℕ) → ⟨ fst a ∈ Lset (# m) ⟩ → m < k → Empty.⊥ aMin m h hm = levelData a .snd .snd m h (lift (subst (λ j → m < j) (sym qk) hm)) ``` The two readings of `LevelAt` are proved at arbitrary positions `b` and `x` in an arbitrary environment. For the outward reading it is useful to name the information hidden by the existential: a carrier element `c` that satisfies the hierarchy graph at the value of `b`, together with a proof that the value of `x` belongs to the underlying set of `c`. The private type `Body` is exactly this witness data before propositional truncation. ```agda module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where private Body : S → Type (ℓ-suc ℓ) Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩ × ⟨ fst (lookup x γ) ∈ fst c ⟩ ``` For the inward reading, suppose that `b` denotes the numeral `# k` and `x` denotes the underlying set of `a`. The conclusion has the three components of `LevelAt`: the value of `b` lies in `ω`, a hierarchy value at `b` contains the value of `x`, and every hierarchy value indexed by a member of `b` omits it. The proof names these components `hω`, `hex`, and `hmin` so that existence and minimality can be established separately. ```agda LevelAt-in : fst (lookup b γ) ≡ # k → fst (lookup x γ) ≡ fst a → ⟨ γ ⊨ LevelAt b x ⟩ LevelAt-in qb qx = hω , (hex , hmin) where hω : ⟨ fst (lookup b γ) ∈ ω ⟩ ``` The first component follows from the elementary fact that every numeral belongs to `ω`. The equation `qb` identifies the value stored at `b` with `# k`; transporting `#∈ω k` along the symmetric direction of that equation gives the required membership. This transport connects a fact about the explicit numeral with the same fact about an environment position. ```agda hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k) ``` For the existential component, choose the packaged finite stage `towerS k`. The lemma `towerGraph`, using `qb`, proves that this witness is the hierarchy value at `b`. Its underlying set is `Lset (# k)` by `towerS-fst k`, so the remaining obligation is the known membership `aIn` after the endpoint is aligned by `qx`. ```agda hex : ⟨ γ ⊨ ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ⟩ hex = ∣ towerS k , (towerGraph k γ b qb , hm) ∣₁ where hm : ⟨ fst (lookup x γ) ∈ fst (towerS k) ⟩ hm = subst (λ u → ⟨ fst (lookup x γ) ∈ u ⟩) (sym (towerS-fst k)) ``` The fact `aIn` already says that the underlying set of `a` belongs to `Lset (# k)`. Transporting it along the symmetric direction of `qx` changes the member from the underlying set of `a` to the value at `x`. Combined with the preceding projection transport, this proves `hm` and completes the existential witness under propositional truncation. ```agda (subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn) ``` The bounded universal expresses global minimality. Given `u` in the value of `b`, a candidate `c` satisfying the hierarchy graph at `u`, and a supposed membership of the value of `x` in `c`, the proof must derive a contradiction. After `qb` rewrites `u` as a member of `# k`, `∈#-elim` says, under propositional truncation, that `u` is `# m` for some `m < k`. The truncation may be eliminated because the target is the empty type, hence a proposition. The resulting contradiction is lifted only to meet the universe level of object-language negation. ```agda hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero) ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩ hmin u u∈ c hg hmem = lift (PT.rec Empty.isProp⊥ step (∈#-elim k (fst u) (subst (λ w → ⟨ fst u ∈ w ⟩) qb u∈))) where ``` Fix an explicit decoding `m < k` and `fst u ≡ # m`. The graph proof `hg` does more than certify that `c` is some possible witness: `Lset-only`, supplied with the ordinal proof transported from the numeral `# m`, identifies its underlying set with `Lset (fst u)`. Thus the formula cannot hide an arbitrary set behind its existential witness; the hierarchy graph determines the finite stage. ```agda step : Σ[ m ∈ ℕ ] ((m < k) × (fst u ≡ # m)) → Empty.⊥ step (m , (hm , qu)) = aMin m inStage hm where qc : fst c ≡ Lset (fst u) qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg ``` Now transport the alleged membership through the three identifications. First `qc` places the value of `x` in `Lset (fst u)`; then `qx` replaces that value by the underlying set of `a`; finally `qu` replaces `fst u` by `# m`. The result is `fst a ∈ Lset (# m)`, precisely the statement that `aMin` rules out when `m < k`. Hence no finite stage indexed below `k` contains `a`. ```agda (subst IsOrd (sym qu) (numeral-ord m)) inStage : ⟨ fst a ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ fst a ∈ Lset w ⟩) qu (subst (λ w → ⟨ w ∈ Lset (fst u) ⟩) qx (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem)) ``` For the outward reading, assume `LevelAt b x` and continue to identify the value of `x` with the underlying set of the fixed member `a`. The aim is to prove that the candidate at `b` is the true numeral `# k`. Its membership in `ω` reveals a natural-number index only under propositional truncation. The target is an equality in the cumulative hierarchy, and `setIsSet` shows that this equality type is a proposition, so the truncated numeral data may be eliminated into it. ```agda LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → fst (lookup x γ) ≡ fst a → fst (lookup b γ) ≡ # k LevelAt-out (hω , (hex , hmin)) qx = PT.rec (setIsSet (fst (lookup b γ)) (# k)) named hω where ``` First exclude a decoded index `m` above the true level, so assume `k < m` and that the value of `b` is `# m`. By `#mono`, `# k` belongs to `# m`; the wrappers `numS k` and `towerS k` therefore let the minimality clause of `LevelAt` be tested at the genuine finite stage `Lset (# k)`. That clause says the value of `x` is absent there, contradicting `aIn`. It returns a lifted contradiction, and `lower` removes only this universe lift, an instance of propositional resizing rather than propositional truncation. ```agda notAbove : (m : ℕ) → fst (lookup b γ) ≡ # m → k < m → Empty.⊥ notAbove m qb hk = lower (hmin (numS k) (subst (λ w → ⟨ w ∈ fst (lookup b γ) ⟩) (sym (numS-fst k)) (subst (λ w → ⟨ # k ∈ w ⟩) (sym qb) (#mono k m hk))) (towerS k) (towerGraph k (numS k ∷ γ) zero (numS-fst k)) ``` The last argument to that minimality clause is the positive membership it is about to refute. Starting from `aIn`, the symmetric direction of `qx` replaces the underlying set of `a` by the value of `x`, and the symmetric direction of `towerS-fst k` replaces `Lset (# k)` by the underlying set of its carrier wrapper. The formula and the external minimal-level argument are thereby speaking about the same member of the same finite stage. ```agda (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) (sym (towerS-fst k)) (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn))) ``` Next exclude a decoded index below the true level. If `m < k`, the existential component of `LevelAt` supplies, under propositional truncation, a carrier `c` that satisfies the hierarchy graph at `b` and contains the value of `x`. This is exactly the data named by `Body`. Since the desired result is a contradiction, the truncation may be eliminated into the empty type; each explicit witness will force `a` to occur at stage `m`. ```agda notBelow : (m : ℕ) → fst (lookup b γ) ≡ # m → m < k → Empty.⊥ notBelow m qb hm = PT.rec Empty.isProp⊥ atTower hex where atTower : Σ[ c ∈ S ] Body c → Empty.⊥ atTower (c , (hg , hmem)) = aMin m inStage hm ``` For such a witness, `Lset-only` first identifies the underlying set of `c` with the hierarchy stage indexed by the value of `b`. Its ordinal premise comes from `numeral-ord m`, transported along the equation that the value of `b` is `# m`. Composing the resulting equality with `cong Lset qb` yields the concrete identification `fst c ≡ Lset (# m)`. ```agda where qc : fst c ≡ Lset (# m) qc = Lset-only zero (suc b) (c ∷ γ) hg (subst IsOrd (sym qb) (numeral-ord m)) ∙ cong Lset qb ``` The membership stored in the witness can now be read at the concrete finite stage. Transport along `qc` turns it into membership of the value of `x` in `Lset (# m)`, and transport along `qx` turns that value into the underlying set of `a`. Thus `a` occurs at stage `m`; together with `m < k`, this contradicts `aMin`. The candidate index is therefore not below the true level. ```agda inStage : ⟨ fst a ∈ Lset (# m) ⟩ inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem) ``` It remains to identify the numeral decoded from membership in `ω`. An explicit decoded package contains `j : Lift ℕ` and an equality from `# (lower j)` to the value at `b`. Reversing that equality gives `qb`. Once the natural-number comparison proves `lower j ≡ k`, applying the numeral map and composing equalities yields the required value `fst (lookup b γ) ≡ # k`. ```agda named : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst (lookup b γ)) → fst (lookup b γ) ≡ # k named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k)) where qb : fst (lookup b γ) ≡ # (lower j) ``` Trichotomy for natural numbers supplies exactly the required equality. The case `lower j < k` contradicts `notBelow`, while the case `k < lower j` contradicts `notAbove`; the equality case returns its proof unchanged. Consequently the two readings are inverse at the level of truth: the true least stage satisfies `LevelAt`, and any candidate reported by that formula for the fixed member `a` must be its true level. ```agda qb = sym qj decide : NatOrder.Trichotomy (lower j) k → lower j ≡ k decide (NatOrder.lt h) = Empty.rec (notBelow (lower j) qb h) decide (NatOrder.eq e) = e decide (NatOrder.gt h) = Empty.rec (notAbove (lower j) qb h) ``` ## The earliest disagreement, said inside To compare sets by a formula, external members of a constructible carrier must first be presented as elements of the semantic carrier `S`. If `A : S` and `z` belongs to its underlying set, transitivity of constructibility turns the certificate stored in `A` into a certificate that `z` is constructible. `memS` packages `z` with this inherited proof. It constructs an element of the dependent carrier, not a set-theoretic ordered pair. ```agda opaque memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A) ``` The projection equation `memS-fst` states that this packaging preserves the set being discussed: the underlying set of `memS A z h` is `z`. It holds by reflexivity, but exposing it as a lemma is what allows later transports to pass between a quantified carrier element and the external set it represents without unfolding the package. ```agda memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z memS-fst A z h = refl ``` `PrecedesAt` expresses one earliest-disagreement step relative to a relation already stored at `r` and a carrier stored at `A`. For the sets at `x` and `y`, it asks for a witness `z` in the carrier such that `z` belongs to `y` but not to `x`. This orientation determines the comparison: at the deciding point the right-hand set has membership value one and the left-hand set has membership value zero, so `x` precedes `y`. ```agda PrecedesAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n PrecedesAt r A x y = ∃̇ ( (var zero ∈̇ var (suc A)) ∧̇ ( (var zero ∈̇ var (suc y)) ∧̇ ( ¬̇ (var zero ∈̇ var (suc x)) ``` The witness must also be the first disagreement according to the relation at `r`. For every `w` in the carrier `A`, if that relation places `w` before `z`, membership of `w` in `x` and in `y` must agree in both directions. The formula consults the relation through `appAt`: semantically this asks whether the set-theoretic pair of `w` and `z` belongs to the relation set stored at `r`. The existential binder for `z` and the universal binder for `w` account for the two-position shift applied to the older variables. ```agda ∧̇ ∀̇∈ (var (suc A)) ( appAt (sh2 r) zero (suc zero) ⇒̇ ( ((var zero ∈̇ var (sh2 x)) ⇒̇ (var zero ∈̇ var (sh2 y))) ∧̇ ((var zero ∈̇ var (sh2 y)) ⇒̇ (var zero ∈̇ var (sh2 x))) ) ) ) ) ) ``` The module `Precedes` states precisely what is required to read this formula. Besides the four positions and their environment, it fixes a meta-level relation `R`. The law `Rrep` reads membership of a set-theoretic pair in the relation set at `r` as an `R`-fact, while `Rfill` writes such a fact back as membership. These laws need only constructible endpoints because every quantified endpoint already lies in `S`, and external carrier members can be wrapped by `memS`. No order axiom for `R` is assumed: the formula represents the definition of one comparison step independently of any later proof that a particular relation is a well-order. ```agda module Precedes {n : ℕ} (r A x y : Fin n) (γ : S ^ n) (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (Rrep : (u v : S) → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩ → ⟨ R (fst u) (fst v) ⟩) (Rfill : (u v : S) → ⟨ R (fst u) (fst v) ⟩ ``` Fix the carrier first. Every claim about a point earlier than the disagreement is bounded by the constructible set denoted by the value at `A`, so the comparison never ranges beyond the stage on which its base relation acts. ```agda → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩) where private Aʟ : S Aʟ = lookup A γ ``` Write `xv` for the set denoted by the value at `x`. This lets the argument state membership in the left set without repeating the environment lookup in every clause. ```agda xv : V ℓ xv = fst (lookup x γ) ``` Likewise, `yv` denotes the set given by the value at `y`. The order of these two names matters because the first disagreement belongs to the right set and fails to belong to the left one. ```agda yv : V ℓ yv = fst (lookup y γ) ``` Before the first disagreement, the two sets must give the same membership answer. `Both w` records precisely this equivalence: membership of `w` in `xv` implies membership in `yv`, and conversely. ```agda Both : V ℓ → Type (ℓ-suc ℓ) Both w = (⟨ w ∈ xv ⟩ → ⟨ w ∈ yv ⟩) × (⟨ w ∈ yv ⟩ → ⟨ w ∈ xv ⟩) ``` For a proposed disagreement witness `z`, `Agreeing z` examines every `w` in the carrier that the coded base relation places before `z`. The atom `appAt r w z` means that the relation set contains the ordered pair of `w` and `z`; under that premise, `xv` and `yv` must agree at `w`. ```agda Agreeing : S → Type (ℓ-suc ℓ) Agreeing z = (w : S) → ⟨ fst w ∈ fst Aʟ ⟩ → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ → Both (fst w) ``` The witness itself must lie in the carrier and in `yv`, while being absent from `xv`; all base-earlier carrier members must satisfy the agreement condition. Thus this orientation says that `xv` precedes `yv`. No order laws for the supplied base relation are assumed here, so calling the disagreement earliest is justified only when that relation really is an order. ```agda Body : S → Type (ℓ-suc ℓ) Body z = ⟨ fst z ∈ fst Aʟ ⟩ × ( ⟨ fst z ∈ yv ⟩ × ( (⟨ fst z ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥) × Agreeing z ) ) ``` To read the formula outward, eliminate its propositionally truncated existential into the proposition `precedes R A xv yv`. It is enough to transform each displayed model witness into a witness for the host-level definition, because the target retains only its propositional truncation. ```agda PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩ → ⟨ precedes R (fst Aʟ) xv yv ⟩ PrecedesAt-out = PT.rec squash₁ atZ where atZ : Σ[ z ∈ S ] Body z → ⟨ precedes R (fst Aʟ) xv yv ⟩ ``` The underlying set of `z` supplies the host witness, and the first three fields already give its carrier membership and the directed disagreement. The remaining task is to prove agreement at an arbitrary host-level `w` that lies before it. ```agda atZ (z , (z∈A , (z∈y , (z∉x , hag)))) = ∣ fst z , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , ag))) ∣₁ where ag : Agrees R (fst Aʟ) xv yv (fst z) ag w w∈A hR = subst Both (memS-fst Aʟ w w∈A) (hag wS w∈A' happ) ``` Since `w` belongs to the constructible carrier, it inherits constructibility and can be packaged as a model element `wS`. Its projection equation transports the original carrier-membership proof to the form expected by the bounded object-language clause. ```agda where wS : S wS = memS Aʟ w w∈A w∈A' : ⟨ fst wS ∈ fst Aʟ ⟩ w∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A ``` The premise currently says `R w z` at the host level. After aligning `w` with `wS`, `Rfill` writes this fact as membership of the ordered pair in the relation set, exactly the information needed to establish the application atom. ```agda hp : ⟨ pr (fst wS) (fst z) ∈ fst (lookup r γ) ⟩ hp = Rfill wS z (subst (λ u → ⟨ R u (fst z) ⟩) (sym (memS-fst Aʟ w w∈A)) hR) happ : ⟨ (wS ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩ happ = subst ⟨_⟩ ``` Adequacy for `appAt` converts that pair-membership statement into satisfaction in the environment extended by `wS` and `z`. The object-language agreement hypothesis can now be applied. ```agda (sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp ``` The converse starts with the propositionally truncated witness in `precedes`. Because satisfaction of `PrecedesAt` is itself a proposition, the truncation may be eliminated while each host witness is converted into an object-language existential witness. ```agda PrecedesAt-in : ⟨ precedes R (fst Aʟ) xv yv ⟩ → ⟨ γ ⊨ PrecedesAt r A x y ⟩ PrecedesAt-in = PT.rec squash₁ atZ where atZ : Σ[ z ∈ V ℓ ] Witness R (fst Aʟ) xv yv z ``` Unpack a host witness `z` together with its carrier membership, its membership in the right set, its exclusion from the left set, and its earlier-point agreement. Its carrier membership makes `z` constructible, so `zS` can serve as the formula’s quantified witness. ```agda → ⟨ γ ⊨ PrecedesAt r A x y ⟩ atZ (z , (z∈A , (z∈y , (z∉x , ag)))) = ∣ zS , (z∈A' , (z∈y' , (z∉x' , hag))) ∣₁ where zS : S ``` The projection `fst zS` is equal to the original `z`. Transport along this equality shows that the packaged witness still belongs to the carrier, so packaging changes only its presentation and not its mathematical role. ```agda zS = memS Aʟ z z∈A qz : fst zS ≡ z qz = memS-fst Aʟ z z∈A z∈A' : ⟨ fst zS ∈ fst Aʟ ⟩ z∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym qz) z∈A ``` The same projection equation transports membership in `yv` and nonmembership in `xv`. It remains to translate the formula’s relation premise back to `R`, so that the host agreement hypothesis can be used. ```agda z∈y' : ⟨ fst zS ∈ yv ⟩ z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y z∉x' : ⟨ fst zS ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥ z∉x' h = lift (z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h)) hag : Agreeing zS ``` Given a model element `w` in the carrier, adequacy for `appAt` first reads satisfaction as membership of the pair of `w` and `zS` in the coded relation. This is the reverse passage from the one used in the outward proof. ```agda hag w w∈A happ = ag (fst w) w∈A hR where hp : ⟨ pr (fst w) (fst zS) ∈ fst (lookup r γ) ⟩ hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ hR : ⟨ R (fst w) z ⟩ ``` Now `Rrep` reads relation-set membership back as `R (fst w) zS`; transporting the second endpoint from `fst zS` to `z` supplies the premise expected by the original agreement proof. The two membership implications in `Both` follow. ```agda hR = subst (λ u → ⟨ R (fst w) u ⟩) qz (Rrep w zS hp) ``` ## The order, composed An element `a : Limit` carries a proof that its underlying set belongs to `Lset ω`. Membership in this constructible stage yields the `isL` evidence needed to regard the same underlying set as an element of the model, called `limitEl a`. ```agda opaque limitEl : Limit → S limitEl a = fst a , Lset→isL ω ω-ord (fst a) (snd a) ``` Packaging does not alter the set: projecting `limitEl a` returns `fst a` by definition. This equation will later align model-built pairs with the ambient pairs used in the statement of representation. ```agda limitEl-fst : (a : Limit) → fst (limitEl a) ≡ fst a limitEl-fst a = refl ``` To place a relation inside `L`, its related endpoints must be represented by an ordered pair that is itself a model element. `prS` supplies that internal pair for any two constructible endpoints. ```agda prS : S → S → S prS a b = prʟ a b ``` The projection law for `prS` identifies its underlying set with the ambient ordered pair of the two underlying endpoints. Hence internal pair construction and external relation membership speak about the same set. ```agda prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b) prS-fst a b = prʟ-fst a b ``` Before separation can select the ordered pairs satisfying the comparison, all candidate pairs need one set-sized bound. Present `Lset ω` by its small fiber of members, package each presented member as constructible, and index pairs by the product of those two small fibers. ```agda pairsBound : Σ[ D ∈ S ] ((u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst D ⟩) pairsBound = d .fst , onPair where ixL : ⟪ Lset ω ⟫ → S ixL m = ⟪ Lset ω ⟫↪ m , Lset→isL ω ω-ord (⟪ Lset ω ⟫↪ m) ``` Each presentation index really denotes a member of `Lset ω`. The membership bridge turns that presentation fact into ordinary membership, and membership in the stage supplies the constructibility proof used by the package `ixL`. ```agda (∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m)) ``` Applying `smallDom` to this small product produces a constructible set containing every internally formed pair. It is only a common bound: it can contain additional objects, and the exact comparison relation will be obtained by separation inside it. ```agda d : Σ[ D ∈ S ] ((p : ⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩) d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p))) ``` For arbitrary `u,v : Limit`, their underlying sets have presentation indices in the small fiber of `Lset ω`. The pair at those indices belongs to the bound, and the projection equations transport that membership to the ambient pair `pr (fst u) (fst v)`. ```agda onPair : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst (d .fst) ⟩ onPair u v = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩) (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd)) (d .snd (fu .fst , fv .fst)) where ``` The two fiber witnesses recover exactly the presentation indices used above, together with equations identifying their displayed members with `fst u` and `fst v`. These equations are why the small presentation suffices for every actual limit-stage endpoint. ```agda fu = ∈-asFiber {a = fst u} {b = Lset ω} (snd u) fv = ∈-asFiber {a = fst v} {b = Lset ω} (snd v) ``` Reading a formula can yield only the propositional truncation of a strict limit comparison. `strictLimit` recovers the comparison by first consulting trichotomy for the already proved strict well-order `limitOrder`; if trichotomy gives `a ≺ˡ b`, there is nothing left to choose. ```agda strictLimit : (a b : Limit) → ∥ a ≺ˡ b ∥₁ → a ≺ˡ b strictLimit a b h = decide (SWO.tri∙ limitOrder a b) where decide : Tri (a ≺ˡ b) (a ≡ b) (b ≺ˡ a) → a ≺ˡ b decide (lt k) = k ``` The other two trichotomy cases are impossible under the truncated forward comparison. If `a = b`, transport would give a self-comparison; if `b ≺ˡ a`, transitivity with the hidden forward comparison would again give a self-comparison. Irreflexivity refutes both propositions, so truncation is eliminated only into contradiction. ```agda decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥ (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h) decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥ (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h) ``` The defining property of `level a` places `fst a` in `finiteStage (level a)`. An equation `level a ≡ k` transports this membership to `finiteStage k`, providing exactly the stage boundary required when the finite comparison is invoked. ```agda levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ fst a ∈ finiteStage k ⟩ levelStage a k q = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) q (level-in a) ``` `Described` is a conditional framework. It accepts a formula `BeforeAt` intended to describe `before m`, together with an inward direction that may be used only when the value at `b` denotes `# m` and the first endpoint lies in `finiteStage m`. ```agda module Described (BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) (BeforeAt-in : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ) → fst (lookup b γ) ≡ # m → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩ ``` The inward hypothesis also requires the second endpoint to lie in the same finite stage and requires the actual comparison `before m x y`; from these data it produces satisfaction of `BeforeAt`. Thus the framework does not construct a finite-stage relation or infer its order laws. ```agda → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩) (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ) → fst (lookup b γ) ≡ # m ``` The outward hypothesis has the same numeral and stage boundaries and reads satisfaction back as `before m x y`. Only a formula satisfying both directions can instantiate the framework; the actual `BeforeAt` and hence the resulting `codeOrder` are supplied by `EarliestDisagreement`, not unconditionally at this point. ```agda → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩ → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩) where ``` The first branch of `LimitOrdAt` handles unequal levels. It binds two candidate numerals, proves separately that they are the least levels of `x` and `y`, and requires the numeral for `x` to be a member of the numeral for `y`, which expresses strict inequality of natural-number levels. ```agda opaque LimitOrdAt : ∀ {n} → Fin n → Fin n → Formula S n LimitOrdAt x y = ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ``` The second branch handles equal levels by binding one common numeral. Both `LevelAt` clauses identify that same numeral as the least level, after which the assumed `BeforeAt` compares the endpoints inside that finite stage. Sharing one witness expresses equality without adding a separate object-language equality. ```agda ∨̇ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) ) ``` To prove adequacy of this formula, fix the two positions `x` and `y` in the environment and identify their values with actual `u,v : Limit`. Explicit indices `ku,kv` and equations to the true levels allow the proof to move cleanly between natural-number comparisons, numeral membership, and stage membership. ```agda module Order {n : ℕ} (x y : Fin n) (γ : S ^ n) (u v : Limit) (ku kv : ℕ) (qu : level u ≡ ku) (qv : level v ≡ kv) (qx : fst (lookup x γ) ≡ fst u) (qy : fst (lookup y γ) ≡ fst v) ``` The two `Level` instances provide more than convenient names: each one supplies the verified reading of `LevelAt` for the corresponding actual endpoint and its least level. They are the bridge that rules out spurious numeral witnesses in the outward direction. ```agda where private module Lu = Level u ku qu module Lv = Level v kv qv ``` `Split c d` is the semantic content of the unequal-level branch. It says that `c` is the least-level numeral for the left endpoint, `d` is the least-level numeral for the right endpoint, and `c ∈ d`; the last clause fixes the direction as left level smaller than right level. ```agda Split : S → S → Type (ℓ-suc ℓ) Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩ × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩ × ⟨ fst c ∈ fst d ⟩ ) ``` `Same c` is the semantic content of the equal-level branch. The same `c` must describe the least level of both endpoints, and only then may `BeforeAt c x y` supply their comparison within that common finite stage. ```agda Same : S → Type (ℓ-suc ℓ) Same c = ⟨ (c ∷ γ) ⊨ LevelAt zero (suc x) ⟩ × ( ⟨ (c ∷ γ) ⊨ LevelAt zero (suc y) ⟩ × ⟨ (c ∷ γ) ⊨ BeforeAt zero (suc x) (suc y) ⟩ ) ``` Suppose `ku < kv`. Choose the genuine numerals `# ku` and `# kv`, packaged as model elements, for the two existential witnesses. The two `LevelAt-in` results verify that these numerals describe the actual least levels of the aligned endpoints. ```agda split-in : ku < kv → Split (numS ku) (numS kv) split-in hlt = Lu.LevelAt-in (suc zero) (sh2 x) (numS kv ∷ numS ku ∷ γ) (numS-fst ku) qx , ( Lv.LevelAt-in zero (sh2 y) (numS kv ∷ numS ku ∷ γ) ``` Strict inequality of natural numbers gives `# ku ∈ # kv` by numeral monotonicity. Transporting along the projection equations of the two packaged numerals supplies the membership `fst (numS ku) ∈ fst (numS kv)` required by `Split`. ```agda (numS-fst kv) qy , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv)) (#mono ku kv hlt) ) ``` For the equal-level branch, an equation `level v ≡ level u` lets the one numeral `# ku` describe both endpoints. The left `LevelAt` reading uses `qu` directly, while the right reading uses the equality to express the level of `v` by the same index `ku`. ```agda same-in : (e : level v ≡ level u) → ⟨ before (level u) (fst u) (fst v) ⟩ → Same (numS ku) same-in e h = Lu.LevelAt-in zero (suc x) (numS ku ∷ γ) (numS-fst ku) qx , ( Level.LevelAt-in v ku (e ∙ qu) zero (suc y) (numS ku ∷ γ) ``` The conditional hypothesis `BeforeAt-in` may be used only after its boundaries are established. The level equations place both looked-up endpoints in `finiteStage ku`, while the projection equation for `numS ku` shows that the common value supplied for the numeral really denotes `# ku`. ```agda (numS-fst ku) qy , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)) (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy) ``` Finally, transport the given comparison from index `level u` to `ku` and align its two endpoints with the environment values. Together with the two stage-membership proofs, this satisfies every premise of `BeforeAt-in` and completes `Same (numS ku)`. ```agda (levelStage v ku (e ∙ qu))) (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy) (subst (λ j → ⟨ before j (fst u) (fst v) ⟩) qu h)) ) ``` Reading a `Split c d` outward first identifies `c` with `# ku` and `d` with `# kv` by the two `LevelAt-out` lemmas. After transporting `c ∈ d` along those identifications, numeral membership eliminates to `ku < kv`, and the stored level equations turn this into `level u < level v`. ```agda split-out : (c d : S) → Split c d → level u < level v split-out c d (hx , (hy , hlt)) = subst2 _<_ (sym qu) (sym qv) (#∈#-elim ku kv (subst2 (λ s t → ⟨ s ∈ t ⟩) qc qd hlt)) where qc : fst c ≡ # ku ``` Each numeral identification is obtained in the correct extended environment: the first `LevelAt` refers past both new witnesses to `x`, while the second refers to `y`. This binder alignment ensures that the final inequality compares the true levels of the original two endpoints rather than the witnesses themselves. ```agda qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx qd : fst d ≡ # kv qd = Lv.LevelAt-out zero (sh2 y) (d ∷ c ∷ γ) hy qy ``` In the common-level branch, one model element `c` serves as the proposed level numeral for both `u` and `v`. Reading its two `LevelAt` certificates therefore has two consequences: the actual levels must agree, and the assumed finite-stage formula can be read as the comparison of `u` with `v` at that common level. ```agda same-out : (c : S) → Same c → (level v ≡ level u) × ⟨ before (level u) (fst u) (fst v) ⟩ same-out c (hx , (hy , hb)) = e , below where qc : fst c ≡ # ku ``` The first certificate identifies the underlying set of `c` with `# ku`, while the second identifies it with `# kv`. Injectivity of numeral coding then gives `ku = kv`; composing this equality with the equations that define `ku` and `kv` yields `level v = level u`. Thus level equality is recovered from the shared witness rather than asserted inside the object-language formula. ```agda qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx qc' : fst c ≡ # kv qc' = Lv.LevelAt-out zero (suc y) (c ∷ γ) hy qy e : level v ≡ level u e = qv ∙ sym (#-inj′ (sym qc ∙ qc')) ∙ sym qu ``` To use the assumed reading of `BeforeAt`, both compared sets must be known to lie in the same finite stage. The level membership of `u` supplies this fact at `ku`; the newly established level equality supplies it for `v` at that very stage. The environment equations then identify those two sets with the values at `x` and `y`. ```agda xIn : ⟨ fst (lookup x γ) ∈ finiteStage ku ⟩ xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu) yIn : ⟨ fst (lookup y γ) ∈ finiteStage ku ⟩ yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy) (levelStage v ku (e ∙ qu)) ``` The abstract `BeforeAt-out` hypothesis now applies at the numeral represented by `c`. It returns `before ku` for the two environment values; replacing those values by `fst u` and `fst v`, and replacing `ku` by `level u`, produces the finite-stage component required by the limit order. This completes the common-level reading without assuming any meaning for `BeforeAt` outside its stated stage boundary. ```agda below : ⟨ before (level u) (fst u) (fst v) ⟩ below = subst (λ j → ⟨ before j (fst u) (fst v) ⟩) (sym qu) (subst2 (λ s t → ⟨ before ku s t ⟩) qx qy (BeforeAt-out zero (suc x) (suc y) (c ∷ γ) ku qc xIn yIn hb)) ``` The two mathematical clauses of `LimitOrdAt` remain visible through their adequacy laws: different levels are compared by their numeral codes, while equal levels are compared by the supplied finite-stage formula. The opaque boundary makes every use of the definition pass through those two laws. Consequently, every result inside `Described` remains conditional on its three inputs. ```agda opaque unfolding LimitOrdAt ``` Suppose first that `u` appears at a strictly earlier finite level than `v`. The object-language witness consists of the two model numerals `# ku` and `# kv`; their `LevelAt` certificates identify the levels of the two objects, and membership of the first numeral in the second expresses `ku < kv`. These data inhabit the different-level branch of `LimitOrdAt`. ```agda LimitOrdAt-in : u ≺ˡ v → ⟨ γ ⊨ LimitOrdAt x y ⟩ LimitOrdAt-in h = decide-in h where lower-in : ku < kv → ⟨ γ ⊨ LimitOrdAt x y ⟩ lower-in hlt = ∣ inl ∣ numS ku , ∣ numS kv , split-in hlt ∣₁ ∣₁ ∣₁ ``` If the levels agree, a single numeral `# ku` certifies both `LevelAt` statements. The finite-stage part of the external comparison is then written into the assumed `BeforeAt` formula at that common stage. Using one witness is significant: equality of the two levels is conveyed by sharing the numeral, so no object-language equality between two level codes is needed. ```agda inner-in : (e : level v ≡ level u) → ⟨ before (level u) (fst u) (fst v) ⟩ → ⟨ γ ⊨ LimitOrdAt x y ⟩ inner-in e k = ∣ inr ∣ numS ku , same-in e k ∣₁ ∣₁ ``` The external limit comparison presents exactly these alternatives. In its first branch, `Lift` only raises the universe of the proposition; `lower` removes that resizing and reveals the ordinary inequality of natural numbers. After the defining equations for `ku` and `kv` align the indices, the different-level constructor applies. ```agda decide-in : Lift {ℓ-zero} {ℓ-suc ℓ} (level u < level v) ⊎ ((level v ≡ level u) × ⟨ before (level u) (fst u) (fst v) ⟩) → ⟨ γ ⊨ LimitOrdAt x y ⟩ decide-in (inl k) = lower-in (subst2 _<_ qu qv (lower k)) ``` The second external alternative already contains both ingredients needed at a common level: the equality of levels and the `before` comparison there. Passing them to the common-level construction completes the filling direction. Hence `LimitOrdAt-in` follows the lexicographic definition of the existing limit order, rather than introducing a new order. ```agda decide-in (inr (e , k)) = inner-in e k ``` Reading `LimitOrdAt` starts from a propositionally truncated choice of its two branches, so the result is initially a propositionally truncated comparison. In the different-level branch, the two existential witnesses are read by `split-out`, which turns numeral membership back into strict inequality of the actual levels. That inequality is inserted into the first branch of the external limit comparison and kept under truncation. ```agda LimitOrdAt-out : ⟨ γ ⊨ LimitOrdAt x y ⟩ → ∥ u ≺ˡ v ∥₁ LimitOrdAt-out = PT.rec squash₁ decide where atSplit : (c : S) → Σ[ d ∈ S ] Split c d → ∥ u ≺ˡ v ∥₁ atSplit c (d , hs) = ∣ inl (lift (split-out c d hs)) ∣₁ ``` In the common-level branch, `same-out` returns equality of the actual levels together with the finite-stage `before` comparison. Those two pieces are precisely the second branch of the external limit comparison. No inequality is derived in this case; the ordering information comes entirely from the within-level comparison. ```agda atSame : Σ[ c ∈ S ] Same c → ∥ u ≺ˡ v ∥₁ atSame (c , hs) = ∣ inr (same-out c hs) ∣₁ ``` The semantic disjunction separates the two mathematical cases before any witnesses are inspected. Its left side contains two nested existential levels and numeral membership; its right side contains one shared level and the finite-stage formula. This shape mirrors the level-primary, then within-level, comparison of the limit order. ```agda decide : ⟨ γ ⊨ ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x) ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ⟩ ⊎ ⟨ γ ⊨ ∃̇ ( LevelAt zero (suc x) ∧̇ ( LevelAt zero (suc y) ``` Each existential is eliminated only into the propositionally truncated target. The different-level case exposes a candidate for each level and applies `atSplit`; the common-level case exposes its single shared candidate and applies `atSame`. The witnesses are used locally to justify the comparison, and no choice of level numeral escapes the truncation. ```agda ∧̇ BeforeAt zero (suc x) (suc y) ) ) ⟩ → ∥ u ≺ˡ v ∥₁ decide (inl h) = PT.rec squash₁ (λ { (c , hd) → PT.rec squash₁ (atSplit c) hd }) h decide (inr h) = PT.rec squash₁ atSame h ``` ## The order, as a set To turn comparison into a relation set, the separating condition must recognize a candidate ordered pair. `Cond₀` binds possible components `c` and `d`, requires the candidate to be the coded pair of those components, and requires `LimitOrdAt c d`. Thus the condition speaks about both the shape of an element and the direction of the represented comparison. ```agda Cond₀ : Formula S 1 Cond₀ = ∃̇ ( ∃̇ ( prAtL (sh2 zero) (suc zero) zero ∧̇ LimitOrdAt (suc zero) zero ) ) ``` Within an instance of `Described`, separation applies `Cond₀` to the common bound containing all pairs of limit-stage elements. The resulting model element `codeOrder` contains exactly the candidates in that bound that satisfy the comparison condition. Its existence is conditional on the supplied `BeforeAt` formula and its two adequacy directions; the concrete instance is provided in the next chapter. ```agda opaque codeOrder : S codeOrder = hasSeparationL (pairsBound .fst) Cond₀ .fst .fst ``` The separation specification is the usable characterization of membership: a candidate lies in `codeOrder` exactly when it lies in `pairsBound` and satisfies `Cond₀`. The bound alone may contain extra elements, so it supplies only set-sized containment. Exactness comes from the second conjunct, which identifies an ordered pair and verifies its limit comparison. ```agda codeOrder-mem : (z : S) → (z ∈ˢ codeOrder) ≡ ((z ∈ˢ pairsBound .fst) ⊓ ((z ∷ []) ⊨ Cond₀)) codeOrder-mem = hasSeparationL (pairsBound .fst) Cond₀ .fst .snd ``` For fixed `z`, `c`, and `d`, `Inner` isolates the two facts required by the separating formula: `z` is the coded ordered pair of `c` and `d`, and `c` precedes `d` according to `LimitOrdAt`. Keeping these facts together makes clear that the endpoints used by the comparison are the very components encoded by the candidate pair. ```agda private Inner : S → S → S → Type (ℓ-suc ℓ) Inner z c d = ⟨ (d ∷ c ∷ z ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ × ⟨ (d ∷ c ∷ z ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩ ``` `Outer z` displays the witness pattern of the two nested existential quantifiers. A first component `c` is accompanied by the propositionally truncated existence of a second component `d` satisfying `Inner z c d`. The nesting matches the semantics of `Cond₀` and preserves witness dependence without choosing a canonical decomposition of `z`. ```agda Outer : S → Type (ℓ-suc ℓ) Outer z = Σ[ c ∈ S ] ∥ (Σ[ d ∈ S ] Inner z c d) ∥₁ ``` Given actual components and the two facts in `Inner`, the separating condition is satisfied by placing those components under its nested existential quantifiers. Both existential witnesses are propositionally truncated, as object-language existence records only that suitable components occur. This is sufficient for separation because membership in the resulting set is itself a proposition. ```agda cond-in : (z c d : S) → Inner z c d → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ cond-in z c d hi = ∣ c , ∣ d , hi ∣₁ ∣₁ ``` Conversely, satisfaction of `Cond₀` already has the truncated nested shape recorded by `Outer`. The reading therefore preserves that evidence directly, without selecting either component. This small observation is what allows later membership proofs to unpack the separating condition while remaining entirely within propositionally truncated existence. ```agda cond-out : (z : S) → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ → ∥ Outer z ∥₁ cond-out z h = h ``` The filling law begins with an external comparison `u ≺ˡ v` and aims to place the ordinary ordered pair of their underlying sets in `codeOrder`. The proof first works with `limitEl u` and `limitEl v`, which are genuine elements of the model, and with their model-coded pair. A final equality relates that internal presentation to `pr (fst u) (fst v)`. ```agda codeOrder-fill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ codeOrder-fill u v h = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) qz (subst ⟨_⟩ (sym (codeOrder-mem (prS (limitEl u) (limitEl v)))) ``` The separation specification reduces the membership goal to two mathematical obligations. The model-coded pair must lie in the common bound, and `Cond₀` must hold with `limitEl u` and `limitEl v` as its two witnesses. Once these obligations are met, separation returns membership, which is then transported along the equality of the two pair presentations. ```agda (inBound , cond-in (prS (limitEl u) (limitEl v)) (limitEl u) (limitEl v) (hpr , hord))) where qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v) qz = prS-fst (limitEl u) (limitEl v) ``` The alignment equality is obtained in two transparent steps. The projection of the model pairing is the external pair of the projections, and each `limitEl` projects to the underlying set of its original limit element. Combining these facts ensures that changing presentation does not change either endpoint or their order. ```agda ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v) ``` The first separation obligation uses the defining property of `pairsBound`: it covers the ordered pair arising from every two elements of the limit stage. The pair is aligned with that covered external pair before the bound certificate is used. No converse property of the bound is needed, since `Cond₀` supplies the exact comparison criterion. ```agda inBound : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst (pairsBound .fst) ⟩ inBound = subst (λ t → ⟨ t ∈ fst (pairsBound .fst) ⟩) (sym qz) (pairsBound .snd u v) ``` The pairing conjunct of `Cond₀` is established by adequacy of `prAtL`. The model pairing already projects to the required ordered pair, so that adequacy law turns the projection equality into satisfaction of the pairing atom. This connects the set-theoretic pair used by the bound with the object-language description used by separation. ```agda hpr : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate (sh2 zero) (suc zero) zero (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []))) (prS-fst (limitEl u) (limitEl v)) ``` The comparison conjunct is supplied by `LimitOrdAt-in` at the environment containing the candidate pair and its two components. Its alignment equations are reflexive after the components are chosen as `limitEl u` and `limitEl v`, and the original hypothesis `u ≺ˡ v` supplies the comparison. This finishes the conditional representation of the forward direction. ```agda hord : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩ hord = Order.LimitOrdAt-in (suc zero) zero (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v) refl refl (limitEl-fst u) (limitEl-fst v) h ``` The reading law starts from membership of `pr (fst u) (fst v)` in `codeOrder`. Separation will yield a propositionally truncated pair of components satisfying the pairing and comparison conditions; reading those conditions gives only `∥ u ≺ˡ v ∥₁`. The final use of `strictLimit` is justified by the already proved strict well order `limitOrder`, whose trichotomy excludes equality and the reverse comparison. ```agda codeOrder-rep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ → u ≺ˡ v codeOrder-rep u v h = strictLimit u v (PT.rec squash₁ atC (cond-out (prS (limitEl u) (limitEl v)) ``` As in the filling direction, the model-coded pair is identified with the external pair of the two underlying sets. After membership is transferred to that presentation, `codeOrder-mem` exposes the two conjuncts of separation, and its second conjunct is satisfaction of `Cond₀`. The proof can ignore the bound conjunct from this point, because all endpoint information lies in the separating condition. ```agda (subst ⟨_⟩ (codeOrder-mem (prS (limitEl u) (limitEl v))) inSet .snd))) where qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v) qz = prS-fst (limitEl u) (limitEl v) ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v) ``` The given membership concerns the external pair, whereas the separating specification is applied to the model element produced by `prS`. Their underlying sets are equal by the pair-alignment equation, so membership transports to the model presentation. This change of presentation is essential before the object-language condition can be read in the environment carried by that model element. ```agda inSet : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst codeOrder ⟩ inSet = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) (sym qz) h ``` For particular witnesses `c` and `d`, the pairing atom first shows that they are the endpoints encoded by the original pair. With those endpoint equalities in the required orientation, `LimitOrdAt-out` reads the accompanying comparison formula as a propositionally truncated `u ≺ˡ v`. Thus the comparison cannot be read independently of the pairing conjunct: the latter identifies which external limit elements the formula is about. ```agda atD : (c d : S) → Inner (prS (limitEl u) (limitEl v)) c d → ∥ u ≺ˡ v ∥₁ atD c d (hpr , hord) = Order.LimitOrdAt-out (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v) refl refl (sym (split .fst)) (sym (split .snd)) hord where ``` Adequacy of the pairing atom turns its satisfaction into an equality between the candidate's underlying set and `pr (fst c) (fst d)`. The earlier alignment identifies that same candidate with `pr (fst u) (fst v)`. Composing the two equalities therefore equates the two ordered pairs and prepares the endpoint identities needed to read `LimitOrdAt`. ```agda qcd : pr (fst u) (fst v) ≡ pr (fst c) (fst d) qcd = sym qz ∙ subst ⟨_⟩ (prAtL-adequate (sh2 zero) (suc zero) zero (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ [])) hpr split : (fst u ≡ fst c) × (fst v ≡ fst d) ``` Injectivity of ordered-pair coding separates that pair equality into `fst u = fst c` and `fst v = fst d`. Both position and direction are preserved, so the left component cannot be exchanged with the right. Reversing these equalities gives exactly the alignment hypotheses expected by the reading theorem for `LimitOrdAt`. ```agda split = pr-inj qcd ``` The outer reader processes the nested witnesses in the same order as `Cond₀` binds them: first `c`, then a truncated `d` together with `Inner`. Each elimination targets the propositionally truncated comparison already produced by `atD`, so truncation is respected throughout. After all possible decompositions have been mapped to that proposition, `strictLimit` supplies the final untruncated comparison. ```agda atC : Outer (prS (limitEl u) (limitEl v)) → ∥ u ≺ˡ v ∥₁ atC (c , hd) = PT.rec squash₁ (λ { (d , hi) → atD c d hi }) hd ``` ## The code slot, filled `CodeKeys` records one possible use of the conditional code relation in name comparison over an arbitrary constructible carrier `A`. Besides `A` and its constructibility proof, it fixes a strict well-order `w` on the small type of members of `A`. The name-comparison adequacy results may then use `w` for parameters and the current `Described` instance for codes. This nested module is a reusable consequence of the representation theorem; the main construction does not depend on it. ```agda module CodeKeys (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where private module Ad = Adequacy A pA w ``` The strict relation of `w` is given a local symbol to keep the parameter comparison distinct from `u ≺ˡ v`, the limit-stage comparison used for codes. This distinction matters because the two relations live on different carriers and receive separate internal relation sets. Their adequacy laws have the same shape, but their mathematical inputs are independent. ```agda open SWO w using () renaming ( _<∙_ to _≺ₚ_ ) ``` If a model relation `Ps` represents the parameter order in both directions, `AtParams` presents it together with `codeOrder` and the two code-order representation laws to `Adequacy.Keys`. The two represented relations remain mathematically independent. The actual downstream route instantiates `Described` in `EarliestDisagreement`, exports `codeOrder`, `codeOrder-fill`, and `codeOrder-rep`, and has `InternalWellOrder` pass those three results directly to `NameComparisonAdequacy.At.Least` together with the separately represented parameter order. ```agda module AtParams (Ps : S) (Prep : (a b : ⟪ A ⟫) → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩ → a ≺ₚ b) (Pfill : (a b : ⟪ A ⟫) → a ≺ₚ b → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩) where open Ad.Keys codeOrder Ps codeOrder-rep codeOrder-fill Prep Pfill public ``` ## What is left, named exactly The remaining input to `Described` is a formula `BeforeAt` together with its two readings. These readings are required only when the first value is the numeral `# m` and the two endpoints belong to `finiteStage m`; under those hypotheses, satisfaction of the formula is equivalent to `before m` comparing the endpoints. The module `EarliestDisagreement` supplies exactly this data: `relAt m` represents `before m`, `beforeFam` collects these represented relations over the internal natural numbers, and its `BeforeAt` retrieves the relation at the given numeral before applying it. Instantiating `Described` with these results yields the public relation set `codeOrder` and its two representation laws, `codeOrder-fill` and `codeOrder-rep`. ## Recap `LevelAt` identifies the numeral coding the least finite stage in which a given limit-stage member appears, while `PrecedesAt` represents one earliest-disagreement comparison relative to any already represented base relation. Given the bounded two-way reading of `BeforeAt`, `Described` combines unequal-level and equal-level comparison in `LimitOrdAt`, bounds all candidate ordered pairs, and separates the conditional relation set `codeOrder`. Its filling and reading laws give, for every `u,v : Limit`, both directions between `u ≺ˡ v` and membership of `pr (fst u) (fst v)` in that set; the reading direction uses `strictLimit` and the existing strict well-order to recover a comparison from propositional truncation. `EarliestDisagreement` discharges the finite-stage hypotheses, but this chapter neither asserts an object-language well-ordering of `codeOrder` nor proves the Axiom of Choice.