Bedrock可构造宇宙中的 ω 递归
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图可构造集合上的可定义步骤与一个起点，通过宿主自然数上的递归确定一列有限次迭代。本章在 L 内表示每次迭代：有限的正确表证明内部数码处取值的存在性与唯一性，替换收集这些值及其带索引的图，并集则组成包含每个有限阶段所得成员的集合。
{-# OPTIONS --cubical --safe --guardedness #-}
打开基础库，并以全书一贯形式将排中律作为显式假设引入。
open import Base.Prelude open import Base.Classical using ( LEM )
模块固定宇宙层级并命名经典假设：下文每条定理都准确记录它消耗哪个层级的排中律实例。
module L.GCH.OmegaRecursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
迭代的描述用对象语言书写：公式由相等、合取、蕴涵以及无界存在与全称量词构成；公式改名与绝对性支持同一公式在不同环境下的读取。
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
外围层级供给隶属与数码，有序对的分量可单射恢复，可构造结构承载层机制及其传递性与单调性。
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 )
要把宿主序列化为 L 中的集合，需要四类内部构造：为可构造性提供界的层、容纳近似表的有限集、码化有序对与并，以及内部自然数集 ωʟ。借助这些构造，后文可从每个宿主指标各自的一张有限表，过渡到模型内部带索引的单一值域与图。
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 ( ωʟ )
递归接口把内部定义域上可在内部定义且取值唯一的关系打包起来。相应的图构造，以及表示应用、有序对和集合论后继的编码公式，稍后会把有限表的语义论证化为 L 上的一阶关系，再化为 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 )
自然数序、有界索引，以及有界索引与数码之间的转换，支撑本章的有限簿记。
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' )
下文若干同一视发生在依值对中：底层集合附带一个证明其可构造的命题。累积层级的 h-集合结构保证底层集合之间的等式是命题；和类型与二元搬运则处理解码有序对时出现的分支及同步代换。
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 )
层级的后继运算与截断机制补全各构造。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( sucV; #_ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
可构造载体连同其隶属被打开，因为每次迭代都是 L 的元素。
open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
绝对性读法以两个名字引入，用于在 L 内部于环境处读取公式。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
改名语义在恒等常元字母表下实例化，于是被改名的公式可在槽位重排后的环境中读取。
module Ren = Sat 𝒮ʟ id
载体是 h-集合，因为层级是 h-集合且可构造性是命题；因此可构造集合之间的相等是命题。
isSetS : isSet S isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
底层集合相等即可构造集合相等，依据是可构造性证明的命题性。每当等式先在底层集合层面获得时，就使用这一转换。
S≡ : {x y : S} → fst x ≡ fst y → x ≡ y S≡ = Σ≡Prop (λ v → snd (isL v))
编码图先记录输入、再记录值：Holds F x y 表示有序对 (x,y) 在底层集合层面属于 F。公式环境中的列表次序相反，因此输入为 x、输出为 y 的步进关系在 (y ∷ x ∷ []) 环境下读取。
Holds : S → S → S → Type (ℓ-suc ℓ) Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
自然数 k 的可构造数码把外围数码连同其可构造性打包；数码正是各次迭代将被记录的位置。
nn : ℕ → S nn k = # k , numL k
若一个元素的底层集合与 a 或 b 的底层集合相等，它便属于内部无序对 pairʟ a b。证明沿一条等式搬运这一二择分支；该等式把 pairʟ a b 的底层集合与外围无序对认同起来。
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 ∣₁)
要把 y 放入 A 的内部并，只需给出一个明确的可构造集合 B，满足 B ∈ A 且 y ∈ B。这两条隶属构成并集隶属的通常见证，再沿 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) ∣₁)
并中的隶属仅仅给出包含该元素的某个中间集合；中间集合是外围元素，自身不带可构造性证明。
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)
可定义步骤的有限次迭代
迭代模块收取全章的五份材料：起点、按「输出在前输入在后」次序的步进公式、实际的步进函数、「公式处处定义该函数」的证明，以及「只有该值满足公式」的证明。在整个载体上的全域性是数据的一部分。
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
迭代序列是宿主层面关于自然数的递归：从 a 出发，把步进函数作用于前值。此处它只是 Agda 序列；其内部表示才是本章的工作。
it : ℕ → S it zero = a it (suc n) = step (it n)
零点子句说：在数码零处记录的每个值，其底层集都与起点相同。它并不声称零点处有值被记录。
Zero : S → Type (ℓ-suc ℓ) Zero F = (v : S) → Holds F (nn 0) v → fst v ≡ fst a
后继子句说：只要表同时记录 (x, v) 与 (x', v')，且 x' 的底层集是 x 的后继，步进关系就在两个值之间成立。
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 ⟩
向下子句说：在每个被记录条目之下，仅仅地存在某个被记录的值。它是定义域的完备条款，其结论因未选定见证而是截断的。
Down : S → Type (ℓ-suc ℓ) Down F = (x' v' x : S) → Holds F x' v' → ⟨ fst x ∈ fst x' ⟩ → ∥ Σ[ v ∈ S ] Holds F x v ∥₁
正确近似是三条子句的合取。它刻意弱于「函数图的正确性」：既不固定精确定义域，也不施加唯一性。
Correct : S → Type (ℓ-suc ℓ) Correct F = Zero F × (Step F × Down F)
零点子句写成对象语言公式：对每个等于数码零的 z，以及在 z 处记录的每个值，该值都等于起点。
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) ) )
读取零点子句即在数码零处应用它，并把应用原子经充分性搬运，得到 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)
反过来，宿主层的零点子句可填入对象语言公式。先沿前提 z = nn 0 改写被量化集合 z，再把零点处的图隶属搬入应用原子，最后由该子句把其值认同为 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))
步进公式的改名使用两个槽位：第一个变元留在位置零，第二个移到位置二，从而四个被量化槽位可以环绕改名后的主体。
private ρ : ∀ {n} → Fin 2 → Fin (suc (suc (suc (suc n)))) ρ zero = zero ρ (suc zero) = suc (suc zero)
改名一致检查两个环境在被改名槽位上一致，而这些正是改名公式读取的位置。
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
后继子句全称量化表中的两个条目 (x,v) 与 (x',v')。层层嵌套的蕴涵先假设两个条目都出现在表中，再假设指标 x' 的底层集合是 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
在这三项前提下，结论是把 v' 与 v 联系起来的改名步进公式。改名从四个被量化变元中选出输出槽与输入槽，从而把有限表的相邻两行连接到原来的二元 step 定义。
⇒̇ ( sucAtL (suc (suc (suc zero))) (suc zero) ⇒̇ renameFo ρ stepFo ) ) ))))
改名路径由改名语义证明：改名公式在长环境处的满足等于原公式在短环境处的满足，因为两个环境在被改名槽位上一致。
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'))
读取后继子句逆着充分性搬运两个应用原子，应用四个全称量词，并使用改名路径。
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)
最后一项前提将 x' 认作 x 的集合论后继。它与两条表隶属关系合在一起，恰好构成比较相邻两行所需的假设，因此语义读法给出两行取值之间的步进关系。
(subst ⟨_⟩ (sym (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ))) s))
填充后继子句从宿主层的步进实例出发，反向运行同样的搬运。
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)
反过来，宿主层关于相邻两行的证明可满足对象语言子句：充分性等式将三项前提分别认同为两个编码条目与后继关系，而改名语义则恢复原来的二元步进公式。
(subst ⟨_⟩ (sucAtL-adequate (suc (suc (suc zero))) (suc zero) (v' ∷ x' ∷ v ∷ x ∷ γ)) s))
向下子句含有三个全称量词与一个存在量词。若表含有 (x',v')，且 x 属于 x' 的底层集合，公式便断言在 x 处记录了某个值；存在量词的语义只保留「这种值存在」这一命题。
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)))
该存在结论恰是一个被记录值的截断存在。
⇒̇ ∃̇ (appAt (suc (suc (suc (suc f)))) (suc zero) zero) ) )))
读取向下公式时，存在量词仍保留为命题截断。证明把截断中的每个见证值及其应用原子映到相应的宿主层图隶属，而不从截断外部选取见证。
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)
填充把搬运反向运行：从宿主层的截断条目到存在式的满足。
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)
对象语言中的正确性即三条子句的合取。
opaque corrAt : ∀ {n} → Fin n → Formula S n corrAt f = zeroAt f ∧̇ (stepAt f ∧̇ downAt f)
三个合取分量恰好恢复先前分别提出的 Zero、Step 与 Down 语义条件。尤其是，把公式读回数学陈述时，既不会引入定义域等式，也不会增加单值性假设。
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)
反向证明表明，这三个语义条件足以满足该合取。因此，corrAt 精确地一阶呈现了刻意较弱的 Correct 概念，而没有加强为「该近似已经是全函数图」的断言。
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)
公式 itFo 表示某个正确近似在指标 q 处记录值 y：在图的内部编码中，条目是有序对 (q,y)，而公式环境为 (y ∷ q ∷ [])。因此 itFo 并不陈述递归方程；它把由有限正确近似见证的关系内化。
opaque itFo : Formula S 2 itFo = ∃̇ ( corrAt zero ∧̇ appAt zero (suc (suc zero)) (suc zero) )
从 itFo 的满足只能恢复一个见证表 F 的命题截断，并在截断内得到 Correct F 及条目 (q,y)。因此，该公式证明合适的有限近似存在，同时刻意隐藏所用的是哪张近似表。
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 ) })
反方向上，任何包含 (q,y) 的特定正确近似都可见证 itFo(y,q)。该近似的身份立即被置于命题截断之下，所以后续论证可以使用存在性与唯一性，却不能抽取一张优先选定的表。
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 ) ∣₁
itFo 的满足沿「数码槽的等式」搬运；值槽保持不动。
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
唯一性引理按迭代指标分情形开始：在零点，零点子句直接给出等式；在后继，须先消去向下的截断见证。由于目标在 h-集合中是等式，消去合法。
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
在后继指标处，Down 在命题截断下给出前驱数码处记录的某个值。归纳假设将此前驱值认同为 it k；随后 Step 表明当前值与前驱值满足 stepFo，而 only 唯一确定当前值。
(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 ⟩)
归纳假设给出 u 与 it k 的底层集合相等。由于可构造性是命题，S≡ 将它提升为 S 中的等式，因此可把 stepFo 的输入替换为 it k。随后，子句 only 将 v 认同为 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)))
正準数码处的取值唯一：迭代公式在 nn k 处的任何满足，其所记录取值的底层集合都等于 it k 的底层集合。证明消去截断的正确表，并在该表内应用唯一性引理。
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)
每次迭代被呈现为模型元素：其数码与迭代自身组成的有序对，二者皆可构造。
private e : ℕ → S e k = prʟ (nn k) (it k)
所有条目层索引的公共上界序数由界引理施于条目对的层索引族而得。
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))
将这个公共序数上界记为 entryBound。命名它的意义在于，即使后续有限表的长度随 n 变化，每张表仍可在同一个层 Lset entryBound 中构造。
entryBound : V ℓ entryBound = entryStages .fst
该上界本身是序数，因而可以索引一个可构造层。这里不需要任何最小性结论：只要某个序数高于所有条目的层索引，就足以进行有限集构造。
entryBound-ord : IsOrd entryBound entryBound-ord = entryStages .snd .fst
每个条目都属于公共上界所索引的可构造层。具体而言，条目属于其自身的层，而 Lset 的单调性沿 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))
固定 n 后，表 Fn n 是由指标从 0 到 n 的条目对组成的有限集。公共上界证明所有这些有序对都属于同一个可构造层，因此有限集构造可将整张表打包为 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))
若 k ≤ n，正準条目 (nn k, it k) 就出现在 Fn n 中。因此，这张表包含在末指标 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)) ∣₁)
向外读法把任何成员分解为有界索引及其迭代取值，均在截断下恢复。
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)
对的读法用 Kuratowski 对的单射性把有限表的任何条目分解为有界索引及其迭代取值。
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))
有限表是正确的：三条子句由表条目的对读取装配。
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))
为证明零点子句，从 nn 0 处的条目可读出某个数码等于 # 0 的指标 k。数码编码的单射性迫使 k = 0，随附的取值等式遂将记录值认同为 it 0 = a。
(λ { (k , (_ , (ex , ev))) → ev ∙ cong (λ j → fst (it j)) (sym (#-inj 0 k ex)) }) (Fn-pair n (nn 0) v h)
为证明步进子句，先在命题截断下读取两个表条目。由于 stepFo 的满足是命题，两层截断都可消去到这一目标中；余下只须证明两个指标相邻，并将两个值分别认同为相应的迭代。
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 ⟩
第一次读取给出 k 后，第二次读取给出相邻行的指标 k'。两个见证始终位于以命题性满足判断为目标的消去之内；这样既守住截断边界，又能同时使用它们的指标等式与取值等式。
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'))) =
两次表读取分别将 v 认同为 it k、将 v' 认同为 it k'。两个位置之间的后继等式迫使 k' = suc k；完成这些认同后，所需的满足恰由 defines (it k) 给出。模型载体中的等式由 S≡ 获得，其中用到了可构造性证明分量是命题这一事实。
subst2 (λ p q → ⟨ (p ∷ q ∷ []) ⊨ stepFo ⟩) (S≡ (sym (ev' ∙ cong (λ j → fst (it j)) k'≡))) (S≡ (sym ev)) (defines (it k)) where
为得到 k' = suc k，将「第二个位置是第一个位置的后继」这一等式，与分别把两个位置认同为 # k' 和 # k 的等式合成。数码编码的单射性便把编码后有限序数的相等化为自然数指标的相等。
k'≡ : k' ≡ suc k k'≡ = #-inj k' (suc k) (sym ex' ∙ s ∙ cong sucV ex)
向下子句的证明由消去截断的对读取并找到已有正準条目的更小索引完成。
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 ∥₁
更小索引的条目由有限表的向内读式产出，沿数码等式运输。
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))
每条正準对都满足迭代公式，以各自的有限表为见证。每个目标数码都有自己的表；不主张任何单表同时服务所有位置。
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)
数码表示是自然数与「认同其为载体元素」的等式的显式对。
Num : S → Type (ℓ-suc ℓ) Num q = Σ[ k ∈ ℕ ] (nn k ≡ q)
从模型内部自然数集 ωʟ 的成员关系，只能在命题截断下恢复这种数码表示。这足以用于后续结论为命题的唯一性论证，却不会给出一个可供任意计算使用的自然数。
ω-num : (q : S) → ⟨ q ∈ˢ ωʟ ⟩ → ∥ Num q ∥₁ ω-num q = PT.map (λ { (i , p) → lower i , S≡ p })
现在可以把 itFo 看作内部集合 ωʟ 上的全且单值的关系。记录 valR 将定义域、图关系与尚待给出的函数性证明打包；随后对该记录应用替换，即可在 L 中收集这些取值。
private valR : Recursion valR = record { dom = ωʟ ; graph = itFo
函数性由「仅存在的数码表示」装配：解码产出迭代取值，唯一性在解码出的数码处证明。
; 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))
给定一个明确的表示 nn k ≡ q，取 it k 为纤维中心。先将图证明向前搬运到 q；对任何竞争取值，则将其证明反向搬运到 nn k，再由 itFo-val 认同。外围的 mereFunct 把这种带唯一性的中心之截断存在化为纤维的可缩性。
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)) )
与 valR 关联的一般替换构造现在给出一个收集其取值的集合，并附带精确的隶属规则。这些规则将内部收集所得的集合与宿主侧定义的序列 it 联系起来。
module VR = Of valR
集合 values 是 ωʟ 经关系 itFo 所得的替换像：它包含各次有限迭代的取值，而重复取值因集合性自然合并。它是取值集合，并非下文构造的带索引函数图。
values : S values = VR.table
每个宿主侧定义的迭代都属于这个取值集合。在内部数码 nn n 处，nn n ∈ ωʟ 与有限表见证 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)
值域的每个成员仅是某次迭代的取值：向外读法恢复数码表示与迭代公式满足，唯一性引理认同取值。
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)
值域的并由模型的并运算形成，是 L 的集合。
iterUnion : S iterUnion = unionʟ values
每次有限迭代的所有成员都属于 iterUnion：先由 values-in 将该迭代本身放入 values，再由并的隶属规则将它的每个成员放入并中。这里证明的是 it n ⊆ iterUnion，并非 it n 本身属于 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
并的每个成员仅属于某次有限迭代。证明消去并的隶属以找到中间集合，将其打包为可构造，再经值域向外读法读取。
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) })
并的向外规则在命题截断下给出一个中间集合 B，满足 B ∈ values 且 z ∈ B。L 的传递性补出把 B 视为 S 元素所需的可构造性见证；随后 values-out 将它认同为某个 it n，而指标仍不被选出命题截断之外。
(unionʟ-out values z h)
带索引的图与有限增长
除取值集合及其并之外，同一递归记录还确定一个内部函数图。图中的元素同时保留输入数码及相应的迭代取值，因而后续论证若须指称某个特定有限层，而不只是所有取值的集合，便可使用此图。
private module TR = RecursionGraph valR using ( F; F-in; F-out )
函数图收集数码与迭代取值组成的有序对。
iter : S iter = TR.F
每条正準对都是图的成员，沿替换取值的唯一性运输。
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))
反过来，图的每个成员都仅仅等于某个自然数 n 对应的正準有序对 (# n, it n)。一般图规则给出的源及其数码表示始终留在命题截断之下，而取值唯一性认同第二分量，却不会把 n 暴露到截断之外。
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∈) })
一般函数图的向外隶属规则先给出一个源 q ∈ ωʟ，以及由它的唯一取值组成的编码有序对。将 q 解码为数码并使用取值唯一性，便得到所述正準有序对；自然数指标始终留在命题截断之下。
(TR.F-out (fst y) hy)
增长模块以「每个集合包含于自身步进」的假设为参数。
module Closure (grows : (x z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ fst (step x) ⟩) where
增长假设给出相邻迭代之间的单向包含：it n 的每个成员也属于 it (suc n)。该结论不蕴含反向包含、不动点性质，也不蕴含 iterUnion 对 step 封闭。
it-mono : (n : ℕ) (z : S) → ⟨ fst z ∈ fst (it n) ⟩ → ⟨ fst z ∈ fst (it (suc n)) ⟩ it-mono n z = grows (it n) z
将相邻包含重复 k 次可得 it n ⊆ it (k + n)。归纳变量是额外步数，因此结论比较的是两个以明确步数分隔的有限层；它既不主张 step 对任意包含关系单调，也不主张这些层的并具有任何封闭性。
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)