---
title: "ω-recursion inside the constructible universe"
module: L.GCH.OmegaRecursion
lang: en
site: "Bedrock"
description: "Iterating a definable step through ω"
stage: "Proving GCH"
reading_order: 103
canonical: https://bedrock.institute/en/L.GCH.OmegaRecursion.html
html: L.GCH.OmegaRecursion.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/OmegaRecursion.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Numerals, L.Axioms.Infinity, L.Recursion, L.Recursion.Graph, L.Coding.Model, L.Coding.Expressions]
routes: [gch-descriptions]
translations: [https://bedrock.institute/zh/L.GCH.OmegaRecursion.md, https://bedrock.institute/ja/L.GCH.OmegaRecursion.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# ω-recursion inside the constructible universe

A definable step on constructible sets and a starting point determine, by recursion on the host natural numbers, a sequence of finite iterates. This chapter represents each iterate inside `L`: finite correct tables establish existence and uniqueness at the internal numerals, replacement gathers their values and their indexed graph, and union forms the set containing every member reached at a finite stage.

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

The base library is opened, and excluded middle is received as an explicit hypothesis, in the standing form of the book.

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

The module fixes the universe level and names the classical hypothesis: every theorem below records exactly which level instance of excluded middle it consumes.

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

The description of the iteration is written in the object language, whose formulas use equality, conjunction, implication, and the unbounded existential and universal quantifiers; formula renaming and absoluteness support reading the same formula under different environments.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
```

The ambient hierarchy supplies membership and the numerals, ordered pairs have injective components, and the constructible structure carries the stage machinery with its transitivity and monotonicity.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import V.Model {ℓ} using ( pair-spec; union-spec; self∈sucV )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono )
open import L.Ordinal {ℓ} using ( #∈ω; ∈#-elim; boundingOrd )
```

To turn a host sequence into sets of `L`, we need four internal constructions: stages that bound constructibility, finite sets that hold approximating tables, coded ordered pairs and unions, and the set `ωʟ` of internal natural numbers. Together they let the later argument pass from one finite table for each host index to a single range and graph indexed inside the model.

```agda
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( finSet; finSet-in; finSet-out; module FinOf )
open import L.Axioms.Numerals {ℓ}
  using ( pairʟ; pairʟ-fst; unionʟ; unionʟ-fst )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

The recursion interface packages an internally definable, uniquely valued relation on an internal domain. Its graph construction and the coding formulas for application, ordered pairs, and set-theoretic successor will later turn the semantic finite-table argument into a first-order relation over `L` and then into actual sets of `L`.

```agda
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; prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate; numL )
```

The arithmetic of natural numbers, their bounded indices, and the conversions between bounded indices and numerals support the finite bookkeeping of the chapter.

```agda
open import Cubical.Data.Nat.Order
  using ( _≤_; ≤-refl; ≤-trans; <-weaken; pred-≤-pred; suc-≤-suc )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
```

Several identifications below live in dependent pairs: an underlying set is accompanied by a propositional proof of constructibility. The h-set structure of the cumulative hierarchy makes equalities between underlying sets propositions, while sums and two-variable transport handle the alternatives and simultaneous substitutions arising when coded pairs are decoded.

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_ )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

The successor operation of the hierarchy and the truncation machinery complete the constructions.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV; #_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

The constructible carrier is opened with its membership, since every iterate is an element of `L`.

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

The absoluteness reading is imported under two names, for formulas read inside `L` at environments.

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

The renaming semantics is instantiated under the identity of constant alphabets, so a renamed formula is read in an environment with its slots rearranged.

```agda
module Ren = Sat 𝒮ʟ id
```

The carrier is an h-set, since the hierarchy is an h-set and constructibility is propositional; equalities of constructible sets are therefore propositions.

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

Equal underlying sets make equal constructible sets, by the propositionhood of the constructibility proof. This conversion is used whenever an equality has first been obtained at the level of underlying sets.

```agda
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))
```

A coded graph records the input first and the value second: `Holds F x y` means that the ordered pair `(x,y)` belongs to `F`, at the level of underlying sets. Formula environments use the opposite list order, so the step relation at input `x` and output `y` is read under `(y ∷ x ∷ [])`.

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

The constructible numeral of `k` packages the ambient numeral with its constructibility; numerals are the indices at which the iterates will be recorded.

```agda
nn : ℕ → S
nn k = # k , numL k
```

An element enters the internal unordered pair `pairʟ a b` once its underlying set is identified with the underlying set of either `a` or `b`. The proof transports this alternative through the equation identifying the underlying set of `pairʟ a b` with the ambient unordered pair.

```agda
pairʟ-in : (a b y : S) → (fst y ≡ fst a) ⊎ (fst y ≡ fst b) → ⟨ y ∈ˢ pairʟ a b ⟩
pairʟ-in a b y k = subst (λ w → ⟨ fst y ∈ w ⟩) (sym (pairʟ-fst a b))
  (subst ⟨_⟩ (sym (pair-spec (fst a) (fst b) (fst y))) ∣ k ∣₁)
```

To place `y` in the internal union of `A`, it suffices to exhibit a particular constructible set `B` with `B ∈ A` and `y ∈ B`. The two memberships form the usual witness for membership in a union and are transported through the underlying-set equation for `unionʟ A`.

```agda
unionʟ-in : (A y B : S) → ⟨ fst B ∈ fst A ⟩ → ⟨ fst y ∈ fst B ⟩ → ⟨ y ∈ˢ unionʟ A ⟩
unionʟ-in A y B hB hy = subst (λ w → ⟨ fst y ∈ w ⟩) (sym (unionʟ-fst A))
  (subst ⟨_⟩ (sym (union-spec (fst A) (fst y))) ∣ fst B , (hB , hy) ∣₁)
```

Membership in a union yields, merely, an intermediate set containing the element; the intermediate set is an ambient element, without a constructibility proof of its own.

```agda
unionʟ-out : (A y : S) → ⟨ y ∈ˢ unionʟ A ⟩
           → ∥ Σ[ B ∈ V ℓ ] (⟨ B ∈ fst A ⟩ × ⟨ fst y ∈ B ⟩) ∥₁
unionʟ-out A y h = subst ⟨_⟩ (union-spec (fst A) (fst y))
  (subst (λ w → ⟨ fst y ∈ w ⟩) (unionʟ-fst A) h)
```

## Finite iterates of a definable step

The iteration module receives the five ingredients of the whole chapter: a starting point, a step formula in the output-first input-second order, the actual step function, a proof that the formula defines the function everywhere, and a proof that only that value satisfies it. Totality over the whole carrier is part of the data.

```agda
module Iterate (a : S) (stepFo : Formula S 2) (step : S → S)
               (defines : (x : S) → ⟨ (step x ∷ x ∷ []) ⊨ stepFo ⟩)
               (only : (x y : S) → ⟨ (y ∷ x ∷ []) ⊨ stepFo ⟩ → y ≡ step x) where
```

The iteration sequence is a host-level recursion on the natural numbers: it starts at `a` and applies the step function to the previous value. At this stage it is only an Agda sequence; its internal representation is the work of the chapter.

```agda
  it : ℕ → S
  it zero    = a
  it (suc n) = step (it n)
```

The zero clause says that every value recorded at the zeroth numeral has the same underlying set as the starting point. It does not say that a value is recorded there.

```agda
  Zero : S → Type (ℓ-suc ℓ)
  Zero F = (v : S) → Holds F (nn 0) v → fst v ≡ fst a
```

The successor clause says that whenever the table records both `(x, v)` and `(x', v')` with the underlying set of `x'` the successor of that of `x`, the step relation holds between the two values.

```agda
  Step : S → Type (ℓ-suc ℓ)
  Step F = (x v x' v' : S) → Holds F x v → Holds F x' v'
         → fst x' ≡ sucV (fst x) → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
```

The downward clause says that below every recorded entry, a recorded value exists, merely. It is the domain-completion clause, and its conclusion is truncated because a witness is not chosen.

```agda
  Down : S → Type (ℓ-suc ℓ)
  Down F = (x' v' x : S) → Holds F x' v' → ⟨ fst x ∈ fst x' ⟩
         → ∥ Σ[ v ∈ S ] Holds F x v ∥₁
```

A correct approximation is the conjunction of the three clauses. It is deliberately weaker than being a function graph: it fixes no exact domain and imposes no uniqueness.

```agda
  Correct : S → Type (ℓ-suc ℓ)
  Correct F = Zero F × (Step F × Down F)
```

The zero clause is written in the object language. It says that for every `z` equal to the zeroth numeral, and every value recorded there, that value equals the starting point.

```agda
  opaque
    zeroAt : ∀ {n} → Fin n → Formula S n
    zeroAt f = ∀̇ ( (var zero ≐ con (nn 0))
                 ⇒̇ ∀̇ ( appAt (suc (suc f)) (suc zero) zero ⇒̇ (var zero ≐ con a) ) )
```

Reading the zero clause applies it at the numeral zero and transports the application atom through its adequacy, producing the underlying-set equation of `Zero`.

```agda
    zero-out : ∀ {n} (f : Fin n) (γ : S ^ n) → ⟨ γ ⊨ zeroAt f ⟩ → Zero (lookup f γ)
    zero-out f γ h v hv = h (nn 0) refl v
      (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ nn 0 ∷ γ))) hv)
```

Conversely, a host-level proof of the zero clause fills the object-language formula. The quantified set `z` is rewritten along the premise `z = nn 0`, and the graph membership at zero is transported into the application atom before the clause identifies its value with `a`.

```agda
    zero-in : ∀ {n} (f : Fin n) (γ : S ^ n) → Zero (lookup f γ) → ⟨ γ ⊨ zeroAt f ⟩
    zero-in f γ h z ez v hv = h v
      (subst (λ t → ⟨ pr t (fst v) ∈ fst (lookup f γ) ⟩) ez
        (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ z ∷ γ)) hv))
```

The renaming of the step formula uses two slots: the first variable stays at position zero, and the second moves to position two, so that four quantified slots can surround the renamed body.

```agda
  private
    ρ : ∀ {n} → Fin 2 → Fin (suc (suc (suc (suc n))))
    ρ zero       = zero
    ρ (suc zero) = suc (suc zero)
```

The renaming agreement checks that the two environments agree on the renamed slots, which are the only positions the renamed formula reads.

```agda
    ag : ∀ {n} (γ : S ^ n) (x v x' v' : S)
       → Ren.Agrees ρ (v' ∷ x' ∷ v ∷ x ∷ γ) (v' ∷ v ∷ [])
    ag γ x v x' v' zero       = refl
    ag γ x v x' v' (suc zero) = refl
```

The successor clause universally quantifies two table entries `(x,v)` and `(x',v')`. Its nested implications first assume that both entries occur in the table and then assume that the underlying index `x'` is the set-theoretic successor of `x`.

```agda
  opaque
    stepAt : ∀ {n} → Fin n → Formula S n
    stepAt f = ∀̇ (∀̇ (∀̇ (∀̇ (
        appAt (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero))
      ⇒̇ ( appAt (suc (suc (suc (suc f)))) (suc zero) zero
```

Under these three premises, the conclusion is the renamed step formula relating `v'` to `v`. Renaming selects the output and input slots from the four quantified variables, thereby connecting the finite table's adjacent rows to the original two-variable definition of `step`.

```agda
      ⇒̇ ( sucAtL (suc (suc (suc zero))) (suc zero)
      ⇒̇ renameFo ρ stepFo ) ) ))))
```

The renaming path is proved by the renaming semantics: satisfaction of the renamed formula at the long environment equals satisfaction of the original at the short one, because the two environments agree on the renamed slots.

```agda
    private
      gr : ∀ {n} (γ : S ^ n) (x v x' v' : S)
         → ⟨ (v' ∷ x' ∷ v ∷ x ∷ γ) ⊨ renameFo ρ stepFo ⟩ ≡ ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
      gr γ x v x' v' = cong ⟨_⟩
        (Ren.⊨-rename ρ stepFo (v' ∷ x' ∷ v ∷ x ∷ γ) (v' ∷ v ∷ []) (ag γ x v x' v'))
```

Reading the successor clause transports the two application atoms against their adequacy, applies the four quantifiers, and uses the renaming path.

```agda
    step-out : ∀ {n} (f : Fin n) (γ : S ^ n) → ⟨ γ ⊨ stepAt f ⟩ → Step (lookup f γ)
    step-out f γ h x v x' v' p q s = transport (gr γ x v x' v')
      (h x v x' v'
        (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero)) (v' ∷ x' ∷ v ∷ x ∷ γ))) p)
        (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v' ∷ x' ∷ v ∷ x ∷ γ))) q)
```

The last premise recognizes `x'` as the set-theoretic successor of `x`. Together with the two table memberships, it is exactly the hypothesis needed to compare adjacent rows, so the semantic reading yields the step relation between their values.

```agda
        (subst ⟨_⟩ (sym (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ))) s))
```

Filling the successor clause runs the same transports in reverse, starting from the host-level step instance.

```agda
    step-in : ∀ {n} (f : Fin n) (γ : S ^ n) → Step (lookup f γ) → ⟨ γ ⊨ stepAt f ⟩
    step-in f γ h x v x' v' p q s = transport (sym (gr γ x v x' v'))
      (h x v x' v'
        (subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc (suc (suc zero))) (suc (suc zero)) (v' ∷ x' ∷ v ∷ x ∷ γ)) p)
        (subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v' ∷ x' ∷ v ∷ x ∷ γ)) q)
```

Conversely, a host-level proof of the adjacent-row condition satisfies the object-language clause: the adequacy equations identify its three premises with the two encoded entries and the successor relation, while renaming restores the original two-variable step formula.

```agda
        (subst ⟨_⟩ (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ)) s))
```

The downward clause has three universal quantifiers and one existential. If the table contains `(x',v')` and `x` is a member of the underlying set of `x'`, the formula asserts that some value is recorded at `x`; the existential semantics retains only the proposition that such a value exists.

```agda
  opaque
    downAt : ∀ {n} → Fin n → Formula S n
    downAt f = ∀̇ (∀̇ (∀̇ (
        appAt (suc (suc (suc f))) (suc (suc zero)) (suc zero)
      ⇒̇ ( (var zero ∈̇ var (suc (suc zero)))
```

The existential conclusion is exactly a truncated existence of a recorded value.

```agda
      ⇒̇ ∃̇ (appAt (suc (suc (suc (suc f)))) (suc zero) zero) ) )))
```

Reading the downward formula preserves the existential as a propositional truncation. It maps each hidden witness value and its application atom to the corresponding host-level graph membership, without selecting a witness outside the truncation.

```agda
    down-out : ∀ {n} (f : Fin n) (γ : S ^ n) → ⟨ γ ⊨ downAt f ⟩ → Down (lookup f γ)
    down-out f γ h x' v' x p m = PT.map
      (λ { (v , q) → v , subst ⟨_⟩ (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v ∷ x ∷ v' ∷ x' ∷ γ)) q })
      (h x' v' x (subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero) (x ∷ v' ∷ x' ∷ γ))) p) m)
```

Filling runs the transport the other way, from the host-level truncated entry to the satisfaction of the existential.

```agda
    down-in : ∀ {n} (f : Fin n) (γ : S ^ n) → Down (lookup f γ) → ⟨ γ ⊨ downAt f ⟩
    down-in f γ h x' v' x p m = PT.map
      (λ { (v , q) → v , subst ⟨_⟩ (sym (appAt-adequate (suc (suc (suc (suc f)))) (suc zero) zero (v ∷ x ∷ v' ∷ x' ∷ γ))) q })
      (h x' v' x (subst ⟨_⟩ (appAt-adequate (suc (suc (suc f))) (suc (suc zero)) (suc zero) (x ∷ v' ∷ x' ∷ γ)) p) m)
```

Correctness in the object language is the conjunction of the three clauses.

```agda
  opaque
    corrAt : ∀ {n} → Fin n → Formula S n
    corrAt f = zeroAt f ∧̇ (stepAt f ∧̇ downAt f)
```

The three conjuncts recover exactly the semantic conditions already isolated as `Zero`, `Step`, and `Down`. In particular, translating the formula back to mathematics introduces neither a domain equation nor a single-valuedness assumption.

```agda
    corr-out : ∀ {n} (f : Fin n) (γ : S ^ n) → ⟨ γ ⊨ corrAt f ⟩ → Correct (lookup f γ)
    corr-out f γ (z , (s , d)) = zero-out f γ z , (step-out f γ s , down-out f γ d)
```

The converse direction shows that these three semantic conditions suffice to satisfy the conjunction. Hence `corrAt` is an exact first-order presentation of the deliberately weak notion `Correct`, rather than a stronger assertion that the approximation is already a total function graph.

```agda
    corr-in : ∀ {n} (f : Fin n) (γ : S ^ n) → Correct (lookup f γ) → ⟨ γ ⊨ corrAt f ⟩
    corr-in f γ (z , (s , d)) = zero-in f γ z , (step-in f γ s , down-in f γ d)
```

The formula `itFo` says that some correct approximation records value `y` at index `q`: internally, the graph entry is the ordered pair `(q,y)`, while the formula environment is `(y ∷ q ∷ [])`. Thus `itFo` does not state a recursion equation; it internalizes the relation witnessed by a finite correct approximation.

```agda
  opaque
    itFo : Formula S 2
    itFo = ∃̇ ( corrAt zero ∧̇ appAt zero (suc (suc zero)) (suc zero) )
```

From a satisfaction of `itFo` one recovers only the propositional truncation of a witness table `F`, together with `Correct F` and the entry `(q,y)`. The formula therefore certifies that a suitable finite approximation exists, while deliberately hiding which approximation was used.

```agda
    itFo-out : (y q : S) → ⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
             → ∥ Σ[ F ∈ S ] (Correct F × Holds F q y) ∥₁
    itFo-out y q = PT.map (λ { (F , (hc , ha)) → F
      , ( corr-out zero (F ∷ y ∷ q ∷ []) hc
        , subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero) (F ∷ y ∷ q ∷ [])) ha ) })
```

In the other direction, any particular correct approximation containing `(q,y)` witnesses `itFo(y,q)`. Its identity is immediately placed under propositional truncation, which is why later arguments may use existence and uniqueness but may not extract a preferred table.

```agda
    itFo-in : (y q F : S) → Correct F → Holds F q y → ⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
    itFo-in y q F hc hq = ∣ F
      , ( corr-in zero (F ∷ y ∷ q ∷ []) hc
        , subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero) (F ∷ y ∷ q ∷ []))) hq ) ∣₁
```

The satisfaction of `itFo` is transported along an equality of the numeral slot alone; the value slot stays fixed.

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

The uniqueness lemma begins by cases on the iterate index: at zero, the zero clause gives the equation directly; at a successor, the truncated downward witness must first be eliminated. That elimination is legitimate because the target is an equality in an h-set.

```agda
  corr-val : (F : S) → Correct F → (k : ℕ) (v : S)
           → Holds F (nn k) v → fst v ≡ fst (it k)
  corr-val F (z , (s , d)) zero    v h = z v h
  corr-val F (z , (s , d)) (suc k) v h =
    PT.rec (setIsSet (fst v) (fst (it (suc k)))) read
```

At a successor index, `Down` supplies, under propositional truncation, a value recorded at the predecessor numeral. The induction hypothesis identifies this predecessor value with `it k`; then `Step` shows that the current and predecessor values satisfy `stepFo`, and `only` determines the current value uniquely.

```agda
      (d (nn (suc k)) v (nn k) h (self∈sucV (# k)))
    where
    read : Σ[ u ∈ S ] Holds F (nn k) u → fst v ≡ fst (it (suc k))
    read (u , hu) = cong fst (only (it k) v
      (subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ stepFo ⟩)
```

The induction hypothesis gives equality of the underlying sets of `u` and `it k`. Since constructibility is a proposition, `S≡` lifts this to an equality in `S`, allowing the input of `stepFo` to be replaced by `it k`. The clause `only` then identifies `v` with `step (it k) = it (suc k)`.

```agda
        (S≡ (corr-val F (z , (s , d)) k u hu))
        (s (nn k) u (nn (suc k)) v hu h refl)))
```

The value at a canonical numeral is unique: any satisfaction of the iteration formula at `nn k` records a value whose underlying set equals that of `it k`. The proof eliminates the truncated correct table and applies the uniqueness lemma within that table.

```agda
  itFo-val : (k : ℕ) (v : S) → ⟨ (v ∷ nn k ∷ []) ⊨ itFo ⟩ → fst v ≡ fst (it k)
  itFo-val k v h = PT.rec (setIsSet (fst v) (fst (it k)))
    (λ { (F , (hc , hv)) → corr-val F hc k v hv }) (itFo-out v (nn k) h)
```

Each iterate is presented as a model element: the ordered pair of its numeral with the iterate itself, both constructible.

```agda
  private
    e : ℕ → S
    e k = prʟ (nn k) (it k)
```

The bounding ordinal for all entry stages is assembled by the bounding lemma applied to the family of stage indices of the entry pairs.

```agda
  private
    entryStages = boundingOrd (Lift {ℓ-zero} {ℓ} ℕ)
      (λ k → stage (fst (e (lower k))) (e (lower k) .snd))
      (λ k → stage-ord (fst (e (lower k))) (e (lower k) .snd))
```

Write `entryBound` for this common ordinal bound. The point of naming it is that every finite table can be constructed inside the same level `Lset entryBound`, even though the table length will later vary with `n`.

```agda
    entryBound : V ℓ
    entryBound = entryStages .fst
```

The bound is itself an ordinal, as required for it to index a constructible level. No leastness claim is needed: any ordinal lying above all the entry stages is enough for the finite-set construction.

```agda
    entryBound-ord : IsOrd entryBound
    entryBound-ord = entryStages .snd .fst
```

Each entry belongs to the constructible level indexed by the common bound. Indeed, its own stage contains it, and monotonicity of `Lset` carries that membership along the comparison supplied by `boundingOrd`.

```agda
    entry-in-bound : (k : ℕ) → ⟨ fst (e k) ∈ Lset entryBound ⟩
    entry-in-bound k = Lset-mono (entryStages .snd .snd (lift k))
      (stage-mem (fst (e k)) (e k .snd))
```

For a fixed `n`, the table `Fn n` is the finite set of entry pairs with indices `0` through `n`. The common bound proves that every such pair lies in one constructible level, so the finite-set construction packages the whole table as an element of `L`.

```agda
  Fn : ℕ → S
  Fn n = finSet (suc n) (λ i → fst (e (toℕ i))) ,
    FinOf.finSetL entryBound entryBound-ord
      (suc n) (λ i → fst (e (toℕ i))) (λ i → entry-in-bound (toℕ i))
```

If `k ≤ n`, the canonical entry `(nn k, it k)` occurs in `Fn n`. Thus the table contains exactly the initial segment needed to witness the iteration formula at its final index `n`.

```agda
  Fn-in : (n k : ℕ) → k ≤ n → Holds (Fn n) (nn k) (it k)
  Fn-in n k p = subst (λ w → ⟨ w ∈ fst (Fn n) ⟩) (prʟ-fst (nn k) (it k))
    (finSet-in (suc n) (λ i → fst (e (toℕ i))) (fst (e k))
      ∣ fromℕ' (suc n) k (suc-≤-suc p)
      , cong (λ j → fst (e j)) (toFromId' (suc n) k (suc-≤-suc p)) ∣₁)
```

The outward reading decomposes any member into a bounded index and its iterate value, both recovered under truncation.

```agda
  Fn-out : (n : ℕ) (y : S) → ⟨ y ∈ˢ Fn n ⟩
         → ∥ Σ[ k ∈ ℕ ] ((k ≤ n) × (fst y ≡ pr (# k) (fst (it k)))) ∥₁
  Fn-out n y h = PT.map (λ { (i , q) → toℕ i
    , (pred-≤-pred (toℕ<n i) , sym q ∙ prʟ-fst (nn (toℕ i)) (it (toℕ i))) })
    (finSet-out (suc n) (λ i → fst (e (toℕ i))) (fst y) h)
```

The pair reading decomposes any entry of the finite table into a bounded index and its iterate value, using the injectivity of the Kuratowski pair.

```agda
  Fn-pair : (n : ℕ) (x v : S) → Holds (Fn n) x v
          → ∥ Σ[ k ∈ ℕ ] ((k ≤ n) × ((fst x ≡ # k) × (fst v ≡ fst (it k)))) ∥₁
  Fn-pair n x v h = PT.map (λ { (k , (p , q)) → k , (p , pr-inj (sym (prʟ-fst x v) ∙ q)) })
    (Fn-out n (prʟ x v) (subst (λ w → ⟨ w ∈ fst (Fn n) ⟩) (sym (prʟ-fst x v)) h))
```

The finite table is correct: the three clauses are assembled from the pair readings of the table entries.

```agda
  Fn-correct : (n : ℕ) → Correct (Fn n)
  Fn-correct n = zeroC , (stepC , downC)
    where
    zeroC : Zero (Fn n)
    zeroC v h = PT.rec (setIsSet (fst v) (fst a))
```

For the zero clause, reading an entry at `nn 0` yields some index `k` whose numeral is `# 0`. Injectivity of the numeral encoding forces `k = 0`, and the accompanying value equation then identifies the recorded value with `it 0 = a`.

```agda
      (λ { (k , (_ , (ex , ev))) → ev ∙ cong (λ j → fst (it j)) (sym (#-inj 0 k ex)) })
      (Fn-pair n (nn 0) v h)
```

For the step clause, read the two table entries under propositional truncation. Since satisfaction of `stepFo` is a proposition, both truncations may be eliminated there; the remaining task is to identify their indices as consecutive and their values as the corresponding iterates.

```agda
    stepC : Step (Fn n)
    stepC x v x' v' hxv hx'v' s = PT.rec (snd ((v' ∷ v ∷ []) ⊨ stepFo)) outer (Fn-pair n x v hxv)
      where
      outer : Σ[ k ∈ ℕ ] ((k ≤ n) × ((fst x ≡ # k) × (fst v ≡ fst (it k))))
            → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
```

After the first reading has exposed `k`, the second exposes an index `k'` for the adjacent row. Keeping both witnesses inside eliminations into the propositional satisfaction judgment respects the truncation boundary while making their index and value equations simultaneously available.

```agda
      outer (k , (_ , (ex , ev))) = PT.rec (snd ((v' ∷ v ∷ []) ⊨ stepFo)) inner (Fn-pair n x' v' hx'v')
        where
        inner : Σ[ k' ∈ ℕ ] ((k' ≤ n) × ((fst x' ≡ # k') × (fst v' ≡ fst (it k'))))
              → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩
        inner (k' , (_ , (ex' , ev'))) =
```

The two table readings identify `v` with `it k` and `v'` with `it k'`. The successor equation between their positions forces `k' = suc k`; after these identifications, the required satisfaction is precisely `defines (it k)`. Equalities in the model carrier are obtained with `S≡`, using that the constructibility proof component is propositional.

```agda
          subst2 (λ p q → ⟨ (p ∷ q ∷ []) ⊨ stepFo ⟩)
            (S≡ (sym (ev' ∙ cong (λ j → fst (it j)) k'≡)))
            (S≡ (sym ev))
            (defines (it k))
          where
```

To obtain `k' = suc k`, compare the equation saying that the second position is the successor of the first with the two equations identifying those positions as `# k'` and `# k`. Injectivity of the numeral encoding then turns equality of the encoded finite ordinals into equality of their natural-number indices.

```agda
          k'≡ : k' ≡ suc k
          k'≡ = #-inj k' (suc k) (sym ex' ∙ s ∙ cong sucV ex)
```

The downward clause is proved by eliminating the truncated pair reading and finding a smaller index whose canonical entry is already present.

```agda
    downC : Down (Fn n)
    downC x' v' x h m = PT.rec squash₁ outer (Fn-pair n x' v' h)
      where
      outer : Σ[ k' ∈ ℕ ] ((k' ≤ n) × ((fst x' ≡ # k') × (fst v' ≡ fst (it k'))))
            → ∥ Σ[ v ∈ S ] Holds (Fn n) x v ∥₁
```

The smaller index's entry is produced by the inward reading of the finite table, transported along the numeral equation.

```agda
      outer (k' , (p' , (ex' , _))) = PT.map
        (λ { (j , (j< , ej)) → it j
           , subst (λ t → ⟨ pr t (fst (it j)) ∈ fst (Fn n) ⟩) (sym ej)
               (Fn-in n j (≤-trans (<-weaken j<) p')) })
        (∈#-elim k' (fst x) (subst (λ w → ⟨ fst x ∈ w ⟩) ex' m))
```

Each canonical pair satisfies the iteration formula, using its own finite table as the witness. Every target numeral thus has its own table; no single table is claimed to serve all positions.

```agda
  it-graph : (k : ℕ) → ⟨ (it k ∷ nn k ∷ []) ⊨ itFo ⟩
  it-graph k = itFo-in (it k) (nn k) (Fn k) (Fn-correct k) (Fn-in k k ≤-refl)
```

A numeral representation is an explicit pair of a natural number with the equation identifying it with the carrier element.

```agda
  Num : S → Type (ℓ-suc ℓ)
  Num q = Σ[ k ∈ ℕ ] (nn k ≡ q)
```

Membership in the model's natural-number set `ωʟ` recovers such a numeral representation only under propositional truncation. This is enough for later uniqueness arguments, whose conclusions are propositions, but it does not expose a natural number for unrestricted computation.

```agda
  ω-num : (q : S) → ⟨ q ∈ˢ ωʟ ⟩ → ∥ Num q ∥₁
  ω-num q = PT.map (λ { (i , p) → lower i , S≡ p })
```

We can now regard `itFo` as a total, single-valued relation on the internal set `ωʟ`. The record `valR` packages this domain and graph together with the remaining functionality proof; applying Replacement to this record will collect their values in `L`.

```agda
  private
    valR : Recursion
    valR = record
      { dom   = ωʟ
      ; graph = itFo
```

Functionality is assembled from a merely-existing numeral representation: the decode produces the iterate value, and the uniqueness is proved at the decoded numeral.

```agda
      ; funct = λ q q∈ → mereFunct itFo q (PT.map (wit q) (ω-num q q∈)) }
      where
      wit : (q : S) → Num q
          → Σ[ y ∈ S ] (⟨ (y ∷ q ∷ []) ⊨ itFo ⟩
                       × ((y' : S) → ⟨ (y' ∷ q ∷ []) ⊨ itFo ⟩ → y' ≡ y))
```

For a displayed representation `nn k ≡ q`, take `it k` as the centre of the fibre. The graph proof is transported forward to `q`, while any competing value is transported back to `nn k` and identified by `itFo-val`. The surrounding `mereFunct` turns the truncated existence of such a centre with uniqueness into contractibility of the fibre.

```agda
      wit q (k , eq) = it k
        , ( itFo-at (it k) eq (it-graph k)
          , λ y' h → S≡ (itFo-val k y' (itFo-at y' (sym eq) h)) )
```

The general Replacement construction associated with `valR` now provides a set containing its values, together with exact membership rules. These rules will connect the internally collected set with the host-defined sequence `it`.

```agda
    module VR = Of valR
```

The set `values` is the Replacement image of `ωʟ` under the relation `itFo`: it contains the finite iterate values, with repetitions automatically collapsed by sethood. It is a set of values, rather than the indexed function graph constructed below.

```agda
  values : S
  values = VR.table
```

Every host-defined iterate belongs to this value set. At the internal numeral `nn n`, membership follows from `nn n ∈ ωʟ` together with the finite-table witness `it-graph n`.

```agda
  values-in : (n : ℕ) → ⟨ fst (it n) ∈ fst values ⟩
  values-in n = VR.table-in (nn n) (it n) (#∈ω n) (it-graph n)
```

Every member of the value domain is, merely, some iterate value: the outward reading recovers the numeral representation and the iteration formula satisfaction, and the uniqueness lemma identifies the value.

```agda
  values-out : (y : S) → ⟨ y ∈ˢ values ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ fst (it n)) ∥₁
  values-out y hy = PT.rec squash₁
    (λ { (q , (q∈ , h)) → PT.map
      (λ { (k , eq) → k , itFo-val k y (itFo-at y (sym eq) h) }) (ω-num q q∈) })
    (VR.table-out y hy)
```

The union of the value domain is a set of `L`, formed by the model's union operation.

```agda
  iterUnion : S
  iterUnion = unionʟ values
```

Every member of a finite iterate belongs to `iterUnion`: first `values-in` places that iterate itself in `values`, and then the defining membership rule for union places each of its members in the union. Notice that this proves `it n ⊆ iterUnion`, rather than that `it n` itself is a member of `iterUnion`.

```agda
  iterUnion-in : (n : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ z ∈ˢ iterUnion ⟩
  iterUnion-in n z hz = unionʟ-in values z (it n) (values-in n) hz
```

Every member of the union merely lies in some finite iterate. The proof eliminates the union membership to find the intermediate set, packages it as constructible, and reads it through the value domain's outward reading.

```agda
  iterUnion-out : (z : S) → ⟨ z ∈ˢ iterUnion ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ fst z ∈ fst (it n) ⟩ ∥₁
  iterUnion-out z h = PT.rec squash₁
    (λ { (B , (hB , hz)) → PT.map
      (λ { (n , eB) → n , subst (λ w → ⟨ fst z ∈ w ⟩) eB hz })
      (values-out (B , isL-trans {x = fst values} {y = B} hB (snd values)) hB) })
```

The outer union rule yields an intermediate set `B` with `B ∈ values` and `z ∈ B`, still under propositional truncation. Transitivity of `L` supplies the constructibility witness needed to regard `B` as an element of `S`; `values-out` then identifies it with some `it n`, again without selecting an index outside the truncation.

```agda
    (unionʟ-out values z h)
```

## The indexed graph and finite growth

Besides the value set and its union, the same recursion record determines an internal function graph. Its elements retain both the numeral input and the corresponding iterate value, which is needed when later arguments must refer to a particular finite stage rather than merely to the set of all values.

```agda
  private
    module TR = RecursionGraph valR using ( F; F-in; F-out )
```

The function graph collects the ordered pairs of numerals and iterate values.

```agda
  iter : S
  iter = TR.F
```

Every canonical pair is a member of the graph, transported along the uniqueness of the replacement value.

```agda
  iter-in : (n : ℕ) → ⟨ pr (# n) (fst (it n)) ∈ fst iter ⟩
  iter-in n = subst (λ v → ⟨ pr (# n) (fst v) ∈ fst iter ⟩)
    (VR.val-uniq (nn n) (#∈ω n) (it n) (it-graph n)) (TR.F-in (nn n) (#∈ω n))
```

Conversely, every graph member is merely equal to a canonical pair `(# n, it n)` for some natural number `n`. The source supplied by the general graph rule and its numeral representation both remain under propositional truncation, and value uniqueness identifies the second component without exposing `n` outside that truncation.

```agda
  iter-out : (y : S) → ⟨ y ∈ˢ iter ⟩ → ∥ Σ[ n ∈ ℕ ] (fst y ≡ pr (# n) (fst (it n))) ∥₁
  iter-out y hy = PT.rec squash₁
    (λ { (q , q∈ , e) → PT.map (λ { (k , eq) → k
      , e ∙ cong₂ pr (cong fst (sym eq))
        (cong fst (VR.val-uniq q q∈ (it k) (itFo-at (it k) eq (it-graph k)))) }) (ω-num q q∈) })
```

The outward membership rule for the general graph first supplies a source `q ∈ ωʟ` and the encoded pair involving its unique value. Decoding `q` as a numeral and using value uniqueness turns this into the stated canonical pair, while the natural-number index remains under propositional truncation.

```agda
    (TR.F-out (fst y) hy)
```

The growth module is parameterized by the hypothesis that each set is contained in its own step.

```agda
  module Closure (grows : (x z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ fst (step x) ⟩) where
```

The growth hypothesis gives one-way containment between adjacent iterates: every member of `it n` also belongs to `it (suc n)`. No reverse containment, fixed-point property, or closure of `iterUnion` under `step` follows from this statement.

```agda
    it-mono : (n : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ fst z ∈ fst (it (suc n)) ⟩
    it-mono n z = grows (it n) z
```

Iterating the adjacent containment `k` times proves `it n ⊆ it (k + n)`. The induction measures the number of additional steps, so the result compares two explicitly separated finite stages; it asserts neither monotonicity of `step` with respect to arbitrary inclusions nor any closure property of their union.

```agda
    it-up : (n k : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ fst z ∈ fst (it (k + n)) ⟩
    it-up n zero    z h = h
    it-up n (suc k) z h = it-mono (k + n) z (it-up n k z h)
```