BedrockThe hierarchy, said as a sequence
在这条路线上，塔是唯一一个没法照满足关系那场递归的办法内化的构造。一个图不可以点名它所定义的对象，而塔在某个阶段处是由该阶段以下的塔造出来的，故直接为塔写下的图将不得不点名它自己在诸子实参处的取值。它没有可点名的取值。
能说出口的是逼近是什么。函数 f 是层级在 a 上的一个逼近，当它恰好定义在 a 的诸成员上，且它所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。那一步只在实参以下查阅 f，故这个条件永不查看该函数尚未记录的取值，而塔自己在 a 处的取值就是「由这样一个 f 所得的那一步」。这是一条序列刻画，而它是一个只谈 f 的一阶句子。
本章的每一位都是一位。逼近由图仅有的那个存在量词绑定，实参与取值是图的两个自由变元，而任何地方都没有点名的常元，正是这一点让整条描述能在层级所需之处说出口：在持有阶段的那层绑定之下。下面每一条读式都陈述在变元环境上，理由与前两章相同：在具体环境上解除的适足性，把那个环境的构造塞进了一个满足关系里面，同一条陈述于是从几秒变成几分钟。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Sequence {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇_; ∀̇_ ) import FOL.Absoluteness open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ ) open import L.Coding.Model {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both; appAt; appAt-adequate ; domAt; domAt-in; domAt-out ) open import L.Coding.Powerset {ℓ} lem using ( DefAt; DefAt-in; DefAt-out ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
某个实参处的那一步说了什么
v 是 b 处的阶段 (给定 b 以下的逼近 f)，当 v 的诸成员恰是「落在 f 于 b 中某个实参处所记录的某个取值的可定义幂集之中」的那些集合。三个相邻的存在量词承载它：那个实参 c、逼近在其处所记录的取值 w，以及该取值的可定义幂集 d。幂集必须被绑定，因为上一章交付的是关于它的一条描述、而不是指称它的一个词项；DefAt 说的是 d 是 w 的可定义幂集，故使用它的唯一办法就是对它所描述的那个东西作量化。
整一步是一次 extAt，而这是一项决定、不是图省事。阶段是一个集合，而凡取值为集合的递归，其每一条子句说的都是同一句话：这个取值恰是满足某个条件的那些东西之集。若手写成一对包含，那个条件就要出现两次、每条包含之下各一次，于是那三个存在量词被复制一份，此后对它们的每一次改动都得在两处各做一遍，而每一种读法都得由「互非逆」的两半重新拼起来。extAt 把条件只写一次，并把两种读法作为投影交回来，而它存在的意义恰在于此。
有一个旁条件随这一步一同旅行，而一条假设在两个方向上都把它解除。要满足这条描述，必须把可定义幂集作为模型的元素拿出来，因为对象语言的存在量词在 L 上取值；要把描述读回来，则需要 DefAt 的消去，而它的旁条件是「载体的诸可定义子集皆可构造」。前者蕴含后者：若 𝒟ₒ w 是 L 的元素，则由该类的传递性，它的诸成员皆可构造。故两个方向索取的是同一样东西，即 PowOK，而位于某个阶段处的消费方用后继恒等式把它解除。
private sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n)))) sh4 i = suc (suc (suc (suc i))) StepBody : ∀ {n} → Fin n → Fin n → Formula S (suc (suc (suc (suc n)))) StepBody b f = (var (suc (suc zero)) ∈̇ var (sh4 b)) ∧̇ ( appAt (sh4 f) (suc (suc zero)) (suc zero) ∧̇ ( DefAt zero (suc zero) ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n StepAt v b f = extAt v (∃̇ (∃̇ (∃̇ (StepBody b f)))) Records : ∀ {n} → Fin n → Fin n → S ^ n → S → S → Type (ℓ-suc ℓ) Records b f γ c w = ⟨ fst c ∈ fst (lookup b γ) ⟩ × ⟨ pr (fst c) (fst w) ∈ fst (lookup f γ) ⟩ StepOf : ∀ {n} → Fin n → Fin n → S ^ n → S → Type (ℓ-suc ℓ) StepOf b f γ z = Σ[ c ∈ S ] Σ[ w ∈ S ] (Records b f γ c w × ⟨ fst z ∈ 𝒟ₒ (fst w) ⟩) PowOK : ∀ {n} → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ) PowOK b f γ = (c w : S) → Records b f γ c w → ⟨ isL (𝒟ₒ (fst w)) ⟩
那一步，两个方向
读体是那三个存在量词被花掉之处，而下面每一次 PT.rec 都为自己载荷的类型点名。这是上一章据以写下的规矩，且它不是文风问题：若交给推断，载荷就是一个元变元，代表着「某条公式的满足关系」，而消解器尚未对那条公式作出承诺，同样两行于是从两秒变成跑过两分钟。
装配体则是把同样三个存在量词填上。可定义幂集以 PowOK 所提供的那个模型元素供上，它自己的编码等式在那个元素处是 refl，而 DefAt 的引入别无所需。这一步的诸读法于是就是 extAt 的诸方向、把那两半插进去；而它们有三条而非两条：StepAt-out 把这一步的一个成员读作一份载荷，StepAt-back 把一份载荷放回去，而 StepAt-in 由两个方向一并造出这一步，因为一个以外延造出的集合，必须从两侧逐成员地重新进入。读体与装配体为三者所共用，故每个投影都只有一行。
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where private Φ : Formula S (suc n) Φ = ∃̇ (∃̇ (∃̇ (StepBody b f))) readBody : PowOK b f γ → (z c w d : S) → ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩ → StepOf b f γ z readBody ok z c w d (hb , (ha , (hd , hz))) = c , w , rec , subst (λ X → ⟨ fst z ∈ X ⟩) qd hz where -- perf: env spelled out at both ends; via an abbreviation, 15 s per conversion rec : Records b f γ c w rec = hb , subst ⟨_⟩ (appAt-adequate (sh4 f) (suc (suc zero)) (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)) ha qd : fst d ≡ 𝒟ₒ (fst w) qd = DefAt-out w zero (suc zero) (d ∷ w ∷ c ∷ z ∷ γ) (λ x x∈ → isL-trans {x = 𝒟ₒ (fst w)} {y = x} x∈ (ok c w rec)) refl hd unfold : PowOK b f γ → (z : S) → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ∥ StepOf b f γ z ∥₁ unfold ok z = PT.rec squash₁ viaArg where viaPow : (c w : S) → Σ[ d ∈ S ] ⟨ (d ∷ w ∷ c ∷ z ∷ γ) ⊨ StepBody b f ⟩ → ∥ StepOf b f γ z ∥₁ viaPow c w (d , hd) = ∣ readBody ok z c w d hd ∣₁ viaVal : (c : S) → Σ[ w ∈ S ] ⟨ (w ∷ c ∷ z ∷ γ) ⊨ ∃̇ (StepBody b f) ⟩ → ∥ StepOf b f γ z ∥₁ viaVal c (w , hw) = PT.rec squash₁ (viaPow c w) hw viaArg : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (∃̇ (StepBody b f)) ⟩ → ∥ StepOf b f γ z ∥₁ viaArg (c , hc) = PT.rec squash₁ (viaVal c) hc fill : PowOK b f γ → (z : S) → StepOf b f γ z → ⟨ (z ∷ γ) ⊨ Φ ⟩ fill ok z (c , (w , (rec , hz))) = ∣ c , ∣ w , ∣ D , (rec .fst , (ha , (hdef , hz))) ∣₁ ∣₁ ∣₁ where -- perf: env spelled out at both ends; via an abbreviation, 15 s per conversion D : S D = 𝒟ₒ (fst w) , ok c w rec ha : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ appAt (sh4 f) (suc (suc zero)) (suc zero) ⟩ ha = subst ⟨_⟩ (sym (appAt-adequate (sh4 f) (suc (suc zero)) (suc zero) (D ∷ w ∷ c ∷ z ∷ γ))) (rec .snd) hdef : ⟨ (D ∷ w ∷ c ∷ z ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hdef = DefAt-in w zero (suc zero) (D ∷ w ∷ c ∷ z ∷ γ) refl refl StepAt-out : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ → (z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁ StepAt-out h ok z z∈ = unfold ok z (extAt-out v Φ γ h z z∈) StepAt-back : ⟨ γ ⊨ StepAt v b f ⟩ → PowOK b f γ → (z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩ StepAt-back h ok z s = extAt-in v Φ γ h z (fill ok z s) StepAt-in : PowOK b f γ → ((z : S) → ⟨ fst z ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ z ∥₁) → ((z : S) → StepOf b f γ z → ⟨ fst z ∈ fst (lookup v γ) ⟩) → ⟨ γ ⊨ StepAt v b f ⟩ StepAt-in ok into back = extAt-in-both v Φ γ (λ z z∈ → PT.rec (snd ((z ∷ γ) ⊨ Φ)) (fill ok z) (into z z∈)) (λ z h → PT.rec (snd (fst z ∈ fst (lookup v γ))) (back z) (unfold ok z h))
成为一个逼近是什么意思
两个合取项，没有第三个。f 定义在 a 上，且 f 所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。第二个合取项无须加上「实参落在 a 中」这道防护：第一个合取项已经在两个方向上把定义域钉在 a 上，故凡记录了东西的实参都是 a 的成员，再说一遍只会把句子拉长。
这一对是一条隶属等价，而这比看上去更要紧。若反过来陈述为「对 a 中的每个实参，仅仅存在一个取值是那里的那一步」，这句话就容许 f 在正确的对之外还持有一些垃圾对，故它并不确定 f，那条存在性断言不是命题，而针对它的归纳需要一条内部的函数外延性引理，才能从两个逼近走到一个。作为等价，动机是命题，而那条引理根本无须写下。
此处刻意没有单值性合取项。它断言不出第二个合取项尚未给出的任何东西：若在同一个实参处记录了两个取值，则两者都是那个实参处的那一步，而那一步是一条集合等式，同成员的两个集合相等。带上它，等于拿三个置于满足关系之下的全称量词去换一条推论。
三个投影就是消费方要问的三个问题：有条目的实参在定义域中、定义域中的实参有条目、被记录的取值是一步。引入之所以放在此处而不放在调用处，理由与每一条读式相同：它解除一次适足性，而那必须在变元环境上做。
private sh2 : ∀ {n} → Fin n → Fin (suc (suc n)) sh2 i = suc (suc i) ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n ApproxAt f a = domAt f a ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero ⇒̇ StepAt zero (suc zero) (sh2 f) )) module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ fst x ∈ fst (lookup a γ) ⟩ ApproxAt-dom h = domAt-out f a γ (h .fst) ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (x : S) → ⟨ fst x ∈ fst (lookup a γ) ⟩ → ∥ (Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩) ∥₁ ApproxAt-value h = domAt-in f a γ (h .fst) ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩ ApproxAt-step h x y p = h .snd x y (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ))) p) ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩ → ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩ → ⟨ (y ∷ x ∷ γ) ⊨ StepAt zero (suc zero) (sh2 f) ⟩) → ⟨ γ ⊨ ApproxAt f a ⟩ ApproxAt-in hd hs = hd , λ x y p → hs x y (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (y ∷ x ∷ γ)) p)
那个图
在逼近上的一个存在量词，其下是本章为之而写的那两个合取项：f 是那个实参上的一个逼近，而那个取值是「在那个实参处、由 f 算出的那一步」。取值站在第一位、实参站在第二位，这正是模型的替换字段读一个图所用的顺序，而 LsetGraph 就是把那两位填好之后的那个句子。
逼近被绑定，而这是不得不然。一个图不可以点名它所定义的对象，且仅当某物已知是 L 的元素时，它才可以断言该物存在，因为满足关系是在模型处读的。逼近正是这样一样东西：它是由较低的诸实参经替换收集起来的对之集，而不是它被用来描述的那座塔。消费方供上一个；图只说仅仅存在一个。
两种读法各只一行，因为被满足的存在量词就是一个截断的 sigma，被满足的合取就是一个对。它们买到的不是证明，而是那个名字与那一位：GraphOf 把载荷的类型写了出来、不交给推断，而两种读法都站在一个变元环境的变元位上，故消费方是去实例化它们，而不是去与它们作转换。
命名就是本节的全部代价，而这个数字值得留存，因为对它的第一次诊断是错的。若把图以它那个闭句别名来称呼，同样两行花掉了本章 130 秒中的 98 秒。当初怪罪的是那两位，而它们是清白的：下一章一次隔离测量把「读式落在完全具体的位上」量到十五毫秒，而把「同一条读式对着一个别名」量到五十一秒。真正花钱的是「判定别名的满足关系与它展开式的满足关系相等」，而 Agda 解决它的办法，是把一个内部装着整条可定义幂集描述的满足关系正规化。落在变元位上，诸读式根本碰不到这个问题，而那个闭句只差一次展开。
LsetGraphAt : ∀ {n} → Fin n → Fin n → Formula S n LsetGraphAt y x = ∃̇ (ApproxAt zero (suc x) ∧̇ StepAt (suc y) (suc x) zero) LsetGraph : Formula S 2 LsetGraph = LsetGraphAt zero (suc zero) module _ {n : ℕ} (y x : Fin n) (γ : S ^ n) where GraphOf : Type (ℓ-suc ℓ) GraphOf = Σ[ f ∈ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc x) ⟩ × ⟨ (f ∷ γ) ⊨ StepAt (suc y) (suc x) zero ⟩ ) LsetGraph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc x) ⟩ → ⟨ (f ∷ γ) ⊨ StepAt (suc y) (suc x) zero ⟩ → ⟨ γ ⊨ LsetGraphAt y x ⟩ LsetGraph-in f ha hs = ∣ f , (ha , hs) ∣₁ LsetGraph-out : ⟨ γ ⊨ LsetGraphAt y x ⟩ → ∥ GraphOf ∥₁ LsetGraph-out h = h
小结
LsetGraph 是对象语言中「取值是实参处的阶段」这个句子，写下来时不点名任何阶段、任何塔、任何序数。StepAt 是一次 extAt 罩住三个相邻的存在量词，即那个实参、在其处所记录的取值，以及它的可定义幂集；ApproxAt 是两个合取项，即定义域与那条步进条件，再无其他。
此处没有任何东西被证两遍。可定义幂集以「落在一位上的描述」的形式从上一章到来，并按交付时的原样使用；函数机器从 appAt 与 domAt 上读出；而那一步的两种读法就是 extAt 自己的那两个。本章所贡献的是形状：一个查阅逼近、而非查阅塔的图，而那是一个图被允许拥有的唯一形状。
有两条裁定被记录在读者与之相遇之处。那一步是一条隶属等价，而非一个单向的收集，这使即将到来的那场归纳的动机保持为命题，并把一条内部的函数外延性引理整个从路线上移除。以及，没有单值性合取项，因为步进条件已经把「在一个实参处记录的每个取值」钉住了，故单值性是一条推论、不是一条假设。
一次测量，而紧随本章的下一章更正了它的诊断。本章曾经花掉的每一秒，都是「同一样东西的两种写法」之间的一次转换，而 Agda 每一次都用「把一个内部装着整条可定义幂集描述的满足关系正规化」来作答：两条读法对着图的那个闭句别名而取，98 秒；每一处「假设把环境写开、而应用把它藏在一个缩写背后」，各 15 秒。具体位不是那个机制，它们分文不取。写成两侧是同一个表达式之后，本章在两秒之内、而不是 130 秒检查完毕，数学分毫未改。前几章据以写下的那条规矩，即适足性在变元实参处解除，对一条陈述成立，与它对一次代换成立完全一样。