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