BedrockThe limit-stage order inside L
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapAn 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
⇒̇ ¬̇ (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.
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.
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.
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.
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.
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.
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.
(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.
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.
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.
(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.
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.
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.
(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.
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).
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.
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.
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.
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.
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.
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.
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.
∧̇ ∀̇∈ (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.
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.
→ ⟨ 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(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.
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.
→ ⟨ γ ⊨ 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(∈∈ₛ {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.
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).
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.
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.
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.
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.
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.
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.
→ ⟨ 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.
→ ⟨ 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.
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.
∨̇ ∃̇ ( 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.
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.
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.
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.
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.
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.
(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.
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.
(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).
(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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
∧̇ 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.
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.
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.
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.
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.
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.
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.
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).
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.
(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.
∙ 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.
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.
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.
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.
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.
(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.
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.
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.
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.
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.
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.
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.
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.
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.