后续的凝聚论证需要搬运「某集合是给定序数处的可构造层」这一断言。初等性搬运的是公式，而不是外围定义的运算 Lset，所以本章构造一条有界的对象语言公式来识别同一个层关系，并以第三个集合作为全部辅助见证的公共界。

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

这一构造的经典性只来自一个固定的排中律实例。不过，有界存在公式仍被读作命题截断的存在，因此经典背景并不会把隐藏的诸表变成全局选定的数据。

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

固定宇宙层级 ℓ，并假设层级 ℓ-suc ℓ 上命题的排中律。本章的每条公式、读引理与最终正确性定理都相对于这一个显式经典假设陈述。

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

这里的对象语言只需要隶属、合取、真、假与有界量词；这些构造子都具有结构性的 Δ₀ 见证。稍后证明公式不含常元，便可把常元域改为空字母表，使最终的三变元公式成为无参公式，同时保留其自由变元。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀; δ-∧; δ-∃∈ )
open import FOL.Manipulation.ConstantOccurrences using ( countFo )
open import FOL.Manipulation.ConstantMapping using ( embed )

同一条有界公式既可在可构造载体内部读取，也可在外围累积层级中读取；Δ₀ 绝对性认同这两种读法。隶属归纳将由更低的表行验证当前表行，外延性则把由此得到的两个隶属蕴含化为层的相等。

open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀ )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr )

层 Lset b 由此前各层的可定义幂集组装而成：它的每个成员都来自某个满足 c ∈ b 的 𝒟ₒ (Lset c)，而每一份这样的贡献都属于 Lset b。向内与向外的隶属规则表达这两个方向；序数事实则保证后文使用的索引确实是层索引。

open import L.Constructible {ℓ} using
  ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; #∈ω )
open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc )
open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )

在模型内部识别一个可定义幂集，需要公式码、满足关系表与环境塔；有序对编码再把每个层索引同其记录值连接起来。这些辅助集合都将由同一个见证集 z 界住，从而使完整描述保持在 Δ₀ 中。

open import L.Coding.Expressions {ℓ} using ( sucAtL )
open import L.Coding.NumeralBound {ℓ} lem using ( module Bound )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )
open import L.Coding.Model {ℓ} using ( container )
open import L.Coding.Quantification {ℓ} using

在对象语言内部，不能用无界运算投影集合编码的有序对分量。这里改用有界的分量公式，在一个小容器中遍历并读取或填入该有序对。十个具名槽位保存编码描述所用的数码标签；每次新见证扩展环境时，对这些名称作移位便能保持槽位对齐。

  ( sh; i0; i1; i2; i3; i8; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9
  ; down; suc-out; suc-in; sndEx; sndAll; bothAll
  ; sndEx-out; sndAll-in; bothAll-in; fillSnd; useSnd; useBoth; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags; shN )
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; module Tower )

这里汇合了三类语义规格。层级表在一个界以下记录形如 (c,Lset c) 的有序对；满足描述识别一层上的真实码、环境与满足关系数据；可定义幂集描述则识别集合 𝒟ₒ (Lset c)。可靠性只会恢复表性质 Values 与 Entries，完备性则从精确规格 IsHier 出发。

open import L.Hierarchy {ℓ} lem using ( hierL-spec; IsHier; hier-out; hier-in; Values; Entries )
open import L.GCH.SkolemHull {ℓ} lem using ( module Cnt; erase-Δ₀; isOrd-at-p; Δ₀-isOrd-at-p; _⊨ₚ_ )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; sat-complete )
open import L.GCH.DefinablePowerSetDescription {ℓ} lem using ( defAt; def-sound; def-complete )

完备性需要一个包含全部辅助见证的公共层。若 γ 充分且 c ∈ γ，则 Lset γ 含有在 c 处所需的层级表、码集、满足关系表与环境塔；后继封闭还把下一层放入其中，而 ω ∈ γ 则供给全部十个有限数码标签。

open import L.GCH.AdequateStages {ℓ} lem using ( Adequate; module Adequate; module At; Lset∈suc )

环境是可构造集合组成的有限向量。引入一个有界见证时，它被放到向量前端，原有每个槽位都后移一位；有限索引把这些移位显式记录下来。正因如此，同一组层、表与界的名称才能穿过多层嵌套量词而保持不变。

open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _∷_; []; map; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.FinData using ( toℕ; weakenFin )

存在公式的满足只保留命题截断：它记录合适的数据存在，却忘去具体用了哪一份数据。因此后文每次消去都以命题为目标。这里隶属取命题值，而累积层级中集合的相等也是命题，所以证明所需的这两类结论都可作为合法目标。

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

十个有限标签由层级内部的 von Neumann 数码表示。零是空集，之后每个标签由集合论后继得到，而且十个数码都属于 ω。隶属读式把这些外围集合与它们作为可构造载体元素的呈现连接起来。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV; ω )

以 S 表示可构造模型的载体。它的元素由外围集合及其可构造性证明组成。所有隐藏的表与见证都在这一载体上量化；最终保留的可见槽位也分别呈现取值 a、层索引 p 与公共界 z。

open hPropStructure 𝒮ʟ using ( S )

L 内部的满足关系与外围层级中的满足关系使用不同结构，但当 Δ₀ 公式的参数来自 L 时，两种读法一致。引理 abs₀ 正是二者之间的桥。借助它，完备性可以在内部构造公式的满足，而可靠性可以把搬运后的公式读回外围的层相等。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_; abs₀ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
module SemVᵃ = FOL.Semantics 𝒮ᵥ

公式 defIn w z N body 用四层嵌套的有界存在量词，把满足关系表 T、码集 C、环境塔 E 与取值 d 放入 z。满足描述验证 w 处取值上的 T、C、E，可定义幂集描述把 d 认同为该取值的可定义幂集，而 body 则陈述对 d 的进一步要求。满足关系只保留这些见证的命题截断，并且该公式并不唯一刻画 z。

defIn : ∀ {k} → Fin k → Fin k → (Fin  → Fin k) → Formula S ( + k) → Formula S k
defIn w z N body =
  ∃̇∈ (var z) (∃̇∈ (var (sh  z)) (∃̇∈ (var (sh  z)) (∃̇∈ (var (sh  z))
    (satAt i3 (sh  w) i2 i1 (shN  N) ∧̇ (defAt i0 (sh  w) i3 i2 (shN  N) ∧̇ body)))))

内向包含式 intoAt 说，每个 x ∈ v 都由某个更早的层索引 c ∈ b 说明：f 中有一个有序对形的成员在 c 处记录取值 w，而 x 属于 w 的可定义幂集。其外层有界形状是 ∀[ x ∈ v ] ∃[ c ∈ b ] ...；余下的有界见证展开该表行以及识别这个幂集所需的数据。

intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
intoAt v b f z N =
  ∀̇∈ (var v) (∃̇∈ (var (sh  b)) (∃̇∈ (var (sh  f))
    (sndEx i0 i1 (defIn i0 (sh  z) (shN  N) (var i8 ∈̇ var i0)))))

反向包含式 overAt 遍历 c ∈ b，并遍历 f 中可呈现为有序对 (c,w) 的成员。对每个这样的呈现，w 的可定义幂集的每个成员都必须属于 v。该子句不讨论 f 中无法如此呈现的成员，因此不能把它读成从整个候选表中排除了任意垃圾成员。

overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
overAt v b f z N =
  ∀̇∈ (var b) (∀̇∈ (var (sh  f))
    (sndAll i0 i1 (defIn i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v))))))

合取式 stepAt 合并这两个包含。相对于 b 以下记录的有序对表行，intoAt 说明 v 没有额外成员，overAt 则说明可定义幂集的贡献一项不缺。表中取值的正确性是后续读引理另行要求的假设。

stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
stepAt v b f z N = intoAt v b f z N ∧̇ overAt v b f z N

approxAt 的前半给出覆盖性：每个 c ∈ b 在 f 中都有某个有序对形的表项。后半则在 f 的一个成员被呈现为 (c,w) 时检验 stepAt w c f z N。它并未断言 f 的每个成员都是有序对，也未断言每个被记录的第一分量都低于 b。因此，approx-out 恰好恢复 Values f b × Entries f b，既不恢复与整个层级图的相等，也不恢复全局的无垃圾性质。

approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
approxAt f b z N =
    ∀̇∈ (var b) (∃̇∈ (var (sh  f)) (sndEx i0 i1 ⊤̇))
  ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh  f) (sh  z) (shN  N)))

子句 hierAt a p f z N 把 p 以下的逼近与 p 处的最后一步连接起来。若逼近给出 Values 与 Entries，最后一步便把 a 认同为 Lset p；反过来，精确的层级表 IsHier p f 与充分的见证供应可以填入两个合取支。这就是最终三变元公式将在有界见证之后隐藏的局部层关系。

hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
hierAt a p f z N = approxAt f p z N ∧̇ stepAt a p f z N

标签子句把十个槽位钉在数码上：第一个槽位没有成员，故它是空集。

pins : ∀ {m} → (Fin  → Fin m) → Formula S m
pins N =
    ∀̇∈ (var (N f0)) ⊥̇
  ∧̇ ( sucAtL (N f0) (N f1) ∧̇ ( sucAtL (N f1) (N f2) ∧̇ ( sucAtL (N f2) (N f3)
  ∧̇ ( sucAtL (N f3) (N f4) ∧̇ ( sucAtL (N f4) (N f5) ∧̇ ( sucAtL (N f5) (N f6)

其余九个槽位由九条后继断言串联，于是十个槽位恰是数码零至九。

  ∧̇ ( sucAtL (N f6) (N f7) ∧̇ ( sucAtL (N f7) (N f8) ∧̇ sucAtL (N f8) (N f9) ))))))))

层级表的有界子句

为了在后续描述中使用这十个标签，对象语言中的固定条件必须与语义记录 Tags γ N 一致。接下来的两个引理证明两个方向：一个从 pins 读出数码等式，另一个由这些等式重建 pins。

module PinsRead {m : ℕ} (N : Fin  → Fin m) (γ : S ^ m) where

读取标签子句先证第一个槽位为空：它没有成员。

  pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N
  pins-out (h0 , hs) = go
    where
    q0 : fst (lookup (N f0) γ) ≡ # 
    q0 = extensionalV (λ y → ⇔toPath

空性是双向的外延性论证：第一个槽位的任何成员都会与假值子句矛盾，而空集本无成员。

      (λ y∈ → Empty.rec* (h0 (down (lookup (N f0) γ) y y∈) y∈))
      (λ y∈ → Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))))

辅助引理 up 沿数码链前进一步。若槽位 i 表示 # k 且 sucAtL i j 成立，则其可靠读法把槽位 j 认同为 sucV (# k)，因而认同为数码 # (suc k)。

    up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → fst (lookup i γ) ≡ # k
       → fst (lookup j γ) ≡ # (suc k)
    up i j k h q = suc-out i j γ h ∙ cong sucV q

从零的等式出发，前五条后继子句依次给出 q1 至 q5。因此，由 f1 至 f5 命名的槽位分别被认同为数码一至五。

    q1 = up (N f0) (N f1)  (hs .fst) q0
    q2 = up (N f1) (N f2)  (hs .snd .fst) q1
    q3 = up (N f2) (N f3)  (hs .snd .snd .fst) q2
    q4 = up (N f3) (N f4)  (hs .snd .snd .snd .fst) q3
    q5 = up (N f4) (N f5)  (hs .snd .snd .snd .snd .fst) q4

余下四条后继子句延续同一条链，给出 q6 至 q9。由此，槽位 f6 至 f9 分别被认同为数码六至九，数码读取也随之完成。

    q6 = up (N f5) (N f6)  (hs .snd .snd .snd .snd .snd .fst) q5
    q7 = up (N f6) (N f7)  (hs .snd .snd .snd .snd .snd .snd .fst) q6
    q8 = up (N f7) (N f8)  (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7
    q9 = up (N f8) (N f9)  (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8

记录 Tags γ N 要求对 Fin 10 的每个元素给出相应的数码等式。前四个情形返回 q0、q1、q2 与 q3，分别对应标签零至三。

    go : Tags γ N
    go zero = q0
    go (suc zero) = q1
    go (suc (suc zero)) = q2
    go (suc (suc (suc zero))) = q3

go 接下来的五个情形返回 q4 至 q8。这些模式写成嵌套后继，直接穷尽标签四至八，无须再引入算术论证。

    go (suc (suc (suc (suc zero)))) = q4
    go (suc (suc (suc (suc (suc zero))))) = q5
    go (suc (suc (suc (suc (suc (suc zero)))))) = q6
    go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7
    go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8

Fin 10 唯一剩余的情形是零的第九次后继，它返回 q9。至此，分类讨论供给了 Tags γ N 所需的全部十条数码等式。

    go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9

反过来，设这些槽位已经满足 Tags γ N。零槽位的任意假定成员都可沿标签等式搬运为空集的成员，因而不可能存在；同一组标签等式随后供给填入九条后继子句所需的数据。

  pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩
  pins-in tg =
      (λ x x∈ → Empty.rec (∅-empty (fst x) (∈∈ₛ {a = fst x} {b = ∅} .fst
                  (subst (λ u → ⟨ fst x ∈ u ⟩) (tg f0) x∈))))
    , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl

每条后继子句都先沿相应的数码等式改写两个标签槽，再应用后继公式的向内读法来重建。

    , ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl ))))))))
    where
    st : (j k : Fin ) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩
    st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j)))

固定一个环境 δ，其中十个具名槽位都具有所要求的数码值。以 Wv 表示 w 处的底层集合，以 Zv 表示 z 处的底层集合。前者是解释可定义性的层，后者则是必须容纳四个见证的公共界。

module DefInRead {k : ℕ} (w z : Fin k) (N : Fin  → Fin k) (body : Formula S ( + k))
  (δ : S ^ k) (tg : Tags δ N) where
  private
    Wv = fst (lookup w δ)
    Zv = fst (lookup z δ)

四个见证依次绑定为 T、C、E 与 d。由于每个新约束子都从环境前端扩展，主体在 d ∷ E ∷ C ∷ T ∷ δ 上求值。因此，其前四个槽位依次指向可定义幂集的取值、环境塔、码集与满足关系表。

  δ4 : (T C E d : S) → S ^ ( + k)
  δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ

读取 defIn 时，四个见证 T、C、E、d 外面的命题截断保持不变。其结论有意只保留 d ∈ z、d = 𝒟ₒ Wv，以及主体在扩展环境中成立。T、C、E 属于 z 的证明，以及内部的满足描述与幂集描述证明，都在导出这条较弱陈述时被消耗。

  defIn-out : ⟨ δ ⊨ defIn w z N body ⟩
            → ∥ Σ[ T ∈ S ] Σ[ C ∈ S ] Σ[ E ∈ S ] Σ[ d ∈ S ]
                (⟨ fst d ∈ Zv ⟩ × ((fst d ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁
  defIn-out = PT.rec squash₁ (λ { (T , (T∈ , h1)) → PT.rec squash₁ (λ { (C , (C∈ , h2)) →
    PT.rec squash₁ (λ { (E , (E∈ , h3)) → PT.map (λ { (d , (d∈ , (hs , (hd , hb)))) →

四层嵌套截断暴露见证之后，def-sound 把满足描述 hs 与可定义幂集描述 hd 合并起来。这里保留的唯一等式正是其结论 d = 𝒟ₒ Wv；主体的证明则原样继续传递。

      T , C , E , d , ( d∈ , ( def-sound i0 (sh  w) i3 i2 i1 (shN  N) (δ4 T C E d) (lookup w δ) refl tg hs hd
                             , hb )) })
      h3 }) h2 }) h1 })

反过来，要从语义数据证明 defIn，就必须显式给出真实见证：由 w 表示的可构造载体 W、四个集合及其属于 z 的证明、它们分别与真实满足关系表、码集、环境塔和可定义幂集的同一视，以及主体的证明。因此，这个方向所假设的数据多于向外读取有意保留的数据。

  defIn-in : (W : S) → Wv ≡ fst W → (T C E d : S)
           → ⟨ fst T ∈ Zv ⟩ → ⟨ fst C ∈ Zv ⟩ → ⟨ fst E ∈ Zv ⟩ → ⟨ fst d ∈ Zv ⟩
           → fst T ≡ fst (SatGraph.pairs W) → fst C ≡ fst (AllCodes W) → fst E ≡ fst (Tower.tower W)
           → fst d ≡ 𝒟ₒ (fst W) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩
  defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb =

在向内读法中，sat-complete 先证明真实的满足关系表、码集与环境塔满足 satAt。def-complete 再使用这一证明和给定的 d 的等式，证明可定义幂集子句。给定的主体证明补全合取，随后四个见证及其隶属证明被依次引入嵌套的命题截断中。

    ∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs
      , ( def-complete i0 (sh  w) i3 i2 i1 (shN  N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁
    where
    hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh  w) i2 i1 (shN  N) ⟩
    hs = sat-complete i3 (sh  w) i2 i1 (shN  N) (δ4 T C E d) W qw qT qC qE tg

谓词 Supply 说：对序数 c，defIn 所需的四个见证都已在公共界之内，即层 Lset c 的满足图、码集与环境塔，以及下一层 Lset (sucV c)。

Supply : (Zv : V ℓ) (c : V ℓ) → IsOrd c → Type (ℓ-suc ℓ)
Supply Zv c oc =
    ⟨ fst (SatGraph.pairs (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (AllCodes (LsetS c oc)) ∈ Zv ⟩
  × ( ⟨ fst (Tower.tower (LsetS c oc)) ∈ Zv ⟩

第四分量是下一层，正是逼近的后继一步所需的。

  × ⟨ Lset (sucV c) ∈ Zv ⟩ ))

现固定环境 γ 中一个拟议的层级步骤。以 Vv 表示拟议结果，以 Bv 表示此前索引组成的集合，以 Fv 表示候选表的底层集合。要问的是：一旦知道 Fv 中相关表行取值正确且确实存在，这两个有界包含是否迫使 Vv 等于 Lset Bv。

module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Vv = fst (lookup v γ)
    Bv = fst (lookup b γ)
    Fv = fst (lookup f γ)

以 Zv 表示公共界的底层集合。它控制可在何处找到辅助的满足关系、码、环境塔与可定义幂集见证。单步所求的等式本身不提及 Zv；这个界使描述能够成立，却不成为所得层取值的一部分。

    Zv = fst (lookup z γ)

在内向主体中，d 是由 defIn 识别的可定义幂集，而 x 是外层对 v 的有界全称量词引入的成员。原子主体陈述 x ∈ d。一旦把记录值 w 认同为 Lset c，这就成为对某个 c ∈ b 的 𝒟ₒ (Lset c) 的隶属。

    intoBody : Formula S ( + m)
    intoBody = defIn i0 (sh  z) (shN  N) (var i8 ∈̇ var i0)

over 主体是一条可定义幂集描述，其内层公式断言，被描述集合的每个成员都属于拟议的下一取值。这给出并集等式所需的反向包含。

    overBody : Formula S ( + m)
    overBody = defIn i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))

单步读引理另行假设：Bv 以下每条有序对表行都具有正确取值 (Values)，并且 Bv 以下每个索引都有其正準表行 (Entries)。恰在这两个假设下，stepAt 的两半给出相反方向的隶属蕴含，外延性遂得到 Vv = Lset Bv。这些假设只约束相关的有序对表行，并不排除候选表中无关的成员。

  step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv
  step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩
    fwd x x∈ = PT.rec (snd (x ∈ Lset Bv)) (λ { (c , (c∈ , h1)) → PT.rec (snd (x ∈ Lset Bv))

对正向包含，intoAt 给出层索引 c ∈ Bv、表中的有序对表行 (c,w)，以及包含 x 的可定义幂集值 d。假设 Values 把 w 认同为 Lset c，故 d = 𝒟ₒ (Lset c)；层的向内规则 Lset-in 随即把 x 从这一份贡献送入 Lset Bv。

      (λ { (q , (q∈ , h2)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (w , s , (eq , h3)) →
        PT.rec (snd (x ∈ Lset Bv)) (λ { (T , C , E , d , (d∈ , (qd , hx))) →
          Lset-in Bv (fst c) x c∈
            (subst (λ u → ⟨ x ∈ u ⟩)
              (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) })

嵌套存在式的各层读取都保持命题截断。sndEx-out 先从有序对形的表项中仅仅恢复第二分量 w，defIn-out 再仅仅恢复辅助数据，以及把 d 认同为 w 的可定义幂集的等式。每一层截断都直接消去到隶属命题 x ∈ Lset Bv。

        (DefInRead.defIn-out i0 (sh  z) (shN  N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) })
        (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) })
      h1 })
      (hi xS x∈)
      where

证明从外围成员 x ∈ Vv 出发，但公式是在可构造载体 S 上解释的。运算 down 利用这一隶属证明把 x 呈现为载体元素 xS；再把 xS 放到环境前端，便使新约束的槽位表示同一个底层集合 x。

      xS : S
      xS = down (lookup v γ) x x∈

step-out 的反向包含把真实层 Lset Bv 的成员送入拟议取值 Vv。它消去 Lset Bv 的截断层分解，把目标化归为更早层 δ，其中 x 属于该层的可定义幂集。

    bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩
    bwd x x∈ = PT.rec (snd (x ∈ Vv)) put (Lset-out Bv x x∈)
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩
      put (δ , (δ∈ , xD)) = PT.rec (snd (x ∈ Vv))

Lset-out 给出更早的索引 δ 后，完备性提供典范表条目 (δ, Lset δ)。over 子句施用于这条目，defIn-out 再把其中的有界集合 d 同认于 𝒟ₒ (Lset δ)。因此，其全称体把给定的 x 放入拟议取值 Vv。这个方向使用 Entries 提供的典范条目，无须另行诉诸 Values。

        (λ { (T , C , E , d , (d∈ , (qd , hsub))) →
          hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) })
        (DefInRead.defIn-out i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))
          (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg
          (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈))))

两个被命名的对象是编码实参与编码对：二者都沿其隶属证明下降而呈现为载体元素。

        where
        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)

该行的取值 w 从对呈现中读取，正是体的满足所消耗的分量。

        w : S
        w = sndS q δ (Lset δ) refl

步进子句的向内方向需要五条假设：界的序数性、拟议取值与界处层的等同、表在界处的正确性与完备性，以及把界的每个成员所需的辅助见证放进见证界的供给函数。证明分为两个合取项。

  step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv
          → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
          → ⟨ γ ⊨ stepAt v b f z N ⟩
  step-in ob vq vals ents sup = into , over
    where

into 合取项从拟议取值的成员 x 向外读取：界处层的截断分解名指更早序数与可定义幂集隶属，存在引入把它们填入两个有界量词。

    into : ⟨ γ ⊨ intoAt v b f z N ⟩
    into x x∈ = PT.rec squash₁ put (Lset-out Bv (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) vq x∈))
      where
      put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ fst x ∈ 𝒟ₒ (Lset δ) ⟩)
          → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh  b)) (∃̇∈ (var (sh  f)) (sndEx i0 i1 intoBody)) ⟩

这些嵌套有界存在量词的填充并不从命题截断中取出数据。证明把 δ 呈现为载体元素 c，用 Entries 把典范对呈现为 q，再由 fillSnd 提供有序对分解；余下的公式体就是 hb。每次构造都保留 ∃[]-syntax 内含的命题截断，因为满足关系本身是命题。

      put (δ , (δ∈ , xD)) =
        ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁
        where
        oδ : IsOrd δ
        oδ = mem-ord {A = Bv} ob δ δ∈

三个载体元素有不同的来源。隶属 δ ∈ Bv 把更早的索引呈现为 c；典范对属于表的证明把该对呈现为 q；而 δ 的序数性使 LsetS 能把层 Lset δ 呈现为 w。组装有界见证时，必须区分这三种来源。

        c : S
        c = down (lookup b γ) δ δ∈
        q : S
        q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
        w : S

这里的 w 是可构造载体中的真实层 Lset δ。在 δ 处应用供给假设，得到满足关系表、码集、环境塔与后继层都属于 Zv 的证明。有了这四个界及其定义等式，defIn-in 把余下义务归结为数学事实 x ∈ 𝒟ₒ (Lset δ)。

        w = LsetS δ oδ
        s = sup δ oδ δ∈
        hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩
        hb = DefInRead.defIn-in i0 (sh  z) (shN  N) (var i8 ∈̇ var i0)
               (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl

四个有界对象分别是真实的满足关系表、码集、环境塔与 Lset (sucV δ)。供给假设证明它们都属于 Zv，前三个对象则由自反等式同描述所要求的结构对齐。最后，Lset-suc δ 把第四个对象同认于 𝒟ₒ (Lset δ)，于是 x 原有的隶属可被运输到公式体中。

               (SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ))
               (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ)
               (subst (λ u → ⟨ fst x ∈ u ⟩) (sym (Lset-suc δ)) xD)

证明 over 合取项时，固定 c ∈ Bv、表的成员 q，以及把 q 呈现为有序对 (c,w) 的方式。正确性随即把 w 同认于 Lset c。余下目标对 y 一致：每个 y ∈ 𝒟ₒ w 都必须属于拟议取值 Vv。这正是把拟议取值同认于 Bv 处层所需的第二个包含关系。

    over : ⟨ γ ⊨ overAt v b f z N ⟩
    over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e →
      let wq : fst w ≡ Lset (fst c)
          wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈)
          oc : IsOrd (fst c)

c 的序数性承继自界；层被呈现为载体元素；供给函数在 c 处产出四个见证。

          oc = mem-ord {A = Bv} ob (fst c) c∈
          W : S
          W = LsetS (fst c) oc
          s' = sup (fst c) oc c∈
      in DefInRead.defIn-in i0 (sh  z) (shN  N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh  v)))

c 处的供给把真实的满足关系表、码集、环境塔与后继层都界定在 Zv 内，因此 defIn-in 可以建立可定义幂集描述。若 y 属于那里描述的集合，Lset-suc c 先把它化为 y ∈ 𝒟ₒ (Lset c)，再由 c ∈ Bv 通过 Lset-in 得到 y ∈ Lset Bv。最后沿 Vv ≡ Lset Bv 运输，便得到 y 属于拟议取值。

           (w ∷ s ∷ q ∷ c ∷ γ) tg W wq
           (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (fst c)) (suc-ord oc))
           (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (fst c))
           (λ y y∈d → subst (λ u → ⟨ fst y ∈ u ⟩) (sym vq)
             (Lset-in Bv (fst c) (fst y) c∈ (subst (λ u → ⟨ fst y ∈ u ⟩) (Lset-suc (fst c)) y∈d))))

逼近读取器以表、界、见证界、标签映射与环境为参数。三个底层集合一次性命名。

module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Fv = fst (lookup f γ)
    Bv = fst (lookup b γ)
    Zv = fst (lookup z γ)

步进体是在四个平移槽位处的步进子句。

    stepBody : Formula S ( + m)
    stepBody = stepAt i0 i1 (sh  f) (sh  z) (shN  N)

逼近子句的向外读法产出表在界处的正确性与完备性。谓词 P 记录对每个实参须证之事：其被记录取值是该实参处的层。请仔细注意所证与所未证：结果恰为 Values 与 Entries；它不说表中没有非对成员、也没有第一分量落在界外的条目。

  approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv
  approx-out (hd , hs) ob = vals , ents
    where
    P : V ℓ → Type (ℓ-suc ℓ)
    P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (fst w) ∈ Fv ⟩ → fst w ≡ Lset c

覆盖子句说：对每个 c ∈ Bv，仅命题截断地存在一个表成员，它呈现为第一分量是 c 的有序对。读取这个对会显出取值 w，并把原隶属证明运输到典范记号 pr c w 上。结果仍受命题截断，因此 entryOf 只为后续命题推理提供存在性，并不在全局选出一个取值。

    entryOf : (c : S) → ⟨ fst c ∈ Bv ⟩ → ∥ Σ[ w ∈ S ] ⟨ pr (fst c) (fst w) ∈ Fv ⟩ ∥₁
    entryOf c c∈ = PT.rec squash₁
      (λ { (q , (q∈ , h)) → PT.map (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ })
                              (sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) })
      (hd c c∈)

归纳步验证任意一条满足 c ∈ Bv 的被记录对 (c,w)。它的隶属证明使逼近的第二子句给出 stepAt w c；归纳假设提供 c 以下每个实参处的正确性，覆盖子句则将在这些位置提供相应的典范条目。于是 StepRead.step-out 可断定，被记录取值恰为 Lset c。

    step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
    step c IH c∈ w rec =
      StepRead.step-out i0 i1 (sh  f) (sh  z) (shN  N) env tg
        (useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents'
      where

证明现在把有关集合呈现在可构造载体中。隶属 c ∈ Bv 给出载体元素 cS，而 pr c (fst w) 属于表的假设给出 q。取值 w 已经是归纳谓词所接收的载体元素；接下来的环境把这三个呈现放入步进公式所要求的槽位。

      cS : S
      cS = down (lookup b γ) c c∈
      q : S
      q = down (lookup f γ) (pr c (fst w)) rec
      env : S ^ ( + m)

扩展环境为步进读法装配四个槽位。界的序数性把更小的实参限制到界以下，而更小实参处的正确性读取即归纳假设的限制。

      env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ
      in' : (y : S) → ⟨ fst y ∈ c ⟩ → ⟨ fst y ∈ Bv ⟩
      in' y y∈ = ob .fst {x = c} {y = fst y} y∈ c∈
      vals' : Values (lookup f γ) c
      vals' y w' y∈ rec' = IH (fst y) y∈ (in' y y∈) w' rec'

更小实参处的完备性以同一限制恢复：对每个更小实参，消耗其截断条目，而归纳假设的取值等式把典范条目运到位。

      ents' : Entries (lookup f γ) c
      ents' y y∈ = PT.rec (snd (pr (fst y) (Lset (fst y)) ∈ Fv))
        (λ { (w' , rec') → subst (λ u → ⟨ pr (fst y) u ∈ Fv ⟩) (IH (fst y) y∈ (in' y y∈) w' rec') rec' })
        (entryOf y (in' y y∈))

Bv 以下的正确性通过在外围累积层级中对底层实参 c 作隶属归纳而得。谓词 P c 以 c ∈ Bv 为条件；这项隶属既把定理限制在所需界内，又借助 Bv 的序数性，使每个更小实参都可使用归纳假设。把归纳结论施于任意被记录取值，便得到 Values。

    vals : Values (lookup f γ) Bv
    vals c w c∈ rec = ∈-induction {P = P} step (fst c) c∈ w rec

界处的完备性复合截断条目与刚证的正确性：取值等式把被记录条目运成典范条目。

    ents : Entries (lookup f γ) Bv
    ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ Fv))
      (λ { (w , rec) → subst (λ u → ⟨ pr (fst c) u ∈ Fv ⟩) (vals c w c∈ rec) rec })
      (entryOf c c∈)

逼近子句的向内方向从更强的语义假设出发：表在界处实现层级。这一不对称是有意的：向外方向只证两条表条件，而向内方向消耗完整的层级规格。

  approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ)
            → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc)
            → ⟨ γ ⊨ approxAt f b z N ⟩
  approx-in ob sp sup = dom , steps
    where

层级规格的向外读法说：每条被记录对的实参低于界，其取值等于该处的层。

    hout : (c w : S) → ⟨ pr (fst c) (fst w) ∈ Fv ⟩ → ⟨ fst c ∈ Bv ⟩ × (fst w ≡ Lset (fst c))
    hout = hier-out Bv ob (lookup f γ) sp

向内读法说：界以下每条典范对都被记录。

    hin : (c : S) → ⟨ fst c ∈ Bv ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ Fv ⟩
    hin = hier-in Bv ob (lookup f γ) sp

定义域合取项的证明：对界以下每个实参呈现其层，并把典范对注入表。

    dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh  f)) (sndEx i0 i1 ⊤̇)) ⟩
    dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁
      where
      w : S
      w = LsetS (fst c) (mem-ord {A = Bv} ob (fst c) c∈)

正準对沿其隶属证明下降而呈现为载体元素。

      q : S
      q = down (lookup f γ) (pr (fst c) (Lset (fst c))) (hin c c∈)

逼近的第二合取项须对表的每个成员 q，以及把 q 呈现为有序对 (c,w) 的每种方式成立。在这样的呈现下，精确的层级规格同时给出 c ∈ Bv 与 w ≡ Lset c，从而可在 c 处证明步进公式。这里并未断言候选表的任意成员都具有这种有序对呈现。

    steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩
    steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e →
      let rec : ⟨ pr (fst c) (fst w) ∈ Fv ⟩
          rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈
          c∈ : ⟨ fst c ∈ Bv ⟩

实参由层级向外读法低于界；序数性被承继；StepRead.step-in 接收全部五条假设，包括限制后的正确性与完备性及每个更小实参处的供给。

          c∈ = hout c w rec .fst
          oc : IsOrd (fst c)
          oc = mem-ord {A = Bv} ob (fst c) c∈
      in StepRead.step-in i0 i1 (sh  f) (sh  z) (shN  N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd)
           (λ d w' d∈ rec' → hout d w' rec' .snd)

在当前实参 c 以下，完备性来自 hier-in：序数界的传递性把 d ∈ c ∈ Bv 化为 d ∈ Bv，于是典范条目确实存在。辅助界有不同的来源：它们来自给定的供给函数 sup，并沿同一传递性论证限制到 c 以下。因此，层级规格提供表条目，而 sup 提供四个有界编码对象。

           (λ d d∈ → hin d (ob .fst {x = fst c} {y = fst d} d∈ c∈))
           (λ d od d∈ → sup d od (ob .fst {x = fst c} {y = d} d∈ c∈)))

层级读法有四个特殊槽位：拟议层 a、它的层索引 p、逼近表 f 与公共见证界 z。标签映射解释编码公式所用的十个数码位置，环境则为所有这些槽位提供载体元素。

module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Av = fst (lookup a γ)
    Pv = fst (lookup p γ)
    Zv = fst (lookup z γ)

层级公式的可靠性定理说：若公式成立且序数槽是序数，则层槽等于序数槽处的层。证明分别读取逼近与最后一步。

  hier-sound : ⟨ γ ⊨ hierAt a p f z N ⟩ → IsOrd Pv → Av ≡ Lset Pv
  hier-sound (ha , hs) op = StepRead.step-out a p f z N γ tg hs (ve .fst) (ve .snd)
    where
    ve = ApproxRead.approx-out f p z N γ tg ha op

层级公式的完备性定理取索引槽的序数性、层槽与层的等同、索引处的真实层级表与供给函数，构造满足。

  hier-complete : (op : IsOrd Pv) → Av ≡ Lset Pv → IsHier Pv (lookup f γ)
                → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Pv ⟩ → Supply Zv c oc)
                → ⟨ γ ⊨ hierAt a p f z N ⟩
  hier-complete op aq sp sup =
      ApproxRead.approx-in f p z N γ tg op sp sup

证明把层级规格的向内逼近与最后一步复合，后者的正确性与完备性子句在每个更小实参处由层级规格向外读取。

    , StepRead.step-in a p f z N γ tg op aq
        (λ c w c∈ rec → hier-out Pv op (lookup f γ) sp c w rec .snd)
        (hier-in Pv op (lookup f γ) sp) sup

读取逼近与完整层级

内部模块封存最终将在对象语言内表达可构造层级的公式。

module Inner where

十四槽环境以前十个数码标签开头。反复使用 weakenFin 会把各索引嵌入 Fin 14 而不改变其数值位置，因此 N14 占据零至九号槽。这与后文使用的具体环境一致，其中前十项正是冯·诺伊曼数码。

  N14 : Fin  → Fin 
  N14 k = weakenFin (weakenFin (weakenFin (weakenFin k)))

末尾四个槽位补全内部公式的数学数据：十号槽存放表 ff，十一号槽存放拟议层 aa，十二号槽存放其层索引 pp，十三号槽存放公共界 zz。因此，完整环境的顺序是十个标签，随后依次为 f、a、p 与 z。

  ff aa pp zz : Fin 
  ff = sh  (i0 {})
  aa = sh  (i0 {})
  pp = sh  (i0 {})
  zz = sh  (i0 {})

内部公式合取两项数学要求。pins N14 把前十个槽位固定为编码描述所需的数码标签；hierAt aa pp ff zz N14 则说 ff 逼近 pp 以下的层级，而 aa 是它在 pp 处的下一取值，所有辅助数据均由 zz 界定。不透明性把这条大型公式保留在已经证明的读引理之后。

  opaque
    inner : Formula S 
    inner = pins N14 ∧̇ hierAt aa pp ff zz N14

为证明有界性，检查器可以在此局部展开 inner，连同封存的描述 satAt 与 defAt。这一受限展开表明，大型合取只由原子式、联结词与有界量词构成。在这道证明边界之外，公式的数学内容通过读引理恢复，而不靠归约展开后的公式。

  opaque
    unfolding inner satAt defAt

经过局部展开，checkΔ₀ inner tt 给出结构性的 Δ₀ 见证：inner 中出现的每个量词都有界。这是对这条特定公式的句法核验，并不声称 checkΔ₀ 在两个方向上判定有界性。外围模块及其导出结果仍以 lem : LEM (ℓ-suc ℓ) 为参数。

    Δ₀-inner : Δ₀ inner
    Δ₀-inner = checkΔ₀ inner tt

封存公式的读法经由同一边界暴露。

  opaque
    unfolding inner

合取的向外读法是其两个合取项组成的对，因为合取就是一对命题。

    inner-out : (γ : S ^ ) → ⟨ γ ⊨ inner ⟩ → ⟨ γ ⊨ pins N14 ⟩ × ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩
    inner-out γ h = h

反过来，pin 子句与层级子句的证明正好构成满足其合取所需的两个分量。它与 inner-out 合在一起，给出后文所需的两个精确方向：既可从大型公式推出两个数学部分，也可在两部分均已证明时重新构造该公式。

    inner-in : (γ : S ^ ) → ⟨ γ ⊨ pins N14 ⟩ → ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ → ⟨ γ ⊨ inner ⟩
    inner-in γ h1 h2 = h1 , h2

对具有 suc n 个位置的外层环境，lastFin 表示其最后一个位置。在下文每次应用中，该位置都存放为新存在量词提供界的公共界集。有界量词引入的见证占据公式体中新添的最前位置，并不是 lastFin 所指的位置。

  lastFin : {n : ℕ} → Fin (suc n)
  lastFin {zero} = zero
  lastFin {suc n} = suc (lastFin {n})

操作 wrap 以存在量词约束公式体最前的见证位置，并要求该见证属于外层最后位置所命名的集合。因此，公式的元数减少一，而有界性保持。反复施用这一操作，会把十个数码标签与表逐个量化，并要求它们都属于公共界 z。

  wrap : {n : ℕ} → Formula S (suc (suc n)) → Formula S (suc n)
  wrap {n} φ = ∃̇∈ (var (lastFin {n})) φ

Δ₀ 见证在包裹下保持，因为有界存在量化本身就是有界构造。

  δ-wrap : {n : ℕ} {φ : Formula S (suc (suc n))} → Δ₀ φ → Δ₀ (wrap {n} φ)
  δ-wrap d = δ-∃∈ d

五步包裹消耗十个数码槽中的五个，把自由位置从十四逐次减到九。

  s13 = wrap {} inner
  s12 = wrap {} s13
  s11 = wrap {} s12
  s10 = wrap {}  s11
  s9  = wrap {}  s10

再五步包裹把自由位置从九减到四，只余层、序数索引、表与见证界。

  s8  = wrap {}  s9
  s7  = wrap {}  s8
  s6  = wrap {}  s7
  s5  = wrap {}  s6
  s4  = wrap {}  s5

第十一次包裹再次以 z 为界，用存在量词约束最后的辅助槽，即层级表 f。此时恰余三个自由位置，顺序为 (a,p,z)：拟议层、它的层索引与公共见证界。因此，three 是三元公式而不是句子；后续擦除步骤会移除其未使用的常元域，但不会移除这三个自由变元。

  three : Formula S 
  three = wrap {} s4

见证公式被包裹十一次，对应公共界内部引入的十一个有界存在量词。每次包裹增加一层 Δ₀ 见证，因此包裹后的公式始终有界。

  Δ₀-three : Δ₀ three
  Δ₀-three =
    δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap
      (δ-wrap (δ-wrap (δ-wrap (δ-wrap Δ₀-inner))))))))))

为了验证包裹后的公式不含常元，这项计算可以查看已密封的 inner、satAt 与 defAt 的定义。这样的局部展开只暴露化简出现次数所需的语法；在外围论证中，这些大型公式本身仍由各自的读引理与写引理来使用。

  opaque
    unfolding inner satAt defAt

three 的常元出现次数为零。它留下的三个位置是供 a、p 与 z 使用的自由变元，并非常元。为这项计算展开密封成分后，该等式按定义化简，因为公式中的每个词项都由变元构成。

    count-three : countFo three ≡ 
    count-three = refl

由于 three 不含常元，擦除把它的常元域从可构造载体改为空类型，同时保持其变元与量词结构。所得 erased 因而是无参公式，但元数仍为三；把它嵌回原常元域便恢复 three。

  erased : Formula (⊥* {ℓ-suc ℓ}) 
  erased = Cnt.erase three count-three

擦除也保持 Δ₀ 见证。它只改变已经不出现的常元符号，所以 three 中的每个有界量词仍然有界；同一项结构论证由此证明 erased 是 Δ₀ 公式。

  Δ₀-erased : Δ₀ erased
  Δ₀-erased = erase-Δ₀ three count-three Δ₀-three

在语义上，一层包裹是一份受命题截断的有界见证。若界中的每个成员 x 只要满足主体就能推出 P，则 unwrap 可把这项受截断的存在消去到 P 中。声明 P : hProp 恰好提供这种消去所要求的命题条件。

  unwrap : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) {P : hProp (ℓ-suc ℓ)}
         → ((x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ P ⟩)
         → ⟨ γ ⊨ wrap {n} φ ⟩ → ⟨ P ⟩
  unwrap φ γ {P} k h = PT.rec (snd P) (λ { (x , xz , hx) → k x xz hx }) h

wrap-in 由一个被点名的成员及其扩展处的主体满足构造有界存在，即有界存在量词的引入规则。

  wrap-in : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) (x : S)
          → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ wrap {n} φ ⟩
  wrap-in φ γ x m h = ∣ x , (m , h) ∣₁

描述可构造层的无参公式

可见公式 levelFo 有三个自由位置 (a,p,z)。它把「p 是序数」与「由 z 限界的已擦除层级描述」合取起来。因此，尽管可靠性的结论只提及 a 与 p，z 仍是一个自由输入。

levelFo : Formula (⊥* {ℓ-suc ℓ}) 
levelFo = isOrd-at-p ∧̇ Inner.erased

levelFo 的两个合取项都是 Δ₀ 公式，而 Δ₀ 类对合取封闭。因此，合取构造子把两份 Δ₀ 见证合成 Δ₀-levelFo，并未引入无界量词。

Δ₀-levelFo : Δ₀ levelFo
Δ₀-levelFo = δ-∧ Δ₀-isOrd-at-p Inner.Δ₀-erased

读取引理对任何无常元 Δ₀ 公式复合三条路径：从限制载体到外围层级的 Δ₀ 绝对性、空常元域嵌入下满足的不变性、以及空解释的唯一性。结果是两个满足命题的等式。

read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : S ^ n)
     → (δ ⊨ embed φ) ≡ (map fst δ ⊨ₚ φ)
read {n} {φ} dφ δ =
    AbsL.abs₀ (mapΔ₀ Empty.rec* dφ) δ
  ∙ embed-⊨ 𝒮ᵥ {K = S} fst φ (map fst δ)

这条路径的最后一项等式处理常元解释。由于常元域为空，任何这类解释都逐点等于空类型消去给出的解释。函数外延性把它认同于典范的空解释，于是前一步的嵌入比较最终到达同一无参公式的外围读法。

  ∙ cong (λ ι → SemVᵃ.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ)
         (funExt (λ b → Empty.rec* b))

向外序数读取把序数性原子的两个子句展开为：p 的底层集合的传递性，以及其每个成员的传递性；所有条目都经 p 的呈现降下。

ord-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ → IsOrd (fst p)
ord-out a p z h =
    ( λ {x} {y} y∈x x∈p → h .fst (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x )
  , ( λ x x∈p {y} {u} u∈y y∈x →
        h .snd (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x

对序数性的第二个子句，取 x ∈ p、y ∈ x 与 u ∈ y。把这三层隶属都降入可构造载体后，公式的第二个合取项推出 u ∈ x。这恰是 p 的每个成员 x 的传递性；连同第一个子句便得到 IsOrd p。

          (down (down (down p x x∈p) y y∈x) u u∈y) u∈y )

向内序数读取由序数性证明构造两个子句，所有条目都打包为 L 的元素。

ord-in : (a p z : S) → IsOrd (fst p) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩
ord-in a p z op =
    (λ x x∈p y y∈x → op .fst {x = fst x} {y = fst y} y∈x x∈p)
  , (λ x x∈p y y∈x u u∈y → op .snd (fst x) x∈p {x = fst y} {y = fst u} u∈y y∈x)

可靠性论证现在转入隐藏公式的十四槽位读法。它要丢弃受限界的辅助见证，同时保留这些见证的数学后果：槽位 a 中的值就是由槽位 p 索引的可构造层。

private
  module Sound where
    open Inner

finish 引理分开读取 inner 的两个合取项。pins 读引理把第一项化为层级读引理所需的十条数码等式。对于第二项中的逼近，hier-sound 只恢复 Values × Entries；再给出 p 的序数性后，这已足以把最后一步读成 a = Lset p。这里并未断言隐藏表不含畸形成员，也未断言其中没有基点落在 p 之外的条目。

    finish : (γ : S ^ ) → ⟨ γ ⊨ inner ⟩ → IsOrd (fst (lookup pp γ))
           → fst (lookup aa γ) ≡ Lset (fst (lookup pp γ))
    finish γ h op = HierRead.hier-sound aa pp ff zz N14 γ tg (inner-out γ h .snd) op
      where
      tg : Tags γ N14

被固定的数码由 pins 读式向外读取，从对象语言子句推导出十条数码等式。

      tg = PinsRead.pins-out N14 γ (inner-out γ h .fst)

内部可靠性引理从可构造载体的三个元素 a、p 与 z 出发，并假设 embed levelFo 在其上成立。它先用擦除逆等式恢复十一重包裹公式的满足。所求结论把 a 的底层集合与 p 的底层索引处的 Lset 相比较。

    sound-L : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed levelFo ⟩ → fst a ≡ Lset (fst p)
    sound-L a p z (ho , hφ) =
      go (subst (λ ψ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ ψ ⟩) (Cnt.erase-inv three count-three) hφ)
      where
      ordp : IsOrd (fst p)

序数性合取项经向外序数读取产生 p 的序数性证明，这是层级读式所需的剩余输入。

      ordp = ord-out a p z ho

需要保留的等式被组成命题 G。累积层级中的集合构成 h-集合，因此 setIsSet 证明该等式类型是 hProp。由此，每份受命题截断的有界见证都可被消去到 G 中，而不会暴露一个选定见证。

      G : hProp (ℓ-suc ℓ)
      G = (fst a ≡ Lset (fst p)) , setIsSet (fst a) (Lset (fst p))

可靠性逐一消去十一个有界存在，把截断的见证消耗为命题等式。消去的顺序镜像公式的绑定顺序。

      go : ⟨ (a ∷ p ∷ z ∷ []) ⊨ three ⟩ → ⟨ G ⟩
      go =
        unwrap s4 (a ∷ p ∷ z ∷ []) {G} λ F mF →
        unwrap s5 (F ∷ a ∷ p ∷ z ∷ []) {G} λ x9 m9 →
        unwrap s6 (x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x8 m8 →

接下来的五次消去恢复数码见证 x7 至 x3。每一步都在环境前端加入一个元素，而最后一个槽位始终是 z，也就是十一份见证共同来自的界。

        unwrap s7 (x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x7 m7 →
        unwrap s8 (x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x6 m6 →
        unwrap s9 (x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x5 m5 →
        unwrap s10 (x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x4 m4 →
        unwrap s11 (x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x3 m3 →

最内层见证完成消去：十四槽位环境连同序数性证明一起交给 finish 引理，产出两个底层集合的等式。

        unwrap s12 (x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x2 m2 →
        unwrap s13 (x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x1 m1 →
        unwrap inner (x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G}
          λ x0 m0 hm →
            finish (x0 ∷ x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) hm ordp

对于已知可构造的周遭集合 a、p 与 z，各自的可构造性证明把它们呈现为可构造载体的元素。反向读取 Δ₀ 绝对性，便把 levelFo 的周遭满足搬到这些呈现上的满足，从而可应用内部可靠性论证。投影回去后得到 a = Lset p。因此，三个输入全都可构造是显式假设，并非公式自身的结论。

level-sound : (a p z : V ℓ) → ⟨ isL a ⟩ → ⟨ isL p ⟩ → ⟨ isL z ⟩
            → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ levelFo ⟩ → a ≡ Lset p
level-sound a p z la lp lz h =
  Sound.sound-L (a , la) (p , lp) (z , lz)
    (subst ⟨_⟩ (sym (read Δ₀-levelFo ((a , la) ∷ (p , lp) ∷ (z , lz) ∷ []))) h)

为证明完备性，固定带有充分性数据的 lam 以及序数 p ∈ lam。序数性字段使 lam 成为层索引，其对应的层是 Lset lam；其余字段给出后继封闭、包含 ω，以及 lam 以下各处所需的编码见证。证明将用这些性质说明，特定的界 Lset lam 包含描述层 Lset p 所需的每份见证。

private
  module Complete (lam : V ℓ) (ad : Adequate lam) (p : V ℓ) (op : IsOrd p) (p∈λ : ⟨ p ∈ lam ⟩) where
    open Inner
    open Adequate lam ad using ( ord; succ; ω∈; wit )

充分层 lam 的传递性由其序数性提取：两个嵌套的隶属复合为一个。

    private
      tr : (x y : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ lam ⟩
      tr x y x∈ y∈ = ord .fst {x = x} {y = y} y∈ x∈

空集属于充分层，依据是对链 ∅ ∈ ω ∈ lam 施用的传递性。

      ∅∈λ : ⟨ ∅ ∈ lam ⟩
      ∅∈λ = tr ω ∅ ω∈ (#∈ω zero)

数码限界论证在 lam 处特化到可构造层级。由序数性、后继封闭与 ∅ ∈ lam 可得，每个模型数码的底层集合都属于 Lset lam。这给出稍后十个标签数码共同需要的界。

      module B = Bound lam ord succ ∅∈λ using ( num∈λ )

令 K = Lset lam。这是第三个自由输入 zS 所呈现的公共界集；层级表、十个数码，以及论证每一行所用的全部辅助集合，都必须证明属于 K。

      K : V ℓ
      K = Lset lam

若 c ∈ lam，后继封闭给出 sucV c ∈ lam。标准的后继层事实把 Lset c 放入 Lset (sucV c)，再沿 sucV c ∈ lam 使用单调性，便把这条隶属提升为 Lset c ∈ K。稍后把同一引理应用于 sucV c，并再用一次后继封闭，即可得到 Lset (sucV c) ∈ K；这才是在 c 行所需的可定义幂集见证。

      Lset∈K : (c : V ℓ) → ⟨ c ∈ lam ⟩ → ⟨ Lset c ∈ K ⟩
      Lset∈K c c∈ = Lset-mono {α = lam} {β = sucV c} (succ c c∈) (Lset∈suc c)

数码限界定理先把模型数码的底层集合放入 K。投影等式 numeralL-fst 把该集合认同于周遭的 von Neumann 数码 # k，沿此搬运便得 # k ∈ K。因此，十个数码见证与层级表满足同一个界。

      num∈K : (k : ℕ) → ⟨ # k ∈ K ⟩
      num∈K k = subst (λ u → ⟨ u ∈ K ⟩) (numeralL-fst k) (B.num∈λ k)

四个集合被命名：层 Lset p、序数 p、层 Lset lam、以及 p 处的层级表，各处于相应的载体中。

    aS pS zS F : S
    aS = LsetS p op
    pS = p , At.cL p op
    zS = LsetS lam ord
    F = At.hier p op

环境 E 现在记录完整的十四槽位赋值。从前到后依次是数码 0 至 9、p 处的真实层级表、预定值 Lset p、索引 p，以及公共界 Lset lam。这恰是 inner 读取数据的槽位次序。

    E : S ^ 
    E = nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn  ∷ nn 
      ∷ F ∷ aS ∷ pS ∷ zS ∷ []