Bedrockω-recursion inside the constructible universe
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapA 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.
{-# 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
The absoluteness reading is imported under two names, for formulas read inside L at environments.
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.
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.
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.
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 ∷ []).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
⇒̇ ( 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.
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.
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.
(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.
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.
(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.
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.
⇒̇ ∃̇ (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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(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).
(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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
(λ { (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.
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.
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.
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.
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.
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.
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.
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.
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.
ω-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.
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.
; 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.
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.
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.
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.
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.
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.
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.
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.
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.
(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.
private module TR = RecursionGraph valR using ( F; F-in; F-out )
The function graph collects the ordered pairs of numerals and iterate values.
iter : S iter = TR.F
Every canonical pair is a member of the graph, transported along the uniqueness of the replacement value.
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.
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.
(TR.F-out (fst y) hy)
The growth module is parameterized by the hypothesis that each set is contained in its own step.
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.
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.
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)