BedrockL 内部的可构造层级
可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。
阅读指南 · 依赖地图L 内的一阶图记录外部的可构造层级，直至给定序数。表中的值与外部层级逐一对照，被证明具有函数性且精确；随后这些对被收集成一个可构造集合，其成员恰是此前各层。
本章构造内部层级。对层级中的序数 α，hierL 在 α 处是 L 的一个元素，其成员恰是有序对「低于 α 的序数 β 与塔在该处的取值 Lset β」。全章重复同一个模式。表是有序对之集；说它在集合 B 上正确，指它在 B 以下记录的每个取值都是元层面的塔在那里的取值；说它完备，指它在以下的每个实参处都记录了取值。正确且完备的表，恰是图的步进条件所读出的内容，也恰是步进条件据以写下的内容；因此连接步进与塔的那对引理同时服务于消去与引入。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Hierarchy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
本章在模型自身层级的后继处取一份排中律实例并在其下运行；以下每个构造都陈述于本模块之内，只在公理章传递之处携带这一假设。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula ) import FOL.Absoluteness import FOL.ZFModel
这里有两个结构。环境层级贡献其结构 𝒮ᵥ，本章将使用它的隶属归纳与外延性；可构造结构 𝒮ʟ 贡献载体 S，其元素是层级中的集合连同「其可构造」的证明，故每个载体元素 x 都有底层集合 fst x。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Coding {ℓ} using ( pr; pr-inj )
层级给出全章使用的三件工具：沿隶属的归纳、集合的外延性，以及有序对 pr 连同找回其分量的单射性。这个对住在层级那一层，而表的被记录条目也住在那里。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; Lset; Lset-in; Lset-out; IsOrd )
可构造一侧给出塔 Lset，它把层级的一个序数送到该处的可构造层；可定义幂集 𝒟ₒ；两条隶属读式 Lset-in 与 Lset-out；序数性 IsOrd；以及「可构造性沿隶属传递」这一事实。塔由序数索引，序数是层级的集合；从不由宇宙层级索引，后者是类型的大小指标。
open import L.Ordinal {ℓ} using ( mem-ord ) open import L.Axioms.Basic {ℓ} using ( LsetS; isL-𝒟ₒ ) open import L.Axioms.Full {ℓ} lem using ( hasReplacementL ) open import L.Recursion {ℓ} lem using ( mereFunct )
另有三件事实支撑全章：序数的成员是序数；一个层可以呈现为 L 的元素，记作 LsetS，且可构造集合的可定义幂集仍可构造；以及 L 内部可用替换，其形式接受「仅知唯一存在」的取值。
模型贡献它自己的有序对 prʟ，连同识别其第一投影的读式 prʟ-fst，以及定义域子句 domAt-intro。
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; domAt-intro )
前一编码章贡献本章要组装的词汇：带见证与三条读式的步进条件，带定义域、取值与步进子句的逼近，有两条读式的塔之图，以及有序对图。
open import L.Coding.HierarchySequence {ℓ} lem using ( StepAt; StepOf; PowOK; StepAt-in; StepAt-out; StepAt-back ; ApproxAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step; ApproxAt-in ; LsetGraphAt; LsetGraph-in; LsetGraph-out; GraphOf ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )
命题机制是常用的那一套：截断的存在、其注入与消去、「第二分量为命题的序对在第一分量相等时即相等」，以及把隶属的逐点等价转成集合路径的操作。
open import Cubical.Data.Sigma using ( Σ≡Prop ) open import Cubical.Foundations.HLevels using ( isProp× ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
层级自身以类型的身份出现：其元素正是本章制表的对象，其隶属是三个条件所谈论的关系，而其 h-集合性使两个被制表集合的相等成为命题。
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
在可构造结构内部，S 是载体，⊨ 是满足判断；SetOf 把候选集合与「它实现一个类」的断言配成对，record 的各字段正是以这种形式陈述其公理。
open hPropStructure 𝒮ʟ module ModelL = FOL.ZFModel 𝒮ʟ open ModelL using ( SetOf )
满足关系最终在可构造结构处读取：全章的记号 γ ⊨ φ 都是在载体元素的环境处、以取自 L 的常元判断对象语言公式。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
一个私有辅助把变元槽后移两位：当一步要在「先加取值、再加实参」而扩展的环境中判读时，所有旧槽都后移两位。凡从表自身的条目内部判读该表的步进时，它都会出现。
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i)
表记录什么
表是有序对之集，这里总是取层级配对所成的对：一个实参连同一个取值。三个条件刻画表在界集 B 上的样子，它们是互补的条件，而不是同一句陈述的三种读法。Values 要求：在 B 以下记录的每个取值都是塔在那里的取值。Entries 要求：B 以下的每个实参处都记录了正準条目。Domain 要求：B 以外的东西完全没有被记录。
Values : S → V ℓ → Type (ℓ-suc ℓ) Values h B = (c z : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → fst z ≡ Lset (fst c)
正确性是关于被记录条目的陈述。若「B 以下的实参 c 与某个 z 组成的对」是表的一条目，则 z 就是塔在 c 处的取值。隶属 fst c ∈ B 是层级中的隶属，因为 B 是层级的集合；表 h 是载体元素，fst h 是它呈现的那个集合。
Entries : S → V ℓ → Type (ℓ-suc ℓ) Entries h B = (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩
完备性是关于覆盖范围的镜像要求：在 B 以下的每个实参 c 处，典范条目，即 c 与塔值 Lset c 组成的对，都被记录。两个条件合起来，正确且完备的表在 B 以下记录的恰是那些典范条目，没有任何走样。
Domain : S → V ℓ → Type (ℓ-suc ℓ) Domain h B = (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩
这些条件分开保留，因为各应用所需的子集不同。对逼近的归纳只用前两条，且用不了第三条：逼近的诸条目落在它自己的定义域以下，而不落在归纳所处的那个实参以下。内部层级将三条全有，因为它就是按「恰好是那些对的集合」构造的。还要注意 B 是什么：它是底层界集，层级中的一个集合。在语义应用中，它经由环境的某个槽位到来，是载体元素的底层部分，而该载体元素另外携带可构造性；B 的序数性是一条独立的假设，不由这些条件供给。此处制表的层是层级的集合、由序数索引；宿主的宇宙层级从不进入制表。
与外部层级对照的步骤
本节把上一章的步进条件与塔连接起来。实参 b 处的步进，沿 b 以下的诸实参 c 与在其处记录的诸取值 w，收集 w 的可定义幂集的成员。塔在 b 处收集的成员与之相同，只是把被记录的 w 换成 Lset c。三个私有事实为对照做准备：ok 解除旁条件 PowOK，below 把塔的一次分解变成步进见证，above 把步进见证变成塔的成员。
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where private
三个槽位命名取值、实参与表，全部从同一环境 γ 的载体元素读出。
ok : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → PowOK b f γ
旁条件被一次性解除，同时服务两个方向。PowOK 要求：每个被记录取值的可定义幂集是 L 的元素；而被记录取值是塔在 B 以下某个实参处的取值，该实参因 B 是序数而是序数，且以序数为索引的层，其可定义幂集可构造。故那一步所需的全部，就是正确性加上单独一条序数性假设，而两种读法的陈述里都不带该条件。两个方向分开命名，因为它们分开使用。向上是「被记录取值的可定义幂集落在 B 处的塔里面」，即 Lset-in。向下是塔自身的分解 Lset-out，随后把分解给出的序数记为模型的元素，这一步由类的传递性供给。
ok ob vals c z rec = subst (λ u → ⟨ isL (𝒟ₒ u) ⟩) (sym (vals c z (rec .fst) (rec .snd))) (isL-𝒟ₒ (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) (rec .fst)))
证明把两条假设拼起来。见证 rec 说 c 在实参以下，于是由实参的序数性，c 是序数；正确性把被记录的取值同认于塔在 c 处的取值；而可构造层的可定义幂集可构造，这正是 isL-𝒟ₒ。两行 transport 把两条事实对齐到同一个取值上。
below : IsOrd (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → (z : S) → Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ fst z ∈ 𝒟ₒ (Lset δ) ⟩) → StepOf b f γ z
below 把塔的一次分解变成步进见证。塔在 b 处分解它的每个成员：成员 z 坐在某个 δ (b 以下) 处的层的可定义幂集里。见证须指名一个低于实参的实参，以及一个其幂集含有 z 的被记录取值。
below ob ents z (δ , (δ∈ , hz)) = d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))
见证在实参 d，即 δ 的载体元素处给出：由完备性，表在该处记录典范条目。那里的被记录取值是 δ 处的层 (呈现为 L 的元素)，而由分解，z 落在其可定义幂集中。
where oδ : IsOrd δ oδ = mem-ord {A = fst (lookup b γ)} ob δ δ∈ d : S d = δ , isL-trans {x = fst (lookup b γ)} {y = δ} δ∈ (lookup b γ .snd)
两个簿记事实完成构造。δ 的序数性由 b 的序数性而来，因为序数的成员是序数；δ 可构造，因为它属于实参底层那个可构造集合。载体元素 d 把集合与这份证书打包在一起。
above : Values (lookup f γ) (fst (lookup b γ)) → (z : S) → StepOf b f γ z → ⟨ fst z ∈ Lset (fst (lookup b γ)) ⟩
above 是镜像：步进见证把一个成员放进塔里。见证指名低于实参的实参 c、其处被记录的取值 w，以及 z 属于 w 之可定义幂集的成员资格。
above vals z (c , (w , (rec , hz))) = Lset-in (fst (lookup b γ)) (fst c) (fst z) (rec .fst) (subst (λ u → ⟨ fst z ∈ 𝒟ₒ u ⟩) (vals c w (rec .fst) (rec .snd)) hz)
正确性把被记录的 w 同认于塔在 c 处的取值，于是 z 落在那个层的可定义幂集中；再由塔的向上读式，借助见证所携带的 c 之序数性，把 z 放进 b 处的塔里。
step-Lset : ⟨ γ ⊨ StepAt v b f ⟩ → IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → fst (lookup v γ) ≡ Lset (fst (lookup b γ))
向上引理读作：若步进条件在该环境处成立、实参是序数、且表在其上正确而完备，则在取值槽位记录的取值就是塔在实参处的取值。
step-Lset h ob vals ents = extensionalV {a = fst (lookup v γ)} {b = Lset (fst (lookup b γ))} pt where
层级中成员相同的两个集合相等，这是环境层级的外延性。证明给出逐点等价 pt，把路径的组装交给外延性。
fwd : (x : V ℓ) → ⟨ x ∈ fst (lookup v γ) ⟩ → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩ fwd x hx = PT.rec (snd (x ∈ Lset (fst (lookup b γ)))) (above vals z) (StepAt-out v b f γ h (ok ob vals) z hx)
向前方向：被记录取值的成员 x 给出一个步进见证，因为步进条件成立；该见证被消去到「x 属于塔」这条命题中，而 above 由见证证明这条命题。
where z : S z = x , isL-trans {x = fst (lookup v γ)} {y = x} hx (lookup v γ .snd)
要应用 above，须把 x 视为载体元素；其可构造性由被记录取值的可构造性而来，因为 x 是它的成员。
bwd : (x : V ℓ) → ⟨ x ∈ Lset (fst (lookup b γ)) ⟩ → ⟨ x ∈ fst (lookup v γ) ⟩ bwd x hx = PT.rec (snd (x ∈ fst (lookup v γ))) put (Lset-out (fst (lookup b γ)) x hx)
向后方向：塔分解它的每个成员 x，给出低于实参的一个层，其可定义幂集含有 x。该分解被消去到「x 属于被记录取值」这条命题中。
where z : S z = x , isL-trans {x = Lset (fst (lookup b γ))} {y = x} hx (LsetS (fst (lookup b γ)) ob .snd)
这里同样要把 x 载入：其可构造性由属于实参处的层而来，而该层的 L 元素呈现正是取序数性 ob 的 LsetS。
put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ fst (lookup b γ) ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ fst (lookup v γ) ⟩ put s = StepAt-back v b f γ h (ok ob vals) z (below ob ents z s)
分解经 below 变成步进见证，而步进条件的向后读式 StepAt-back 把见证变成对被记录取值的隶属。
pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ Lset (fst (lookup b γ))) pt x = ⇔toPath (fwd x) (bwd x)
对每个成员而言，属于被记录取值与属于塔是同一命题；两个方向给出等价，外延性再逐成员把它提升为集合的相等。
step-table : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ)) → Entries (lookup f γ) (fst (lookup b γ)) → fst (lookup v γ) ≡ Lset (fst (lookup b γ)) → ⟨ γ ⊨ StepAt v b f ⟩
向下引理把方向反过来：给定实参的序数性、正确性、完备性，以及「被记录取值就是塔」这一事实，步进条件即告成立。
step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back where
步进条件由它的两个方向引入：每个成员都有见证，且每个见证都可靠；旁条件由 ok 一并供给。
into : (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁ into z hz = PT.map (below ob ents z) (Lset-out (fst (lookup b γ)) (fst z) (subst (λ u → ⟨ fst z ∈ u ⟩) q hz))
被记录取值的成员 z 先沿同认 q 运入塔中，再由塔分解，而 below 把分解变成见证；见证只需存在即可。
back : (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩ back z s = subst (λ u → ⟨ fst z ∈ u ⟩) (sym q) (above vals z s)
反过来，见证经 above 把 z 放进塔里，而运输沿 q 反向进行。
逼近所记录的每个值
一次归纳，在实参上，在元语言中，逼近与它的定义域保持固定。动机说：逼近在这个实参处所记录的任何取值，都是元层面的塔在那里的取值。动机对一切被记录的取值作量化，而这正是单值性在任何地方都不作为假设的原因。在同一个实参处记录的两个取值都被钉在同一个塔值上，故两者相等；被记录取值的唯一性由归纳读出，而非假设。
归纳的步进就是 step-Lset 施于被记录的那个取值。实参以下的正确性就是归纳假设，一字不差。实参以下的完备性则是逼近的取值子句被花掉之处：比这个实参更低的实参落在逼近的定义域以下，因为定义域是序数、而序数传递；逼近于是在那里有取值；而归纳假设把它与塔的取值认同。那个取值只是「仅仅」被拿出来的，而这已经够了，因为要对它证的是一条隶属关系。
module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where private Value : V ℓ → Type (ℓ-suc ℓ) Value u = ⟨ isL u ⟩ → (z : S) → ⟨ pr u (fst z) ∈ fst (lookup f γ) ⟩ → fst z ≡ Lset u
动机 Value u 说：对可构造的 u，表中第一分量为 u 的每条记录都记录塔在 u 处的取值。「u 可构造」这一前提之所以被携带，是因为表的条目是载体元素，其第一分量是可构造集合；归纳将从某个序数中的隶属供给这一前提。
approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ)) → (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst (lookup f γ) ⟩ → fst z ≡ Lset (fst x) approx-val h oa x = ∈-induction {P = Value} go (fst x) (snd x)
定理对 x 的底层集合作归纳，x 正是所问其被记录取值的那个实参。隶属归纳在层级中直接可用：要证 u 的动机，就证 u 的每个成员的动机。关于 a 的序数性假设将在归纳步内被消耗。
where go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u go u IH hu z p = step-Lset zero (suc zero) (sh2 f) (z ∷ d ∷ γ) (ApproxAt-step f a γ h d z p) ou vals ents
归纳步就是把 step-Lset 施于逼近自己的步进子句。这一步在「加入取值 z、再加入实参 u」的扩展环境处判读，因此步进的三个槽位后移两位，这正是 sh2 所做的事。结论恰是动机：被记录的 z 就是塔在 u 处的取值。
where d : S d = u , hu u∈a : ⟨ u ∈ fst (lookup a γ) ⟩ u∈a = ApproxAt-dom f a γ h d z p
取值与实参以载体元素的身份旅行：d 把 u 与可构造性 hu 打包。逼近的定义域子句证明 u 低于实参 a，归纳之所以能够到达这一步，全凭于此。
ou : IsOrd u ou = mem-ord {A = fst (lookup a γ)} oa u u∈a
u 的序数性由 a 的序数性而来，因为 u 是 a 的成员；这正是该步所需要的关于其所处实参的全部。
vals : Values (lookup f γ) u vals c y c∈ q = IH (fst c) c∈ (snd c) y q
u 以下的正确性就是归纳假设，按原样使用：对 u 的成员 c，第一分量为 c 的被记录对所记录的是塔在 c 处的取值。c 的可构造性随归纳而来，归纳由隶属供给它。
ents : Entries (lookup f γ) u ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ))) named (ApproxAt-value f a γ h c (oa .fst {x = u} {y = fst c} c∈ u∈a))
u 以下的完备性是逼近的取值子句被花掉之处。对 u 以下的 c，序数 a 内部的传递性给出 c 低于 a，逼近在该处记录了某个取值；该条目只是「仅仅」存在，而消去的目标是「典范条目被记录」这条命题。
where named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst (lookup f γ) ⟩ named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst (lookup f γ) ⟩) (IH (fst c) c∈ (snd c) y q) q
那个仅仅给出的被记录取值，由归纳假设同认于塔；运输之后，被记录的恰是典范条目，这正是完备性所要求的。
图只对正确值成立
塔之图说：槽位处的取值就是塔在实参处的取值，而它经由一个逼近这样说：仅存在一个逼近，其在该实参处的步进正是那个取值。展开之后，所需的材料全部就位。实参以下的正确性来自刚完成的归纳；实参以下的完备性来自逼近的取值子句，经同一场归纳运输；最后再应用一次 step-Lset，就把被记录取值同认于塔。因此图确定它的取值：凡在某个序数处满足它的对象，都是元层面的塔在该处的取值。
这条读式以变元槽形式陈述，这并非装饰。它的各处实例化住在不同的具体环境中；若在某一处陈述，就得通过一个内部装着整条塔描述的满足关系，把它运到另一处。
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where Lset-only : ⟨ γ ⊨ LsetGraphAt w b ⟩ → IsOrd (fst (lookup b γ)) → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
陈述取塔之图在取值槽与实参槽处的满足、实参的序数性，结论是被记录取值就是塔。除了图成立之外，不假设关于图的任何东西。
Lset-only h ob = PT.rec (setIsSet (fst (lookup w γ)) (Lset (fst (lookup b γ)))) read (LsetGraph-out w b γ h) where
图展开为一个单纯见证：一个逼近，连同其满足与其在取值处的步进。消去是合法的，因为目标是两个 h-集合的相等，即一条命题；而见证本身也只在这条命题内部被需要。
read : GraphOf w b γ → fst (lookup w γ) ≡ Lset (fst (lookup b γ)) read (f , (ha , hs)) = step-Lset (suc w) (suc b) zero (f ∷ γ) hs ob vals ents
见证交出一个在实参上的逼近 f、其满足 ha、及其在取值处的步进 hs。步进引理在由 f 扩展的环境中施用：逼近占据新增的零号槽，取值与实参各上移一位。
where vals : Values f (fst (lookup b γ)) vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p
步进引理所需的正确性，就是把上一节的归纳施于逼近 ha：f 在实参以下记录的每个取值都是塔在该处的取值。
ents : Entries f (fst (lookup b γ)) ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ fst f)) named (ApproxAt-value zero (suc b) (f ∷ γ) ha c c∈)
完备性来自逼近的取值子句：在以下的每个实参处，都「仅仅」记录了某条目。消去的目标是「典范条目被记录」这条命题，因此那个缺席的见证永远不会被需要。
where named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst f ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst f ⟩ named (y , q) = subst (λ t → ⟨ pr (fst c) t ∈ fst f ⟩) (approx-val zero (suc b) (f ∷ γ) ha ob c y q) q
那个仅仅给出的被记录取值，由同一场归纳再次同认于塔；运输之后，被记录的恰是典范条目。
表就是逼近
反方向需要一个见证，而一张正确且完备的表就是。graph-table 把这样一张表变成对塔之图的满足，办法是填上上一章的诸子句，此外什么也不做。
逼近的定义域合取项是「实参在定义域中」的两种说法之间的等价，Domain 与 Entries 分别证明其两个方向：在 c 处记录的条目把 c 放到界以下；而只要 c 低于界，c 处的正準条目就被记录。某条被记录的对 (c, y) 处的步进合取项，是施于 c 的 step-table；序数的传递性把表的正确性与完备性限制到 c 以下的实参，那正是步进引理在该处所消费的。图所问的取值是整个实参处的步进，这同样是 step-table，取「被记录取值同认于塔」的等式为输入。
陈述取表 h、实参的序数性、表在实参上的三个条件，以及「被记录取值就是塔」的断言。
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where graph-table : (h : S) → IsOrd (fst (lookup b γ)) → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ)) → Domain h (fst (lookup b γ)) → fst (lookup w γ) ≡ Lset (fst (lookup b γ))
结论是塔之图在取值槽与实参槽处成立。
→ ⟨ γ ⊨ LsetGraphAt w b ⟩ graph-table h ob vals ents dom q = LsetGraph-in w b γ h approx (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents q) where
塔之图由一个逼近与一个外层步进引入。逼近就是表本身，被放进扩展环境；外层步进是施于实参的 step-table，其正确性、完备性与对塔的同认恰是手头的假设。
onDom : (c : S) → (⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩ → ⟨ fst c ∈ fst (lookup b γ) ⟩) × (⟨ fst c ∈ fst (lookup b γ) ⟩ → ⟨ ∃[ y ∶ S ] pr (fst c) (fst y) ∈ fst h ⟩)
逼近的定义域子句是「c 在定义域中」的两种说法之间的等价：有以 c 为第一分量的条目被记录，与 c 低于实参。两个方向都需要，因为逼近的定义域条件会以相反的次序使用它们。
onDom c = (λ hy → PT.rec (snd (fst c ∈ fst (lookup b γ))) named hy) , (λ c∈ → ∣ LsetS (fst c) (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈) , ents c c∈ ∣₁)
把等价向右读：c 处的一条被记录条目，连同表的完备性，给出典范条目，即呈现为 L 元素的 c 处之层 (c 的序数性取自实参的序数性) 的记录。向左读：表的定义域条件把 c 放到实参以下。
where named : Σ[ y ∈ S ] ⟨ pr (fst c) (fst y) ∈ fst h ⟩ → ⟨ fst c ∈ fst (lookup b γ) ⟩ named (y , p) = dom c y p
辅助事实 named 是对见证读取定义域条件：存在第一分量为 c 的条目，故 c 低于实参。其内容就是表的第三个条件的一次应用。
onStep : (c y : S) → ⟨ pr (fst c) (fst y) ∈ fst h ⟩ → ⟨ (y ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩ onStep c y p = step-table zero (suc zero) (suc (suc zero)) (y ∷ c ∷ h ∷ γ) oc vals' ents' (vals c y c∈ p)
步进合取项在每条被记录的对 (c, y) 处证明。在加入取值 y、实参 c 与表 h 的扩展环境中，步进条件经由表槽把取值槽与实参槽联系起来；施于 c 的 step-table 恰好建立这一点，而所需的同认 fst y ≡ Lset (fst c) 由正确性在该被记录对处供给。
where c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩ c∈ = dom c y p oc : IsOrd (fst c) oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
关于 c 的两件事实从被记录对读出：其底层集合低于实参，由定义域条件；它是序数，由实参的序数性。
vals' : Values h (fst c) vals' e t _ r = vals e t (dom e t r) r ents' : Entries h (fst c) ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈)
c 以下的正确性与完备性是表自己的条件限制到 c 以下：正确性限制定义域假设，完备性则用实参的传递性看出「低于 c 的实参低于实参」。这是本章对该传递性的第二次、也是最后一次使用。
approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩ approx = ApproxAt-in zero (suc b) (h ∷ γ) (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep
把两个合取项装配起来，表本身就是逼近：其定义域子句是刚才证明的等价，其步进子句是之前的那个。所谓「正确且完备的表包含实参以下层级的记录」，其含义就在于此。
有序对图
表必须被构造出来，而 L 内部可用的建造者只有替换，替换需要一个图。替换在函数性图的描述之后收集这张表：表的一条目是实参 c 与取值 z 的有序对；当 z 满足塔在 c 处的图时，图对该条目成立，而塔所遍及的载体被钉在某个常元上。一个存在量词绑定塔的取值，对读式把条目与「实参和被绑定取值」组成的对等同起来，塔之图则说明被绑定的取值是正确的。
它的两种读法把那个句子取作参数，并把该句子自己的等式取作假设，本章的调用处是 refl。该框架对句子保持通用：无论传入什么公式，读法都在「它拼出有序对图」的假设下谈论它。等式随句子同行，因此读法的施用无需更多论证。
内部层级
Recorded 为内部层级在 α 处要收集的类命名：底层集合低于 α 的实参 c，连同塔在 c 处的取值组成的对，此外别无他物。IsHier 说模型的某个集合逐成员地实现这个类：对每个载体元素 z，属于该集合恰当 z 呈现为这样的对。这条陈述的两个方向都有使用。HierOf 把实现集合连同其规格收为一对；构造所建造的是这个形式，两条读式所消费的也是这个形式。
两条读式都针对一个由其规格抵达的变元实现集合，这样即将到来的构造就可以把它们应用于自己正在建造的集合。向外读取时，对某个成员应用层级配对的单射性：实现集合的一条目指名低于 B 的实参与塔在该处的取值。向内写入时，把正準对呈现为模型的元素，这由模型自身的配对给出；它还需要实参的序数性，否则根本无法指称塔在该处的取值。
然后是构造，在序数上作一次沿成员的归纳。在 α 处，成对的那个图在以下的每个实参上都是函数性的：归纳假设给出直到那个实参为止的层级，graph-table 把它变成对塔之图的满足，而 Lset-only 说别的东西都不满足它。替换把这些对收集成模型的一个集合。每个实参的序数性取自 mem-ord；函数性要求由 mereFunct 满足，因为某个实参处的取值是一个构造。
Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ) Recorded B z = ∃[ c ∶ S ] (fst c ∈ B) ⊓ ((z ≡ pr (fst c) (Lset (fst c))) , setIsSet z (pr (fst c) (Lset (fst c))))
Recorded B z 是一个命题，它说：存在某个载体元素 c，其底层集合低于 B，使得 z 的底层集合是 fst c 与塔在 c 处取值的有序对。两个 h-集合的相等本身就是命题，因此这是一个命题上的析取聚合。
IsHier : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ)) IsHier B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z)
IsHier B h 说 h 所呈现的集合逐成员地实现被记录的类：在每个 z 处，属于该集合与被记录是同一命题。两个方向都不丢弃，因为各有其用：只有隶属而无被记录，会放进陌生者；只有被记录而无隶属，会漏掉应有的对。
HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ)) HierOf B = Σ[ h ∈ S ] IsHier B h
HierOf B 把实现集合连同其规格收集为一对。这对正是归纳要在每个序数处构造的东西；它的两个分量分别回答对任何构造都要问的两个问题：它是什么，以及它为何合格。
module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where
两条读式对一个带规格的变元实现集合陈述，这样即将到来的构造就可以把它们应用于自己正在建造的集合，无论归纳当前站在哪个层。
hier-out : (c z : S) → ⟨ pr (fst c) (fst z) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c))
向外读：若 c 与 z 组成的对是实现集合的成员，则 c 低于 B，且 z 是塔在 c 处的取值。两个结论都由规格施加于该成员而来。
hier-out c z p = PT.rec (isProp× (snd (fst c ∈ B)) (setIsSet (fst z) (Lset (fst c)))) read (subst ⟨_⟩ (sp k) p) where
该成员的隶属沿规格被运进被记录命题，而那是一条截断的存在；消去的目标是一对命题构成的命题，因此可以在这里消耗见证。
k : S k = pr (fst c) (fst z) , isL-trans {x = fst h} {y = pr (fst c) (fst z)} p (h .snd)
成员自身也须被命名为载体元素：底层集合的有序对可构造，因为它属于 h 所呈现的可构造集合。
read : Σ[ d ∈ S ] (⟨ fst d ∈ B ⟩ × (pr (fst c) (fst z) ≡ pr (fst d) (Lset (fst d)))) → ⟨ fst c ∈ B ⟩ × (fst z ≡ Lset (fst c)) read (d , (d∈ , eq)) = subst (λ t → ⟨ t ∈ B ⟩) (sym (pr-inj eq .fst)) d∈
被记录命题给出低于 B 的 d，且该成员等于 d 与塔在 d 处取值组成的对。层级配对的单射性拆开这条等式：第一分量的等同把 c 同认于 d，从而把隶属搬成「c 低于 B」；第二分量的等同把 z 同认于塔在 d 处的取值，再经第一等同变成塔在 c 处的取值。
, (pr-inj eq .snd ∙ cong Lset (sym (pr-inj eq .fst))) hier-in : (c : S) → ⟨ fst c ∈ B ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ fst h ⟩ hier-in c c∈ = subst (λ t → ⟨ t ∈ fst h ⟩) (prʟ-fst c (LsetS (fst c) oc)) (subst ⟨_⟩ (sym (sp k)) ∣ c , (c∈ , prʟ-fst c (LsetS (fst c) oc)) ∣₁)
向内读：典范条目，即模型自身的「c 与塔在 c 处取值」之对，是成员。规格说被记录的类被实现，而典范对正是被记录命题的见证 (以 c 本身为实参)；条目与模型之对相等，则由该对的定义读式给出。
where oc : IsOrd (fst c) oc = mem-ord {A = B} oB (fst c) c∈ k : S k = prʟ c (LsetS (fst c) oc)
c 的序数性来自 B 的序数性；有了它，塔在 c 处的取值才能呈现为 L 的元素，而这正是模型的配对所需要的第二分量。
opaque hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α} (build (PairGraphAt zero (suc zero)) refl) where
归纳的步进函数把成对的那个图保持为随身携带自己等式的变元句子，而不写出它将被实例化成的闭句子。等式随句子同行，因此下面的每条读式都在调用处以 refl 施用。
build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero) → (α : V ℓ) → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ) → ⟨ isL α ⟩ → IsOrd α → HierOf α
步进接收句子及其等式、序数 α、它的两张证书，以及归纳假设：α 的每个成员处的层级均已建成。它须返回 α 处的层级及其规格。
build φ qφ α IH hα oα = r .fst .fst , spec where A : S A = α , hα
α 处的层级是实现者的第一分量，在替换产出之后一次提取；A 是呈现为载体元素的 α，正是替换消费定义域时所用的形式。
value : (c : S) → ⟨ fst c ∈ α ⟩ → S value c c∈ = LsetS (fst c) (mem-ord {A = α} oα (fst c) c∈) entry : (c : S) → ⟨ fst c ∈ α ⟩ → S entry c c∈ = prʟ c (value c c∈)
在 α 以下，两个辅助构造为数据命名。实参 c 处的取值是 c 处的层，由层呈现而成为 L 的元素，c 的序数性取自 α 的序数性。c 处的条目是模型自身的「c 与其取值」的有序对，正是被记录类所要求的形式。
below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S) → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩ below c c∈ k = graph-table zero (suc (suc zero)) (value c c∈ ∷ k ∷ c ∷ []) (hc .fst) oc
塔之图在为 α 的成员 c 所记录的取值处成立。归纳假设正是在此被花掉：它交出 c 处的层级，那是实参 c 上一张正确且完备的表，恰是 graph-table 所要的。环境中载着取值、给图自身量词留的新槽，以及实参。
(λ d z _ p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .snd) (hier-in (fst c) oc (hc .fst) (hc .snd)) (λ d z p → hier-out (fst c) oc (hc .fst) (hc .snd) d z p .fst) refl
表的三个条件从 c 处层级的规格读出：正确性说每个被记录取值都是塔在那里；完备性说典范条目被记录；定义域条件说此外无他。最后一个参数 refl 是有序对图自己的等式。
where oc : IsOrd (fst c) oc = mem-ord {A = α} oα (fst c) c∈ hc : HierOf (fst c) hc = IH (fst c) c∈ (snd c) oc
c 的序数性来自 α 的序数性；有了它，归纳假设交付 c 处的层级；可构造集合与规格一并交付。
（holds)每条正準条目都满足有序对图：c 上的纤维被给出，其中包括被绑定的塔值、把条目与模型之对等同的等式，以及塔之图在取值与实参处的满足。见证是纤维的一个元素，即图陈述所断言「仅仅存在」的那个类型的元素。
holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩ holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))
（only)在 c 处满足图的其他任何居留者都等于正準条目。图展开为塔值 z 连同在 (z, c) 处成立的塔之图；塔之图确定其取值，配对的单射性等同两条目，而该等式是这些路径的复合。
only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S) → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈ only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)
对的见证拆成塔值 z 与把 k 同认于「c 与 z 之对」的等式 q。一旦底层集合相等，载体元素就相等，Σ≡Prop 把目标化归于此。
where read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈ read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t)) ( q
(z, c) 处的塔之图确定塔值：由 Lset-only 在「加入取值、典范条目与实参」的扩展环境中施用，得 z 就是塔在 c 处的取值；c 的序数性取自 α 的序数性。
∙ cong (pr (fst c)) (Lset-only zero (suc (suc zero)) (z ∷ k ∷ c ∷ []) hg (mem-ord {A = α} oα (fst c) c∈)) ∙ sym (prʟ-fst c (value c c∈)) )
三条路径复合起来，k 就是「c 与塔在 c 处取值」之对，即按其定义读式读出的典范条目。
（fc)c 处的函数性正是替换所要的可缩纤维：正準条目在图中有一席，而每个居留者都等于它。mereFunct 把以「仅仅存在」形式呈现的两半，装配成恰为该可缩纤维的居留。
fc : (c : S) → ⟨ c ∈ˢ A ⟩ → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩) fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁
替换随即收集诸条目：遍及 α 中的实参，每个实参与其唯一确定的取值组成的对构成模型的一个集合，并连同「它恰实现那个对之类」的断言一起呈现。α 处的内部层级作为 L 的集合而存在的时刻，就是此刻。
r : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ))) r = hasReplacementL A φ fc spec : IsHier α (r .fst .fst) spec z = ⇔toPath toRec fromRec where
余下的是验证：收集所得的集合确实实现被记录的类。规格逐成员比较「属于收集集合」与「是被记录的对」；比较的两个方向分别证明，再合并为逐点等价。
toRec : ⟨ fst z ∈ fst (r .fst .fst) ⟩ → ⟨ Recorded α (fst z) ⟩ toRec hz = PT.rec squash₁ conv (subst ⟨_⟩ (r .fst .snd z) hz) where
把收集集合的隶属向外读：替换的规格把它变成 α 的一个成员 c，其取值在 c 处满足有序对图。消去是合法的，因为被记录的类是命题。
conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩) → ⟨ Recorded α (fst z) ⟩ conv (c , (c∈ , hp)) = ∣ c , (c∈ , cong fst (only c c∈ z hp) ∙ prʟ-fst c (value c c∈)) ∣₁
对见证而言，唯一性说在 c 处记录的取值等于典范条目，而典范条目等于模型的「c 与塔在 c 处取值」之对；底层集合随之而来，这正是「被记录」所要求的。
fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst (r .fst .fst) ⟩ fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (PT.map conv hz) where
向内读：一条被记录的对给出低于 α 的实参连同塔在该处的取值；有序对图在该实参的典范条目处成立，而收集集合含有这条条目。
conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × (fst z ≡ pr (fst c) (Lset (fst c)))) → Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
见证从被记录的呈现转换成图的呈现：实参保持不变，而「底层集合等于典范对」的等式变成有序对图在该处的满足。
conv (c , (c∈ , eq)) = c , (c∈ , subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩) (sym zeq) (holds c c∈)) where zeq : z ≡ entry c c∈ zeq = Σ≡Prop (λ t → snd (isL t))
该等式说 z 呈现与 c 的典范条目相同的集合；因此两个对元素相等，把 holds 沿这条路径运输，便得有序对图在 z 与 c 处的满足。
(eq ∙ sym (prʟ-fst c (value c c∈))) hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S hierL α hα oα = hierAt α hα oα .fst
某个序数处的内部层级，就是归纳所得的实现集合，呈现为 L 的元素。它对每个可构造序数都存在；也就是说：模型如今为它的每个序数准备了一个集合，其成员恰是「低于该序数的序数与塔在该处取值」组成的有序对。
hierL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsHier α (hierL α hα oα) hierL-spec α hα oα = hierAt α hα oα .snd
规格随构造同行：归纳交付的实现集合，在其序数处于两个方向上满足 IsHier。日后对内部层级的一切使用，都对照这份说明来检验。
外部层级满足该图
内部层级是用 graph-table 与 Lset-only 建造的：在每个序数处，归纳假设供给以下的表，两条引理把它变成成立的图与唯一的取值。最后一条陈述此刻反向而行。规格 hierL-spec 交出实参上的表条件，Lset-defines 把它们喂给 graph-table：塔之图在被记录取值处成立，与之并置的 Lset-only 说别无其他满足者。于是内部之图与元层面的塔在每个可构造序数处、在两个方向上一致。
module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where Lset-defines : IsOrd (fst (lookup b γ)) → fst (lookup w γ) ≡ Lset (fst (lookup b γ)) → ⟨ γ ⊨ LsetGraphAt w b ⟩
陈述取实参的序数性与「被记录取值就是塔在该处的取值」的断言，结论是塔之图成立。这是上一节的向内读式，之所以在每个可构造序数处都可用，是因为内部层级在每个可构造序数处都存在。
Lset-defines ob q = graph-table w b γ H ob (λ c z _ p → hier-out (fst (lookup b γ)) ob H sp c z p .snd) (hier-in (fst (lookup b γ)) ob H sp) (λ c z p → hier-out (fst (lookup b γ)) ob H sp c z p .fst) q
此处所指名的集合是实参处的内部层级，其规格被读作三个表条件。正确性与完备性是 hier-out 的两个方向：内部表的每条目，其实参低于实参、其取值是塔在那里；且每个低于实参的实参处的正準条目都被记录。定义域条件是 hier-in 一侧的对应物：被记录的只有那样的对。
证明先指名实参处的内部层级，并把其规格向两个方向读出。正确性说内部表在实参以下记录的每个取值都是塔在那里；完备性说典范条目被记录；定义域条件把表封闭；最后的假设 q 把被记录取值同认于塔。这四项输入恰是 graph-table 所消费的。
where H : S H = hierL (fst (lookup b γ)) (lookup b γ .snd) ob sp : IsHier (fst (lookup b γ)) H sp = hierL-spec (fst (lookup b γ)) (lookup b γ .snd) ob
实参处的内部层级之所以存在，是因为实参是可构造序数；其规格恰是归纳所证明的隶属等价。两件事合起来说：塔在每一个层处都被记录在模型内部，且此外无他。
小结
approx-val 通过对实参作一次沿成员归纳，证明逼近记录的每个取值都等于元层面的塔在相应实参处的取值；这里不需要任何单值性假设。在同一个实参处记录的两个取值相等，可由它直接读出。Lset-only 与 Lset-defines 给出图与塔之间的两个方向，而后者用于构造 hierL。hierL 是某个序数处的内部层级，是 L 的一个元素；其成员恰是「低于该序数的序数与塔在该处取值」组成的有序对。其规格是归纳所证明的隶属等价。