BedrockAn internal family of earliest-disagreement relations
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapAt each finite stage, before n compares two sets at their earliest disagreement. This chapter represents that relation by a set relAt n inside L, assembles these sets into a numeral-indexed family, and expresses lookup in that family by the object-language formula BeforeAt. Instantiating Described with this formula yields codeOrder, which later supplies the comparison of codes used in name comparison. The chapter itself neither compares names nor proves that comparison well-founded.
{-# OPTIONS --cubical --safe --guardedness #-}
The construction uses excluded middle only through the explicit hypothesis that will be attached to the module. Thus the classical assumption remains visible in every result exported from this development.
open import Base.Prelude open import Base.Classical using ( LEM )
Fix a universe level ℓ and assume LEM (ℓ-suc ℓ). All sets, formulas, and proposition-valued relations below live at the levels determined by this choice.
module L.Choice.EarliestDisagreement {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
We shall describe relations by first-order formulas over the cumulative hierarchy. Ordered pairs serve as relation entries, and their injectivity will later let us recover the two compared sets from a coded entry.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ¬̇_; ∃̇_; ∀̇∈; ∃̇∈ ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
The finite stage at n is Lset (# n), where # n is the von Neumann numeral inside the hierarchy. Its ordinal and constructibility proofs let us treat both the stage and each of its members as objects of the model of L.
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; Lset-mono ) open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; mem-ord; boundingOrd ) open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
Two set-forming operations play different roles. Separation cuts each single-stage relation out of a bound, while replacement will later collect the relations along the internal ω. Finite approximations themselves will instead be built by finSet and finSetL.
open import L.Axioms.Basic {ℓ} using ( extensionalL; LsetS; ∅ʟ; finSet; finSet-in; finSet-out; module FinOf ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL ) open import L.Recursion {ℓ} lem using ( smallDom; mereFunct ) open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
The mathematical recurrence is already fixed: before zero is empty, and before (suc n) compares members of the next finite stage by their earliest disagreement over finiteStage n, using before n for earlier points. PrecedesAt expresses that successor step in the object language, while RecShape will organize its finite approximations.
open import L.Choice.FiniteStageOrders {ℓ} lem using ( before; precedes; Agrees; Witness; finiteStage ) open import L.Choice.LimitStageOrder {ℓ} lem using ( PrecedesAt; module Precedes; module Described ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt; module RecShape )
Object-language application and extensionality let a formula say that a set is the value of a relation-valued table. They will be used first to describe one recursive step and later to read the completed family at a numeral.
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; appC; appC-adequate; domAt-intro ) open import L.Coding.Expressions {ℓ} using ( numL; extAt; extAt-out; extAt-in; extAt-in-both )
The proofs repeatedly transport equalities of sets and ordered pairs. They also require induction over the strict order on natural numbers, which will establish uniqueness of every value recorded by an approximation.
import FOL.Absoluteness import FOL.ZFModel open import Cubical.Foundations.Prelude using ( subst2 ) open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Data.Nat.Order using
This induction uses the well-foundedness of natural-number <: the value at k is determined after all values at smaller indices have been identified. This is separate from any well-foundedness property of before.
( _<_; <-trans; <-asym; pred-≤-pred; <-wellfounded; _≟_ ) import Cubical.Data.Nat.Order as NatOrder open import Cubical.Induction.WellFounded using ( module WFI ) open import Cubical.Functions.Logic using ( ⇔toPath ) open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )
Several witnesses below are available only under propositional truncation. Such a witness certifies existence without selecting canonical data; it may be eliminated when the target is a proposition, such as membership, before, or equality of sets in V.
open import Cubical.Data.FinData.Base using ( toℕ ) 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 )
A set is accessed through a presentation of its members. This presentation lets us range over all members of a finite stage and construct their ordered pairs, while the internal ω supplies the eventual domain of the whole family.
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet ) open InfinitySet using ( #_; ω )
From now on formulas are interpreted in the proposition-valued structure carried by the constructible sets.
open hPropStructure 𝒮ʟ
The carrier S consists of a set together with evidence that it belongs to L. Thus constructing an internal relation requires both the underlying set and its constructibility evidence.
module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf )
Absoluteness connects satisfaction in this structure with the corresponding assertions about the underlying sets. The notation γ ⊨ φ will express that a valuation γ satisfies an object-language formula φ.
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
Binding two new variables shifts every previous de Bruijn position by two. The map sh2 records this shift so that each free variable still denotes the same object beneath the new binders.
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
Applying the two-place shift twice gives sh4, the adjustment needed under four additional binders.
sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = sh2 (sh2 i)
Similarly, sh6 preserves references under six additional binders. These shifts change only de Bruijn positions, not the mathematical content of the formulas.
sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = sh2 (sh4 i)
The object stageS n packages the finite stage Lset (# n) as an element of the constructible carrier. Keeping this package opaque prevents later reasoning from depending on its particular proof component.
opaque stageS : ℕ → S stageS n = LsetS (# n) (numeral-ord n)
The equation stageS-fst reveals exactly the mathematical set carried by that package: its first component is finiteStage n.
stageS-fst : (n : ℕ) → fst (stageS n) ≡ finiteStage n stageS-fst n = refl
The object numS k similarly packages the von Neumann numeral # k together with the proof that it is constructible.
numS : ℕ → S numS k = # k , numL k
The equation numS-fst lets later formulas read the underlying numeral without exposing the proof stored beside it.
numS-fst : (k : ℕ) → fst (numS k) ≡ # k numS-fst k = refl
If z belongs to a constructible set A, transitivity of L shows that z is constructible as well. The wrapper memS A z h records this consequence so that z may be used as a model element.
memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A)
The first component of memS A z h is still the original set z; the additional component supplies only its membership in L.
memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z memS-fst A z h = refl
For model elements a and b, prS a b forms their ordered pair inside L. Relation sets below will contain objects of precisely this form.
prS : S → S → S prS a b = prʟ a b
Forgetting the constructibility evidence recovers the ordinary ordered pair pr (fst a) (fst b). This equation connects internal membership statements with the relation before on underlying sets.
prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b) prS-fst a b = prʟ-fst a b
In particular, every member x of finiteStage n can be lifted to the carrier S. The stage itself supplies the constructibility proof required for this lift.
stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h
Each stage's relation, as an element of L
To represent a relation by separation, we first need one set containing every possible entry. The object pairsAt n therefore supplies a constructible bound D containing pr u v whenever both u and v belong to finiteStage n.
pairsAt : (n : ℕ) → Σ[ D ∈ S ] ((u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩ → ⟨ pr u v ∈ fst D ⟩) pairsAt n = d .fst , onPair where
A presented member of the finite stage already comes with its membership proof. The map ixL attaches the resulting constructibility proof, turning each presented member into an element of S.
ixL : ⟪ finiteStage n ⟫ → S ixL m = ⟪ finiteStage n ⟫↪ m , Lset→isL (# n) (numeral-ord n) (⟪ finiteStage n ⟫↪ m) (∈∈ₛ {a = ⟪ finiteStage n ⟫↪ m} {b = finiteStage n} .snd (∈ₛ⟪ finiteStage n ⟫↪ m))
The product of the two presentations indexes every pair of stage members. Applying smallDom to their internal ordered pairs places this entire indexed family inside one constructible set D.
d : Σ[ D ∈ S ] ((p : ⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫) → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩) d = smallDom (⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
Given arbitrary u,v ∈ finiteStage n, their membership proofs locate presentation indices fu and fv. The bound contains the pair at those indices, and transport along the recovered component equalities yields membership of pr u v itself.
onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩ → ⟨ pr u v ∈ fst (d .fst) ⟩ onPair u v hu hv = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩) (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd)) (d .snd (fu .fst , fv .fst))
The two fibers fu and fv record exactly the presentation indices and the equalities identifying their represented members with u and v.
where fu = ∈-asFiber {a = u} {b = finiteStage n} hu fv = ∈-asFiber {a = v} {b = finiteStage n} hv
Suppose that, on the same carrier A, every instance of R' w z implies R w z. Then an earliest-disagreement witness for R also gives one for R'. The direction reverses because the earlier-point relation occurs as an assumption in the agreement clause.
precedes-map : (R R' : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (A x y : V ℓ) → ((w z : V ℓ) → ⟨ w ∈ A ⟩ → ⟨ z ∈ A ⟩ → ⟨ R' w z ⟩ → ⟨ R w z ⟩) → ⟨ precedes R A x y ⟩ → ⟨ precedes R' A x y ⟩ precedes-map R R' A x y f = PT.map step where
The disagreement point z, its membership in A and y, and its absence from x remain unchanged. Only the proof that x and y agree before z must be converted.
step : Σ[ z ∈ V ℓ ] Witness R A x y z → Σ[ z ∈ V ℓ ] Witness R' A x y z step (z , (z∈A , (z∈y , (z∉x , ag)))) = z , (z∈A , (z∈y , (z∉x , ag'))) where ag' : Agrees R' A x y z
At an earlier point w, an assumption R' w z is first mapped to R w z and then passed to the original agreement proof. This establishes the required agreement relative to R'.
ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR')
The separation condition receives a candidate relation entry as its only free variable. It existentially binds the previous relation and previous stage, pins them to the supplied constants by equality, and ranges the two endpoints over the current stage.
RelCond : (R A A' : S) → Formula S 1 RelCond R A A' = ∃̇ ( (var zero ≐ con R) ∧̇ ∃̇ ( (var zero ≐ con A) ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A')
The remaining conjunct identifies the candidate with the ordered pair of the two endpoints and asserts PrecedesAt over the supplied earlier stage and relation. This is the successor comparison later used in the recursive step; here RelCond fixes the earlier stage and relation by constants, whereas the recursive formula obtains the relation from an approximation and identifies the stage through the hierarchy graph.
( prAtL (sh2 (sh2 zero)) (suc zero) zero ∧̇ PrecedesAt (sh2 (suc zero)) (sh2 zero) (suc zero) zero ) ) ) )
Now define the representing sets recursively. At zero the relation is empty; at a successor, separation begins with the bound containing all pairs from the larger finite stage.
opaque relAt : ℕ → S relAt zero = ∅ʟ relAt (suc n) = hasSeparationL (pairsAt (suc n) .fst)
From that bound, RelCond (relAt n) (stageS n) (stageS (suc n)) selects exactly the pairs whose endpoints are compared by the successor clause based on the preceding relation.
(RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .fst
The equation relAt-zero records the base case explicitly, so a purported member of the zero-stage relation can later be reduced to membership in the empty set.
relAt-zero : relAt zero ≡ ∅ʟ relAt-zero = refl
For a successor stage, membership in relAt (suc n) has two parts: the candidate lies in the pair bound, and it satisfies the separating formula determined by relAt n, the preceding stage, and the current stage.
relAt-mem : (n : ℕ) (z : S) → (z ∈ˢ relAt (suc n)) ≡ ( (z ∈ˢ pairsAt (suc n) .fst) ⊓ ((z ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n))) ) relAt-mem n =
This equivalence is the exact specification supplied by separation. Later proofs use it in both directions, either extracting the formula from membership or assembling membership from a bound proof and a formula proof.
hasSeparationL (pairsAt (suc n) .fst) (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .snd
The predicate Rel n a b abbreviates membership of the ordered pair pr a b in the representing set relAt n. The next representation lemmas will show, for stage members, that this predicate is equivalent to before n a b.
Rel : ℕ → V ℓ → V ℓ → hProp (ℓ-suc ℓ) Rel n a b = pr a b ∈ fst (relAt n)
The proofs of those lemmas interpret PrecedesAt in an environment of five entries. The names s1 and s2 identify the two endpoint and stage positions after the surrounding binders have shifted them.
private s1 : Fin 5 s1 = suc zero s2 : Fin 5 s2 = sh2 zero
The remaining positions s3 and s4 locate the previous relation and the coded ordered pair. Naming them once keeps the semantic argument aligned with the four roles in RelCond.
s3 : Fin 5 s3 = sh2 (suc zero) s4 : Fin 5 s4 = sh2 (sh2 zero)
To recognize an arbitrary member of the relation set, we must recover its two components. RelOf k zv therefore asks for x,y in finiteStage k, an equation identifying zv with their ordered pair, and a proof that before k x y holds. This witness type contains chosen components, so it is not itself a proposition.
RelOf : (k : ℕ) → V ℓ → Type (ℓ-suc ℓ) RelOf k zv = Σ[ x ∈ S ] Σ[ y ∈ S ] ( ⟨ fst x ∈ finiteStage k ⟩ × ( ⟨ fst y ∈ finiteStage k ⟩ × ( (zv ≡ pr (fst x) (fst y)) × ⟨ before k (fst x) (fst y) ⟩ ) ) )
Membership in relAt k determines such components only under propositional truncation: the relation records that a suitable presentation exists, without choosing one canonically. In the reverse direction, explicit components and their comparison suffice to insert the pair into the relation.
relAt-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ fst (relAt k) ⟩ → ∥ RelOf k zv ∥₁ relAt-in : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ fst (relAt k) ⟩
The base case reflects before zero: since relAt zero is empty, a supposed member yields a contradiction. At a successor, membership first exposes the separated condition, whose existential witnesses are available only through propositional truncation.
relAt-out zero zv h = Empty.rec (∅-empty zv (∈∈ₛ {a = zv} {b = ∅} .fst (subst (λ t → ⟨ zv ∈ fst t ⟩) relAt-zero h))) relAt-out (suc n) zv h = PT.rec squash₁ (λ { (r , (qr , ha)) → PT.rec squash₁
Opening the truncated witnesses reveals a candidate predecessor relation, its finite stage, and the two components of the pair. The proof keeps the result truncated while it passes these data to the final reconstruction, so no particular presentation escapes as chosen data.
(λ { (a , (qa , hx)) → PT.rec squash₁ (λ { (x , (x∈ , hy)) → PT.map (atY r a x qr qa x∈) hy }) hx }) ha }) cond where zS : S zS = memS (relAt (suc n)) zv h
The underlying set zv is packaged as an element of L using its membership in relAt (suc n). This permits the object-language separation condition to be evaluated at the very member being analyzed.
qz : fst zS ≡ zv qz = memS-fst (relAt (suc n)) zv h
The defining property of separation turns the assumed membership into satisfaction of RelCond. Thus the rest of the argument may reason from the mathematical content of the condition rather than merely from membership in the bounded set of pairs.
cond : ⟨ (zS ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩ cond = subst ⟨_⟩ (relAt-mem n zS) (subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (sym qz) h) .snd
For proposed components x,y, the remaining body says two things: the analyzed member is their ordered pair, and x precedes y by earliest disagreement over the preceding stage. The second statement still uses the relation represented by r, since the surrounding witness must identify that relation with relAt n.
Body : (r a x y : S) → Type (ℓ-suc ℓ) Body r a x y = ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ prAtL s4 s1 zero ⟩ × ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩
After x has been chosen from the successor stage, AtY records the remaining choice of y from that same stage together with the pair and comparison facts. This separation of the two choices matches the nested existential structure of RelCond.
AtY : (r a x : S) → Type (ℓ-suc ℓ) AtY r a x = Σ[ y ∈ S ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y)
Once all witnesses are present, the stage equations place both components in finiteStage (suc n). It remains to identify the analyzed member with their ordered pair and to translate the comparison based on the represented relation into before (suc n); the next lemmas perform these two translations.
atY : (r a x : S) → fst r ≡ fst (relAt n) → fst a ≡ fst (stageS n) → ⟨ fst x ∈ fst (stageS (suc n)) ⟩ → AtY r a x → RelOf (suc n) zv atY r a x qr qa x∈ (y , (y∈ , (hpr , hprec))) = x , (y , ( subst (λ t → ⟨ fst x ∈ t ⟩) (stageS-fst (suc n)) x∈ , ( subst (λ t → ⟨ fst y ∈ t ⟩) (stageS-fst (suc n)) y∈
The equation identifying the supplied relation with relAt n lets any recorded predecessor pair be read as Rel n. This is one direction needed to interpret the generic PrecedesAt statement with the concrete relation constructed here.
, (sym qz ∙ qpair , below) ) ) ) where Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩ → ⟨ Rel n (fst s) (fst t) ⟩ Rrep s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) qr p
The converse transport writes a proof of Rel n back into the supplied relation. Having both directions allows the adequacy theorem for PrecedesAt to treat the two presentations as the same base relation.
Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩
→ ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
Rfill s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) (sym qr) p
With these representation maps fixed, the Precedes module supplies the semantic bridge between the object-language formula and the host predicate precedes. The bridge concerns one comparison step; it does not establish any order laws here.
module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ []) (Rel n) Rrep Rfill
Reading PrecedesAt yields a precedes comparison over the stage supplied by the formula. The stage equation then identifies that carrier with finiteStage n, which is the carrier used in the recursive definition of before (suc n).
onStage : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩ onStage = subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩) (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)
Inside the agreement clause, every use of the base relation must be converted from before n to membership in relAt n. The inductive inward lemma performs that conversion, and precedes-map then yields exactly the successor relation before (suc n).
below : ⟨ before (suc n) (fst x) (fst y) ⟩ below = precedes-map (Rel n) (before n) (finiteStage n) (fst x) (fst y) (λ w t hw ht hb → relAt-in n (pr w t) (stageEl n w hw , (stageEl n t ht , (hw , (ht , (refl , hb)))))) onStage
The adequacy of the pair formula identifies the packaged member with pr (fst x) (fst y). Composing this equation with the packaging equation returns the required equality for the original zv.
qpair : fst zS ≡ pr (fst x) (fst y)
qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr
For k = 0, a RelOf witness already contains an impossible proof of before zero, so the inward direction follows by contradiction. At a successor, the intended pair is inserted into the bounded set and shown to satisfy the separation condition.
relAt-in zero zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = Empty.rec* hb relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (prS-fst x y ∙ sym qq) (subst ⟨_⟩ (sym (relAt-mem n (prS x y))) (inBound , cond)) where
The two stage-membership assumptions place the ordered pair inside pairsAt (suc n). This is the bounding half of separation: only pairs of members of the finite stage can enter relAt (suc n).
inBound : ⟨ prS x y ∈ˢ pairsAt (suc n) .fst ⟩ inBound = subst (λ t → ⟨ t ∈ fst (pairsAt (suc n) .fst) ⟩) (sym (prS-fst x y)) (pairsAt (suc n) .snd (fst x) (fst y) x∈ y∈)
For the reverse construction the environment contains the actual predecessor relation relAt n, so its interpretation as Rel n needs only identity maps. The same semantic bridge can therefore be used to build PrecedesAt from a host comparison.
module P = Precedes s3 s2 s1 zero (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) (Rel n) (λ _ _ p → p) (λ _ _ p → p)
The hypothesis before (suc n) x y unfolds to earliest disagreement using before n. To express the same agreement with the internal relation, each recorded preceding pair is read out through relAt-out; propositional truncation may be eliminated because the target before n w t is a proposition.
held : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩ held = precedes-map (before n) (Rel n) (finiteStage n) (fst x) (fst y) (λ w t hw ht hR → PT.rec (snd (before n w t)) (readBack w t) (relAt-out n (pr w t) hR)) hb
A recovered RelOf witness may name components different from w,t, but its pair equation says their ordered pair equals pr w t. Injectivity of ordered pairing identifies both components, after which the recorded before n proof has the required endpoints.
where readBack : (w t : V ℓ) → RelOf n (pr w t) → ⟨ before n w t ⟩ readBack w t (p , (q , (p∈ , (q∈ , (qq' , hbf))))) = subst2 (λ s u → ⟨ before n s u ⟩) (sym (pr-inj qq' .fst)) (sym (pr-inj qq' .snd)) hbf
The converted host comparison now satisfies the hypotheses of PrecedesAt-in. It supplies the comparison clause needed for the separation formula, with the predecessor stage and relation placed in their designated variables.
hprec : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩ hprec = P.PrecedesAt-in (subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩) (sym (stageS-fst n)) held)
The pair-recognition formula is satisfied because the candidate member was built as prS x y. Its adequacy equation connects the internal construction with the underlying ordered pair required by the formula.
hpr : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ prAtL s4 s1 zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate s4 s1 zero (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []))) (prS-fst x y)
The presentation equation for stageS (suc n) transports each known member of finiteStage (suc n) into the stage object used by the formula. No additional closure property is required.
onStage : (w : V ℓ) → ⟨ w ∈ finiteStage (suc n) ⟩ → ⟨ w ∈ fst (stageS (suc n)) ⟩ onStage w hw = subst (λ t → ⟨ w ∈ t ⟩) (sym (stageS-fst (suc n))) hw
The witnesses just constructed satisfy the complete separation condition: they identify the preceding relation and stage, place x,y in the successor stage, and establish both pairing and earliest disagreement. The nested existentials are introduced under propositional truncation, asserting existence without selecting canonical witnesses.
cond : ⟨ (prS x y ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩ cond = ∣ relAt n , (refl , ∣ stageS n , (refl , ∣ x , (onStage (fst x) x∈ , ∣ y , (onStage (fst y) y∈ , (hpr , hprec)) ∣₁) ∣₁) ∣₁) ∣₁
The useful outward interface starts with a known pair pr u v, where both endpoints already lie in finiteStage n. It eliminates the truncated presentation only into the proposition before n u v, so the absence of a canonical presentation causes no loss.
relAt-rep : (n : ℕ) (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩ → ⟨ pr u v ∈ fst (relAt n) ⟩ → ⟨ before n u v ⟩ relAt-rep n u v hu hv h = PT.rec (snd (before n u v)) read (relAt-out n (pr u v) h) where
If the recovered presentation uses components p,q, equality of its ordered pair with pr u v forces p=u and q=v. Transporting along these two equalities turns the stored comparison into the desired one.
read : RelOf n (pr u v) → ⟨ before n u v ⟩ read (p , (q , (p∈ , (q∈ , (qq , hbf))))) = subst2 (λ s t → ⟨ before n s t ⟩) (sym (pr-inj qq .fst)) (sym (pr-inj qq .snd)) hbf
Conversely, stage membership of u,v and a proof of before n u v form an explicit RelOf witness for pr u v. The inward lemma then records that pair in relAt n, completing the pointwise representation in the other direction.
relAt-fill : (n : ℕ) (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩ → ⟨ before n u v ⟩ → ⟨ pr u v ∈ fst (relAt n) ⟩ relAt-fill n u v hu hv h = relAt-in n (pr u v) (stageEl n u hu , (stageEl n v hv , (hu , (hv , (refl , h)))))
The step, generic in everything it consults
The recursive description must accept a relation as data rather than refer directly to relAt. Held r a b gives the needed interpretation: r relates a to b exactly when it contains their ordered pair.
Held : S → V ℓ → V ℓ → hProp (ℓ-suc ℓ) Held r a b = pr a b ∈ fst r
One recursive step first seeks an ∈-maximal member c of the current index. When that index is the successor numeral # (suc n), this member is its predecessor # n; at zero no such member exists. Consequently the relation defined by the step has no members at zero, without requiring a separate base formula.
opaque RelBodyAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n RelBodyAt z b f = ∃̇ ( (var zero ∈̇ var (suc b)) ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero))
Having found c, the formula reads from the approximation the relation stored at c. The hierarchy graph identifies the stages Lset (fst c) and Lset of the current index, and the two candidate endpoints range over the latter. These stages become finite stages only when the current index is identified with a numeral.
∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero)) ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b) ∧̇ ∃̇∈ (var zero) ( ∃̇∈ (var (suc zero))
The innermost clauses require the candidate entry to be the ordered pair of those endpoints and compare them by PrecedesAt over the predecessor stage, using the relation recovered from the approximation. Thus the formula describes the recursive successor step without naming any particular relAt n.
( prAtL (sh6 z) (suc zero) zero ∧̇ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero ) ) ) ) ) ) )
StepOf is the meta-level meaning of this formula. It chooses four model elements: a candidate maximal member c of the current index, the relation value r recorded there, and the endpoints x,y; the candidate entry zv is already an argument of the predicate. Only after the current index is identified with a numeral will c be identified with its predecessor numeral.
StepOf : ∀ {n} → Fin n → Fin n → S ^ n → V ℓ → Type (ℓ-suc ℓ) StepOf b f γ zv = Σ[ c ∈ S ] Σ[ r ∈ S ] Σ[ x ∈ S ] Σ[ y ∈ S ] ( ⟨ fst c ∈ fst (lookup b γ) ⟩ × ( ((d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥)
The accompanying conditions say that c belongs to the current index and is ∈-maximal there, the approximation records r at c, both endpoints lie in the hierarchy stage indexed by the current value, zv is their ordered pair, and precedes (Held r) compares them over Lset (fst c). These are the mathematical data needed for one step; finiteness enters later from the numeral equation.
× ( ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ × ( ⟨ fst x ∈ Lset (fst (lookup b γ)) ⟩ × ( ⟨ fst y ∈ Lset (fst (lookup b γ)) ⟩ × ( (zv ≡ pr (fst x) (fst y)) × ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩ ) ) ) ) ) )
The semantic correspondence is now proved for arbitrary variables z,b,f and an arbitrary environment. The assumption that lookup b γ carries an ordinal is used to identify the stages described by the hierarchy graph with the corresponding Lset values.
module _ {n : ℕ} (z b f : Fin n) (γ : S ^ n) (ob : IsOrd (fst (lookup b γ))) where private Body : (c r A A' x y : S) → Type (ℓ-suc ℓ) Body c r A A' x y =
After the six existential witnesses have extended the environment, the innermost body retains the two decisive facts: the value denoted by z is the ordered pair of x,y, and those endpoints satisfy PrecedesAt for the recovered stage and relation.
⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩ × ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero ⟩
For a fixed first endpoint x, AtY packages the remaining endpoint y, its membership in the current stage, and the two innermost facts. This type mirrors one layer of the formula's nested existential reading.
AtY : (c r A A' x : S) → Type (ℓ-suc ℓ) AtY c r A A' x = Σ[ y ∈ S ] (⟨ fst y ∈ fst A' ⟩ × Body c r A A' x y)
MaxOf c expresses maximality in the membership order: if d also belongs to the current index, then c ∈ d is impossible. Together with c belonging to the index, this makes c membership-maximal. For a successor numeral it is the predecessor, while at zero the membership premise for c already has no witness.
MaxOf : (c : S) → Type (ℓ-suc ℓ) MaxOf c = (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥
To turn the formula's witnesses into StepOf, the conversion assumes the membership and maximality of c, the approximation entry (c,r), equations identifying the predecessor and current stages, and membership of x in the current stage. A final AtY witness supplies y and the two inner facts.
atY : (c r A A' x : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ)) → ⟨ fst x ∈ fst A' ⟩ → AtY c r A A' x → StepOf b f γ (fst (lookup z γ))
The stage equation converts the formula's memberships of x,y into memberships in Lset (lookup b γ), as required by StepOf. The pair equation and the host-level precedes comparison are then supplied by the two adequacy arguments below.
atY c r A A' x c∈ cmax hf qA qA' x∈ (y , (y∈ , (hpr , hprec))) = c , (r , (x , (y , (c∈ , (cmax , (hf , ( subst (λ t → ⟨ fst x ∈ t ⟩) qA' x∈ , ( subst (λ t → ⟨ fst y ∈ t ⟩) qA' y∈ , (qpair , hprec') ) ) ) ) ) ) ) )
Here the relation variable is interpreted directly as Held r, so the representation maps are identities. The Precedes bridge can therefore read the object-language comparison without any appeal to the already constructed relAt family.
where module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) (Held r) (λ _ _ p → p) (λ _ _ p → p)
Reading PrecedesAt gives a comparison over the stage object bound in the formula. Its identifying equation transports that carrier to Lset (fst c), yielding exactly the comparison required in StepOf.
hprec' : ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩ hprec' = subst (λ t → ⟨ precedes (Held r) t (fst x) (fst y) ⟩) qA (P.PrecedesAt-out hprec)
Adequacy of prAtL identifies the value denoted by z with the ordered pair of the recovered endpoints. This supplies the pair equation in the meta-level step witness.
qpair : fst (lookup z γ) ≡ pr (fst x) (fst y) qpair = subst ⟨_⟩ (prAtL-adequate (sh6 z) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) hpr
After the first endpoint x is exposed, the remaining endpoint is still known only to exist propositionally. AtX records exactly this intermediate state: stage membership of x together with a propositionally truncated AtY witness.
AtX : (c r A A' : S) → Type (ℓ-suc ℓ) AtX c r A A' = Σ[ x ∈ S ] (⟨ fst x ∈ fst A' ⟩ × ∥ AtY c r A A' x ∥₁)
Because the desired conclusion is itself propositionally truncated, the hidden y witness may be used without choosing it outside the proposition. Mapping the pointwise conversion over that truncation preserves precisely the amount of existence supplied by the formula.
atX : (c r A A' : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ)) → AtX c r A A' → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ atX c r A A' c∈ cmax hf qA qA' (x , (x∈ , hy)) =
The inner conversion assembles one explicit StepOf witness from the recovered data, and PT.map places it back under propositional truncation. This finishes the outward semantic reading without producing a canonical predecessor or endpoint witness.
PT.map (atY c r A A' x c∈ cmax hf qA qA' x∈) hy
After the stage at c has been recovered, the remaining inner quantifiers identify the stage at the current index. AtA' packages a constructible set A', evidence that it satisfies the stage graph there, and the propositionally truncated existence of the still deeper witnesses x and y. The truncation retains their existence without selecting a distinguished pair of witnesses.
AtA' : (c r A : S) → Type (ℓ-suc ℓ) AtA' c r A = Σ[ A' ∈ S ] ( ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩ × ∥ AtX c r A A' ∥₁ )
To continue from A', the argument keeps the information already obtained about c, the table entry (c,r), and the identification of A with the stage at c. It remains to identify A' with the stage at the current ordinal index before the witnesses hidden in AtX can be interpreted as a semantic step.
atA' : (c r A : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → fst A ≡ Lset (fst c) → AtA' c r A → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ atA' c r A c∈ cmax hf qA (A' , (hg , hx)) =
The stage graph supplies exactly that identification. Its functionality theorem Lset-only, applied with the assumed ordinalness of the index, yields fst A' ≡ Lset (fst (lookup b γ)); the propositionally truncated AtX can then be eliminated into the propositionally truncated step result.
PT.rec squash₁ (atX c r A A' c∈ cmax hf qA qA') hx where qA' : fst A' ≡ Lset (fst (lookup b γ)) qA' = Lset-only zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) hg ob
One quantifier farther out, AtA performs the analogous task for the stage indexed by c. It consists of a constructible set A satisfying the appropriate stage graph and the propositionally truncated existence of an AtA' continuation.
AtA : (c r : S) → Type (ℓ-suc ℓ) AtA c r = Σ[ A ∈ S ] ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ × ∥ AtA' c r A ∥₁ )
Interpreting this layer first requires the equality that tells us which stage A is. Once that equality is available, the truncated continuation can be eliminated into the truncated step, just as at the inner layer.
atA : (c r : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → AtA c r → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ atA c r c∈ cmax hf (A , (hg , hA')) = PT.rec squash₁ (atA' c r A c∈ cmax hf qA) hA'
Because c belongs to the ordinal denoted by b, mem-ord shows that c is itself an ordinal. Functionality of the stage graph at this ordinal then gives fst A ≡ Lset (fst c). No monotonicity of stages is used in this identification.
where qA : fst A ≡ Lset (fst c) qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)
The next outer witness is the relation stored by the approximation at c. AtR records a constructible set r, satisfaction of the application formula that says the table contains the entry (c,r), and the propositionally truncated continuation that reconstructs the two required stages.
AtR : (c : S) → Type (ℓ-suc ℓ) AtR c = Σ[ r ∈ S ] ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ )
The adequacy of appAt converts its satisfaction judgment into the ambient membership statement for the ordered pair (c,r). With this table entry available, the truncated AtA continuation may be eliminated into the truncated semantic step.
atR : (c : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c → AtR c → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ atR c c∈ cmax (r , (happ , hA)) = PT.rec squash₁ (atA c r c∈ cmax hf) hA where hf : ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
Concretely, the recovered fact is pr (fst c) (fst r) ∈ fst (lookup f γ). This is the meta-level form needed by StepOf: the approximation denoted by f assigns relation r to index c.
hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ
At the outermost layer, AtC chooses a member c of the ordinal index and asserts that no member d of that index lies strictly above it, in the sense c ∈ d. Thus c is a membership-maximal element of the index. When the index is later identified with a nonzero von Neumann numeral, this condition identifies its predecessor; the remaining truncated component supplies the relation and stage data.
AtC : Type (ℓ-suc ℓ) AtC = Σ[ c ∈ S ] ( ⟨ fst c ∈ fst (lookup b γ) ⟩ × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ × ∥ AtR c ∥₁ ) )
The bounded negation in the formula is interpreted in a lifted universe. Lowering it yields the ordinary function MaxOf c, which turns any alleged d with d in the index and c ∈ d into a contradiction. The truncated relation witness can then be eliminated through the preceding layers.
atC : AtC → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
atC (c , (c∈ , (hmax , hr))) = PT.rec squash₁ (atR c c∈ cmax) hr
where
cmax : MaxOf c
cmax d hd hc = lower (hmax d hd hc)
These nested interpretations provide the reading direction of the step body. For the converse direction, the same body formula is exposed locally so that an explicit StepOf witness can be placed back into its existential and bounded clauses.
opaque unfolding RelBodyAt
Starting from satisfaction of RelBodyAt, the outer existential yields only the propositionally truncated existence of c. The successive readers recover the remaining data under the same restriction and finally produce ∥ StepOf b f γ (fst (lookup z γ)) ∥₁. They establish that a step exists without choosing canonical witnesses for its nested quantifiers.
RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩ → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁ RelBody-out = PT.rec squash₁ atC
Conversely, an explicit StepOf witness already contains c, the relation r, the compared objects x,y, their stage memberships, the ordered-pair equality, and the predecessor comparison. RelBody-in rebuilds the two intermediate stages and places all of this data into the nested formula. Its existential clauses are propositionally truncated, so the result asserts satisfaction rather than preserving a canonical tuple of internal witnesses.
RelBody-in : StepOf b f γ (fst (lookup z γ)) → ⟨ γ ⊨ RelBodyAt z b f ⟩ RelBody-in (c , (r , (x , (y , (c∈ , (cmax , (hf , (x∈ , (y∈ , (qpair , hprec)))))))))) = ∣ c , (c∈ , (hmax , ∣ r , (happ , ∣ A , (hgA , ∣ A' , (hgA' , ∣ x , (x∈ , ∣ y , (y∈ , (hpr , hprec')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁
The first reconstructed fact is that c is an ordinal. Every member of an ordinal is an ordinal, so this follows from c ∈ fst (lookup b γ) and the ordinalness assumption on that set. It is precisely what is needed to form the constructible stage indexed by c.
where oc : IsOrd (fst c) oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
Using this ordinalness, LsetS packages Lset (fst c) as an element A of the model. This is the predecessor-indexed stage on which the earliest-disagreement comparison is evaluated.
A : S A = LsetS (fst c) oc
The assumed ordinalness of the current index similarly packages Lset (fst (lookup b γ)) as A'. This second stage supplies the bound containing both objects whose ordered pair is to become a member of the current relation.
A' : S A' = LsetS (fst (lookup b γ)) ob
The semantic maximality function must next be expressed by the bounded universal negation in the object language. For each d in the index, any proof of c ∈ d is sent by cmax to contradiction and then lifted to the universe in which formula satisfaction lives.
hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩ hmax d hd hc = lift (cmax d hd hc)
The table entry in StepOf has the ambient form pr (fst c) (fst r) ∈ fst (lookup f γ). Transport along the inverse of the adequacy path for appAt turns this fact into satisfaction of the application atom, which is the form required by the body formula.
happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf
The chosen A is definitionally the stage at c. The presentation theorem for the hierarchy therefore proves the corresponding stage-graph clause from the ordinalness of c and reflexivity of the represented value.
hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl
The same presentation theorem proves the graph clause for A', now at the current index. Here the required ordinalness is the standing assumption ob, so the formula recognizes A' as exactly the stage that bounds x and y.
hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩ hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl
The equality in StepOf identifies the candidate value denoted by z with the Kuratowski pair of x and y. Transport along the inverse adequacy path for prAtL converts this equality into satisfaction of the object-language pairing clause.
hpr : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩ hpr = subst ⟨_⟩ (sym (prAtL-adequate (sh6 z) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ))) qpair
It remains to translate the predecessor-stage comparison. The instance of Precedes interprets the base relation as Held r, namely membership of the ordered pair in r. Both representation maps are identities because this interpretation is already exactly the membership proposition expected by the object-language application formula.
module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) (Held r) (λ _ _ p → p) (λ _ _ p → p)
With that interpretation fixed, PrecedesAt-in converts the semantic earliest-disagreement comparison carried by StepOf into satisfaction of PrecedesAt. This completes every clause of RelBodyAt and hence the converse bridge from semantic steps to the object-language formula.
hprec' : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero))) (suc zero) zero ⟩ hprec' = P.PrecedesAt-in hprec
The body classifies a single candidate ordered pair. A relation value must collect exactly all such candidates, so the next construction takes the extensional closure of this one-step condition over an entire set.
The approximation and the graph
RelStepAt v b f says that the set denoted by v has exactly the elements satisfying RelBodyAt, with the candidate bound as the new variable at position zero and the indices b,f shifted beneath that binder. Thus it gives both inclusions: every member of the candidate relation realizes a semantic step, and every object realizing such a step belongs to the relation.
opaque RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f))
The reading lemmas for this extensional description are valid whenever fst (lookup b γ) is an ordinal. The body formula needs this hypothesis to identify the two hierarchy stages appearing in a step witness.
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (ob : IsOrd (fst (lookup b γ))) where opaque unfolding RelStepAt
The forward inclusion takes a member w of the set denoted by v, reads the body formula at w, and obtains ∥ StepOf b f γ (fst w) ∥₁. The result is truncated because the body discovers its predecessor, stored relation, and compared components through existential quantifiers.
RelStep-out : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁ RelStep-out h w hw = RelBody-out zero (suc b) (suc f) (w ∷ γ) ob (extAt-out v (RelBodyAt zero (suc b) (suc f)) γ h w hw)
The reverse inclusion starts with an explicit semantic step for w. RelBody-in turns it into satisfaction of the body, and the reverse direction of the extensional description concludes that w belongs to the set denoted by v.
RelStep-back : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩ RelStep-back h w s = extAt-in v (RelBodyAt zero (suc b) (suc f)) γ h w (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob s)
The introduction principle states the exact converse. To prove RelStepAt, it suffices to provide a truncated step for every member of the proposed relation and a membership proof for every explicit step witness. These two functions are the two extensional inclusions.
RelStep-in : ((w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁) → ((w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩) → ⟨ γ ⊨ RelStepAt v b f ⟩
For the first inclusion, each truncated step is mapped through RelBody-in and eliminated into the propositional satisfaction judgment. For the second, RelBody-out produces a truncated step, which is eliminated into the propositional membership judgment before applying the supplied reverse function. Truncation is removed only because both targets are propositions.
RelStep-in into back = extAt-in-both v (RelBodyAt zero (suc b) (suc f)) γ (λ w hw → PT.rec (snd ((w ∷ γ) ⊨ RelBodyAt zero (suc b) (suc f))) (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob) (into w hw)) (λ w h → PT.rec (snd (fst w ∈ fst (lookup v γ))) (back w) (RelBody-out zero (suc b) (suc f) (w ∷ γ) ob h))
This extensional step now instantiates the general recursion-shape construction. The resulting ApproxAt describes an initial-segment table whose domain and step clauses agree with RelStepAt, while RelGraphAt describes a value at the current index supported by such an approximation below it. The table becomes finite when that index is later identified with a numeral.
module A = RecShape RelStepAt open A using ( ApproxAt; ApproxAt-value; ApproxAt-step ; ApproxAt-in; GraphOf; PairOf ) renaming ( GraphAt to RelGraphAt; Graph-in to RelGraph-in ; Graph-out to RelGraph-out; PairGraphAt to PairRelGraphAt
The same construction also provides introduction and elimination principles for the approximation graph and its paired form. The local names RelGraphAt and PairRelGraphAt record that this generic machinery is being used specifically for the recursively defined relation values.
; PairGraph-in to PairRelGraph-in ; PairGraph-out to PairRelGraph-out )
The formulas so far describe the shape of a recursion without yet identifying its values. The next task is to prove that any table satisfying this shape records exactly the previously constructed sets relAt m; correctness of recorded values and presence of the standard entries are separated for that purpose.
The step, against the recursion
Values g k is the correctness condition. For every m < k, if g contains an entry pairing # m with any model element w, then the underlying set of w equals the underlying set of relAt m. This states uniqueness of the set value at an already recorded index; it does not choose a unique proof or witness package.
Values : S → ℕ → Type (ℓ-suc ℓ) Values g k = (m : ℕ) → m < k → (w : S) → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m)
Entries g k is the complementary completeness condition. It requires the standard entry (# m, relAt m) to occur in g for every m < k. Together, Values and Entries say that the table has all earlier indices and only the intended set value at each of them.
Entries : S → ℕ → Type (ℓ-suc ℓ) Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩
Any comparison before k x y forces k to be a successor. At zero the relation is empty, so a comparison gives a contradiction; at suc m the predecessor m and the required equality are immediate. This small lemma will let an element of relAt k be turned back into the predecessor data required by StepOf.
before-suc : (k : ℕ) (x y : V ℓ) → ⟨ before k x y ⟩ → Σ[ m ∈ ℕ ] (k ≡ suc m) before-suc zero x y h = Empty.rec* h before-suc (suc m) x y h = m , refl
Fix a candidate relation denoted by v, an index denoted by b, and a table denoted by f. The equation qb identifies the index with the numeral # k, while vals and ents assert that the table is correct and complete below k. Under these hypotheses the semantic step at the index can be compared exactly with membership in relAt k.
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (k : ℕ) (qb : fst (lookup b γ) ≡ # k) (vals : Values (lookup f γ) k) (ents : Entries (lookup f γ) k) where private ob : IsOrd (fst (lookup b γ))
The numeral # k is an ordinal. Transporting this fact against qb : fst (lookup b γ) ≡ # k proves that fst (lookup b γ) is an ordinal, which makes the earlier reading and filling lemmas for the step body available.
ob = subst IsOrd (sym qb) (numeral-ord k)
Consider an explicit StepOf witness for a candidate value x. Its maximal element c belongs to the index, and qb turns this into fst c ∈ # k. Numeral membership elimination recovers, under propositional truncation, a natural number m < k together with fst c ≡ # m; elimination is valid here because the desired membership x ∈ relAt k is a proposition.
into : (x : V ℓ) → StepOf b f γ x → ⟨ x ∈ fst (relAt k) ⟩ into x (c , (r , (xx , (yy , (c∈ , (cmax , (hf , (xx∈ , (yy∈ , (qx , hprec)))))))))) = PT.rec (snd (x ∈ fst (relAt k))) atC (∈#-elim k (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈))
For such an m, membership in relAt k is proved by its introduction lemma. The required RelOf k x witness uses the same components xx and yy, their memberships in finiteStage k, the equality identifying x with their ordered pair, and a comparison before k xx yy. The remaining work is therefore to show that the maximal c really corresponds to the immediate predecessor of k and to translate the recorded comparison accordingly.
where atC : Σ[ m ∈ ℕ ] ((m < k) × (fst c ≡ # m)) → ⟨ x ∈ fst (relAt k) ⟩ atC (m , (hm , qc)) = relAt-in k x (xx , (yy , (xxk , (yyk , (qx , below))))) where
Since c is coded by # m, its being maximal among the members of # k should force k = suc m. Trichotomy compares suc m with k: the equality case gives the desired equation, while each strict case contradicts information already available about m, k, and maximality.
ksuc : k ≡ suc m ksuc = decide (suc m ≟ k) where decide : NatOrder.Trichotomy (suc m) k → k ≡ suc m decide (NatOrder.lt hlt) = Empty.rec
If suc m < k, then the numeral #(suc m) is itself a member of # k. Since c = # m, we also have c ∈ #(suc m). These two membership facts exhibit a member of the index strictly above c, contradicting the maximality clause.
(cmax (numS (suc m)) (subst (λ t → ⟨ fst (numS (suc m)) ∈ t ⟩) (sym qb) (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst (suc m))) (#mono (suc m) k hlt))) (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc m)))
If instead k < suc m, removing the successors yields k ≤ m, which is incompatible with the already known m < k. Hence only equality remains, and reversing the trichotomy equality gives k ≡ suc m in the orientation needed below.
(subst (λ t → ⟨ t ∈ # (suc m) ⟩) (sym qc) (#mono m (suc m) NatOrder.≤-refl)))) decide (NatOrder.eq e) = sym e decide (NatOrder.gt hgt) = Empty.rec (<-asym hm (pred-≤-pred hgt))
The step witness already places xx in Lset (fst (lookup b γ)). Transport along qb identifies this set with Lset (# k), which is finiteStage k, and therefore supplies the first stage-membership component required by RelOf k x.
xxk : ⟨ fst xx ∈ finiteStage k ⟩ xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈
Both endpoints of the pair must lie in the stage indexed by k. For the second endpoint, the equation identifying the bound with # k changes membership in Lset (fst (lookup b γ)) into membership in finiteStage k.
yyk : ⟨ fst yy ∈ finiteStage k ⟩ yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈
The table entry indexed by the predecessor numeral records a relation r. After the first coordinate is changed from fst c to # m, the correctness hypothesis vals identifies the underlying set of r with relAt m.
rval : fst r ≡ fst (relAt m) rval = vals m hm r (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf)
The step witness initially compares the endpoints over Lset (fst c) using the relation held by r. The equations fst c ≡ # m and fst r ≡ fst (relAt m) rewrite this as precedes (Rel m) (finiteStage m).
atM : ⟨ precedes (Rel m) (finiteStage m) (fst xx) (fst yy) ⟩ atM = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage m) (fst xx) (fst yy) ⟩) rval (subst (λ t → ⟨ precedes (Held r) (Lset t) (fst xx) (fst yy) ⟩) qc hprec)
To obtain the recursive comparison, precedes-map replaces the base relation Rel m by before m. Its hypothesis runs in the reverse direction, from before m to membership in relAt m, because the base relation occurs in the premise of the agreement condition. Thus the result is before (suc m), and the equation k ≡ suc m finally yields before k.
below : ⟨ before k (fst xx) (fst yy) ⟩
below = subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) (sym ksuc)
(precedes-map (Rel m) (before m) (finiteStage m) (fst xx) (fst yy)
(λ w t hw ht hbf → relAt-fill m w t hw ht hbf) atM)
For the converse direction, a member described by RelOf k must be turned into a semantic step witness. The two endpoints are already present; the remaining task is to recover the predecessor index, its relation entry, and the assertion that this predecessor is the maximal member of the bound.
from : (x : V ℓ) → RelOf k x → StepOf b f γ x from x (xx , (yy , (xx∈ , (yy∈ , (qx , hbf))))) = numS m , (relAt m , (xx , (yy , (c∈ , (cmax , (hf , (xxb , (yyb , (qx , hprec))))))))) where
A proof of before k cannot exist when k is zero. The lemma before-suc therefore extracts a natural number m for which the comparison occurs at the successor stage.
m : ℕ m = before-suc k (fst xx) (fst yy) hbf .fst
The same successor analysis supplies the equation k ≡ suc m. This equation is the link between the comparison at level k and the recursive step whose base data live at level m.
qk : k ≡ suc m qk = before-suc k (fst xx) (fst yy) hbf .snd
Since k is suc m, the predecessor satisfies m < k. This bound permits the proof to use both the correctness and the completeness assumptions for the approximation table at index m.
hm : m < k hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl
The numeral representing the predecessor must be a member of the bound stored in b. The inequality m < k gives # m ∈ # k; the equations for numS m and the bound transport this membership to the required form.
c∈ : ⟨ fst (numS m) ∈ fst (lookup b γ) ⟩ c∈ = subst (λ t → ⟨ fst (numS m) ∈ t ⟩) (sym qb) (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst m)) (#mono m k hm))
It remains to show that # m is maximal among the members of # k. Given d ∈ # k and # m ∈ d, numeral elimination presents d merely as some # j with j < k; the two memberships would then force both m < j and j ≤ m.
cmax : (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst (numS m) ∈ fst d ⟩ → Empty.⊥ cmax d hd hc = PT.rec Empty.isProp⊥ step (∈#-elim k (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd)) where
In a branch where d ≡ # j, membership of d in # k = # (suc m) gives j ≤ m. Membership of # m in d gives the opposing strict inequality m < j, so asymmetry of the natural-number order closes the branch.
step : Σ[ j ∈ ℕ ] ((j < k) × (fst d ≡ # j)) → Empty.⊥ step (j , (hj , qd)) = <-asym mj (pred-≤-pred (subst (λ i → j < i) qk hj)) where mj : m < j mj = #∈#-elim m j
The derivation of m < j uses the exact correspondence between membership of von Neumann numerals and strict order. The equalities for numS m and d ≡ # j first rewrite the assumed membership into # m ∈ # j, after which numeral membership can be decoded.
(subst (λ t → ⟨ t ∈ # j ⟩) (numS-fst m) (subst (λ t → ⟨ fst (numS m) ∈ t ⟩) qd hc))
Completeness ents supplies the standard table entry (# m , relAt m) because m < k. Rewriting # m as the underlying set of numS m gives exactly the entry required by the semantic step witness.
hf : ⟨ pr (fst (numS m)) (fst (relAt m)) ∈ fst (lookup f γ) ⟩ hf = subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst (lookup f γ) ⟩) (sym (numS-fst m)) (ents m hm)
The RelOf k record places the first endpoint in finiteStage k, which is Lset (# k). Rewriting # k by the bound equation places that endpoint in Lset (fst (lookup b γ)), as required by StepOf.
xxb : ⟨ fst xx ∈ Lset (fst (lookup b γ)) ⟩ xxb = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) (sym qb) xx∈
The same transport places the second endpoint in the stage determined by the bound. The two endpoint conditions ensure that the reconstructed step remains a bounded relation rather than a comparison over arbitrary sets.
yyb : ⟨ fst yy ∈ Lset (fst (lookup b γ)) ⟩ yyb = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) (sym qb) yy∈
The comparison stored in RelOf k is first rewritten along k ≡ suc m, exposing the recursive clause precedes (before m) (finiteStage m). To express the semantic step, its base relation must then be changed from before m to membership in relAt m.
hprec : ⟨ precedes (Held (relAt m)) (Lset (fst (numS m))) (fst xx) (fst yy) ⟩ hprec = subst (λ t → ⟨ precedes (Held (relAt m)) (Lset t) (fst xx) (fst yy) ⟩) (sym (numS-fst m)) (precedes-map (before m) (Rel m) (finiteStage m) (fst xx) (fst yy)
Here precedes-map uses relAt-rep, whose direction is from membership in relAt m back to before m; contravariance in the agreement premise then produces a comparison based on Rel m. Finally the numeral equation rewrites the stage as Lset (fst (numS m)), giving the last field of StepOf.
(λ w t hw ht hR → relAt-rep m w t hw ht hR) (subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) qk hbf))
The lemma step-rel proves that any set satisfying the step formula at index k equals relAt k. Extensionality reduces this set equality to two membership implications. In the forward implication, RelStep-out yields a propositionally truncated step witness, and into sends any such witness to membership in relAt k.
step-rel : ⟨ γ ⊨ RelStepAt v b f ⟩ → fst (lookup v γ) ≡ fst (relAt k) step-rel h = cong fst (extensionalL {a = lookup v γ} {b = relAt k} pt) where fwd : (x : S) → ⟨ fst x ∈ fst (lookup v γ) ⟩ → ⟨ fst x ∈ fst (relAt k) ⟩ fwd x hx = PT.rec (snd (fst x ∈ fst (relAt k))) (into (fst x))
The truncation may be eliminated here because membership in relAt k is a proposition. No particular predecessor or pair witness is selected; only the fact that the original member belongs to the realized relation is retained.
(RelStep-out v b f γ ob h x hx)
For the reverse membership implication, relAt-out gives a propositionally truncated RelOf k description of the member. The map from reconstructs a StepOf witness, and RelStep-back then places the member in the set satisfying the step formula.
bwd : (x : S) → ⟨ fst x ∈ fst (relAt k) ⟩ → ⟨ fst x ∈ fst (lookup v γ) ⟩ bwd x hx = PT.rec (snd (fst x ∈ fst (lookup v γ))) (λ ro → RelStep-back v b f γ ob h x (from (fst x) ro)) (relAt-out k (fst x) hx)
For each constructible element, the two implications give an equivalence between its two membership propositions. Propositional extensionality turns that equivalence into a path, and set extensionality assembles the pointwise paths into the required equality of underlying sets.
pt : (x : S) → (fst x ∈ fst (lookup v γ)) ≡ (fst x ∈ fst (relAt k)) pt x = ⇔toPath (fwd x) (bwd x)
The converse lemma rel-step starts from an equality between the proposed value and relAt k and proves the step formula. The introduction rule asks for both membership directions. For the first, toStep will associate a propositionally truncated semantic step with every member of the proposed value.
rel-step : fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelStepAt v b f ⟩ rel-step q = RelStep-in v b f γ ob toStep backStep where toStep : (w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁ toStep w hw = PT.map (from (fst w))
The equality first transports a candidate member into relAt k. The outward representation of relAt k supplies only a propositionally truncated RelOf k record, and PT.map from preserves that truncation while converting its possible inhabitants into step witnesses.
(relAt-out k (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) q hw))
The second membership direction starts with an explicit StepOf witness. The map into proves membership in relAt k, and the inverse orientation of the assumed equality transports this membership back to the proposed value.
backStep : (w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩ backStep w st = subst (λ t → ⟨ fst w ∈ t ⟩) (sym q) (into (fst w) st)
Every value an approximation records
The lemma entryOf turns value correctness into entry completeness. If j < k, the approximation has some value at # j; if every value recorded there equals relAt j, then the standard pair (# j , relAt j) itself belongs to the approximation.
entryOf : ∀ {n} (f a : Fin n) (γ : S ^ n) (k : ℕ) → fst (lookup a γ) ≡ # k → ⟨ γ ⊨ ApproxAt f a ⟩ → (j : ℕ) → j < k → ((u : S) → ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩ → fst u ≡ fst (relAt j))
Domain completeness in ApproxAt supplies the existence of a value u at the numeral # j, under propositional truncation. Because the target is the proposition that the standard pair is a member, the proof may eliminate this truncation and use the assumed correctness of u.
→ ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩ entryOf f a γ k qa h j hj vs = PT.rec (snd (pr (# j) (fst (relAt j)) ∈ fst (lookup f γ))) named (ApproxAt-value f a γ h (numS j) (subst (λ t → ⟨ fst (numS j) ∈ t ⟩) (sym qa)
The domain argument is justified by j < k: numeral monotonicity gives # j ∈ # k, and the equations for numS j and the bound put that membership into the form expected by ApproxAt-value. The result asserts that some recorded value exists under propositional truncation; it does not choose a particular value.
(subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst j)) (#mono j k hj)))) where named : Σ[ u ∈ S ] ⟨ pr (fst (numS j)) (fst u) ∈ fst (lookup f γ) ⟩ → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩ named (u , p) =
Within such a value branch, the numeral equation first normalizes the recorded pair to the form (# j , u). The correctness hypothesis gives fst u ≡ fst (relAt j), and substitution in the second coordinate converts the recorded membership into membership of the standard pair.
subst (λ t → ⟨ pr (# j) t ∈ fst (lookup f γ) ⟩) (vs u p') p' where p' : ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩ p' = subst (λ t → ⟨ pr t (fst u) ∈ fst (lookup f γ) ⟩) (numS-fst j) p
Fix an approximation whose bound is # k. The induction motive Val m says that, whenever m < k, every constructible value w recorded at the key # m has the same underlying set as relAt m.
module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) (k : ℕ) (qa : fst (lookup a γ) ≡ # k) (h : ⟨ γ ⊨ ApproxAt f a ⟩) where private Val : ℕ → Type (ℓ-suc ℓ) Val m = (m < k) → (w : S) → ⟨ pr (# m) (fst w) ∈ fst (lookup f γ) ⟩
The motive quantifies over every possible recorded value rather than choosing one. Its conclusion is equality of the two underlying sets, which is exactly the form needed both to rewrite table entries and to prove that the approximation is single-valued.
→ fst w ≡ fst (relAt m)
Correctness is proved by well-founded induction on the strict order of natural numbers. To identify a value at m, the induction hypothesis provides correctness at every j < m; the proof then applies step-rel to the proposed value w in an environment extended by w and the numeral for m. This is well-foundedness of natural-number <, not well-foundedness of before.
approx-val : (m : ℕ) → Val m approx-val = WFI.induction <-wellfounded go where go : (m : ℕ) → ((j : ℕ) → j < m → Val j) → Val m go m IH hm w hw = step-rel zero (suc zero) (sh2 f) (w ∷ numS m ∷ γ) m
The hypothesis that (# m , w) is recorded lets ApproxAt-step expose the step formula satisfied by w. To identify that step with relAt m, step-rel also receives two facts about all smaller indices: recorded values are correct, and every standard entry is present.
(numS-fst m) vals ents (ApproxAt-step f a γ h (numS m) w (subst (λ t → ⟨ pr t (fst w) ∈ fst (lookup f γ) ⟩) (sym (numS-fst m)) hw)) where
For j < m, correctness is precisely the induction hypothesis at j. Its own bound requirement j < k follows by composing j < m with the standing assumption m < k.
vals : Values (lookup (sh2 f) (w ∷ numS m ∷ γ)) m vals j hj u hu = IH j hj (<-trans hj hm) u hu
Completeness below m follows from entryOf. For each j < m, transitivity again gives j < k, while the induction hypothesis supplies the premise that every value recorded at j equals relAt j; hence the standard entry at j is present.
ents : Entries (lookup (sh2 f) (w ∷ numS m ∷ γ)) m ents j hj = entryOf f a γ k qa h j (<-trans hj hm) (λ u p → IH j hj (<-trans hj hm) u p)
Once correctness has been proved at every bounded index, entryOf immediately yields completeness of the approximation. Thus approx-ent states that each m < k contributes the standard pair (# m , relAt m) to the recorded table.
approx-ent : (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst (lookup f γ) ⟩ approx-ent m hm = entryOf f a γ k qa h m hm (approx-val m hm)
The graph formula hides, under propositional truncation, an approximation up to k together with a final step. The lemma rel-only eliminates that truncation into an equality of sets, which is a proposition, and asserts that the value stored in v must be relAt k.
module _ {n : ℕ} (v b : Fin n) (γ : S ^ n) (k : ℕ) (qb : fst (lookup b γ) ≡ # k) where rel-only : ⟨ γ ⊨ RelGraphAt v b ⟩ → fst (lookup v γ) ≡ fst (relAt k) rel-only h = PT.rec (setIsSet (fst (lookup v γ)) (fst (relAt k))) read (RelGraph-out v b γ h)
In any represented branch, the graph supplies an approximation g, a proof that g satisfies ApproxAt, and a proof of the step at k. The preceding well-founded induction identifies every value recorded by g below k; step-rel then identifies the final value with relAt k.
where read : GraphOf v b γ → fst (lookup v γ) ≡ fst (relAt k) read (g , (ha , hs)) = step-rel (suc v) (suc b) zero (g ∷ γ) k qb (λ m hm w hw → approx-val zero (suc b) (g ∷ γ) k qb ha m hm w hw)
The other input to step-rel is completeness of that same approximation below k. It is supplied by approx-ent, which uses the value theorem to replace each merely existing entry by the corresponding standard entry.
(λ m hm → approx-ent zero (suc b) (g ∷ γ) k qb ha m hm) hs
The approximation, exhibited
To prepare the finite family used below for collection by finSet, first place all its members in a common constructible stage. More generally, smallStage applies ordinal bounding to the individual stages of any small family g : X → S and returns an ordinal σ such that every fst (g x) belongs to Lset σ.
smallStage : (X : Type ℓ) (g : X → S) → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((x : X) → ⟨ fst (g x) ∈ Lset σ ⟩)) smallStage X g = bd .fst , (bd .snd .fst , mem) where bd = boundingOrd X (λ x → stage (fst (g x)) (g x .snd))
Each g x already belongs to the constructible stage at which it is born. The bounding ordinal lies above every such birth stage, so monotonicity of Lset transports each membership into the common stage Lset σ.
(λ x → stage-ord (fst (g x)) (g x .snd)) mem : (x : X) → ⟨ fst (g x) ∈ Lset (bd .fst) ⟩ mem x = Lset-mono {α = bd .fst} {β = stage (fst (g x)) (g x .snd)} (bd .snd .snd x) (stage-mem (fst (g x)) (g x .snd))
For a fixed bound k, the finite index type Fin k enumerates exactly the smaller natural numbers. The family famOf k assigns to i the constructible ordered pair whose coordinates are the numeral # (toℕ i) and the realized relation relAt (toℕ i).
private famOf : (k : ℕ) → Fin k → S famOf k i = prS (numS (toℕ i)) (relAt (toℕ i))
The lifted copy of Fin k places this finite index type in the universe expected by smallStage. Applying the common-stage lemma to famOf k gives one ordinal stage containing every pair, which supplies the constructibility premise later required by finSetL.
famBnd : (k : ℕ) → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((i : Lift {ℓ-zero} {ℓ} (Fin k)) → ⟨ fst (famOf k (lower i)) ∈ Lset σ ⟩)) famBnd k = smallStage (Lift {ℓ-zero} {ℓ} (Fin k)) (λ i → famOf k (lower i))
The underlying set of famOf k i is the whole ordered pair, not merely its first coordinate. The equation famEq unfolds the constructible pairing and the numeral representation to identify it with pr (# (toℕ i)) (fst (relAt (toℕ i))).
famEq : (k : ℕ) (i : Fin k) → fst (famOf k i) ≡ pr (# (toℕ i)) (fst (relAt (toℕ i))) famEq k i = prS-fst (numS (toℕ i)) (relAt (toℕ i)) ∙ cong (λ t → pr t (fst (relAt (toℕ i)))) (numS-fst (toℕ i))
The approximation approxSet k is built by finSet, which collects the Fin k indexed family of underlying pairs into a finite set. The proof finSetL uses their common stage to show that this finite set is an element of L. No instance of Replacement is used in this construction.
opaque approxSet : ℕ → S approxSet k = finSet k (λ i → fst (famOf k i)) , FinOf.finSetL (famBnd k .fst) (famBnd k .snd .fst) k (λ i → fst (famOf k i)) (λ i → famBnd k .snd .snd (lift i))
The projection equation exposes the underlying set of approxSet k as exactly that finSet. Subsequent membership lemmas can therefore use the introduction and elimination rules for finite sets to show that its entries are precisely the pairs (# j , relAt j) with j < k.
approxSet-fst : (k : ℕ) → fst (approxSet k) ≡ finSet k (λ i → fst (famOf k i)) approxSet-fst k = refl
The finite approximation contains every intended entry: if j < k, then the ordered pair of # j and relAt j belongs to approxSet k. This is a property of the finite-set construction of approxSet, not an application of replacement.
approx-mem-in : (k j : ℕ) → j < k → ⟨ pr (# j) (fst (relAt j)) ∈ fst (approxSet k) ⟩ approx-mem-in k j hj = subst (λ t → ⟨ t ∈ fst (approxSet k) ⟩) (cong (λ i → pr (# i) (fst (relAt i))) (toℕ∘enum j hj))
The inequality supplies enum j hj : Fin k. The equation famEq identifies the corresponding member of the finite family with the desired ordered pair, and finSet-in inserts it into the set built by finSet and certified in L by finSetL.
(subst (λ t → ⟨ pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))) ∈ t ⟩) (sym (approxSet-fst k)) (finSet-in k (λ i → fst (famOf k i)) (pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj))))) ∣ enum j hj , famEq k (enum j hj) ∣₁))
Conversely, membership in approxSet k yields only a propositionally truncated assertion that the member is an intended entry indexed by some j < k. Thus the lemma describes exactly which pairs occur without choosing a canonical index witness.
approx-mem-out : (k : ℕ) (y : V ℓ) → ⟨ y ∈ fst (approxSet k) ⟩ → ∥ Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) ∥₁ approx-mem-out k y h = PT.map named (finSet-out k (λ i → fst (famOf k i)) y (subst (λ t → ⟨ y ∈ t ⟩) (approxSet-fst k) h))
An enumerated index i : Fin k is sent to the natural number toℕ i, together with toℕ<n i. Reversing the membership equation and composing it with famEq gives the required equality from the original member to the standard pair.
where named : Σ[ i ∈ Fin k ] (fst (famOf k i) ≡ y) → Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) named (i , q) = toℕ i , (toℕ<n i , (sym q ∙ famEq k i)) approxVals : (k : ℕ) → Values (approxSet k) k
This membership description proves value correctness. If an entry with first component # m occurs below k, then its second component is the underlying set of relAt m; the propositionally truncated index may be eliminated because equality between sets in V is itself a proposition.
approxVals k m hm u hu = PT.rec (setIsSet (fst u) (fst (relAt m))) named (approx-mem-out k (pr (# m) (fst u)) hu) where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (# m) (fst u) ≡ pr (# j) (fst (relAt j)))) → fst u ≡ fst (relAt m)
Injectivity of ordered pairing separates the equality into its two components. Injectivity of numerals then identifies the recovered index with m, so the second-component equality can be transported from relAt j to relAt m.
named (j , (hj , q)) = pr-inj q .snd ∙ cong (λ i → fst (relAt i)) (sym (#-inj′ (pr-inj q .fst)))
The complementary property is entry completeness: for every m < k, the standard pair (# m, relAt m) is present. It follows immediately from the finite-set membership lemma above.
approxEnts : (k : ℕ) → Entries (approxSet k) k approxEnts k m hm = approx-mem-in k m hm
Fix an environment in which f denotes approxSet k and a denotes the numeral # k. The remaining task is to verify that this concrete finite table satisfies the abstract approximation formula.
module _ (k : ℕ) {n : ℕ} (f a : Fin n) (γ : S ^ n) (qf : fst (lookup f γ) ≡ fst (approxSet k)) (qa : fst (lookup a γ) ≡ # k) where private onDom : (x : S)
The domain condition has two directions. A first component occurring in the table must belong to # k, and every member of # k must occur as the first component of some table entry. The existential assertion about a second component is interpreted with propositional truncation.
→ (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩) × (⟨ fst x ∈ fst (lookup a γ) ⟩ → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) onDom x = fwd , bwd
For the first direction, assume merely that some second component forms an entry with x. Since the target membership x ∈ # k is a proposition, the existential witness may be eliminated before the pair is analyzed through approx-mem-out.
where fwd : ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ fwd = PT.rec (snd (fst x ∈ fst (lookup a γ))) atY where
After transporting the entry into approxSet k, approx-mem-out produces a propositionally truncated j < k and an equality with the standard pair at j. Elimination is again valid because the desired membership in the index is a proposition.
atY : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ atY (y , p) = PT.rec (snd (fst x ∈ fst (lookup a γ))) named (approx-mem-out k (pr (fst x) (fst y)) (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p))
The first-component equality says that the underlying set of x is # j. The equality interpreting a as # k reduces the goal to proving that this set belongs to # k.
where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j)))) → ⟨ fst x ∈ fst (lookup a γ) ⟩ named (j , (hj , q)) = subst (λ t → ⟨ fst x ∈ t ⟩) (sym qa)
Numeral monotonicity turns j < k into # j ∈ # k. Transport along the first-component equality then proves that the original x lies in the required domain.
(subst (λ t → ⟨ t ∈ # k ⟩) (sym (pr-inj q .fst)) (#mono j k hj))
For the converse direction, membership in # k is decoded as a propositionally truncated natural number j < k whose numeral is the given element. Mapping this truncated datum will produce the required truncated table entry.
bwd : ⟨ fst x ∈ fst (lookup a γ) ⟩ → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ bwd hx = PT.map named (∈#-elim k (fst x) (subst (λ t → ⟨ fst x ∈ t ⟩) qa hx)) where
For an explicit decoded j, choose relAt j as the second component. Entry completeness places (# j, relAt j) in approxSet k, and the equations for the table and for the given first component transport this membership back to the original environment.
named : Σ[ j ∈ ℕ ] ((j < k) × (fst x ≡ # j)) → Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ named (j , (hj , q)) = relAt j , subst (λ t → ⟨ pr (fst x) (fst (relAt j)) ∈ t ⟩) (sym qf) (subst (λ t → ⟨ pr t (fst (relAt j)) ∈ fst (approxSet k) ⟩)
The final transport replaces the decoded numeral # j by the original first component. Hence every element of the intended domain has an entry, completing the second half of the domain condition.
(sym q) (approx-mem-in k j hj))
It remains to verify the pointwise recursion condition. Every pair occurring in the finite table must satisfy RelStepAt, so the second component is justified as the recursively determined relation value at the first component.
onStep : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩ onStep x y p = PT.rec (snd ((y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f))) named (approx-mem-out k (pr (fst x) (fst y))
Membership in the table is first transported to approxSet k and read by approx-mem-out. Its propositionally truncated standard form can be eliminated because satisfaction of RelStepAt is a proposition.
(subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p)) where named : Σ[ j ∈ ℕ ] ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j)))) → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩
For a recovered entry at j, rel-step reconstructs the recursion step. Its hypotheses for every i < j come from value correctness and entry completeness for approxSet k; transitivity of < turns i < j < k into the bounds those lemmas require.
named (j , (hj , q)) = rel-step zero (suc zero) (sh2 f) (y ∷ x ∷ γ) j (pr-inj q .fst) (λ i hi u hu → approxVals k i (<-trans hi hj) u (subst (λ t → ⟨ pr (# i) (fst u) ∈ t ⟩) qf hu)) (λ i hi → subst (λ t → ⟨ pr (# i) (fst (relAt i)) ∈ t ⟩) (sym qf)
The first component of the pair equality identifies the argument with # j, while its second component identifies the recorded value with relAt j. These are precisely the endpoint equalities required by rel-step.
(approxEnts k i (<-trans hi hj))) (pr-inj q .snd)
The concrete finite table now satisfies ApproxAt: onDom proves that its domain is exactly # k, and onStep proves the recursion condition at every recorded argument. This establishes an approximation without invoking replacement.
approxSet-approx : ⟨ γ ⊨ ApproxAt f a ⟩ approxSet-approx = ApproxAt-in f a γ (domAt-intro f a γ onDom) onStep
Consequently, relAt k satisfies the recursion graph at the numeral # k, provided the environment components denoting the index and candidate value are identified with # k and relAt k. The finite witness for the existential approximation is approxSet k.
relAt-graph : ∀ {n} (v b : Fin n) (γ : S ^ n) (k : ℕ) → fst (lookup b γ) ≡ # k → fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelGraphAt v b ⟩ relAt-graph v b γ k qb qv = RelGraph-in v b γ (approxSet k) (approxSet-approx k zero (suc b) (approxSet k ∷ γ) refl qb)
The graph introduction combines two facts: approxSet-approx verifies all earlier arguments, and rel-step verifies the current value at k using approxVals and approxEnts. Thus the same finite table supplies exactly the prior information needed to certify relAt k.
(rel-step (suc v) (suc b) zero (approxSet k ∷ γ) k qb (approxVals k) (approxEnts k) qv)
The family, as an element of L
The finite relations have now been verified one stage at a time. The preceding uniqueness argument used well-founded induction on the natural-number order <; it neither establishes nor uses well-foundedness of before. The next construction uses replacement over the internal natural numbers to collect all pairs (# k, relAt k) into one constructible set graph.
private
For any formula φ proved equal to the paired recursion graph, famBuild returns a constructible set h with two precise properties. Every standard pair belongs to h, and any member of h whose first component is known to be # k has second component equal to relAt k.
famBuild : (φ : Formula S 2) → φ ≡ PairRelGraphAt zero (suc zero) → Σ[ h ∈ S ] ( ((k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst h ⟩) × ((cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst h ⟩ → fst rS ≡ fst (relAt k)) )
Replacement requires the fiber of satisfying outputs over each c ∈ ωʟ to be contractible. Membership in ωʟ provides only a propositionally truncated numeral representation; PT.map handles each explicit numeral case, and mereFunct combines the truncated existence with value uniqueness.
famBuild φ qφ = r .fst .fst , (inFam , outFam) where fc : (c : S) → ⟨ c ∈ˢ ωʟ ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ c ∷ []) ⊨ φ ⟩) fc c c∈ = mereFunct φ c (PT.map atK c∈)
In an explicit numeral case fst c = # j, the chosen center of the fiber is the constructible ordered pair of c and relAt j. The proof supplies both its satisfaction of φ and equality of every competing satisfying output with this center; it does not choose a canonical j outside the truncation.
where atK : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst c) → Σ[ y ∈ S ] ( ⟨ (y ∷ c ∷ []) ⊨ φ ⟩ × ((y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ y) ) atK (j , qj) = prS c (relAt (lower j)) , (holds , only)
The numeral decoder gives its equality in the opposite orientation. Reversing it yields fst c = # j, the form required to apply the recursion graph theorem at j.
where qc : fst c ≡ # (lower j) qc = sym qj
To prove that the chosen pair satisfies φ, the equality identifying φ with the paired graph reduces the claim to PairRelGraphAt. Pair formation supplies the outer ordered-pair equation, while relAt-graph supplies the graph assertion for relAt j.
holds : ⟨ (prS c (relAt (lower j)) ∷ c ∷ []) ⊨ φ ⟩ holds = PairRelGraph-in zero (suc zero) (prS c (relAt (lower j)) ∷ c ∷ []) φ qφ (relAt (lower j)) (prS-fst c (relAt (lower j))) (relAt-graph zero (sh2 zero)
The graph assertion is instantiated at index j: the component representing the index is identified with # j by the reversed decoder equation, and the candidate relation is definitionally relAt j. This completes the existence half of the fiber proof.
(relAt (lower j) ∷ prS c (relAt (lower j)) ∷ c ∷ []) (lower j) qc refl)
For uniqueness, let y' be any other output satisfying φ. Reading the paired graph gives a propositionally truncated decomposition of y'; it may be eliminated into y' = prS c (relAt j) because equality in S is a proposition.
only : (y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ prS c (relAt (lower j)) only y' h = PT.rec (isSetS y' (prS c (relAt (lower j)))) read (PairRelGraph-out zero (suc zero) (y' ∷ c ∷ []) φ qφ h) where read : PairOf zero (suc zero) (y' ∷ c ∷ []) φ qφ
An explicit decomposition writes y' as the pair of c with some graph value z. The theorem rel-only identifies the underlying set of z with relAt j, and extensional equality of the proof-bearing elements lifts the resulting equality of ordered pairs to S.
→ y' ≡ prS c (relAt (lower j)) read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t)) ( q ∙ cong (pr (fst c)) (rel-only zero (sh2 zero) (z ∷ y' ∷ c ∷ []) (lower j) qc hg)
The final equality compares the underlying ordered pair with the packaged constructible pair prS c (relAt j). This proves uniqueness of the set-valued output at the decoded numeral, without asserting uniqueness of the graph witness itself.
∙ sym (prS-fst c (relAt (lower j))) )
Replacement over ωʟ now yields a contractible type of constructible sets whose members are exactly the outputs y for which there merely exists c ∈ ωʟ satisfying φ. Contractibility makes the resulting set unique; the existential numeral data remains propositionally truncated.
r : isContr (SetOf (λ y → ∃[ c ∶ S ] (c ∈ˢ ωʟ) ⊓ ((y ∷ c ∷ []) ⊨ φ))) r = hasReplacementL ωʟ φ fc
Each standard pair belongs to the replacement set. The replacement specification is used with witness numS k, together with its membership in ωʟ and the paired-graph proof for relAt k; the packaged pair is then transported to its underlying pair in V.
inFam : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst (r .fst .fst) ⟩ inFam k = subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) qe (subst ⟨_⟩ (sym (r .fst .snd (prS (numS k) (relAt k)))) ∣ numS k , (inω , holds) ∣₁) where
The required transport equation unfolds only the packaging: the underlying set of prS (numS k) (relAt k) is the ordered pair of # k and the underlying set of relAt k. The equation for numS k supplies the first component.
qe : fst (prS (numS k) (relAt k)) ≡ pr (# k) (fst (relAt k)) qe = prS-fst (numS k) (relAt k) ∙ cong (λ t → pr t (fst (relAt k))) (numS-fst k)
The witness numS k lies in the internal natural numbers because its underlying set is # k, and every numeral belongs to ω. Transporting #∈ω k along numS-fst supplies the required membership.
inω : ⟨ numS k ∈ˢ ωʟ ⟩ inω = subst (λ t → ⟨ t ∈ ω ⟩) (sym (numS-fst k)) (#∈ω k)
The remaining witness shows that the packaged standard pair satisfies φ. Pair-graph introduction reduces this to the ordered-pair equation and to the fact that relAt k satisfies the recursion graph at # k.
holds : ⟨ (prS (numS k) (relAt k) ∷ numS k ∷ []) ⊨ φ ⟩ holds = PairRelGraph-in zero (suc zero) (prS (numS k) (relAt k) ∷ numS k ∷ []) φ qφ (relAt k) (prS-fst (numS k) (relAt k)) (relAt-graph zero (sh2 zero)
The graph theorem is instantiated directly at k. The equation numS-fst k identifies the input with # k, and reflexivity identifies the candidate output with relAt k, completing the standard-entry proof.
(relAt k ∷ prS (numS k) (relAt k) ∷ numS k ∷ []) k (numS-fst k) refl)
For the converse specification, suppose an ordered pair belongs to the replacement set and its first component is known to be # k. The goal is only equality of its second component with relAt k, a proposition-valued conclusion into which the truncated replacement membership may be eliminated.
outFam : (cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst (r .fst .fst) ⟩ → fst rS ≡ fst (relAt k) outFam cS rS k qc h = PT.rec (setIsSet (fst rS) (fst (relAt k))) atD
The replacement specification yields, propositionally truncated, an internal natural d such that the packaged input pair satisfies φ over d. No numeral is selected here; the later pair equality will identify the underlying set of d with the already specified # k.
(subst ⟨_⟩ (r .fst .snd (prS cS rS)) (subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) (sym (prS-fst cS rS)) h)) where atD : Σ[ d ∈ S ] ( ⟨ d ∈ˢ ωʟ ⟩ × ⟨ (prS cS rS ∷ d ∷ []) ⊨ φ ⟩ ) → fst rS ≡ fst (relAt k)
Reading the paired graph yields, again under propositional truncation, a relation value z, an equation identifying the packaged member with the pair (d,z), and a proof that z satisfies the recursion graph at d. Equality of sets is propositional, so this truncation can also be eliminated.
atD (d , (d∈ , hp)) = PT.rec (setIsSet (fst rS) (fst (relAt k))) read (PairRelGraph-out zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ hp) where read : PairOf zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ → fst rS ≡ fst (relAt k)
After removing the packaging equation, injectivity of ordered pairs identifies the proposed second component with z. The theorem rel-only then identifies z with relAt k, once the first-component equation has shown that the graph index is # k.
read (z , (q , hg)) = pr-inj q' .snd ∙ rel-only zero (sh2 zero) (z ∷ prS cS rS ∷ d ∷ []) k qd hg where q' : pr (fst cS) (fst rS) ≡ pr (fst d) (fst z) q' = sym (prS-fst cS rS) ∙ q
The needed index equation follows from the first component of the same pair equality. Reversing that component identifies d with the original first component, and composing with the hypothesis about that component yields fst d = # k.
qd : fst d ≡ # k qd = sym (pr-inj q' .fst) ∙ qc
The constructible set selected by famBuild for the actual paired recursion graph is named beforeFam and kept opaque. Its following specification lemmas expose the standard entries and uniqueness of the set value at every known numeral; this construction supplies an internal relation family, without yet comparing names or proving a final well-order.
opaque beforeFam : S beforeFam = famBuild (PairRelGraphAt zero (suc zero)) refl .fst
For each natural number k, the internal graph beforeFam contains the ordered pair of the numeral # k with the realized relation relAt k. This is the forward membership law for the family: it inserts the already known numeral and relation directly, without choosing a numeral decoder from a propositional truncation.
beforeFam-in : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst beforeFam ⟩ beforeFam-in = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .fst
Conversely, suppose an entry of beforeFam has first component equal to # k. Its second component then has the same underlying set as relAt k. Thus the graph has a unique set value at a specified numeral; this does not provide a canonical decoding witness or assert uniqueness of every proof carried by the construction.
beforeFam-out : (cS rS : S) (k : ℕ) → fst cS ≡ # k → ⟨ pr (fst cS) (fst rS) ∈ fst beforeFam ⟩ → fst rS ≡ fst (relAt k) beforeFam-out = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .snd
The order at a numeral held in a slot
The formula BeforeAt b x y asks for a relation r in two steps. First, appC says that the constant family beforeFam assigns r to the value denoted by b. Then appAt says that r contains the ordered pair of the objects denoted by x and y. The next theorem assumes that the value at b is the numeral # m and identifies this internal statement with before m under the precise stage hypotheses stated below.
opaque BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n BeforeAt b x y = ∃̇ ( appC beforeFam (suc b) zero ∧̇ appAt zero (suc x) (suc y) )
Fix an environment and a natural number m. The equation for b says that its value is the numeral # m, while the two membership hypotheses place the values denoted by x and y in finiteStage m. These assumptions connect the three variables to one finite-stage comparison; the adequacy theorem is stated only in this restricted context.
module _ {n : ℕ} (b x y : Fin n) (γ : S ^ n) (m : ℕ) (qb : fst (lookup b γ) ≡ # m) (hx : ⟨ fst (lookup x γ) ∈ finiteStage m ⟩) (hy : ⟨ fst (lookup y γ) ∈ finiteStage m ⟩) where private
The semantic target is the meta-level proposition that the value denoted by x precedes the value denoted by y according to before m. At this point the argument establishes representation of one finite-stage comparison; it makes no new claim about well-foundedness.
Goal : Type (ℓ-suc ℓ) Goal = ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
To read a satisfying assignment, temporarily expose the data hidden by the existential: a relation r, evidence that the family assigns r at b, and evidence that r contains the pair at x,y. This type describes an explicit package, but the semantics of the existential supplies it only under propositional truncation, so no persistent or canonical witness is obtained.
AtR : Type (ℓ-suc ℓ) AtR = Σ[ r ∈ S ] ( ⟨ (r ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩ × ⟨ (r ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩ )
From any explicit package of this form, the two application adequacy laws recover ordinary set membership. The family law identifies the underlying set of r with that of relAt m; after transporting the pair membership along this equality, relAt-rep reads it back as before m. The two finite-stage membership hypotheses are exactly what permits this final representation step.
atR : AtR → Goal atR (r , (happ , hmem)) = relAt-rep m (fst (lookup x γ)) (fst (lookup y γ)) hx hy (subst (λ t → ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ t ⟩) qr (subst ⟨_⟩ (appAt-adequate zero (suc x) (suc y) (r ∷ γ)) hmem))
The first application fact says internally that beforeFam takes the value r at the entry stored in b. Its adequacy law turns this into the external membership statement that the pair consisting of that entry and r belongs to beforeFam.
where hf : ⟨ pr (fst (lookup b γ)) (fst r) ∈ fst beforeFam ⟩ hf = subst ⟨_⟩ (appC-adequate beforeFam (suc b) zero (r ∷ γ)) happ
Because the entry at b is known to equal # m, the backward family law now identifies the underlying set of r with the underlying set of relAt m. This uses uniqueness of the set value at a specified numeral, rather than a global choice of numeral decodings.
qr : fst r ≡ fst (relAt m) qr = beforeFam-out (lookup b γ) r m qb hf
We can now prove the two directions of the exact semantic correspondence. Unfolding BeforeAt locally exposes its single existential and the two application facts, while the hypotheses on b, x, and y remain part of both statements.
opaque unfolding BeforeAt
For the outward direction, satisfaction of the existential gives only a propositionally truncated relation package. The proof eliminates that truncation directly into Goal, which is a proposition, by applying the conversion above to each hypothetical explicit package. It never extracts an inhabitant of the intermediate type as retained data.
BeforeAt-out : ⟨ γ ⊨ BeforeAt b x y ⟩ → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ BeforeAt-out h = PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) atR h
For the inward direction, a proof of before m supplies the relation membership needed for the formula. We exhibit relAt m as a suitable relation, prove the two application facts, and then place the whole package under propositional truncation, as required by the existential semantics. This is a constructed witness for this direction, not a canonical witness recovered from a truncation.
BeforeAt-in : ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩ → ⟨ γ ⊨ BeforeAt b x y ⟩ BeforeAt-in h = ∣ relAt m , (happ , hmem) ∣₁ where happ : ⟨ (relAt m ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩
The family application follows from the known entry (# m, relAt m) in beforeFam. Transporting its first component along the equation for b, and then using application adequacy in the reverse direction, yields the required internal application fact.
happ = subst ⟨_⟩ (sym (appC-adequate beforeFam (suc b) zero (relAt m ∷ γ))) (subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst beforeFam ⟩) (sym qb) (beforeFam-in m))
The second application fact comes from relAt-fill: the two stage-membership hypotheses and the assumed before m comparison place the pair of the values at x,y in relAt m. Reading application adequacy in the reverse direction turns that membership into satisfaction of appAt.
hmem : ⟨ (relAt m ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩ hmem = subst ⟨_⟩ (sym (appAt-adequate zero (suc x) (suc y) (relAt m ∷ γ))) (relAt-fill m (fst (lookup x γ)) (fst (lookup y γ)) hx hy h)
The frame, discharged
The two adequacy directions make BeforeAt an admissible input to the earlier Described framework. That framework first compares the finite levels of two limit-stage codes and, when the levels agree, uses the represented before relation within that level; separation then realizes this comparison as the internal relation codeOrder. This instantiation supplies the code-order component and does not yet compare names or prove a final internal well-order.
private module CodeOrder = Described BeforeAt BeforeAt-in BeforeAt-out
The outcome is the relation set codeOrder together with two representation laws. codeOrder-fill turns a meta-level limitOrder comparison into membership in this set, and codeOrder-rep reads such membership back. Later name comparison uses these three results for comparing codes; the comparison of parameters is supplied separately.
open CodeOrder public using ( codeOrder; codeOrder-fill; codeOrder-rep )
Recap
For every natural number n, the set relAt n in L represents before n on members of finiteStage n. The recursion graph verifies these values, and Replacement is used only at the end to collect the whole family along ωʟ into beforeFam; the finite approximations use finSet and finSetL. If b denotes # m and the values denoted by x,y belong to finiteStage m, then BeforeAt b x y is equivalent to applying before m to those two values. Instantiating Described yields codeOrder, codeOrder-fill, and codeOrder-rep, which later provide the comparison of codes without yet comparing names or proving a final internal well-order.