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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

  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.

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

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.

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.

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.

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.

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.

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.

  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.

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

      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.

    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.

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

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.

    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.

    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.

  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.

  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 α).

  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.

  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.

  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.

  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.

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.

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.

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.

module Described
  (Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n))
  (Cond₀ : S → S → Formula S )
  (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.

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

              → (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.

  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.

  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.

      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.

    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.

    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.

  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.

  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.

    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.

      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.

        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.

          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.

  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.

      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.

        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.

    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.

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

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

      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.

        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.

        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.

      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.

  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.

  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.

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

  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.

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

    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.

      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.

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

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

        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.

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

    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.

  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.

    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.

    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.

    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.

      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.

    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.

            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.

  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.

      build : (φ : Formula S ) → φ ≡ 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.

        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.

        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.

        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.

        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.

        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.

        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.

        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.

          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.

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

        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.

        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.

          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.

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

        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.

        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.

        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.

        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.

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

          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.

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

        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.

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

        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.

        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.

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

  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.

  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.

  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.

    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.