---
title: "An internal family of earliest-disagreement relations"
module: L.Choice.EarliestDisagreement
lang: en
site: "Bedrock"
description: "An internal family of earliest-disagreement relations"
stage: "The canonical well-order and Choice"
reading_order: 82
canonical: https://bedrock.institute/en/L.Choice.EarliestDisagreement.html
html: L.Choice.EarliestDisagreement.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/EarliestDisagreement.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Axioms.Infinity, L.Choice.FiniteStageOrders, L.Choice.LimitStageOrder, L.Coding.HierarchySequence, L.Hierarchy, L.Coding.Model, L.Coding.Expressions, FOL.Absoluteness, FOL.ZFModel]
routes: [choice-completion]
translations: [https://bedrock.institute/zh/L.Choice.EarliestDisagreement.md, https://bedrock.institute/ja/L.Choice.EarliestDisagreement.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# An internal family of earliest-disagreement relations

At 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ¬̇_; ∃̇_; ∀̇∈; ∃̇∈ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
```

The 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`.

```agda
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`.

```agda
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.

```agda
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.

```agda
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.

```agda
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`.

```agda
  ( _<_; <-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`.

```agda
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.

```agda
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.

```agda
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.

```agda
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 `φ`.

```agda
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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
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`.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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`.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
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`.

```agda
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`.

```agda
  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`.

```agda
  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.

```agda
  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`.

```agda
    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.

```agda
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.

```agda
  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'`.

```agda
    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.

```agda
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.

```agda
              ( 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.

```agda
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.

```agda
      (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.

```agda
  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.

```agda
  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.

```agda
    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`.

```agda
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.

```agda
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`.

```agda
  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.

```agda
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.

```agda
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.

```agda
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.

```agda
    (λ { (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.

```agda
  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.

```agda
  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`.

```agda
  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`.

```agda
  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.

```agda
  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.

```agda
               , (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.

```agda
    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.

```agda
    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)`.

```agda
    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)`.

```agda
    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`.

```agda
    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.

```agda
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)`.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
    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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
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.

```agda
  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.

```agda
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.

```agda
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.

```agda
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.

```agda
       ∧̇ ∃̇ ( 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`.

```agda
                               ( 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.

```agda
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.

```agda
      × ( ⟨ 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.

```agda
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.

```agda
        ⟨ (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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
      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`.

```agda
      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.

```agda
      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.

```agda
    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.

```agda
    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.

```agda
      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.

```agda
    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.

```agda
    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.

```agda
      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.

```agda
    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.

```agda
    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.

```agda
      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.

```agda
    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.

```agda
    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`.

```agda
      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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
   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.

```agda
   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`.

```agda
     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.

```agda
     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.

```agda
     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.

```agda
     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.

```agda
     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.

```agda
     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`.

```agda
     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.

```agda
     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.

```agda
     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.

```agda
     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.

```agda
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.

```agda
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.

```agda
   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`.

```agda
   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.

```agda
   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.

```agda
   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.

```agda
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.

```agda
              ; 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.

```agda
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.

```agda
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`.

```agda
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`.

```agda
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.

```agda
    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.

```agda
    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.

```agda
      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.

```agda
        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.

```agda
            (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.

```agda
                (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`.

```agda
        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`.

```agda
        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`.

```agda
        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)`.

```agda
        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`.

```agda
        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.

```agda
    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.

```agda
      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`.

```agda
      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`.

```agda
      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.

```agda
      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`.

```agda
      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.

```agda
        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.

```agda
            (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.

```agda
      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`.

```agda
      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.

```agda
      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`.

```agda
      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`.

```agda
          (λ 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`.

```agda
  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.

```agda
      (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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
      (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.

```agda
    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.

```agda
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`.

```agda
        → ⟨ 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.

```agda
        (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.

```agda
    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`.

```agda
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.

```agda
          → 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`.

```agda
  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.

```agda
      (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`.

```agda
      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.

```agda
      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.

```agda
  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`.

```agda
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`.

```agda
    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.

```agda
        (λ 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 σ`.

```agda
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 σ`.

```agda
         (λ 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)`.

```agda
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`.

```agda
  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)))`.

```agda
  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.

```agda
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`.

```agda
  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.

```agda
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`.

```agda
    (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.

```agda
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.

```agda
  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.

```agda
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`.

```agda
  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.

```agda
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.

```agda
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.

```agda
          → (⟨ ∃[ 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`.

```agda
      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.

```agda
        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`.

```agda
          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.

```agda
            (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.

```agda
      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.

```agda
        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.

```agda
                (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.

```agda
    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.

```agda
        (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.

```agda
      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`.

```agda
            (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.

```agda
  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`.

```agda
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`.

```agda
  (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.

```agda
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`.

```agda
  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.

```agda
  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.

```agda
      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`.

```agda
        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`.

```agda
        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.

```agda
            (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.

```agda
        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`.

```agda
               → 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.

```agda
            ∙ 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.

```agda
    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`.

```agda
    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.

```agda
      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.

```agda
      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`.

```agda
      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.

```agda
          (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.

```agda
    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`.

```agda
        (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.

```agda
      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`.

```agda
        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`.

```agda
          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.

```agda
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.

```agda
  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.

```agda
  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.

```agda
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.

```agda
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.

```agda
    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.

```agda
    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.

```agda
    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`.

```agda
      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.

```agda
      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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
      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`.

```agda
      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.

```agda
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.

```agda
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.