---
title: "Constructing order types inside L"
module: L.GCH.OrderType
lang: en
site: "Bedrock"
description: "Constructing order types inside L"
stage: "Proving GCH"
reading_order: 109
canonical: https://bedrock.institute/en/L.GCH.OrderType.html
html: L.GCH.OrderType.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/OrderType.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Recursion, L.Recursion.Graph, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Cardinal, L.DefinableInjection, L.Mostowski]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.OrderType.md, https://bedrock.institute/ja/L.GCH.OrderType.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
  Dom : Type ℓ
  Dom = ⟪ fst D ⟫
```

The presentation embeds its indices into the ambient hierarchy.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
  opaque
    unfolding correctAt
    colFo : Formula S 2
    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)`.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
      image : PE.Expr 2
      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.

```agda
      opaque
        ψ : Formula S 2
        ψ = (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`.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

```agda
    γ : S ^ 2
    γ = 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.

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

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

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

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

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

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

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

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

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

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

Membership in the source set is recorded as a type, so that the argument can carry it alongside each element being mapped.

```agda
        SourceMem : S → Type (ℓ-suc ℓ)
        SourceMem x = ⟨ fst x ∈ fst X ⟩
```

For `x ∈ X`, let `b` be the collapse preimage selected by `pre`. The inverse function returns `up b`, the constructible carrier element whose underlying set is the represented member `↪ b` of the original domain. The proof argument `mx` is needed because the selected preimage may depend on the evidence that `x` lies in the chosen source.

```agda
        fn : (x : S) → SourceMem x → S
        fn x mx = up (pre x mx .fst)
```

The defining formula reads the existing table in the converse direction. In the environment `y ∷ x ∷ []`, `y` is the proposed output of the inverse map and `x` is its input, while `appC colTable zero (suc zero)` asserts the original table entry `Holds colTable y x`. No new collapse table is assumed; the two coordinates of the old graph are simply assigned their inverse roles.

```agda
        opaque
          graph : Formula S 2
          graph = appC colTable zero (suc zero)
```

The adequacy equation identifies the satisfaction of the swapped graph formula with the membership of the pair in the collapse table, so both readings of the table can be used interchangeably.

```agda
          at : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ ≡ Holds colTable y x
          at y x = cong ⟨_⟩ (appC-adequate colTable zero (suc zero) (y ∷ x ∷ []))
```

It remains to show that the converse formula has only the selected value. From `Holds colTable y x`, `colTable-pair` recovers an index presenting the candidate output `y` and an equation saying that this index collapses to the inverse input `x`. The selected index from `pre` also collapses to `x`; `col-inj` therefore identifies the two indices, and `up-toDom` transports that index equality back to `y ≡ fn x mx`.

```agda
        only : (x : S) (mx : SourceMem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x mx
        only x mx y hy = sym (up-toDom y my)
          ∙ cong up (col-inj (toDom y my) (pre x mx .fst) (sym (f .snd) ∙ sym (pre x mx .snd)))
          where
          f = colTable-pair y x (transport (at y x) hy)
```

The first projection of `f` is the membership proof `my : Mem y`. It is the evidence needed to form the recovered index `toDom y my` and to apply the round-trip lemma; it is not itself that index.

```agda
          my = f .fst
```

These ingredients form a `DefinableMap` from `X` to `Y`. Its external function is `fn`, and `bound` supplies the codomain field. For the defining clause, start with `colTable-in b` for the selected preimage `b`; substitute `col b ≡ fst x` in the output coordinate, then use `at` in the reverse direction to turn the resulting table membership into satisfaction of the converse graph formula.

```agda
        M : DefinableMap
        M = record
          { dom = X ; cod = Y ; fn = fn ; into = bound ; graph = graph
          ; defines = λ x mx → transport (sym (at (fn x mx) x))
              (subst (λ w → ⟨ pr (↪ (pre x mx .fst)) w ∈ fst colTable ⟩)
```

The `defines` field starts from the canonical entry `colTable-in b` and transports its output coordinate along the preimage equation `col b ≡ fst x`. The adequacy equality `at` then turns that table membership into satisfaction of the converse graph formula, while `only` supplies the required uniqueness of the value.

```agda
                (pre x mx .snd)
                (colTable-in (pre x mx .fst)))
          ; only = only }
```

The inverse function is injective for a direct reason. If `fn x mx` and `fn x' mx'` have equal underlying sets, then these sets are `↪ b` and `↪ b'` for the indices selected by `pre`; presentation injectivity `Dom≡` gives `b ≡ b'`. Applying `col` and composing with the two equations stored by `pre` yields `fst x ≡ fst x'`. This proof uses injectivity of the small presentation at `Dom≡`; `col-inj` was used earlier to prove uniqueness of the converse formula, not in this equality chain.

```agda
        inj : (x : S) (mx : SourceMem x) (x' : S) (mx' : SourceMem x')
            → fst (fn x mx) ≡ fst (fn x' mx') → fst x ≡ fst x'
        inj x mx x' mx' e = sym (pre x mx .snd) ∙ cong col (Dom≡ e) ∙ pre x' mx' .snd
```

Applying the general definable-injection construction to `M` and `inj` packages the restricted converse as `InjL X Y`, a propositionally truncated existence claim for a coded injection. Its scope is exactly the supplied data: every member of `X` has a chosen collapse preimage, and the represented original input lies in `Y`. It supplies neither an unconditional inverse on all of `otL` nor a bijection record.

```agda
        injL : InjL X Y
        injL = DefinableInj.injL M inj
```