可构造宇宙中的 ω 递归

迭代序列是宿主层面关于自然数的递归：从 a 出发，把步进函数作用于前值。此处它只是 Agda 序列；其内部表示才是本章的工作。

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

零点子句说：在数码零处记录的每个值，其底层集都与起点相同。它并不声称零点处有值被记录。

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

后继子句说：只要表同时记录 (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'
       → x' .fst ≡ sucV (x .fst) → ⟨ (v' ∷ v ∷ []) ⊨ stepFo ⟩

向下子句说：在每个被记录条目之下，仅仅地存在某个被记录的值。它是定义域的完备条款，其结论因未选定见证而是截断的。

Down : S → Type (ℓ-suc ℓ)
Down F = (x' v' x : S) → Holds F x' v' → ⟨ x .fst ∈ x' .fst ⟩
       → ∥ Σ[ 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 ))
               ⇒̇ ∀̇ ( appAt (suc (suc f)) (suc zero) zero ⇒̇ (var zero ≐ con a) ) )

读取零点子句即在数码零处应用它，并把应用原子经充分性搬运，得到 Zero 的底层集等式。

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

反过来，宿主层的零点子句可填入对象语言公式。先沿前提 z = nn 0 改写被量化集合 z，再把零点处的图成员关系搬入应用原子，最后由该子句把其值认同为 a。

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

步进公式的改名使用两个槽位：第一个变元留在位置零，第二个移到位置二，从而四个被量化槽位可以环绕改名后的主体。

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

改名一致检查两个环境在被改名槽位上一致，而这些正是改名公式读取的位置。

  ag : ∀ {n} (γ : Vec 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} (γ : Vec 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) (γ : Vec 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) (γ : Vec 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) (γ : Vec S n) → ⟨ γ ⊨ downAt f ⟩ → Down (lookup f γ)
  down-out f γ h x' v' x p m = 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) (γ : Vec S n) → Down (lookup f γ) → ⟨ γ ⊨ downAt f ⟩
  down-in f γ h x' v' x p m = 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) (γ : Vec 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) (γ : Vec 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 
  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 = 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 → v .fst ≡ (it k) .fst
corr-val F (z , (s , d))     v h = z v h
corr-val F (z , (s , d)) (suc k) v h =
  rec₁ (setIsSet (v .fst) ((it (suc k)) .fst)) 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 → v .fst ≡ (it (suc k)) .fst
  read (u , hu) = cong (λ p → p .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 ⟩ → v .fst ≡ (it k) .fst
itFo-val k v h = rec₁ (setIsSet (v .fst) ((it k) .fst))
  (λ { (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 ((e (lower k)) .fst) (e (lower k) .snd))
    (λ k → stage-ord ((e (lower k)) .fst) (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 : ℕ) → ⟨ (e k) .fst ∈ Lset entryBound ⟩
  entry-in-bound k = Lset-mono (entryStages .snd .snd (lift k))
    (stage-mem ((e k) .fst) (e k .snd))

固定 n 后，表 Fn n 是由指标从 0 到 n 的条目对组成的有限集。公共上界证明所有这些有序对都属于同一个可构造层，因此有限集构造可将整张表打包为 L 的元素。

Fn : ℕ → S
Fn n = finSet (suc n) (λ i → (e (toℕ i)) .fst) ,
  FinOf.finSetL entryBound entryBound-ord
    (suc n) (λ i → (e (toℕ i)) .fst) (λ 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 ∈ (Fn n) .fst ⟩) (prʟ-fst (nn k) (it k))
  (finSet-in (suc n) (λ i → (e (toℕ i)) .fst) ((e k) .fst)
    ∣ fromℕ' (suc n) k (suc-≤-suc p)
    , cong (λ j → (e j) .fst) (toFromId' (suc n) k (suc-≤-suc p)) ∣₁)

向外读法把任何元素分解为有界索引及其迭代取值，均在截断下恢复。

Fn-out : (n : ℕ) (y : S) → ⟨ y ∈ˢ Fn n ⟩
       → ∥ Σ[ k ∶ ℕ ] ((k ≤ n) × (y .fst ≡ pr (# k) ((it k) .fst))) ∥₁
Fn-out n y h = 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 → (e (toℕ i)) .fst) (y .fst) h)

对的读法用 Kuratowski 对的单射性把有限表的任何条目分解为有界索引及其迭代取值。

Fn-pair : (n : ℕ) (x v : S) → Holds (Fn n) x v
        → ∥ Σ[ k ∶ ℕ ] ((k ≤ n) × ((x .fst ≡ # k) × (v .fst ≡ (it k) .fst))) ∥₁
Fn-pair n x v h = map₁ (λ { (k , (p , q)) → k , (p , pr-inj (sym (prʟ-fst x v) ∙ q)) })
  (Fn-out n (prʟ x v) (subst (λ w → ⟨ w ∈ (Fn n) .fst ⟩) (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 = rec₁ (setIsSet (v .fst) (a .fst))

为证明零点子句，从 nn 0 处的条目可读出某个数码等于 # 0 的指标 k。数码编码的单射性迫使 k = 0，随附的取值等式遂将记录值认同为 it 0 = a。

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

为证明步进子句，先在命题截断下读取两个表条目。由于 stepFo 的满足是命题，两层截断都可消去到这一目标中；余下只须证明两个指标相邻，并将两个值分别认同为相应的迭代。

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

第一次读取给出 k 后，第二次读取给出相邻行的指标 k'。两个见证始终位于以命题性满足判断为目标的消去之内；这样既守住截断边界，又能同时使用它们的指标等式与取值等式。

    outer (k , (_ , (ex , ev))) = rec₁ (((v' ∷ v ∷ []) ⊨ stepFo) .snd) inner (Fn-pair n x' v' hx'v')
      where
      inner : Σ[ k' ∶ ℕ ] ((k' ≤ n) × ((x' .fst ≡ # k') × (v' .fst ≡ (it k') .fst)))
            → ⟨ (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 → (it j) .fst) 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 = rec₁ squash₁ outer (Fn-pair n x' v' h)
    where
    outer : Σ[ k' ∶ ℕ ] ((k' ≤ n) × ((x' .fst ≡ # k') × (v' .fst ≡ (it k') .fst)))
          → ∥ Σ[ v ∶ S ] Holds (Fn n) x v ∥₁

更小索引的条目由有限表的向内读式产出，沿数码等式运输。

    outer (k' , (p' , (ex' , _))) = map₁
      (λ { (j , (j< , ej)) → it j
         , subst (λ t → ⟨ pr t ((it j) .fst) ∈ (Fn n) .fst ⟩) (sym ej)
             (Fn-in n j (≤-trans (<-weaken j<) p')) })
      (∈#-elim k' (x .fst) (subst (λ w → ⟨ x .fst ∈ 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 = map₁ (λ { (i , p) → lower i , S≡ p })

现在可以把 itFo 看作内部集合 ωʟ 上的全且单值的关系。记录 valR 将定义域、图关系与尚待给出的函数性证明打包；随后对该记录应用替换，即可在 L 中收集这些取值。

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

函数性由「仅存在的数码表示」装配：解码产出迭代取值，唯一性在解码出的数码处证明。

    ; funct = λ q q∈ → mereFunct itFo q (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 : ℕ) → ⟨ (it n) .fst ∈ values .fst ⟩
values-in n = VR.table-in (nn n) (it n) (#∈ω n) (it-graph n)

值域的每个元素仅是某次迭代的取值：向外读法恢复数码表示与迭代公式满足，唯一性引理认同取值。

values-out : (y : S) → ⟨ y ∈ˢ values ⟩ → ∥ Σ[ n ∶ ℕ ] (y .fst ≡ (it n) .fst) ∥₁
values-out y hy = rec₁ squash₁
  (λ { (q , (q∈ , h)) → 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) → ⟨ z .fst ∈ (it n) .fst ⟩ → ⟨ z ∈ˢ iterUnion ⟩
iterUnion-in n z hz = unionʟ-in values z (it n) (values-in n) hz

并的每个元素仅属于某次有限迭代。证明消去并的成员关系以找到中间集合，将其打包为可构造，再经值域向外读法读取。

iterUnion-out : (z : S) → ⟨ z ∈ˢ iterUnion ⟩ → ∥ Σ[ n ∶ ℕ ] ⟨ z .fst ∈ (it n) .fst ⟩ ∥₁
iterUnion-out z h = rec₁ squash₁
  (λ { (B , (hB , hz)) → map₁
    (λ { (n , eB) → n , subst (λ w → ⟨ z .fst ∈ w ⟩) eB hz })
    (values-out (B , isL-trans {x = values .fst} {y = B} hB (values .snd)) 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) ((it n) .fst) ∈ iter .fst ⟩
iter-in n = subst (λ v → ⟨ pr (# n) (v .fst) ∈ iter .fst ⟩)
  (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 ∶ ℕ ] (y .fst ≡ pr (# n) ((it n) .fst)) ∥₁
iter-out y hy = rec₁ squash₁
  (λ { (q , q∈ , e) → map₁ (λ { (k , eq) → k
    , e ∙ cong₂ pr (cong (λ p → p .fst) (sym eq))
      (cong (λ p → p .fst) (VR.val-uniq q q∈ (it k) (itFo-at (it k) eq (it-graph k)))) }) (ω-num q q∈) })

一般函数图的向外成员关系规则先给出一个源 q ∈ ωʟ，以及由它的唯一取值组成的编码有序对。将 q 解码为数码并使用取值唯一性，便得到所述正準有序对；自然数指标始终留在命题截断之下。

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

增长模块以「每个集合包含于自身步进」的假设为参数。

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

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

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