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

At a constructible ordinal index `α`, the preceding construction already gives a host-level strict well-order on the members of `Lset α`. The purpose of this chapter is to represent its binary comparison by a set inside `L`, so that formulas interpreted in the model can quantify over that relation. The result is conditional on an adequate object-language description of one recursive step and applies when `α` is both an ordinal and constructible. It represents the relation underlying the existing order; it does not yet assert in the object language that this relation is a well-order.

```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

The single classical assumption is excluded middle at the universe level used throughout the construction. It is already needed by the stage orders and supplies the replacement and separation principles used later; the local arguments about truncation, transport, and extensional uniqueness add no second classical hypothesis.

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

Fixing `lem : LEM (ℓ-suc ℓ)` at the module boundary makes that dependence uniform. In particular, every construction below inherits the same level-indexed assumption rather than silently appealing to excluded middle at an unrestricted size.

```agda
module L.Choice.OrderTable {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

Two levels of discourse must be kept separate. The relation to be represented is defined in the host type theory, while its recursive description is a first-order formula interpreted in `L`. Membership induction connects the stages: its motive may take values in any dependent type family, so the later simultaneous package of a table and a relation does not have to be a proposition for the recursion to be legitimate.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
```

The final relation lives in the constructible model, but its endpoints begin as members of the host set `Lset α`. Once ordinalness `oα` is fixed, `Lset→isL` packages each such endpoint as an element of the model; this conversion uses the ordinalness of `α`, not a separate proof that `α` itself is constructible. The constructibility witness for `α` has a different later role: it packages the index itself as the model element `A`, which serves as the domain for replacement and as a parameter of separation. Ordinal membership supplies ordinalness at smaller indices, while pair injectivity and extensionality recover endpoints and identify sets from their members.

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; isPropIsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
```

The construction will use the two set-existence principles for different purposes. Replacement collects the relation values at all lower indices into one table, after truncated existence and extensional uniqueness have made each graph fiber contractible. Separation then cuts the current relation out of one common containing set. Thus the table and the relation at its bound are produced together, but by distinct arguments.

```agda
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL; hasSeparationL )
open import L.Recursion {ℓ} lem using ( mereFunct; smallDom )
open import L.Coding.Model {ℓ} using ( domAt-intro; prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both )
open import L.Coding.HierarchySequence {ℓ} lem using ( module RecShape )
```

The order itself is already available as `orderAt α oα`, a strict well-order on `Mem (Lset α)`. This chapter uses its underlying comparison, trichotomy, irreflexivity, and transitivity, and later transports the same order to a small presentation of the stage. No new comparison rule or well-foundedness proof is introduced here.

```agda
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf; orderAt; memOf; carry )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
```

Many later equalities compare dependent pairs whose second components are membership proofs. Since membership and ordinalness are propositions, equality of the underlying sets determines equality of the packaged members, and changing a certificate does not create a different mathematical endpoint. Transport along pair-component equalities can therefore align comparisons without turning proofs into extra choices.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
```

Propositional truncation will mark every place where existence is needed without a selected witness. Small presentations serve a different role: they replace a possibly large membership fiber by a small index type whose embedding returns the represented member. Keeping these devices distinct is essential, since one hides a choice while the other controls size.

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber )
```

From this point, propositions and quantifiers are read in the membership structure of `L`. A statement that a model element realizes a class is therefore expressed as a proposition about its members, not as an external collection assembled by metatheoretic comprehension.

```agda
open hPropStructure 𝒮ʟ
```

The internal set-builder interface will later state that a candidate has exactly the members satisfying a formula. This is an extensional specification of a set; existence still has to come from replacement or separation at the appropriate point of the recursion.

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

Formula satisfaction is compared with host-level predicates through absoluteness. The formulas do not themselves contain `orderAt`; instead, adequacy equations will identify their interpreted truth values with the host class of coded comparison pairs.

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

The formulas used below introduce two fresh binders around an existing environment. The private shift preserves the meanings of the older variables by moving each of their indices past those binders, a small syntactic device that lets the mathematical roles of value, index, and table remain fixed.

```agda
private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)
```

## The comparison, read back whole

A class in the model must be proposition-valued, whereas no proof has been given that a witness of `relOf (orderAt α oα) a b` is unique. `Ordering` therefore retains only the propositional truncation of that witness. This changes the logical form needed for class membership while preserving whether the comparison is inhabited.

```agda
Ordering : (α : V ℓ) → IsOrd α → Mem (Lset α) → Mem (Lset α) → hProp (ℓ-suc ℓ)
Ordering α oα a b = ∥ relOf (orderAt α oα) a b ∥₁ , squash₁
```

For this particular comparison, the truncation can later be removed. The reason is the trichotomy of the already constructed strict order: once `a` and `b` have been classified as forward-related, equal, or reverse-related, the latter two alternatives contradict the truncated forward comparison. This is a special property of a strict total comparison, not a general way to extract witnesses from propositional truncation.

```agda
strict : (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α))
       → ⟨ Ordering α oα a b ⟩ → relOf (orderAt α oα) a b
strict α oα a b h = decide (SWO.tri∙ W a b)
  where
  W = orderAt α oα
```

In the forward branch, trichotomy already supplies the required untruncated witness, so the truncated hypothesis is not opened. In the equality branch, the witness may be eliminated only into the empty type: transporting it along `a ≡ b` would make `a` precede itself, contrary to irreflexivity. The final result follows from that contradiction.

```agda
  decide : Tri (relOf W a b) (a ≡ b) (relOf W b a) → relOf W a b
  decide (lt k) = k
  decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥
    (λ k → SWO.irr∙ W a (subst (relOf W a) (sym q) k)) h)
  decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥
```

In the reverse branch, combining a hypothetical forward witness with the reverse comparison by transitivity would again make `a` precede itself. The truncation is opened only to prove this contradiction. Thus `strict` returns a comparison witness without proving that comparison witnesses themselves form a proposition or selecting a preferred proof.

```agda
    (λ j → SWO.irr∙ W a (SWO.trans∙ W a b a j k)) h)
```

## What the relation at a stage is

For an index `α`, `Related α z` says, under propositional truncation, that `z` is the Kuratowski pair of two members of `Lset α` related by the stage order. The ordinalness certificate is quantified inside the class, so the class does not depend on a chosen proof that `α` is an ordinal. The endpoint decomposition and comparison witness remain within their truncation boundaries.

```agda
Related : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Related α z = ∃[ oα ∶ IsOrd α ] (∃[ a ∶ Mem (Lset α) ] (∃[ b ∶ Mem (Lset α) ]
  ((z ≡ pr (fst a) (fst b)) , setIsSet z (pr (fst a) (fst b))) ⊓ Ordering α oα a b))
```

A model set `r` realizes this class when its membership agrees with `Related α` in both directions at every model element `z`. The outward implication excludes unrelated or malformed members, and the inward implication includes every related pair. Quantifying over model elements is sufficient here because constructibility is transitive, so every member of a constructible set can itself be packaged as an element of the model.

```agda
Realizes : V ℓ → S → hProp (ℓ-suc ℓ)
Realizes α r = ∀[ z ∶ S ] ((fst z ∈ fst r) ⇒ Related α (fst z))
                        ⊓ (Related α (fst z) ⇒ (fst z ∈ fst r))
```

`IsRel α r` is the type of evidence for that exact membership specification. It asserts that `r` realizes the host-defined class; it does not add a strict-order structure to `r`, nor does it claim that the relation satisfies an object-language well-order formula.

```agda
IsRel : V ℓ → S → Type (ℓ-suc ℓ)
IsRel α r = ⟨ Realizes α r ⟩
```

The two implications in a realization proof determine a path between the proposition that `z` belongs to `r` and the proposition that `z` is related at `α`. This pointwise path is the rewriting principle used later whenever membership in an arbitrary realizer must be exchanged for the semantic class.

```agda
rel-path : (α : V ℓ) (r : S) → IsRel α r
         → (z : S) → (fst z ∈ fst r) ≡ Related α (fst z)
rel-path α r p z =
  ⇔toPath {P = fst z ∈ fst r} {Q = Related α (fst z)} (p z .fst) (p z .snd)
```

If `r` and `r'` both realize the class, their membership propositions agree pointwise, and extensionality in `L` identifies the two sets. The uniqueness proved here is uniqueness of the realizing set. It does not make the truncated ordinal certificate, endpoint decomposition, or comparison witness in `Related` uniquely chosen.

```agda
rel-unique : (α : V ℓ) (r r' : S) → IsRel α r → IsRel α r' → r ≡ r'
rel-unique α r r' p q = extensionalL
  (λ z → rel-path α r p z ∙ sym (rel-path α r' q z))
```

The forward reading starts with specified members `a,b` and an actual stage-order comparison. Their underlying sets form the coded pair, while the ordinal certificate, the two packaged members, and the truncated comparison give a witness of `Related`. Since the witness is constructed inside the truncations, no choice is being extracted.

```agda
module _ (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α)) where
  related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (fst a) (fst b)) ⟩
  related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁
```

The reverse reading has a deliberately narrower shape. Its input object is already the coded pair of the fixed endpoints `a,b`; only under that presentation can the proof compare an existentially represented pair with those endpoints and recover their stage-order comparison. It does not decompose an arbitrary related object into a selected pair.

```agda
  related-out : ⟨ Related α (pr (fst a) (fst b)) ⟩ → relOf (orderAt α oα) a b
  related-out h = strict α oα a b (PT.rec squash₁ atOrd h)
    where
    atPair : (o : IsOrd α) (a' b' : Mem (Lset α))
           → (pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
```

Suppose the truncated record presents endpoints `a',b'` and an ordinalness proof `o`. Equality of the two coded pairs identifies `a` with `a'` and `b` with `b'`; propositionhood of ordinalness identifies `o` with the fixed proof `oα`. Transporting the recorded comparison along these three identifications yields a truncated comparison at the fixed endpoints.

```agda
           → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩
    atPair o a' b' q = PT.map
      (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb)
        (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k))
      where
```

Pair-code injectivity first recovers equality of the underlying endpoint sets. Each endpoint is a dependent pair of a set and its membership proof in `Lset α`; because that proof is propositional, equality of the first components lifts to equality of the complete members. The comparison can therefore be transported at its correct dependent type.

```agda
      ea : a ≡ a'
      ea = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .fst)
      eb : b ≡ b'
      eb = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .snd)
```

The outer ordinal certificate is explicit, while each endpoint exists only under propositional truncation. The elimination therefore proceeds one truncation at a time into the proposition `Ordering α oα a b`. This target permits temporary representatives to be used without allowing either endpoint to escape as selected data.

```agda
    atOrd : Σ[ o ∈ IsOrd α ] ⟨ ∃[ a' ∶ Mem (Lset α) ] (∃[ b' ∶ Mem (Lset α) ] ((pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
                 , setIsSet _ (pr (fst a') (fst b'))) ⊓ Ordering α o a' b') ⟩
          → ⟨ Ordering α oα a b ⟩
    atOrd (o , h₁) = PT.rec squash₁
      (λ { (a' , h₂) → PT.rec squash₁
```

After both temporary endpoints have been exposed, the pair-alignment argument supplies the truncated comparison at `a,b`; `strict` then turns that specific truncated comparison into the required witness. The composite proves the reverse reading while preserving all existential truncation boundaries except for the comparison witness justified by trichotomy.

```agda
        (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁
```

## Whatever realizes the class, read at both shapes

The useful representation lemmas are stated for any `r` realizing `Related α`, not only for the relation eventually constructed by the recursion. This allows a relation value already recorded in a lower table to be read immediately. For fixed ordinalness `oα`, each member of `Lset α` is constructible and can therefore be packaged as an element of the model.

```agda
module _ (α : V ℓ) (oα : IsOrd α) (r : S) (hr : IsRel α r) where
  private
    memL : Mem (Lset α) → S
    memL c = fst c , Lset→isL α oα (fst c) (snd c)
```

The model's internal ordered pair of the packaged endpoints and the host Kuratowski pair of their underlying sets are propositionally equal, though they are not treated as definitionally identical. Applying membership in `r` to this equality gives the first transport bridge.

```agda
    atRel : (a b : Mem (Lset α))
          → (fst (prʟ (memL a) (memL b)) ∈ fst r)
          ≡ (pr (fst a) (fst b) ∈ fst r)
    atRel a b = cong (λ x → x ∈ fst r) (prʟ-fst (memL a) (memL b))
```

Applying `Related α` to the same pair equality gives the companion bridge on the semantic side. Together, the two bridges let a realization proof be used at an internal pair and then restated at the plain pair of underlying sets, or conversely.

```agda
    atRelated : (a b : Mem (Lset α))
              → ⟨ Related α (fst (prʟ (memL a) (memL b))) ⟩
              ≡ ⟨ Related α (pr (fst a) (fst b)) ⟩
    atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b))
```

The filling direction begins with a host-level comparison of two members. The forward `Related` reading turns it into relatedness of their coded pair, the realization proof turns relatedness into membership in `r`, and the pair bridge returns the statement to the host pair. Hence every pair compared by `orderAt` occurs in any realizing set.

```agda
  rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
           → ⟨ pr (fst a) (fst b) ∈ fst r ⟩
  rel-fill a b h = subst ⟨_⟩ (atRel a b)
    (hr (prʟ (memL a) (memL b)) .snd
      (transport (sym (atRelated a b)) (related-in α oα a b h)))
```

The reading direction reverses the route. Membership of the host pair is transported to membership of the internal pair, read outward through the realization proof as a `Related` fact, transported back to the fixed host pair, and finally converted by `related-out` into the untruncated stage-order comparison.

```agda
  rel-rep : (a b : Mem (Lset α))
          → ⟨ pr (fst a) (fst b) ∈ fst r ⟩ → relOf (orderAt α oα) a b
  rel-rep a b h = related-out α oα a b
    (transport (atRelated a b)
      (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h)))
```

Some later arguments work with the small presentation `⟪ Lset α ⟫` rather than with dependent member pairs. An index in that presentation embeds into the underlying set and carries precisely the membership proof needed to form an element of `Mem (Lset α)`.

```agda
  private
    atIx : ⟪ Lset α ⟫ → Mem (Lset α)
    atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m
```

Carrying `orderAt` along that presentation gives a strict order on the small index type. This is the same comparison viewed through the embedding, so the representation theorems need no new order-theoretic argument.

```agda
  open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ )
```

For presentation indices `u,v`, a carried comparison is first read as the comparison of their associated stage members. The earlier filling theorem then places the Kuratowski pair of the embedded endpoints in `r`. This is the small-index form of comparison-to-membership.

```agda
  ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v
             → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩
  ixRel-fill u v = rel-fill (atIx u) (atIx v)
```

Conversely, membership of the pair of embedded endpoints is read by the earlier theorem as a comparison of the associated stage members. By the definition of the carried order, this is exactly the strict comparison of `u` and `v` in the small presentation.

```agda
  ixRel-rep : (u v : ⟪ Lset α ⟫)
            → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩ → u ≺ᶜ v
  ixRel-rep u v = rel-rep (atIx u) (atIx v)
```

## What a table records

The first table condition is soundness of recorded values. If an index `c` lies below `B` and the coded entry `(c,r)` occurs in `h`, then `r` must realize `Related c`. This condition says nothing about entries whose first component lies outside `B`, so it cannot by itself characterize the table's domain.

```agda
Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c r : S) → ⟨ fst c ∈ B ⟩
           → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → IsRel (fst c) r
```

The second condition is totality below the bound. Every `c ∈ B` has some recorded value `r`, but the existence is propositionally truncated. Thus `Entries` supplies exactly what a propositional step argument may use, while withholding a global function that chooses one value at every index.

```agda
Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ fst c ∈ B ⟩
            → ∥ (Σ[ r ∈ S ] ⟨ pr (fst c) (fst r) ∈ fst h ⟩) ∥₁
```

The third condition excludes entries beyond the bound: every coded pair in `h` has its first component in `B`. Together with `Entries`, it yields the exact domain needed when a completed table is turned back into an approximation. The forward proof that recorded values are sound needs only the first two conditions and therefore keeps `Domain` separate.

```agda
Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩
```

## The step, as a parameter

The recursive construction now assumes two formulas with one semantic meaning. `Cond b f` is the variable-slot form used when an approximation table is bound inside a graph; `Cond₀ B F` is the constant form used when a fixed ordinal and completed table serve as parameters to separation. The first adequacy equation assumes ordinalness together with `Values` and `Entries`, then identifies satisfaction of the variable form with `Related` at every tested object.

```agda
module Described
  (Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n))
  (Cond₀ : S → S → Formula S 1)
  (cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ))
             → Values (lookup f γ) (fst (lookup b γ))
```

The variable-form hypothesis is pointwise and genuinely bidirectional: it both reads a satisfying coded object as a related pair and constructs satisfaction from relatedness. Only correctness and truncated existence of entries below the ordinal are required. No exact-domain claim is assumed here, so possible entries outside the bound play no part in the semantic identification.

```agda
             → Entries (lookup f γ) (fst (lookup b γ))
             → (z : S)
             → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z))
  (cond₀-spec : (b f : S) → IsOrd (fst b)
              → Values f (fst b) → Entries f (fst b)
```

The constant-form equation gives the same pointwise equivalence after the ordinal and table have become fixed model elements. This second presentation is required by separation, whose defining formula has one free slot for the possible relation member. The equation identifies the meanings of the two contexts; it does not claim that `Cond` and `Cond₀` are syntactically equal.

```agda
              → (z : S) → ((z ∷ []) ⊨ Cond₀ b f) ≡ Related (fst b) (fst z))
  where
```

Given the variable condition, `StepAt v b f` specifies a candidate value extensionally: an object belongs to the value in slot `v` exactly when it satisfies `Cond b f`. This is a two-way membership specification, not an existence theorem. The actual set realizing the specification will be produced later by the recursive use of replacement and separation.

```agda
  StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  StepAt v b f = extAt v (Cond b f)
```

Fix slots for the candidate value, ordinal index, and lower table, together with an environment satisfying ordinalness, value soundness, and truncated entry existence. Under these hypotheses, the adequacy equation supplies one common pointwise meaning for the condition. The following two readings will use it in opposite directions: an extensional step specification yields an `IsRel` proof for the candidate value, while an existing `IsRel` proof fills that specification. The whole construction remains relative to the assumed step description until a later chapter supplies a concrete instance.

```agda
  module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
           (ob : IsOrd (fst (lookup b γ)))
           (vals : Values (lookup f γ) (fst (lookup b γ)))
           (ents : Entries (lookup f γ) (fst (lookup b γ))) where
    private
```

Once an ordinal bound, a sound table, and entries at every smaller argument have been fixed, the variable form of the condition has an exact mathematical meaning. A set satisfies it precisely when it is one of the ordered pairs related by the stage order. This equivalence is the semantic bridge between the object-language step and the host-level relation.

```agda
      same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z)
      same = cond-spec b f γ ob vals ents
```

Suppose a candidate value satisfies the extensional step. Membership in that value then implies the condition, hence relatedness, while relatedness implies the condition and therefore membership. These two implications say exactly that the candidate realizes the relation at the chosen ordinal.

```agda
    step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel (fst (lookup b γ)) (lookup v γ)
    step-rel h z =
        (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz))
      , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz))
```

The same argument reverses. If a set already realizes the stage relation, its two membership implications can be transported across the semantic equivalence to prove the extensional step. Thus the step formula and realization carry the same information once the ordinal and the table hypotheses are available.

```agda
    step-table : IsRel (fst (lookup b γ)) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩
    step-table sp = extAt-in-both v (Cond b f) γ
      (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz))
      (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))
```

## Approximations and the graph

The generic recursion shape is now specialized to this step. An approximation is a set-coded table with the prescribed domain and a valid step at every recorded entry; a graph says that some such approximation supports the value at the current argument; and the paired graph records the argument together with that value. The available introduction and elimination principles let the rest of the construction reason through these meanings without choosing witnesses from truncated existences.

```agda
  module A = RecShape StepAt
  open A using ( ApproxAt; GraphAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step
               ; ApproxAt-in; GraphOf; Graph-in; Graph-out
               ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )
```

## Every value an approximation records

To prove that an approximation records only correct values, fix its table and domain and consider one possible argument `u`. The induction property says that if `u` is constructible and ordinal, then every recorded pair `(u,r)` has a value `r` realizing the relation at `u`. It deliberately quantifies over every recorded value, so functionality is not assumed.

```agda
  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    private
      Value : V ℓ → Type (ℓ-suc ℓ)
      Value u = ⟨ isL u ⟩ → IsOrd u → (r : S)
              → ⟨ pr u (fst r) ∈ fst (lookup f γ) ⟩ → IsRel u r
```

Membership induction is applied to the underlying set of the recorded argument `c`. This is legitimate for the Type-valued property just described: membership induction is a recursion principle for arbitrary dependent type families, not only for propositions. The approximation's domain is assumed ordinal so that membership below one recorded argument remains inside that domain.

```agda
    approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ))
               → (c : S) → IsOrd (fst c) → (r : S)
               → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst c) r
    approx-val h oa c = ∈-induction {P = Value} go (fst c) (snd c)
      where
```

At the induction step, let `r` be a value recorded at `u`. The approximation itself says that this entry satisfies the recursive step computed from the same table. To read that step as realization at `u`, it remains to supply a sound and complete restriction of the table below `u`; these are exactly the two obligations discharged by the induction hypothesis and the domain information.

```agda
      go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
      go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents
        (ApproxAt-step f a γ h d r p)
        where
        d : S
```

The argument `u` is paired with its constructibility proof so that it can be used as an element of the model. Because `(u,r)` is recorded, the exact-domain clause of the approximation places `u` in the approximation's ordinal domain. This is the point at which a fact about a table entry becomes the bound needed for all smaller recursive calls.

```agda
        d = u , hu
        u∈a : ⟨ u ∈ fst (lookup a γ) ⟩
        u∈a = ApproxAt-dom f a γ h d r p
        vals : Values (lookup f γ) u
        vals e t e∈ q =
```

For an entry `(e,t)` with `e∈u`, the induction hypothesis proves that `t` realizes the relation at `e`; membership in an ordinal also makes `e` ordinal. Completeness is obtained differently: transitivity of the approximation's ordinal domain turns `e∈u` and `u` in the domain into `e` in the domain, and the approximation supplies some value there under propositional truncation. The recursive step at `u` is therefore fully justified. In particular, two values recorded at one argument can later be identified because both realize the same class, although no separately named uniqueness lemma is introduced here.

```agda
          IH (fst e) e∈ (snd e) (mem-ord {A = u} ou (fst e) e∈) t q
        ents : Entries (lookup f γ) u
        ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = fst e} e∈ u∈a)
```

## The graph holds of nothing else

A graph assertion contains only a propositionally truncated witness for the supporting approximation. Nevertheless, its desired conclusion, that the displayed value realizes the relation at the ordinal argument, is itself a proposition. The truncation may therefore be eliminated into that conclusion. This establishes correctness of a graph value; uniqueness still requires comparing two realizing sets by extensionality.

```agda
  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd (fst (lookup b γ))
               → IsRel (fst (lookup b γ)) (lookup w γ)
    graph-only h ob = PT.rec (snd (Realizes (fst (lookup b γ)) (lookup w γ)))
      read (Graph-out w b γ h)
```

After a graph witness is opened inside this propositional target, it provides an approximation `f` together with the outer step at the bound. The step can be read as realization once `f` is known to have correct values and entries at every argument below the bound. Those two facts are recovered from the approximation rather than assumed afresh.

```agda
      where
      read : GraphOf w b γ → IsRel (fst (lookup b γ)) (lookup w γ)
      read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs
        where
        vals : Values f (fst (lookup b γ))
```

Correctness of every value recorded by `f` is the preceding membership-induction result, applied to each member of the ordinal bound; the member is ordinal by `mem-ord`. Completeness below the bound is already the value-existence half of the approximation's exact-domain specification. Hence the outer step yields the promised realization.

```agda
        vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c
          (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈) r p
        ents : Entries f (fst (lookup b γ))
        ents = ApproxAt-value zero (suc b) (f ∷ γ) ha
```

For the converse direction, begin with a table `h` that is sound on an ordinal bound, has an entry at every point below it, and has no recorded pair whose first component lies outside it. If the proposed current value realizes the relation at the bound, these data are sufficient to exhibit `h` as the approximation hidden by the graph and to verify the graph's outer step.

```agda
    graph-table : (h : S) → IsOrd (fst (lookup b γ))
                → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ))
                → Domain h (fst (lookup b γ))
                → IsRel (fst (lookup b γ)) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩
    graph-table h ob vals ents dom sp = Graph-in w b γ h approx
```

The outer step follows immediately from the realization hypothesis by the reverse semantic bridge. What remains is the approximation. Its domain must be exact: a first component occurs in some table entry precisely when it lies below the bound. The two directions use different table assumptions, which prevents soundness, completeness, and boundedness from being conflated.

```agda
      (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp)
      where
      onDom : (c : S)
            → (⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩
               → ⟨ fst c ∈ fst (lookup b γ) ⟩)
```

If some value is recorded at `c`, the witness for that value is propositionally truncated. It may be eliminated because the conclusion `c` belongs to the bound is a proposition, and boundedness then proves that conclusion. Conversely, completeness supplies a merely existing recorded value for every `c` in the bound. Together these directions give the exact domain required of an approximation.

```agda
            × (⟨ fst c ∈ fst (lookup b γ) ⟩
               → ⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩)
      onDom c = (λ hr → PT.rec (snd (fst c ∈ fst (lookup b γ)))
                          (λ { (r , p) → dom c r p }) hr)
              , ents c
```

The second approximation clause checks the recursive step at each recorded pair `(c,r)`. It uses the same table `h`, but only through the information relevant below `c`. Thus every existing entry must be viewed locally: `c` must be an ordinal, all recorded values below it must be correct, and every smaller argument must have an entry.

```agda
      onStep : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
             → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
      onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ)
        oc vals' ents' (vals c r c∈ p)
        where
```

Boundedness first turns the recorded pair into `c` below the ambient bound. Since that bound is ordinal, `c` is ordinal as well. The soundness hypothesis can now be restricted to `c`: whenever an entry `(e,t)` is actually recorded, boundedness places `e` in the ambient bound and the original soundness statement applies.

```agda
        c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩
        c∈ = dom c r p
        oc : IsOrd (fst c)
        oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
        vals' : Values h (fst c)
```

Notice the asymmetry between local soundness and local completeness. Soundness needs only the fact that an entry is recorded, because boundedness recovers its ambient-domain membership. Completeness starts from `e∈c`; transitivity of the ambient ordinal combines this with `c` below the bound, after which the original completeness hypothesis supplies an entry at `e`.

```agda
        vals' e t _ q = vals e t (dom e t q) q
        ents' : Entries h (fst c)
        ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈)
```

The exact-domain equivalence and the local step proof are precisely the two conjuncts of an approximation. Packaging them makes `h` a witness for the approximation hidden in the graph. Together with the already verified outer step, this completes the passage from a sound, complete, bounded table to the graph assertion.

```agda
      approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
      approx = ApproxAt-in zero (suc b) (h ∷ γ)
        (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep
```

## The pair graph

Replacement acts on a graph whose value is a complete table entry. `PairGraphAt` therefore says that the displayed value is the Kuratowski pair of the current index and some relation set, and that this relation set satisfies `GraphAt` at that index. Its two readings keep the relation-set witness under propositional truncation. This is the bridge from the relation-valued recursion to a replacement image containing indexed entries.

## The table, and the relation at the bound

The class `Recorded B` describes the intended members of a table below `B`. An object belongs to it merely when there are a model element `c` in `B` and a model element `r` realizing the relation at `c`, such that the object is the ordered pair of their underlying sets. The existential data are propositionally truncated. The definition itself does not require `B` to be ordinal; ordinality will matter when this class is used for an ordinal bound.

```agda
  Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  Recorded B z = ∃[ c ∶ S ] (fst c ∈ B) ⊓ (∃[ r ∶ S ]
    ((z ≡ pr (fst c) (fst r)) , setIsSet z (pr (fst c) (fst r)))
    ⊓ Realizes (fst c) r)
```

A model set is a table for `B` when membership in it is pointwise equivalent to belonging to `Recorded B`. Both directions matter. One excludes every unrelated or out-of-domain object, while the other includes every pair `(c,r)` with `c∈B` and `r` realizing the relation at `c`. Thus `IsTable` expresses exact representation, not only closure under correct entries.

```agda
  IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
  IsTable B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z)
```

The recursive datum at `α` contains two model sets: a table representing all correct entries below `α`, and a set realizing the relation at `α` itself. At the next larger argument, the first component supplies the earlier table needed to check an approximation, while the second supplies the relation value to be entered into a later table. This bundle is data returned by membership recursion. No proof that its type is a proposition is given or needed, because membership induction accepts arbitrary Type-valued families.

```agda
  Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
  Bundle α = Σ[ h ∈ S ] Σ[ r ∈ S ] (IsTable α h × IsRel α r)
```

Fix an exact table `h` for a bound `B`. To use its specification at a concrete entry, one must align two versions of ordered pairing: the internal pair of model elements and the host-level Kuratowski pair of their underlying sets. The projection law for internal pairing transports the table equivalence to the underlying pair `(c,r)`.

```agda
  module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where
    private
      atPair : (c r : S)
             → (pr (fst c) (fst r) ∈ fst h) ≡ Recorded B (pr (fst c) (fst r))
      atPair c r = subst (λ x → (x ∈ fst h) ≡ Recorded B x) (prʟ-fst c r)
```

The exact table specification is applied to the internal pair and then viewed through that projection law. Although the surrounding reading fixes `B` as an ordinal, this alignment itself uses only the table specification and the representation of ordered pairs; it contains no additional ordinal argument.

```agda
        (sp (prʟ c r))
```

An actual table entry `(c,r)` can now be read in two ways at once. Exactness yields a recorded decomposition, from which one recovers both `c∈B`, the domain fact, and that `r` realizes the relation at `c`, the value-soundness fact. Applying this reading to every entry gives `Domain h B` and `Values h B`.

```agda
    table-out : Domain h B × Values h B
    table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd)
      where
      read : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
           → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
```

The decomposition supplied by `Recorded` is propositionally truncated, so its elimination needs a proposition-valued target. Here the target is the product of membership in `B` and realization of the relation. Membership is a proposition, realization is a proposition, and their product is again a proposition. This, rather than any property of the whole bundle, is what licenses the elimination.

```agda
      read c r p = PT.rec isPropBoth outer (subst ⟨_⟩ (atPair c r) p)
        where
        isPropBoth : isProp (⟨ fst c ∈ B ⟩ × IsRel (fst c) r)
        isPropBoth = isProp× (snd (fst c ∈ B)) (snd (Realizes (fst c) r))
```

Inside the propositional elimination, suppose the recorded decomposition uses another pair `(d,t)`. Equality of the Kuratowski pairs `(c,r)` and `(d,t)` forces equality of their first underlying components and equality of their second underlying components. The first equality will transfer domain membership, while the second aligns the proposed value with the realizing value from the decomposition.

```agda
        inner : (d t : S) → ⟨ fst d ∈ B ⟩
              → (pr (fst c) (fst r) ≡ pr (fst d) (fst t)) → IsRel (fst d) t
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        inner d t d∈ q hr =
            subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈
```

The first-component equality transports `d∈B` to `c∈B`. Equality of the second underlying sets lifts to equality of the model elements `r` and `t`, because their constructibility certificates are propositions and carry no extra choice. Realization can then be transported simultaneously along the index equality and this value equality, yielding realization at exactly `(c,r)`.

```agda
          , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr
          where
          rt : r ≡ t
          rt = Σ≡Prop (λ x → snd (isL x)) (pr-inj q .snd)
```

The outer recorded witness first provides an index `d` in `B` and a further truncated witness for its realizing value. Since the final pair of facts is propositional, both truncation layers may be eliminated in turn. The endpoint-equality argument just established handles the innermost decomposition.

```agda
        outer : Σ[ d ∈ S ] ( ⟨ fst d ∈ B ⟩
                  × ⟨ ∃[ t ∶ S ] ((pr (fst c) (fst r) ≡ pr (fst d) (fst t))
                        , setIsSet _ (pr (fst d) (fst t))) ⊓ Realizes (fst d) t ⟩ )
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        outer (d , (d∈ , hs)) = PT.rec isPropBoth
```

For each possible realizing value `t`, the equality of pairs reduces the witness to the desired facts about `c` and `r`. Because the result does not retain `t`, this use of truncation does not choose a value from the table; it proves only the proposition that the given entry has the required domain and realization properties.

```agda
          (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs
```

The converse table reading is direct. Given `c∈B` and a model element `r` realizing the relation at `c`, the pair `(c,r)` has the required truncated `Recorded` witness. Exactness of the table then turns that class membership into membership in `h`, with the internal-pair projection supplying the necessary alignment of representations.

```agda
    table-in : (c r : S) → ⟨ fst c ∈ B ⟩ → IsRel (fst c) r
             → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
    table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r))
      ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁
```

Before the relation at an ordinal `α` can be obtained by separation, all possible related pairs need one containing set in `L`. The required bound returns a model set `D` containing every object in `Related α`. It is only a common container and may have unrelated members; exactness is not claimed at this stage.

```agda
  bound : (α : V ℓ) (oα : IsOrd α)
        → Σ[ D ∈ S ] ((z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst D ⟩)
  bound α oα = d .fst , confine
    where
    ixL : ⟪ Lset α ⟫ → S
```

The small presentation of `Lset α` supplies indices for all of its members. Each index is turned into a model element by pairing the presented underlying set with its constructibility proof, obtained from membership in the constructible stage. This makes internal ordered pairing available for every presented endpoint.

```agda
    ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m)
```

Pairs of presentation indices form a small indexing type. Applying the common-domain principle to the family of their internal ordered pairs gives a model set `D` containing every member of that family. The principle supplies containment only; it neither computes the exact image nor filters pairs according to the stage order.

```agda
    d : Σ[ D ∈ S ] ((p : ⟪ Lset α ⟫ × ⟪ Lset α ⟫)
                    → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
    d = smallDom (⟪ Lset α ⟫ × ⟪ Lset α ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
```

The common bound must also be usable for ordinary members `a,b` of `Lset α`, not just for presentation indices. Represent each member by its fiber index, use the bound for the corresponding internal pair, and transport membership along the equality between the presented pair and the host-level pair `pr(fst a,fst b)`. Thus every pair of stage members lies in `D`.

```agda
    onPair : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst (d .fst) ⟩
    onPair a b = subst (λ x → ⟨ x ∈ fst (d .fst) ⟩)
      (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst))
        ∙ cong₂ pr (fa .snd) (fb .snd))
      (d .snd (fa .fst , fb .fst))
```

Membership proofs for `a` and `b` identify them with elements of the small presentation. The resulting fiber equalities identify both endpoints, and congruence of ordered pairing identifies the two host-level pairs. Combined with the projection law for internal pairing, this is the equality used in the preceding transport.

```agda
      where
      fa = ∈-asFiber {a = fst a} {b = Lset α} (snd a)
      fb = ∈-asFiber {a = fst b} {b = Lset α} (snd b)
```

Now take an arbitrary object in `Related α`. Its definition gives, through three nested propositionally truncated existentials, an ordinal certificate and two members `a,b` of `Lset α`, together with an equality identifying the object with their pair and the propositionally truncated comparison fact. The target, membership in `D`, is a proposition, so the three existential truncations may be eliminated one after another. Containment depends only on the endpoints and their pair equality; even the truncated comparison is unnecessary for this coarse bound.

```agda
    confine : (z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst (d .fst) ⟩
    confine z = PT.rec (snd (fst z ∈ fst (d .fst)))
      (λ { (_ , h₁) → PT.rec (snd (fst z ∈ fst (d .fst)))
        (λ { (a , h₂) → PT.rec (snd (fst z ∈ fst (d .fst)))
          (λ { (b , (q , _)) →
```

The pair of recovered endpoints already belongs to `D` by the previous result. Transporting this membership along the reverse of the recovered pair equality places the original object in `D`. The witnesses remain confined to the propositional proof, so the bound does not choose endpoints for each related object.

```agda
            subst (λ x → ⟨ x ∈ fst (d .fst) ⟩) (sym q) (onPair a b) }) h₂ }) h₁ })
```

The table and current relation are constructed together by membership recursion. Its actual input range is a constructible ordinal: `α` is accompanied by both a proof that it belongs to `L` and a proof that it is ordinal. The recursive value is the bundle just described, and the definition is sealed so later arguments use its specifications. This recursion is valid for a Type-valued family; it does not rely on `Bundle α` being a proposition.

```agda
  opaque
    tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α
    tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α}
      (build (PairGraphAt zero (suc zero)) refl)
      where
```

At the induction step for `α`, assume recursively that every member `δ` of `α` has a bundle whenever its constructibility and ordinality are supplied. The task is to produce the corresponding table below `α` and the relation at `α`. The paired graph formula is kept as an explicit parameter together with an equality to the intended formula; this changes no mathematical hypothesis and lets the replacement argument use exactly that graph.

```agda
      build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero)
            → (α : V ℓ)
            → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ)
            → ⟨ isL α ⟩ → IsOrd α → Bundle α
      build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec))
```

The ordinal `α` and its constructibility proof form a model element `A`. This is the internal domain over which the paired graph will be considered: its members are precisely the smaller sets that the membership-recursive hypothesis can address once their ordinalness has been established.

```agda
        where
        A : S
        A = α , hα
```

Every member `c` of an ordinal `α` is itself an ordinal. This inherited ordinalness is essential because the recursive construction is defined only on constructible ordinals, not on arbitrary constructible members. No truncation is involved in obtaining this certificate.

```agda
        ordOf : (c : S) → ⟨ fst c ∈ α ⟩ → IsOrd (fst c)
        ordOf c c∈ = mem-ord {A = α} oα (fst c) c∈
```

For `c∈α`, the model element `c` already carries its constructibility proof, and ordinal membership supplies its ordinalness. These are exactly the inputs needed to apply the induction hypothesis. The result is the full bundle at `c`: both the exact table below `c` and a realizing relation at `c`.

```agda
        bun : (c : S) → ⟨ fst c ∈ α ⟩ → Bundle (fst c)
        bun c c∈ = IH (fst c) c∈ (snd c) (ordOf c c∈)
```

From the recursive bundle at `c`, select its current-relation component and call it the value at `c`. This is a concrete model element, not a witness extracted from the truncated `Entries` field of a table. Its availability is why the recursion carries the relation at each constructible ordinal in its domain together with the table below it.

```agda
        value : (c : S) → ⟨ fst c ∈ α ⟩ → S
        value c c∈ = bun c c∈ .snd .fst
```

The specification stored with that component states that the chosen value realizes `Related c`. This is exactly the semantic correctness supplied by the induction hypothesis. By itself it asserts neither that the value satisfies the paired graph nor that its pair with `c` belongs to a completed table.

```agda
        relOK : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → IsRel (fst c) (value c c∈)
        relOK c c∈ = bun c c∈ .snd .snd .snd
```

For each `c` whose underlying ordinal lies below `α`, the induction hypothesis already supplies the relation set at `c`. Replacement must remember which index produced that relation, so its candidate value is the internal ordered pair of `c` with this relation set, rather than the relation set alone.

```agda
        entry : (c : S) → ⟨ fst c ∈ α ⟩ → S
        entry c c∈ = prʟ c (value c c∈)
```

It remains to show that this candidate lies on the graph used by replacement. Before forming the pair, the chosen relation set must satisfy the recursive graph at `c`. The bundle at `c` provides both its lower table and its realized relation, while membership of `c` in the ordinal `α` makes `c` an ordinal and permits the general table-to-graph argument to be applied.

```agda
        below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
              → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩
        below c c∈ k = graph-table zero (suc (suc zero))
          (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈)
          (reads .snd) ents (reads .fst) (relOK c c∈)
```

The exact specification of the lower table yields two of the three facts required by that argument: every recorded value below `c` realizes the appropriate relation, and no recorded pair has an index outside `c`. The remaining fact is completeness, namely that each member of `c` has some recorded value.

```agda
          where
          reads : Domain (bun c c∈ .fst) (fst c) × Values (bun c c∈ .fst) (fst c)
          reads = table-out (fst c) (ordOf c c∈) (bun c c∈ .fst)
                    (bun c c∈ .snd .snd .fst)
          ents : Entries (bun c c∈ .fst) (fst c)
```

For a member `e` of `c`, transitivity of the ambient ordinal carries `e ∈ c ∈ α` to `e ∈ α`. The induction hypothesis therefore supplies the realized relation at `e`, and the exact table specification at `c` places the pair of `e` with that relation into the lower table. The witness is returned under propositional truncation, exactly as table completeness requires.

```agda
          ents e e∈ = ∣ value e e∈' , table-in (fst c) (ordOf c c∈) (bun c c∈ .fst)
                         (bun c c∈ .snd .snd .fst) e (value e e∈') e∈ (relOK e e∈') ∣₁
            where
            e∈' : ⟨ fst e ∈ α ⟩
            e∈' = oα .fst {x = fst c} {y = fst e} e∈ c∈
```

The recursive graph proof for the relation value can now be combined with the canonical identification of the internal ordered pair. Thus the candidate entry satisfies the paired graph formula at `c`, establishing the existence half of functionality for every index below `α`.

```agda
        holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
        holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
          (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))
```

Functionality also requires uniqueness of the whole paired value. If another `k` satisfies the paired graph at `c`, reading that formula gives, under propositional truncation, a relation set `r`, an identification of the underlying set of `k` with the pair `(c,r)`, and a graph proof for `r`. Since equality in the constructible carrier is a proposition, this truncated information may be eliminated into the desired equality.

```agda
        only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
             → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
        only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read
          (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)
          where
```

The graph proof says that `r` realizes the relation class at `c`; independently, the induction hypothesis says the chosen value at `c` realizes that same class. Extensional uniqueness of realizing relation sets therefore identifies `r` with the chosen value. This is where uniqueness enters, after graph correctness has been established, rather than as an assumption about the lower table.

```agda
          read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
          read (r , (q , hg)) = Σ≡Prop (λ x → snd (isL x))
            ( q
            ∙ cong (pr (fst c)) (cong fst (rel-unique (fst c) r (value c c∈)
                (graph-only zero (suc (suc zero)) (r ∷ k ∷ c ∷ []) hg (ordOf c c∈))
```

Composing the given identification of `k` with `(c,r)`, the equality of the two relation sets, and the canonical projection path for the constructible ordered pair identifies the underlying sets of `k` and the candidate entry. Constructibility is a proposition, so this underlying equality lifts to an equality in the carrier and completes the uniqueness proof.

```agda
                (relOK c c∈)))
            ∙ sym (prʟ-fst c (value c c∈)) )
```

For each `c ∈ α`, existence and uniqueness now describe a single point of the fiber consisting of a graph value together with its satisfaction proof. The unique-existence witness is propositionally truncated, but contractibility is itself a proposition; hence `mereFunct` converts that witness into the contractible fiber required by replacement without making any additional choice.

```agda
        fc : (c : S) → ⟨ c ∈ˢ A ⟩
           → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
        fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁
```

Replacement may therefore collect the paired graph values over the internal domain `α`. Its conclusion is a contractible type of a constructible set equipped with the exact membership specification for that image. In particular, it gives a uniquely specified image set; it does not assert that the members of that set form a contractible type.

```agda
        rep : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))
        rep = hasReplacementL A φ fc
```

The table `H` is the constructible set at the center of this contractible replacement result. Its accompanying membership specification remains available and will now be used to prove that `H` records exactly the intended index-relation pairs.

```agda
        H : S
        H = rep .fst .fst
```

The required table specification is an equality between two propositions: membership in `H` and being an index below `α` paired with a set realizing the relation there. It is obtained from two implications. The forward implication reads replacement membership, and the backward implication turns any such recorded pair back into a value of the replacement graph.

```agda
        spec : IsTable α H
        spec z = ⇔toPath toRec fromRec
          where
          toRec : ⟨ fst z ∈ fst H ⟩ → ⟨ Recorded α (fst z) ⟩
          toRec hz = PT.rec squash₁
```

In the forward direction, replacement membership merely supplies an index `c` below `α` and a proof that `z` satisfies the paired graph there. The uniqueness result identifies `z` with the canonical entry at `c`; its relation component is already known to realize the class at `c`. These facts produce the required recorded-pair witness, still under propositional truncation.

```agda
            (λ { (c , (c∈ , hp)) → ∣ c , (c∈ , ∣ value c c∈
               , ( cong fst (only c c∈ z hp) ∙ prʟ-fst c (value c c∈)
                 , relOK c c∈ ) ∣₁) ∣₁ })
            (subst ⟨_⟩ (rep .fst .snd z) hz)
```

For the reverse implication, a recorded-pair witness may contain any relation set `r` realizing the class at `c`, not necessarily the recursive value chosen above. To reuse the paired graph proof already established for the canonical entry, the argument first eliminates the truncated witness into the propositional satisfaction goal and then transports that proof along an equality between the two entries.

```agda
          fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst H ⟩
          fromRec hz = subst ⟨_⟩ (sym (rep .fst .snd z)) (PT.map
            (λ { (c , (c∈ , hr)) → c , (c∈ , PT.rec (snd ((z ∷ c ∷ []) ⊨ φ))
              (λ { (r , (q , hs)) → subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩)
                (sym (Σ≡Prop (λ x → snd (isL x))
```

That transport path starts with the recorded equality for `z`, replaces `r` by the canonical relation value using extensional uniqueness, and ends with the canonical projection path for the internal ordered pair. Because constructibility proofs are propositional, equality of the underlying sets determines equality in the carrier. The transported graph proof then places `z` in the replacement image and closes the reverse implication.

```agda
                  (q ∙ cong (pr (fst c)) (cong fst
                     (rel-unique (fst c) r (value c c∈) hs (relOK c c∈)))
                     ∙ sym (prʟ-fst c (value c c∈)))))
                (holds c c∈) }) hr) }) hz)
```

The exact table specification now yields correctness of all values recorded by `H` below `α`. If the pair `(c,r)` belongs to `H` with `c ∈ α`, reading the specification shows that `r` realizes the relation class at `c`. No new induction or uniqueness argument is needed at this point.

```agda
        tvals : Values H α
        tvals = table-out α oα H spec .snd
```

Completeness is obtained pointwise. For each `c ∈ α`, the recursive value at `c` is known to realize the required class, so the table specification inserts its pair into `H`. The resulting existential statement is propositionally truncated: it certifies that an entry exists at every index without making a distinguished entry part of the completeness statement.

```agda
        tents : Entries H α
        tents c c∈ = ∣ value c c∈
                    , table-in α oα H spec c (value c c∈) c∈ (relOK c c∈) ∣₁
```

The table has now supplied the value correctness and completeness needed to read the constant form of the step condition at `α`. Separation applies that condition inside the previously constructed common bound. It returns the uniquely specified constructible subset whose members are exactly the bounded elements satisfying the condition; this subset, rather than the bound itself, is the candidate relation at `α`.

```agda
        sep : isContr (SetOf (λ x → (x ∈ˢ bound α oα .fst)
                                  ⊓ ((x ∷ []) ⊨ Cond₀ A H)))
        sep = hasSeparationL (bound α oα .fst) (Cond₀ A H)
```

To prove that the separated set realizes the intended class, first take one of its members. The separation specification yields both membership in the common bound and satisfaction of the constant condition; only the second component is needed in this direction. Adequacy of the condition converts that satisfaction into `Related α`, giving the membership-to-relation implication.

```agda
        rspec : IsRel α (sep .fst .fst)
        rspec z =
            (λ hz → subst ⟨_⟩ (cond₀-spec A H oα tvals tents z)
                      (subst ⟨_⟩ (sep .fst .snd z) hz .snd))
          , (λ hz → subst ⟨_⟩ (sym (sep .fst .snd z))
```

Conversely, an element satisfying `Related α` lies in the common bound by its defining confinement property. Adequacy in the reverse direction turns the same relation fact into satisfaction of the constant condition. These two components meet the separation specification and place the element in the separated set, completing the exact realization in both directions.

```agda
                      ( bound α oα .snd z hz
                      , subst ⟨_⟩ (sym (cond₀-spec A H oα tvals tents z)) hz ))
```

For a layer index `α` equipped with both constructibility and ordinalness, the recursive bundle contains the lower table and the relation set just obtained by separation. The relation `relL` selects the latter. Its scope is therefore the constructible ordinal indices used in `L`, not arbitrary ordinals without a constructibility witness.

```agda
  relL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
  relL α hα oα = tableAt α hα oα .snd .fst
```

The accompanying specification comes from the same bundle. It says exactly that membership in `relL` agrees with the class `Related α`: every member represents a related pair, and every related pair belongs. Later arguments can therefore reason from this equivalence without reopening the replacement and separation construction.

```agda
  relL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsRel α (relL α hα oα)
  relL-spec α hα oα = tableAt α hα oα .snd .snd .snd
```

## The members are the pairs the order relates

For two members `a` and `b` of `Lset α`, the filling direction specializes the general realization lemma to `relL`. A host-level comparison by the already constructed strict well-order `orderAt α` therefore places the encoded ordered pair of their underlying sets in `relL`.

```agda
  module _ (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) where
    relL-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
              → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
    relL-fill = rel-fill α oα (relL α hα oα) (relL-spec α hα oα)
```

The reading direction gives the converse for the same two layer members: membership of their encoded pair in `relL` recovers the host-level comparison in `orderAt α`. Together the two directions give a pointwise representation of the relation graph used by later minimality arguments. They neither construct a new comparison of names nor assert in the object language that this graph is a well-order.

```agda
    relL-rep : (a b : Mem (Lset α))
             → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
             → relOf (orderAt α oα) a b
    relL-rep = rel-rep α oα (relL α hα oα) (relL-spec α hα oα)
```

## Recap

At a constructible ordinal index `α`, the host type theory already has the strict well-order `orderAt α oα` on the members of `Lset α`. `Ordering` turns its comparison into a proposition-valued predicate by propositional truncation, and `Related` packages the related endpoint pairs as a host-defined class. Trichotomy allows `strict` to recover the comparison only at specified endpoints; `IsRel`, `relL-fill`, and `relL-rep` then express the exact pointwise correspondence between that comparison and membership in a realizing set.

The realizing set is obtained indirectly. An approximation records merely existing values below its domain, and membership induction proves that every recorded value realizes the class for its own argument without assuming functionality. Extensional uniqueness identifies competing realizers when the paired graph fiber is compared. `mereFunct` converts the resulting truncated unique existence into contractibility, replacement collects the indexed entries below `α`, and separation cuts the relation at `α` from a common containing set. The recursive bundle carries the completed lower table and the current relation together; the recursion does not require this bundle to be a proposition.

The construction remains relative to the two adequate forms of the object-language step supplied to `Described`. Later chapters provide the concrete description and discharge that parameter. Here `relL` is available only when `α` comes with both `isL` and `IsOrd` evidence. It represents the graph of the already constructed order; it neither completes a new comparison of names nor proves in the object language that the graph is a well-order.