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