Constructing order types inside L

A well-founded relation coded in L can be collapsed after its members are presented by a small type. Transitivity then makes every individual collapse value an ordinal and hence an element of L. This chapter collects those values into the exact range otL and separately collects the graph colTable; it does not package an ordinality theorem for otL. Only after trichotomy is added does the graph become a coded injection from the original domain into that range.

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

The classical assumption is explicit because one later existence proof must decide whether a candidate point precedes the point currently being treated. Well-founded recursion itself does not require this decision; excluded middle enters when a single replacement function is defined by the relation case and its complement.

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

Fix a universe level ℓ and an instance of excluded middle at the level needed by the constructible carrier. All later constructions in this module inherit this one classical parameter; it is not hidden as an axiom.

module L.GCH.OrderType {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The collapse will be recognized by formulas of the first-order language of sets. Ordered-pair membership and equality provide the atomic tests, while conjunction, disjunction, implication, negation, and the unbounded quantifiers express the table conditions. Apparent restrictions such as“for every predecessor”are written by placing the relation atom in an implication, rather than by using a bounded-quantifier constructor.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; ∈-irrefl )

Two representations must agree throughout the construction. Members of D are handled through a small presentation so that well-founded recursion is available, whereas graph entries remain sets encoded as ordered pairs in the cumulative hierarchy. Injectivity of the presentation and of ordered-pair coding lets later proofs return from these representations to the original members and coordinates.

open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )

The proof has to connect a recursively defined value with a formula that L can satisfy internally. Well-founded recursion produces the collapse, recursion graphs collect its values and pairs into sets, and the coding formulas interpret those pairs as applications. The stage theorem then places each ordinal collapse value inside L.

open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; appC; appC-adequate; prʟ; prʟ-fst; svAt; domAt )

There are two distinct goals for the collected graph. First it must represent the collapse as a total single-valued relation on D; only later, under trichotomy, may it satisfy the extra input-uniqueness clause of an internal injection. The ordered-pair formulas express the graph, and the injection code packages the four clauses only after each has been proved.

open import L.Coding.Expressions {ℓ} using ( module PairExpression )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj )
open import L.Mostowski {ℓ} using ( module Mostowski )

The later uniqueness argument repeatedly compares constructible sets by their members. Extensionality turns pointwise equivalence of membership into equality of the underlying sets, and proposition-valued evidence makes equality of the paired constructible objects proof-irrelevant. This is also what permits truncated case analyses to end in equalities without extracting permanent choices.

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ; isPropΣ; isSetΣSndProp )
open import Cubical.Functions.Logic using ( ⇔toPath )

The cumulative hierarchy supplies both the ambient sets and a small presentation of each set's members. Thus an element of D can be viewed either as an ambient set or as a small index, and membership transports the necessary constructibility evidence between the two views. The successor operation on hierarchy sets will later locate an ordinal collapse value at the stage following that ordinal.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; _∈ₛ_; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )

Well-foundedness supplies the induction principle that defines and analyzes the collapse. Empty types discharge impossible relation cases, while propositional truncation records existence when later arguments need only that a predecessor or table entry exists, not a chosen witness.

open import Cubical.Induction.WellFounded using ( WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

Write S for the carrier of the constructible structure. Its structure membership _∈ˢ_ expresses membership between elements of L; it is distinct from the small membership _∈ₛ_ used below to read the presentation of an ambient hierarchy set.

open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

Formulas will be interpreted in the structure carried by L. The notation S ^ n denotes an environment of n constructible sets, and γ ⊨ φ says that the formula φ is satisfied by such an environment γ inside the restricted constructible structure.

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

The underlying hierarchy carrier V ℓ is an h-set, and constructibility evidence is proposition-valued. Therefore the dependent-pair carrier S is also an h-set: equalities of constructible sets are propositions. This is what lets later truncated case analyses eliminate into equalities of carrier elements.

isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))

A coded graph is read on the underlying sets: F holds of x and y when the ordered pair of their underlying elements belongs to the underlying set of F. Every clause below reads this shape.

Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩

Fix a constructible set D and a constructible code R for ordered pairs. The hypothesis Rsub says only that the two endpoints of every pair occurring in R belong to D. Well-foundedness and transitivity are added later when the collapse is formed, and trichotomy is added still later to prove injectivity. No extensionality hypothesis on the relation is assumed anywhere in this chapter.

module Collapse (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

Membership in D is stated as a one-place predicate on the carrier.

  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst D ⟩

This predicate is a proposition, since it is membership in the underlying set of a presented set. Propositionhood here matters later: a construction may depend on a membership proof without thereby carrying choice data.

  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst D)

The members of D are presented by a small type, the index type of the presentation.

  Dom : Type ℓ
  Dom = ⟪ fst D ⟫

The presentation embeds its indices into the ambient hierarchy.

  ↪ : Dom → V ℓ
  ↪ = ⟪ fst D ⟫↪

An index is turned back into a constructible set: the embedded member is paired with a constructibility proof transported along the membership of D, using the transitivity of constructibility.

  up : Dom → S
  up m = ↪ m , isL-trans {x = fst D} {y = ↪ m} (member (fst D) m) (snd D)

The rebuilt constructible set is a member of D, by the presentation's own membership record.

  up-mem : (m : Dom) → Mem (up m)
  up-mem m = member (fst D) m

The presentation has no duplicate indices: equality of two embedded members forces equality of their indices. This will later identify the index recovered from the known member up b with b itself, so that the collected graph contains the expected pair (↪ b, col b). Injectivity of the collapse is a different result and will require trichotomy.

  Dom≡ : {a b : Dom} → ↪ a ≡ ↪ b → a ≡ b
  Dom≡ {a} {b} e = ↪-inj {a = fst D} {m = a} {n = b} e

Conversely, a member of D together with its membership proof recovers a presenting index, by taking the fiber of the presentation at that member.

  toDom : (x : S) → Mem x → Dom
  toDom x mx = fst (fiber (fst D) mx)

The recovered index presents exactly the given member: the fiber carries the identification of the embedded index with the member.

  toDom-val : (x : S) (mx : Mem x) → ↪ (toDom x mx) ≡ fst x
  toDom-val x mx = snd (fiber (fst D) mx)

The code R induces a relation on the small presentation: a ≺ b means that the ordered pair of the represented members ↪ a and ↪ b belongs to R. This is the relation on which well-founded recursion runs. The two lemmas below connect it in both directions with Holds R (up a) (up b) on constructible sets.

  opaque
    _≺_ : Dom → Dom → Type ℓ
    a ≺ b = ⟨ pr (↪ a) (↪ b) ∈ₛ fst R ⟩

For fixed indices a and b, the relation type a ≺ b is a proposition because it is a membership statement in a hierarchy set. Thus the relation records only whether the edge exists, not additional data carried by a particular proof. This propositionhood does not itself decide the edge; excluded middle is invoked later only where such a decision is needed.

    isProp≺ : (a b : Dom) → isProp (a ≺ b)
    isProp≺ a b = snd (pr (↪ a) (↪ b) ∈ₛ fst R)

Membership in the coded relation yields the small relation: the ordered pair recorded in L is recognized by the bridge between the two membership relations.

    ≺-in : (a b : Dom) → Holds R (up a) (up b) → a ≺ b
    ≺-in a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .fst

Conversely, the small relation records a genuine pair of R, so the two readings of the relation agree in both directions.

    ≺-out : (a b : Dom) → a ≺ b → Holds R (up a) (up b)
    ≺-out a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .snd

Well-foundedness of _≺_ supplies the recursion and induction by which col is defined. Transitivity has a different role: it lets predecessor chains remain below their upper endpoint, which is needed to prove that every collapse value is transitive and hence an ordinal. Neither assumption yet makes the collapse injective or the relation a well-order.

  module Col (wf : WellFounded _≺_)
             (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

The Mostowski construction now defines col p as the set of values col r for predecessors r ≺ p. Its computation rule col-eq identifies the recursive value with this explicit predecessor image. The membership lemmas give col r ∈ col p from a specified predecessor and, conversely, only a propositionally truncated predecessor from an arbitrary member; col-ord proves each individual col p is an ordinal.

    open Mostowski Dom _≺_ wf ≺-trans public
      using ( module W; col; col-eq; col-in; col-out; col-ord )

Every collapse value is constructible. The lemma col-ord first shows that col p is an ordinal; the stage lemma then places this ordinal in the stage indexed by its successor, yielding col-isL p.

    opaque
      col-isL : (p : Dom) → ⟨ isL (col p) ⟩
      col-isL p = Lset→isL (sucV (col p)) (suc-ord (col-ord p)) (col p)
                    (ord∈Lset-suc (col p) (col-ord p))

Each collapse value is packaged with its constructibility proof into a constructible set. The collapse thus produces not merely ambient sets but actual elements of the constructible universe.

    colʟ : Dom → S
    colʟ p = col p , col-isL p

The formulas

A table F is complete at x when every R-predecessor y of x has some recorded value u. The existence of u is propositionally truncated: completeness remembers that an entry exists but does not choose one, and it does not yet assert that the value is unique.

Complete : S → S → S → Type (ℓ-suc ℓ)
Complete F R x = (y : S) → Holds R y x → ∥ Σ[ u ∈ S ] Holds F y u ∥₁

The predicate Src F R x w says that w occurs as a value recorded by F at some R-predecessor of x. Both the predecessor and its table entry remain under propositional truncation, since later reasoning uses only the resulting membership fact.

Src : S → S → S → S → Type (ℓ-suc ℓ)
Src F R x w = ∥ Σ[ y ∈ S ] (Holds R y x × Holds F y w) ∥₁

A value v is correct for x when its members are exactly the source values: membership in v yields a source, and every source is a member. The two directions together say that v is the set of recorded predecessor values, read purely through membership.

ValueIs : S → S → S → S → Type (ℓ-suc ℓ)
ValueIs F R x v = (w : S) → (⟨ fst w ∈ fst v ⟩ → Src F R x w)
                          × (Src F R x w → ⟨ fst w ∈ fst v ⟩)

A table is correct when each pair it actually contains is complete at its input and has exactly the predecessor values as its output. This condition does not specify a domain, so it neither requires entries for all of D nor forbids entries outside D. The later uniqueness theorem identifies a recorded value with the collapse only when the recorded input is a member of D.

Correct : S → S → Type (ℓ-suc ℓ)
Correct F R = (x v : S) → Holds F x v → Complete F R x × ValueIs F R x v

The formula completeAt f R x uses an unbounded universal quantifier for a candidate predecessor y. The implication restricts attention to those y for which R records the pair (y,x), and its conclusion uses an unbounded existential quantifier for a value u such that F records (y,u). Under the existential binder, u occupies the new zeroth slot and the earlier variables are shifted.

opaque
  completeAt : ∀ {n} → Fin n → S → Fin n → Formula S n
  completeAt f R x =
    ∀̇ ( appC R zero (suc x)
      ⇒̇ ∃̇ (appAt (suc (suc f)) (suc zero) zero) )

To read the formula as host-level completeness, fix a predecessor y and a proof that R records (y,x). The adequacy path for appC converts this premise into the antecedent expected by the satisfaction proof h. Applying h yields a propositionally truncated candidate value; PT.map keeps the truncation and converts its graph atom into Holds F y u using the adequacy path for appAt.

  complete-out : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ completeAt f R x ⟩
               → Complete (lookup f γ) R (lookup x γ)
  complete-out f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ)) q })

The final application in this direction performs the first of those conversions: it transports the given relation fact along appC-adequate and supplies it to h y. The result is still the truncated existential produced by the object-language semantics; the mapping in the preceding lines changes only the contents of that truncation.

    (h y (subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p))

Conversely, assume host-level completeness. For a candidate predecessor satisfying the formula's antecedent, appC-adequate first turns that antecedent into Holds R y x. Completeness supplies a propositionally truncated value u, and PT.map transports the accompanying fact Holds F y u back into satisfaction of the application atom required by the existential conclusion.

  complete-in : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
              → Complete (lookup f γ) R (lookup x γ)
              → ⟨ γ ⊨ completeAt f R x ⟩
  complete-in f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ))) q })

This line converts the satisfied relation atom into Holds R y x and applies completeness at x to the candidate predecessor y. That application supplies the truncated value which the surrounding map turns into the object-language existential witness.

    (h y (subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p))

The formula srcAt f R x w uses an unbounded existential quantifier to say that some y is both an R-predecessor of x and an input at which F records w. The restriction to predecessors is expressed by the first conjunct, rather than by a bounded existential quantifier.

opaque
  srcAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  srcAt f R x w = ∃̇ ( appC R zero (suc x) ∧̇ appAt (suc f) zero (suc w) )

The semantic existential is already propositionally truncated. The map defining src-out preserves that truncation and converts each hypothetical witness y: appC-adequate reads the first conjunct as Holds R y x, while appAt-adequate reads the second as Holds F y w.

  src-out : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
          → ⟨ γ ⊨ srcAt f R x w ⟩
          → Src (lookup f γ) R (lookup x γ) (lookup w γ)
  src-out f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p

The graph membership of the predecessor closes the reading.

      , subst ⟨_⟩ (appAt-adequate (suc f) zero (suc w) (y ∷ γ)) q ) })

Filling a source is the converse: the predecessor is introduced into the existential with both atoms transported against their adequacy lemmas.

  src-in : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
         → Src (lookup f γ) R (lookup x γ) (lookup w γ)
         → ⟨ γ ⊨ srcAt f R x w ⟩
  src-in f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p

The graph atom is written last, completing the fill.

      , subst ⟨_⟩ (sym (appAt-adequate (suc f) zero (suc w) (y ∷ γ))) q ) })

The formula valueAt f R x v quantifies over an arbitrary set w and states both implications between w ∈ v and srcAt f R x w. Thus it expresses the extensional characterization of v: its members are exactly the values recorded at predecessors of x. The definition unfolds srcAt so that this characterization is presented as one first-order formula.

opaque
  unfolding srcAt
  valueAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  valueAt f R x v =
    ∀̇ ( ((var zero ∈̇ var (suc v)) ⇒̇ srcAt (suc f) R (suc x) zero)

The biconditional is the conjunction of its two directions, with the source formula unfolded inside both.

      ∧̇ (srcAt (suc f) R (suc x) zero ⇒̇ (var zero ∈̇ var (suc v))) )

Reading valueAt outward instantiates its universal quantifier at each w. The forward implication first turns membership in v into satisfaction of the source formula, and src-out then reads that satisfaction as Src F R x w, giving the forward half of ValueIs.

  value-out : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
            → ⟨ γ ⊨ valueAt f R x v ⟩
            → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
  value-out f R x v γ h w =
      (λ w∈ → src-out (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))

The backward direction is read symmetrically, through the source filling. Thus the formula says exactly that v collects the source values, which is the reading the later uniqueness argument consumes.

    , (λ s → h w .snd (src-in (suc f) R (suc x) zero (w ∷ γ) s))

To prove the forward implication of valueAt, take a member w of the proposed value v. The host-level value equation says, merely, that w already occurs as the value of some R-predecessor of x. Reading that source statement inward supplies the existential witness required by the object-language formula in the environment extended by w.

  value-in : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
           → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
           → ⟨ γ ⊨ valueAt f R x v ⟩
  value-in f R x v γ h w =
      (λ w∈ → src-in (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))

For the converse implication, a satisfaction proof of the source formula is first read as the mere existence of a predecessor whose table value is w. The reverse half of ValueIs then places w in the recorded value. Thus valueAt expresses exactly the recursive value equation relative to the candidate table; identifying that value with the Mostowski collapse will require well-founded induction later.

    , (λ s → h w .snd (src-out (suc f) R (suc x) zero (w ∷ γ) s))

Correctness is tested only where the candidate table actually has an entry. The two universal quantifiers range over an argument x and a value v; if the table contains the ordered pair (x,v), the formula requires the two conditions that make this entry a valid recursive step.

opaque
  unfolding completeAt valueAt
  correctAt : ∀ {n} → Fin n → S → Formula S n
  correctAt f R =
    ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero

Those two conditions separate existence from the value equation. Completeness says that every R-predecessor of x has some entry in the table, while the value clause says that the members of v are exactly the values appearing at those predecessor entries. The formula imposes no domain condition beyond entries already present in the table.

          ⇒̇ ( completeAt (suc (suc f)) R (suc zero)
            ∧̇ valueAt (suc (suc f)) R (suc zero) zero ) ))

To read the formula outward, begin with an actual table entry (x,v). Adequacy of appAt turns its membership proof into the antecedent required by the formula. Instantiating the two quantifiers at x and v then yields completeness at x and the corresponding value equation; this line reads the completeness half back into the host-level predicate.

  correct-out : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
              → ⟨ γ ⊨ correctAt f R ⟩ → Correct (lookup f γ) R
  correct-out f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ))) p)
    in complete-out (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c

The second component is read by value-out, giving the equivalence between membership in v and occurrence as a value at an R-predecessor of x. Paired with completeness, this proves the host-level correctness of the chosen entry. Since the construction works for every entry of the table, it proves Correct F R.

     , value-out (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w

Conversely, suppose the table is correct at the host level. After choosing an argument x, a value v, and an entry (x,v), adequacy of appAt turns the antecedent of the object-language implication into the corresponding host-level entry. Correctness then supplies completeness and the value equation for that entry; this line inserts the completeness half into the formula.

  correct-in : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
             → Correct (lookup f γ) R → ⟨ γ ⊨ correctAt f R ⟩
  correct-in f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ)) p)
    in complete-in (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c

The value equation is inserted by value-in, completing the conjunction required for the entry (x,v). Abstracting over the two chosen elements gives the two universal quantifiers. Thus correct-in and correct-out establish the exact correspondence between correctAt and the host-level predicate Correct.

     , value-in (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w

The next formula fixes the relation R but leaves the witnessing table existentially bound. This separation is mathematically useful: a value can be recognized locally by some correct table before a single table over the whole domain has been constructed.

module ColFo (R : S) where

At an environment (z ∷ p ∷ []), the formula says that there merely exists a set F which is correct for R and contains the entry (p,z). The table is bound existentially, so this is a local characterization of the value at p; it does not yet assert that one fixed table works simultaneously over the whole domain.

  opaque
    unfolding correctAt
    colFo : Formula S 
    colFo = ∃̇ ( correctAt zero R
              ∧̇ appAt zero (suc (suc zero)) (suc zero) )

Reading colFo outward preserves the propositional truncation around its table witness. The existential supplies a table F; inside the same truncation, the conjunction supplies a proof that F is correct for R and the object-language application atom for the entry (p,z).

    colFo-out : (z p : S) → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
              → ∥ Σ[ F ∈ S ] (Correct F R × Holds F p z) ∥₁
    colFo-out z p = PT.map (λ { (F , (hc , ha)) → F
      , ( correct-out zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero)

Adequacy of appAt converts the remaining application atom into Holds F p z. The result is therefore merely a correct table together with the required entry, exactly the host-level reading of the formula.

            (F ∷ z ∷ p ∷ [])) ha ) })

For the inward direction, an explicitly given correct table F containing (p,z) serves as the existential witness. The correctness proof is translated by correct-in; the remaining task is to express the given table entry by the application atom.

    colFo-in : (z p F : S) → Correct F R → Holds F p z
             → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
    colFo-in z p F hc hp = ∣ F
      , ( correct-in zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero)

Adequacy of appAt, used in the reverse direction, turns Holds F p z into satisfaction of that atom. The table witness, its correctness, and this entry are then enclosed by the existential truncation, proving colFo at (z,p).

            (F ∷ z ∷ p ∷ []))) hp ) ∣₁

A pointwise value formula such as colFo must later be used to define a set of ordered pairs. The generic PairFo construction makes that passage: it recognizes a pair (p,z) precisely when z satisfies the chosen formula at p. This lets the local collapse formula serve as the value relation for the recursion constructed below.

open import L.Recursion.Graph {ℓ} lem public using ( module PairFo )

Uniqueness, existence, and the tables

The internal construction starts with a coded domain D and a coded relation R. Its only initial side condition is that every pair belonging to R has both coordinates in D. Well-foundedness and transitivity are absent from this module boundary and will be supplied separately when the collapse argument begins.

module Internal (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

The domain representation and its coded relation now provide the common setting for two formula constructions. CF is the local collapse-value formula for R, and PF recognizes the ordered pair formed from an argument and a value satisfying that formula. Neither construction at this point asserts existence or uniqueness of collapse values.

  open Collapse D R Rsub public
  module CF = ColFo R using ( colFo; colFo-in; colFo-out )
  module PF = PairFo CF.colFo using ( pair-in; pair-out; pairFo )

If q is a member of D, decoding its membership proof gives an index toDom q mq. Re-embedding that index has the same underlying iterative set as q by toDom-val; since the constructibility component of S is proposition-valued, equality of the underlying sets upgrades to equality in S.

  up-toDom : (q : S) (mq : Mem q) → up (toDom q mq) ≡ q
  up-toDom q mq = Σ≡Prop (λ v → snd (isL v)) (toDom-val q mq)

The collapse formula depends on its argument through the second environment slot. Hence an equality x ≡ y permits direct substitution in that slot: any value v satisfying the formula at x also satisfies it at y. This is what later reconciles the canonical representative up (toDom q mq) with the original element q.

  colFo-at : (v : S) {x y : S} → x ≡ y
           → ⟨ (v ∷ x ∷ []) ⊨ CF.colFo ⟩ → ⟨ (v ∷ y ∷ []) ⊨ CF.colFo ⟩
  colFo-at v e = subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ CF.colFo ⟩) e

The module now assumes that the small relation is well-founded and transitive. Well-foundedness supports the recursive definition of col and the inductions used for uniqueness; transitivity is used to show that the resulting collapse values are ordinals. These assumptions play different roles and neither follows from the earlier endpoint condition on R.

  module Graph (wf : WellFounded _≺_)
               (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

With these two hypotheses, the Mostowski recursion assigns to each a the set col a of collapse values of its predecessors. Its introduction and elimination lemmas characterize membership in that set, and col-ord proves that each individual col a is an ordinal. This statement concerns the pointwise collapse values, not yet the set otL collected later.

    open Col wf ≺-trans public

Well-foundedness rules out a loop a ≺ a. In the induction step, such a loop lets the induction hypothesis for predecessors be applied to a itself, with the same loop serving both as the evidence that a is smaller and as the contradiction-producing hypothesis.

    ≺-irrefl : (a : Dom) → a ≺ a → Empty.⊥
    ≺-irrefl = W.induction {P = λ a → a ≺ a → Empty.⊥} (λ a rec h → rec a h h)

The uniqueness statement is conditional on an entry being present: if a correct table F records v at the genuine domain point up a, then the underlying set of v equals col a. It does not claim that every correct table contains an entry at every member of D. The proof proceeds by well-founded induction on a, with the displayed equality as its motive.

    correct-val : (F : S) → Correct F R → (a : Dom) (v : S)
                → Holds F (up a) v → fst v ≡ col a
    correct-val F hc = W.induction {P = λ a → (v : S) → Holds F (up a) v → fst v ≡ col a} go
      where
      go : (a : Dom) → ((b : Dom) → b ≺ a → (v : S) → Holds F (up b) v → fst v ≡ col b)

The proof reduces to a pointwise equivalence: w belongs to the recorded value if and only if w belongs to the collapse. Two helper facts are extracted from the correctness hypothesis: completeness at up a, and the value clause.

         → (v : S) → Holds F (up a) v → fst v ≡ col a
      go a IH v hv = extensionalV {a = fst v} {b = col a} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        cmp : Complete F R (up a)
        cmp = hc (up a) v hv .fst

The correctness of the entry at a has two complementary consequences. The preceding cmp supplies table entries for all predecessors, while val identifies membership in v with occurrence as a predecessor value. The two directions of the coming extensionality argument use these consequences in opposite orders.

        val : ValueIs F R (up a) v
        val = hc (up a) v hv .snd

For the first inclusion, let w be a member of the recorded value v. Since v is constructible, membership makes w constructible as well, so it can be packaged as the carrier element wS. The forward half of val then gives, under propositional truncation, an R-predecessor y of a at which the table records wS.

        fwd : (w : V ℓ) → ⟨ w ∈ fst v ⟩ → ⟨ w ∈ col a ⟩
        fwd w w∈ = PT.rec (snd (w ∈ col a)) read (val wS .fst w∈)
          where
          wS : S
          wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)

The source entry is converted into the two facts needed: the relation between the carried predecessor and the argument, and the table entry at the carried predecessor. The predecessor is then decoded to its internal index.

          read : Σ[ y ∈ S ] (Holds R y (up a) × Holds F y wS) → ⟨ w ∈ col a ⟩
          read (y , (ry , fy)) = subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b b≺a)
            where
            my : Mem y
            my = Rsub y (up a) ry .fst

The internal index b is recovered by descending along the membership, and the relation entry is transported to the internal form b ≺ a. The equation e records the identification of w with the collapse of b, to be proved next.

            b : Dom
            b = toDom y my
            b≺a : b ≺ a
            b≺a = ≺-in b a (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val y my)) ry)
            e : w ≡ col b

The equation is exactly the induction hypothesis applied to the decoded predecessor: the table's value at the carried predecessor equals the collapse of its internal index, which by transport equals w.

            e = IH b b≺a wS (subst (λ t → ⟨ pr t w ∈ fst F ⟩) (sym (toDom-val y my)) fy)

For the reverse inclusion, suppose w ∈ col a. The elimination rule for the collapse says, under propositional truncation, that col r ≡ w for some predecessor r ≺ a. Because the goal w ∈ fst v is a proposition, the proof may reason inside that truncation. The carried element wS is constructible because it belongs to the constructible set col a.

        bwd : (w : V ℓ) → ⟨ w ∈ col a ⟩ → ⟨ w ∈ fst v ⟩
        bwd w w∈ = PT.rec (snd (w ∈ fst v)) read (col-out a w w∈)
          where
          wS : S
          wS = w , isL-trans {x = col a} {y = w} w∈ (col-isL a)

For the predecessor r supplied by col-out, completeness of the entry at a gives merely some table value u at up r. The inner elimination is legitimate because membership of w in v is a proposition. It remains to use correctness at r to compare u with col r, and hence with w.

          read : Σ[ r ∈ Dom ] ((r ≺ a) × (col r ≡ w)) → ⟨ w ∈ fst v ⟩
          read (r , (ra , e)) = PT.rec (snd (w ∈ fst v)) inner (cmp (up r) (≺-out r a ra))
            where
            inner : Σ[ u ∈ S ] Holds F (up r) u → ⟨ w ∈ fst v ⟩
            inner (u , fu) = val wS .snd

The reverse half of the value equation turns a source witness into membership in v. Here that witness uses the predecessor up r, its relation to up a, and the table entry with value u; the induction hypothesis identifies u with col r, and the equation col r ≡ w transports the entry so that its value is w.

              ∣ up r , (≺-out r a ra , subst (λ t → ⟨ pr (↪ r) t ∈ fst F ⟩) (IH r ra u fu ∙ e) fu) ∣₁

Now suppose q is genuinely a member of D and v satisfies the local collapse formula at q. The formula supplies only a propositionally truncated correct table containing (q,v), but the desired set equality is a proposition, so the truncation can be eliminated. After transporting the entry from q to its decoded representative, correct-val identifies fst v with col (toDom q mq).

    colFo-val : (q : S) (mq : Mem q) (v : S) → ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩
              → fst v ≡ col (toDom q mq)
    colFo-val q mq v h = PT.rec (setIsSet (fst v) (col (toDom q mq)))
      (λ { (F , (hc , hv)) → correct-val F hc (toDom q mq) v
             (subst (λ t → ⟨ pr t (fst v) ∈ fst F ⟩) (sym (toDom-val q mq)) hv) })

The outward reading of the collapse formula supplies the correct table and the table entry, which are the two inputs of the uniqueness lemma.

      (CF.colFo-out v q h)

The local-table module is parameterized by an argument a of the domain and the induction hypothesis providing the collapse formula at every smaller argument. It will build, for a, a table whose entries at real predecessors record the collapse values and whose other entries record a default pair.

    module Approx (a : Dom)
                  (IH : (b : Dom) → b ≺ a → ⟨ (colʟ b ∷ up b ∷ []) ⊨ CF.colFo ⟩) where

The default entry ea is the ordered pair of the carried argument with its own collapse, presented as a carrier element.

      ea : S
      ea = prʟ (up a) (colʟ a)

The body of the local formula has two disjuncts. The left disjunct says that q is a real predecessor of a and that z pairs q with a value satisfying the collapse formula. The right disjunct says that q is not a predecessor and z is the default entry. This case split is decided by excluded middle.

      Body : S → S → Type (ℓ-suc ℓ)
      Body z q =
          (Holds R q (up a)
             × ∥ Σ[ v ∈ S ] ((fst z ≡ pr (fst q) (fst v)) × ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩) ∥₁)
        ⊎ ((Holds R q (up a) → Empty.⊥) × (fst z ≡ fst ea))

To distinguish the predecessor and default cases inside the object language, the relation test must mention the ordered pair formed from the varying argument q and the fixed point a. Pair expressions provide this term uniformly in the two free slots used by the local formula.

      module PE = PairExpression

The expression image denotes the pair (q,up a): its first coordinate comes from the argument slot and its second is the literal carrier element representing a. Consequently, membership of image in R says exactly that q is an R-predecessor of a; it does not describe an entry of the local table.

      image : PE.Expr 
      image = PE.pair (PE.slot (suc zero)) (PE.literal (up a))

The formula ψ mirrors the two cases of Body. If q R a, the first branch requires the output z to pair q with some value satisfying colFo at q. If q is not a predecessor of a, the second branch requires z to equal the fixed default entry ea. The classical decision choosing between these branches is used later in the functionality proof, not built into the disjunction itself.

      opaque
        ψ : Formula S 
        ψ = (PE.member image (con R) ∧̇ PF.pairFo)
          ∨̇ ((¬̇ PE.member image (con R)) ∧̇ (var zero ≐ con ea))

Reading ψ outward preserves the truncation of its disjunction. In the predecessor branch, the pair-expression reader turns the first conjunct into q R a, while PF.pair-out says merely that z is (q,v) for some v satisfying colFo at q. In the default branch, the object-language negation must instead be converted into a host-level refutation of q R a.

        ψ-out : (z q : S) → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩ → ∥ Body z q ∥₁
        ψ-out z q = PT.map
          (λ { (inl (h1 , h2)) → inl (PE.member-out image (con R) (z ∷ q ∷ []) h1
                                         , PF.pair-out z q h2)
             ; (inr (h1 , h2)) → inr

To obtain that host-level refutation, assume q R a. The inward reading of the pair expression turns this assumption into satisfaction of the membership atom, which the object-language negation rules out. The equality identifying z with the default entry already has the required host-level form and is retained unchanged.

                 ((λ k → lower (h1 (PE.member-in image (con R) (z ∷ q ∷ []) k))) , h2) })

The inward reading injects the left branch through the pair-expression introduction and the pair-graph introduction, eliminating the truncated value into the proposition-valued satisfaction.

        ψ-in : (z q : S) → Body z q → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
        ψ-in z q (inl (h1 , hv)) = PT.rec (snd ((z ∷ q ∷ []) ⊨ ψ))
          (λ { (v , (e , hc)) → ∣ inl (PE.member-in image (con R) (z ∷ q ∷ []) h1
                                     , PF.pair-in z q v e hc) ∣₁ }) hv
        ψ-in z q (inr (h1 , e)) =

The right branch lifts the host-side refutation into the object language and carries the default equation. Both branches are injected into the truncated disjunction of the formula.

          ∣ inr ((λ k → lift (h1 (PE.member-out image (con R) (z ∷ q ∷ []) k))) , e) ∣₁

The helper b≺a-of decodes the host-side relation membership into the internal comparison: if q relates to a, then the internal index of q is below a. The decoding is by descending along the membership to recover the index.

      private
        b≺a-of : (q : S) (mq : Mem q) → Holds R q (up a) → toDom q mq ≺ a
        b≺a-of q mq h = ≺-in (toDom q mq) a
          (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val q mq)) h)

The induction hypothesis is stated at the canonical representative up (toDom q mq), whereas the local formula must be satisfied at the original carrier element q. The round-trip equality identifies these two presentations, and colFo-at transports the satisfaction proof from the canonical representative to q.

        IHq : (q : S) (mq : Mem q) → toDom q mq ≺ a
            → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
        IHq q mq k = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (IH (toDom q mq) k)

Replacement requires the values satisfying ψ at each q ∈ D to form a contractible fiber. The proof asks excluded middle whether q R a. In either case it will produce, under propositional truncation, a canonical satisfying output and a proof that every other satisfying output equals it; mereFunct converts this merely unique existence into contractibility.

        fc : (q : S) → ⟨ q ∈ˢ D ⟩ → isContr (Σ[ z ∈ S ] ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩)
        fc q mq = mereFunct ψ q (decide (lem (pr (fst q) (↪ a) ∈ fst R)))
          where
          b : Dom
          b = toDom q mq

In the predecessor branch, the canonical output is zb = prʟ q (colʟ b), whose underlying set codes (q,col b); here b is the internal index decoded from q. The non-predecessor branch instead uses the default output ea. The local decision lemma will show, under propositional truncation, that whichever branch applies has one satisfying output and that every other satisfying output equals it.

          zb : S
          zb = prʟ q (colʟ b)
          decide : Holds R q (up a) ⊎ (Holds R q (up a) → Empty.⊥)
                 → ∥ Σ[ z ∈ S ] (⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
                                × ((z' : S) → ⟨ (z' ∷ q ∷ []) ⊨ ψ ⟩ → z' ≡ z)) ∥₁

Assume q R a. The canonical output zb satisfies the left branch because the induction hypothesis supplies colFo for col b at q, while prʟ-fst supplies the required equality between fst zb and the ordered-pair code pr (fst q) (col b). To prove uniqueness, an arbitrary satisfying output is read through the same two cases: a left-branch witness will be determined by colFo-val, while a right-branch witness contradicts the standing assumption q R a.

          decide (inl h) = ∣ zb
            , ( ψ-in zb q (inl (h , ∣ colʟ b , (prʟ-fst q (colʟ b) , IHq q mq (b≺a-of q mq h)) ∣₁))
              , λ z' hz' → PT.rec (isSetS z' zb)
                  (λ { (inl (_ , hv)) → PT.rec (isSetS z' zb)
                         (λ { (v , (e , hcol)) → Σ≡Prop (λ w → snd (isL w))

For a competing witness in the left branch, colFo-val identifies its second coordinate with col b; combining this with its pair equation proves that the whole output is zb. A competing right-branch witness is impossible because it contains a refutation of q R a. This finishes uniqueness in the predecessor case. The final line then opens the separate non-predecessor case by choosing the default output ea; its uniqueness proof continues in the next block.

                                (e ∙ cong (pr (fst q)) (colFo-val q mq v hcol) ∙ sym (prʟ-fst q (colʟ b))) })
                         hv
                     ; (inr (nh , _)) → Empty.rec (nh h) })
                  (ψ-out z' q hz') ) ∣₁
          decide (inr nh) = ∣ ea

The refuted-membership case closes the uniqueness argument. The default entry ea satisfies ψ. Reading any competing witness outward either produces a positive membership, contradicting nh, or gives the default-branch equality fst z' ≡ fst ea. In the latter case, propositionality of constructibility lifts this equality of underlying sets to the required equality z' ≡ ea in S.

            , ( ψ-in ea q (inr (nh , refl))
              , λ z' hz' → PT.rec (isSetS z' ea)
                  (λ { (inl (h , _)) → Empty.rec (nh h)
                     ; (inr (_ , e)) → Σ≡Prop (λ w → snd (isL w)) e })
                  (ψ-out z' q hz') ) ∣₁

The local recursion ranges over every q ∈ D. If q R up a, its unique value is the ordered pair of q with the collapse at the index presented by q; otherwise its value is the single default entry ea. Replacement applied to ψ and this uniqueness proof collects the resulting values into one constructible set.

        module T = Of (record { dom = D ; graph = ψ ; funct = fc }) using ( table; table-in; table-out )

Fa names this replacement range. The following membership lemmas show that its elements are exactly the pairs pr(↪ b,col b) with b ≺ a, together with the top pair pr(↪ a,col a) contributed by the default branch.

      Fa : S
      Fa = T.table

Below b states that the index b is at or below the current one: either strictly below, or equal. This two-case predicate drives both the introduction and the correctness of the local table.

      Below : Dom → Type ℓ
      Below b = (b ≺ a) ⊎ (b ≡ a)

For b at or below a, Fa-in inserts the graph entry with input up b and value colʟ b. A strict comparison uses the induction hypothesis to satisfy the first disjunct of ψ; an equality b ≡ a uses the default branch after identifying this pair with ea.

      Fa-in : (b : Dom) → Below b → Holds Fa (up b) (colʟ b)
      Fa-in b k = subst (λ w → ⟨ w ∈ fst Fa ⟩) (prʟ-fst (up b) (colʟ b))
        (T.table-in (up b) (prʟ (up b) (colʟ b)) (up-mem b) (ψ-in _ (up b) (bodyOf k)))
        where
        bodyOf : Below b → Body (prʟ (up b) (colʟ b)) (up b)

In the strict case, the body contains the relation witness b ≺ a and the induction hypothesis saying that colʟ b satisfies the collapse formula at up b. In the equality case, irreflexivity rules out up b R up a, while transport along b ≡ a identifies the proposed pair with the default pair.

        bodyOf (inl k) = inl (≺-out b a k , ∣ colʟ b , (prʟ-fst (up b) (colʟ b) , IH b k) ∣₁)
        bodyOf (inr e) = inr
          ( (λ h → ≺-irrefl a (≺-in a a (subst (λ t → Holds R (up t) (up a)) e h)))
          , prʟ-fst (up b) (colʟ b) ∙ cong (λ t → pr (↪ t) (col t)) e ∙ sym (prʟ-fst (up a) (colʟ a)) )

Conversely, membership in Fa merely yields an index b with b ≺ a or b ≡ a, together with an equality identifying the member with pr(↪ b,col b). The index remains under propositional truncation, so this result does not choose a representative.

      Fa-out : (y : S) → ⟨ y ∈ˢ Fa ⟩
             → ∥ Σ[ b ∈ Dom ] (Below b × (fst y ≡ pr (↪ b) (col b))) ∥₁
      Fa-out y hy = PT.rec squash₁
        (λ { (q , (mq , hψ)) → PT.rec squash₁
          (λ { (inl (h , hv)) → PT.map

In the predecessor branch, colFo-val identifies the value supplied by the formula with the collapse at toDom q mq; the presentation equation for q then rewrites the pair into canonical form. In the default branch, the recorded pair is the one indexed by a itself.

                 (λ { (v , (e , hcol)) → toDom q mq
                    , (inl (b≺a-of q mq h)
                      , e ∙ cong₂ pr (sym (toDom-val q mq)) (colFo-val q mq v hcol)) })
                 hv
             ; (inr (_ , e)) → ∣ a , (inr refl , e ∙ prʟ-fst (up a) (colʟ a)) ∣₁ })

Both the replacement reader and ψ-out return truncated witnesses. Since the desired conclusion is itself propositionally truncated, the proof may eliminate the outer truncation, then the inner one, without selecting either witness globally.

          (ψ-out y q hψ) })
        (T.table-out y hy)

Specializing the preceding result to the ordered-pair code of x and v recovers its two coordinates. Thus a graph entry Holds Fa x v merely determines an index b ≤ a for which fst x ≡ ↪ b and fst v ≡ col b.

      Fa-pair : (x v : S) → Holds Fa x v
              → ∥ Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v)) ∥₁
      Fa-pair x v h = PT.map step
        (Fa-out (prʟ x v) (subst (λ w → ⟨ w ∈ fst Fa ⟩) (sym (prʟ-fst x v)) h))
        where

The transport re-points the equation at the internal pair, and the helper splits it through the injectivity of the ordered pair into the naming equation of the index and that of the collapse value.

        step : Σ[ b ∈ Dom ] (Below b × (fst (prʟ x v) ≡ pr (↪ b) (col b)))
             → Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
        step (b , (k , e)) = b , (k , sym (fst q) , sym (snd q))
          where
          q : (fst x ≡ ↪ b) × (fst v ≡ col b)

Applying pr-inj to the composite pair equality yields fst x ≡ ↪ b and fst v ≡ col b. The result expected by Fa-pair has the canonical coordinates first, so step reverses both component equalities before returning them.

          q = pr-inj (sym (prʟ-fst x v) ∙ e)

If c ≺ b and b ≺ a, transitivity gives c ≺ a. If instead b ≡ a, substituting this equality into c ≺ b gives the same conclusion. These are exactly the two cases of Below b.

      below-trans : {c b : Dom} → c ≺ b → Below b → c ≺ a
      below-trans cb (inl k) = ≺-trans cb k
      below-trans {c} cb (inr e) = subst (c ≺_) e cb

To prove Correct Fa R, fix an actual entry (x,v) of Fa. The paired reader gives only a truncated index representing this entry, but both Complete Fa R x and ValueIs Fa R x v are propositions. Their conjunction is therefore a valid target for eliminating that truncation.

      Fa-correct : Correct Fa R
      Fa-correct x v hxv = PT.rec
        (isProp× (isPropΠ (λ _ → isPropΠ (λ _ → squash₁)))
                 (isPropΠ (λ w → isProp× (isPropΠ (λ _ → squash₁))
                                          (isPropΠ (λ _ → snd (fst w ∈ fst v))))))

Suppose the chosen entry is represented by b ≤ a, so that x presents b and v has underlying set col b. Completeness must give every R-predecessor of x a value in Fa; the value condition must prove, for each w, that w ∈ v exactly when some such predecessor is paired with w in Fa.

        build (Fa-pair x v hxv)
        where
        build : Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
              → Complete Fa R x × ValueIs Fa R x v
        build (b , (k , ex , ev)) = cmp , (λ w → fwd w , bwd w)

The central conversion takes a coded predecessor y R x to a strict comparison in Dom. The entry representation identifies fst x with the represented member ↪ b, rather than identifying the carrier element x with the external index b. After Rsub places y in D, toDom recovers the index that can be compared with b.

          where

From y R x, the containment hypothesis supplies y ∈ D, so toDom y my defines an index c. Transporting the relation witness along the presentation equations for y and x proves c ≺ b; the second coordinate records that ↪ c is the underlying set of y.

          pred : (y : S) → Holds R y x → Σ[ c ∈ Dom ] ((c ≺ b) × (↪ c ≡ fst y))
          pred y hy = c , (≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩)
                              (sym (toDom-val y my)) (sym ex) hy) , toDom-val y my)
            where
            my : Mem y

The proof my is precisely the first endpoint membership supplied by Rsub; it is the evidence needed to form toDom y my. Since membership in D is a proposition, using this evidence does not add a choice of presentation.

            my = Rsub y x hy .fst
            c : Dom
            c = toDom y my

For a predecessor y R x, let c be the index just recovered. The witness for completeness is the value colʟ c; Fa-in supplies the canonical entry at up c, and transport along ↪ c ≡ fst y turns it into the required entry at y. Transitivity through b ≤ a ensures that c lies below a.

          cmp : Complete Fa R x
          cmp y hy = ∣ colʟ c , subst (λ t → ⟨ pr t (col c) ∈ fst Fa ⟩) ec
                                 (Fa-in c (inl (below-trans cb k))) ∣₁
            where
            c = pred y hy .fst

The two projections of pred y hy are now named cb and ec: cb is the strict comparison c ≺ b, while ec identifies the canonical representative ↪ c with the actual input y. They provide, respectively, the bound needed by Fa-in and the transport to y.

            cb = pred y hy .snd .fst
            ec = pred y hy .snd .snd

For the forward half of ValueIs, rewrite w ∈ v as fst w ∈ col b. The outward collapse lemma merely gives r ≺ b and col r ≡ fst w; these data produce an R-edge from up r to x and a table entry pairing up r with w.

          fwd : (w : S) → ⟨ fst w ∈ fst v ⟩ → Src Fa R x w
          fwd w w∈ = PT.map read (col-out b (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) (sym ev) w∈))
            where
            read : Σ[ r ∈ Dom ] ((r ≺ b) × (col r ≡ fst w)) → Σ[ y ∈ S ] (Holds R y x × Holds Fa y w)
            read (r , (rb , er)) = up r

The two memberships are transported along the equation of the index and the strict comparison, placing both the relation and the table membership at the named predecessor.

              , ( subst (λ t → ⟨ pr (↪ r) t ∈ fst R ⟩) ex (≺-out r b rb)
                , subst (λ t → ⟨ pr (↪ r) t ∈ fst Fa ⟩) er (Fa-in r (inl (below-trans rb k))) )

For the reverse half, a witness of Src Fa R x w merely supplies some y with y R x and a table entry from y to w. The target fst w ∈ fst v is a proposition, so the truncated source witness and then the truncated table reading may both be eliminated into it.

          bwd : (w : S) → Src Fa R x w → ⟨ fst w ∈ fst v ⟩
          bwd w = PT.rec (snd (fst w ∈ fst v)) (λ { (y , (hy , fy)) →
            PT.rec (snd (fst w ∈ fst v)) (read y hy) (Fa-pair y w fy) })
            where
            read : (y : S) → Holds R y x

Reading the table entry gives an index c, an equation identifying y with ↪ c, and an equation identifying w with col c. Combining the first equation with y R x and the representation of x by b yields c ≺ b; hence col-in places col c in col b, and the remaining equations transport this membership to w ∈ v.

                 → Σ[ c ∈ Dom ] (Below c × (↪ c ≡ fst y) × (col c ≡ fst w))
                 → ⟨ fst w ∈ fst v ⟩
            read y hy (c , (_ , ey , ew)) =
              subst2 (λ s t → ⟨ s ∈ t ⟩) ew ev (col-in b c cb)
              where

The strict comparison between c and b is filled from the two naming equations and the relation witness, completing the predecessor data.

              cb : c ≺ b
              cb = ≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩) (sym ey) (sym ex) hy)

The local table satisfies the graph formula at the top element, with the default entry witnessing the value clause. This is the induction step of the whole section.

      approx-step : ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
      approx-step = CF.colFo-in (colʟ a) (up a) Fa Fa-correct (Fa-in a (inr refl))

Well-founded induction now proves the collapse formula at every a : Dom. The induction hypothesis supplies the formula at each strict predecessor; Approx.approx-step uses those witnesses to build a correct local table at a. The conclusion concerns every index in Dom; it does not require D itself to have already been identified with an ordinal.

    approx : (a : Dom) → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
    approx = W.induction {P = λ a → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩}
      (λ a IH → Approx.approx-step a IH)

For q : S with mq : Mem q, the preceding induction gives the formula at the canonical representative up (toDom q mq). The round-trip equality up-toDom q mq identifies that representative with q, and colFo-at transports satisfaction to the original member of D.

    approx-at : (q : S) (mq : Mem q) → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
    approx-at q mq = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (approx (toDom q mq))

The recursion otR uses D as its domain and CF.colFo as its value relation. At a member q ∈ D, its chosen value is the collapse at the small index toDom q mq; the preceding approximation proves that this value satisfies the formula at q.

    private
      otR : Recursion
      otR = record
        { dom   = D
        ; graph = CF.colFo

The funct field must make the fiber of values satisfying CF.colFo at each q ∈ D contractible. Its center is colʟ (toDom q mq) together with approx-at q mq. For any competing (v,hv), colFo-val identifies the underlying set of v with the same collapse value; propositionality of constructibility and of satisfaction then lifts that equality first to v and finally to the whole fiber element.

        ; funct = λ q mq → (colʟ (toDom q mq) , approx-at q mq)
            , λ { (v , hv) → Σ≡Prop (λ w → snd ((w ∷ q ∷ []) ⊨ CF.colFo))
                (sym (Σ≡Prop (λ w → snd (isL w)) (colFo-val q mq v hv))) } }

The generic replacement construction Of now turns this functional recursion into its value table. It provides both directions of the membership characterization: values satisfying the recursion enter the table, and every table member comes from some input in D with the required formula witness.

      module OT = Of otR using ( table; table-in; table-out )

otL is the replacement range of otR, hence an element of L. Its underlying set collects all collapse values col b for b : Dom, without requiring those values to have distinct indices. At this point the construction uses only this exact-range description; ordinality of the whole range is a further conclusion.

    otL : S
    otL = OT.table

For each b : Dom, the approximation proves that colʟ b is a value of otR at up b. The introduction half of replacement therefore gives col b ∈ fst otL.

    otL-in : (b : Dom) → ⟨ col b ∈ fst otL ⟩
    otL-in b = OT.table-in (up b) (colʟ b) (up-mem b) (approx b)

Conversely, every y ∈ fst otL merely has an index b : Dom with col b ≡ y. The result deliberately retains propositional truncation, so it describes the exact range without choosing a preimage for every member.

    otL-out : (y : V ℓ) → ⟨ y ∈ fst otL ⟩ → ∥ Σ[ b ∈ Dom ] (col b ≡ y) ∥₁
    otL-out y hy = PT.map (λ { (q , (mq , h)) → toDom q mq , sym (colFo-val q mq yS h) })
      (OT.table-out yS hy)
      where
      yS : S

To apply the replacement reader, the ambient set y must be regarded as an element of the constructible carrier. Downward closure of constructibility supplies this packaging from y ∈ fst otL and the fact that otL is constructible.

      yS = y , isL-trans {x = fst otL} {y = y} hy (snd otL)

Applying the recursion-graph construction to otR collects ordered pairs rather than bare values. For every input in D it records the input together with its uniquely determined collapse value, and it supplies the corresponding inward and outward readings, single-valuedness, and exact-domain statement.

    module CT = RecursionGraph otR using ( F; F-in; F-out; pair-out; sv; dm )

colTable is the graph set constructed from otR inside L. Its canonical entry at b : Dom is pr(↪ b,col b): the stored input is the represented member ↪ b of D, while b itself remains an index in the external small presentation.

    colTable : S
    colTable = CT.F

At the canonical representative up b, the recursion graph initially records the value col (toDom (up b) (up-mem b)). The presentation equation induces equality of this recovered index with b; transporting the second coordinate along its image under col yields the advertised pair pr(↪ b,col b).

    colTable-in : (b : Dom) → ⟨ pr (↪ b) (col b) ∈ fst colTable ⟩
    colTable-in b = subst (λ t → ⟨ pr (↪ b) t ∈ fst colTable ⟩)
      (cong col (Dom≡ (toDom-val (up b) (up-mem b)))) (CT.F-in (up b) (up-mem b))

Conversely, colTable-out says that any member y of the graph is merely equal in its underlying set to pr(↪ b,col b) for some b : Dom. The index remains under propositional truncation, so this outward reading characterizes the graph without selecting a representing index for each member.

    colTable-out : (y : S) → ⟨ y ∈ˢ colTable ⟩
                 → ∥ Σ[ b ∈ Dom ] (fst y ≡ pr (↪ b) (col b)) ∥₁
    colTable-out y hy = PT.map (λ { (q , mq , e) → toDom q mq
      , e ∙ cong (λ t → pr t (col (toDom q mq))) (sym (toDom-val q mq)) }) (CT.F-out (fst y) hy)

The fiber predicate says that a member v paired with x is the collapse value of the index that x presents, with the presentation membership as data.

    Fib : S → S → Type (ℓ-suc ℓ)
    Fib x v = Σ[ mx ∈ Mem x ] (fst v ≡ col (toDom x mx))

For fixed x and v, Fib x v is a proposition. Membership mx : Mem x is proposition-valued, and for each such mx the equality fst v ≡ col (toDom x mx) is a proposition because V is a set. Thus the dependent sum carries no additional choice data.

    isPropFib : (x v : S) → isProp (Fib x v)
    isPropFib x v = isPropΣ (isPropMem x) (λ mx → setIsSet (fst v) (col (toDom x mx)))

Membership of the encoded pair of x and v in colTable therefore yields untruncated information: x belongs to D, and the underlying set of v equals the collapse at the index presented by x. Propositionality of Fib x v is what permits the graph reader's truncated witness to be eliminated.

    colTable-pair : (x v : S) → Holds colTable x v → Fib x v
    colTable-pair = CT.pair-out

The graph as a coded injection

To study when the collapse graph codes an injection, fix D, R, and the endpoint condition Rsub. This condition says only that both endpoints of every recorded R-edge lie in D; well-foundedness, transitivity, and trichotomy remain separate hypotheses.

module Code (D R : S)
            (Rsub : (y x : S) → Holds R y x
                  → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where

The small presentation Dom, its coded relation _≺_, and the conversions between members of D and their indices are the same ones used above. The coding argument will build on that collapse construction rather than introduce a second relation.

  open Internal D R Rsub public

The hypotheses play different roles. Well-foundedness defines col by recursion, while transitivity proves each collapse value is an ordinal and hence constructible; the local-table assembly also uses the chapter's classical parameter lem. Together these ingredients construct the exact range otL and the graph colTable, and yield single-valuedness, exact domain, and containment of all graph values in otL. Trichotomy is added only in the next module, where it proves injectivity.

  module Conjuncts (wf : WellFounded _≺_)
                   (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where

With these two hypotheses fixed, the preceding graph construction supplies col, otL, and colTable together with their membership characterizations. At this stage equal inputs have equal recorded values, but equality of recorded values has not yet been shown to recover equal inputs.

    open Graph wf ≺-trans public

In the two-slot environment γ, slot zero contains colTable and slot one contains D. The formulas for single-valuedness and exact domain can therefore refer to the graph and its intended domain by these fixed positions.

    γ : S ^ 
    γ = colTable ∷ D ∷ []

The first condition is single-valuedness: if colTable contains pairs with the same input and values y and y', then fst y ≡ fst y'. It follows from uniqueness of the recursion value and does not assert that every input has a value.

    sv : ⟨ γ ⊨ svAt zero ⟩
    sv = CT.sv

The domain condition is an equivalence: an input has some value in colTable exactly when it belongs to D. Thus it includes both exclusion of entries outside D and totality on every member of D; the existential value in the latter direction remains propositionally truncated.

    dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
    dm = CT.dm

The range condition follows from the paired graph reading: an entry from x to y gives a domain witness for x and identifies fst y with the corresponding collapse value, which otL-in places in otL. This establishes only that graph values lie in otL; injectivity of colTable still requires the trichotomy hypothesis introduced next.

    ran : (x y : S) → Holds colTable x y → ⟨ fst y ∈ fst otL ⟩
    ran x y h = subst (λ t → ⟨ t ∈ fst otL ⟩) (sym (snd (colTable-pair x y h)))
      (otL-in (toDom x (fst (colTable-pair x y h))))

The collapse table is already total and single-valued on D, and its values already lie in the exact range otL. The remaining condition for a coded injection is input uniqueness. Assume trichotomy on the small domain: for any a and b, either a ≺ b, a ≡ b, or b ≺ a. Together with the well-foundedness and transitivity fixed by the enclosing module, this comparison will make equal collapse values force equal indices.

    module Inj (tri : (a b : Dom) → (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a))) where

To prove that col is injective, fix a and b with col a ≡ col b and split their trichotomy. The equality case is already the desired conclusion. Each strict case instead turns a genuine membership between the two collapse values into self-membership after transport along their equality, so it suffices to refute that impossible membership.

      col-inj : (a b : Dom) → col a ≡ col b → a ≡ b
      col-inj a b e = go (tri a b)
        where
        go : (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a)) → a ≡ b
        go (inl k)       = Empty.rec (∈-irrefl (col b)

In the left case, a precedes b, so col a is a member of col b; transporting along the value equality makes col b a member of itself, which irreflexivity refutes. The middle case returns the equality directly. The right case is symmetric: col a would be a member of itself.

          (subst (λ t → ⟨ t ∈ col b ⟩) e (col-in b a k)))
        go (inr (inl q)) = q
        go (inr (inr k)) = Empty.rec (∈-irrefl (col a)
          (subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b k)))

The object-language clause injAt asks whether two graph entries with the same output have the same input. Reading p and q with colTable-pair produces membership proofs m and m' for the two inputs in D, together with equations identifying the common output y with both recovered collapse values. Composing those equations supplies the hypothesis needed by col-inj.

      ij : ⟨ γ ⊨ injAt zero ⟩
      ij = injAt-in zero γ (λ y x x' p q →
        let (m , e)   = colTable-pair x y p
            (m' , e') = colTable-pair x' y q
        in sym (toDom-val x m)

The recovered indices are equal by col-inj, and the round-trip lemma transports that equality back to the underlying sets of the original carrier elements. The three equations compose into the required equality.

         ∙ cong ↪ (col-inj (toDom x m) (toDom x' m') (sym e ∙ e'))
         ∙ toDom-val x' m')

The four fields now have distinct sources. The recursion graph supplies single-valuedness and the exact domain clause; colTable-pair and otL-in give the range bound; trichotomy supplied the missing injectivity clause. Packaging these proofs yields InjCode colTable D otL. Thus colTable is a coded injection only inside the module carrying tri; this record makes no separate claim that otL has been packaged here as an ordinal.

      code : InjCode colTable D otL
      code = sv , dm , ij , ran

The converse construction is intentionally local to chosen source and target sets X and Y. For every x ∈ X, pre must choose an index b : Dom with col b ≡ fst x; this is a collapse preimage, and it need not be a predecessor of any fixed point of the relation. The second argument bound proves that the represented original input ↪ b lies in Y. These data are extra obligations at each use of the inverse interface, rather than consequences of otL-out alone.

      module Inverse (X Y : S)
        (pre : (x : S) → ⟨ fst x ∈ fst X ⟩ → Σ[ b ∈ Dom ] (col b ≡ fst x))
        (bound : (x : S) (mx : ⟨ fst x ∈ fst X ⟩) → ⟨ ↪ (pre x mx .fst) ∈ fst Y ⟩) where