可构造层级的序列

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

module L.Coding.HierarchySequence {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章用函数图描述逐次取可定义幂集所得的层，刻画该函数的部分逼近，并封装后面用来识别可构造层级初始段的图。

在这条路线上，塔是唯一一个没法照满足关系那场递归的办法内化的构造。一个图不可以点名它所定义的对象，而塔在某一层处是由该层以下的塔造出来的，故直接为塔写下的图将不得不点名它自己在诸子实参处的取值。它没有可点名的取值。

能说出口的是逼近是什么。函数 f 是层级在 a 上的一个逼近，当它恰好定义在 a 的诸元素上，且它所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。那一步只在实参以下查阅 f，故这个条件永不查看该函数尚未记录的取值，而塔自己在 a 处的取值就是「由这样一个 f 所得的那一步」。这是一条序列刻画，而它是一个只谈 f 的一阶句子。

本章中的每个槽位都由变元表示。逼近由图中唯一的存在量词绑定，实参与取值是图的两个自由变元，整个描述不含任何具名常元，因此可以放在层级所需的位置，即持有层的那层绑定之下。下面每条读式也都在变元环境中陈述，理由与前两章相同：若在具体环境中解除充分性，环境的构造会进入满足关系，使同一陈述的检查时间从几秒增加到几分钟。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

open hPropView 𝒮ʟ

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

后继层关系

StepAt v b f 表示 v 是 f 定义域中的后继实参，并且 f 在该处的取值是其在前驱 b 处取值的可定义幂集。Records、StepOf 与 PowOK 分别揭示该陈述的三个部分。

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 → Vec S n → S → S → Type (ℓ-suc ℓ)
Records b f γ c w = ⟨ c .fst ∈ (lookup b γ) .fst ⟩
                  × ⟨ pr (c .fst) (w .fst) ∈ (lookup f γ) .fst ⟩

StepOf : ∀ {n} → Fin n → Fin n → Vec S n → S → Type (ℓ-suc ℓ)
StepOf b f γ z = Σ[ c ∶ S ] Σ[ w ∶ S ]
                   (Records b f γ c w × ⟨ z .fst ∈ 𝒟ₒ (w .fst) ⟩)

PowOK : ∀ {n} → Fin n → Fin n → Vec S n → Type (ℓ-suc ℓ)
PowOK b f γ = (c w : S) → Records b f γ c w → ⟨ isL (𝒟ₒ (w .fst)) ⟩

读取并构造层级步骤

StepAt-out 从已满足的步骤中提取可定义幂集条件，StepAt-in 从该条件及所需定义域数据构造满足关系。StepAt-back 以后续证明所用的形式保留提取出的条件。

读体是消去那三个存在量词之处，下面每一次 rec₁ 都明确写出自身载荷的类型。这是上一章已经采用的规则，并非文风选择：若交给推断，载荷会成为一个元变元，表示「某条公式的满足关系」，而消解器尚未确定是哪条公式；同样两行代码的检查时间便会从两秒增加到两分钟以上。

装配体则是把同样三个存在量词填上。可定义幂集由 PowOK 所提供的那个模型元素给出，它自己的编码等式在那个元素处是 refl，而 DefAt 的引入别无所需。这一步的诸读法于是就是 extAt 的诸方向：把那两半插进去；而它们有三条而非两条，StepAt-out 把这一步的一个元素读作一份载荷，StepAt-back 把一份载荷放回去，而 StepAt-in 由两个方向一并造出这一步，因为一个以外延造出的集合，必须从两侧逐元素地重新进入。读体与装配体为三者所共用，故每个投影都只有一行。

module _ {n : ℕ} (v b f : Fin n) (γ : Vec 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 → ⟨ z .fst ∈ X ⟩) qd hz
    where

    rec : Records b f γ c w
    rec = hb , subst ⟨_⟩ (appAt-adequate
      (sh4 f) (suc (suc zero)) (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)) ha

    qd : d .fst ≡ 𝒟ₒ (w .fst)
    qd = DefAt-out w zero (suc zero) (d ∷ w ∷ c ∷ z ∷ γ)
      (λ x x∈ → isL-trans {x = 𝒟ₒ (w .fst)} {y = x} x∈ (ok c w rec)) refl hd

  unfold : PowOK b f γ → (z : S)
         → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ∥ StepOf b f γ z ∥₁
  unfold ok z = 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) = rec₁ squash₁ (viaPow c w) hw

    viaArg : Σ[ c ∶ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (∃̇ (StepBody b f)) ⟩
           → ∥ StepOf b f γ z ∥₁
    viaArg (c , hc) = 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

    D : S
    D = 𝒟ₒ (w .fst) , 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) → ⟨ z .fst ∈ (lookup v γ) .fst ⟩ → ∥ 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 → ⟨ z .fst ∈ (lookup v γ) .fst ⟩
StepAt-back h ok z s = extAt-in v Φ γ h z (fill ok z s)

StepAt-in : PowOK b f γ
          → ((z : S) → ⟨ z .fst ∈ (lookup v γ) .fst ⟩ → ∥ StepOf b f γ z ∥₁)
          → ((z : S) → StepOf b f γ z → ⟨ z .fst ∈ (lookup v γ) .fst ⟩)
          → ⟨ γ ⊨ StepAt v b f ⟩
StepAt-in ok into back = extAt-in-both v Φ γ
  (λ z z∈ → rec₁ (((z ∷ γ) ⊨ Φ) .snd) (fill ok z) (into z z∈))
  (λ z h → rec₁ ((z .fst ∈ (lookup v γ) .fst) .snd) (back z) (unfold ok z h))

层级序列的逼近

ApproxAt f a 描述一个定义域为序数 a 的函数：它具有指定初值，且每个后继处的取值都由 StepAt 关联。GraphAt 以存在量词封装这类函数，其读取引理则揭示定义域、取值与步骤方程。

两个合取项，没有第三个。f 定义在 a 上，且 f 所记录的每个取值都是「在那个实参处、由 f 自身算出的那一步」。第二个合取项无须加上「实参落在 a 中」这一限制：第一个合取项已经在两个方向上把定义域限制为 a，故凡记录了东西的实参都是 a 的元素，再说一遍只会把句子拉长。

这一对是一条成员关系等价，而这比看上去更要紧。若反过来陈述为「对 a 中的每个实参，仅仅存在一个取值是那里的那一步」，这句话就容许 f 在正确的对之外还带有多余的对，故它并不确定 f，那条存在性断言不是命题，而针对它的归纳需要一条内部的函数外延性引理，才能从两个逼近得到一个。作为等价，动机是命题，而那条引理根本无须写下。

此处刻意没有单值性合取项。它断言不出第二个合取项尚未给出的任何东西：若在同一个实参处记录了两个取值，则两者都是那个实参处的那一步，而那一步是一条集合等式，同元素的两个集合相等。若加上它，等于拿三个置于满足关系之下的全称量词去换一条推论。

这三个投影就是使用这些定义的人要问的三个问题：有条目的实参在定义域中、定义域中的实参有条目、被记录的取值是一步。把引入放在此处而不放在调用处，理由与每一条读式相同：它解除一次充分性，而那必须在变元环境上做。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

module RecShape (Step : ∀ {n} → Fin n → Fin n → Fin n → Formula S n) where

Domain₀ : S → V ℓ → Type (ℓ-suc ℓ)
Domain₀ h B = (c z : S) → ⟨ pr (c .fst) (z .fst) ∈ h .fst ⟩ → ⟨ c .fst ∈ B ⟩

ApproxAt : ∀ {n} → Fin n → Fin n → Formula S n
ApproxAt f a = domAt f a
             ∧̇ ∀̇ (∀̇ ( appAt (sh2 f) (suc zero) zero
                     ⇒̇ Step zero (suc zero) (sh2 f) ))

GraphAt : ∀ {n} → Fin n → Fin n → Formula S n
GraphAt w b = ∃̇ (ApproxAt zero (suc b) ∧̇ Step (suc w) (suc b) zero)

module _ {n : ℕ} (f a : Fin n) (γ : Vec S n) where

ApproxAt-dom : ⟨ γ ⊨ ApproxAt f a ⟩ → Domain₀ (lookup f γ) ((lookup a γ) .fst)
ApproxAt-dom h = domAt-out f a γ (h .fst)

ApproxAt-value : ⟨ γ ⊨ ApproxAt f a ⟩ → (c : S)
               → ⟨ c .fst ∈ (lookup a γ) .fst ⟩
               → ∥ (Σ[ z ∶ S ] ⟨ pr (c .fst) (z .fst) ∈ (lookup f γ) .fst ⟩) ∥₁
ApproxAt-value h = domAt-in f a γ (h .fst)

ApproxAt-step : ⟨ γ ⊨ ApproxAt f a ⟩ → (c z : S)
              → ⟨ pr (c .fst) (z .fst) ∈ (lookup f γ) .fst ⟩
              → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩
ApproxAt-step h c z p = h .snd c z
  (subst ⟨_⟩ (sym (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ))) p)

ApproxAt-in : ⟨ γ ⊨ domAt f a ⟩
            → ((c z : S) → ⟨ pr (c .fst) (z .fst) ∈ (lookup f γ) .fst ⟩
               → ⟨ (z ∷ c ∷ γ) ⊨ Step zero (suc zero) (sh2 f) ⟩)
            → ⟨ γ ⊨ ApproxAt f a ⟩
ApproxAt-in hd hs = hd , λ c z p → hs c z
  (subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (z ∷ c ∷ γ)) p)

module _ {n : ℕ} (w b : Fin n) (γ : Vec S n) where

GraphOf : Type (ℓ-suc ℓ)
GraphOf = Σ[ f ∶ S ] ( ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
                     × ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ )

Graph-in : (f : S) → ⟨ (f ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
         → ⟨ (f ∷ γ) ⊨ Step (suc w) (suc b) zero ⟩ → ⟨ γ ⊨ GraphAt w b ⟩
Graph-in f ha hs = ∣ f , (ha , hs) ∣₁

Graph-out : ⟨ γ ⊨ GraphAt w b ⟩ → ∥ GraphOf ∥₁
Graph-out h = h

PairGraphAt : ∀ {n} → Fin n → Fin n → Formula S n
PairGraphAt e c = ∃̇ (prAtL (suc e) (suc c) zero ∧̇ GraphAt zero (suc c))

module _ {n : ℕ} (e c : Fin n) (γ : Vec S n)
         (φ : Formula S n) (qφ : φ ≡ PairGraphAt e c) where

PairOf : Type (ℓ-suc ℓ)
PairOf = Σ[ z ∶ S ] ( ((lookup e γ) .fst ≡ pr ((lookup c γ) .fst) (z .fst))
                    × ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ )

PairGraph-in : (z : S) → (lookup e γ) .fst ≡ pr ((lookup c γ) .fst) (z .fst)
             → ⟨ (z ∷ γ) ⊨ GraphAt zero (suc c) ⟩ → ⟨ γ ⊨ φ ⟩
PairGraph-in z q hg = subst (λ ψ → ⟨ γ ⊨ ψ ⟩) (sym qφ)
  ∣ z , (subst ⟨_⟩
    (sym (prAtL-adequate (suc e) (suc c) zero (z ∷ γ))) q , hg) ∣₁

PairGraph-out : ⟨ γ ⊨ φ ⟩ → ∥ PairOf ∥₁
PairGraph-out h = map₁
  (λ { (z , (hq , hg)) →
    z , (subst ⟨_⟩ (prAtL-adequate (suc e) (suc c) zero (z ∷ γ)) hq , hg) })
  (subst (λ ψ → ⟨ γ ⊨ ψ ⟩) qφ h)

open RecShape StepAt public renaming ( GraphAt to LsetGraphAt
                                     ; Graph-in to LsetGraph-in
                                     ; Graph-out to LsetGraph-out )

层级逼近之图

PairGraphAt 识别由序数实参与逼近在该处所赋取值组成的有序对。最后的图公式恰好汇集这些有序对，把逐点逼近变成表示层级序列的集合。

在逼近上有一个存在量词，其下是本章为之而写的两个合取项：f 是那个实参上的一个逼近，而那个取值是「在那个实参处、由 f 算出的那一步」。取值排在第一位，实参排在第二位，这正是模型的替换字段读一个图时所用的顺序；LsetGraph 就是把这两个分量填好之后的那个句子。

逼近被绑定，而且必须如此。一个图不可以点名它所定义的对象；且仅当某物已知是 L 的元素时，它才可以断言该物存在，因为满足关系是在模型处读的。逼近正是这样：它是由较低的诸实参经替换收集起来的对之集，而不是它所描述的那座塔。消费方提供一个逼近，而图只断言存在一个。

两种读法各只一行，因为被满足的存在量词就是一个截断的 sigma，被满足的合取就是一个对。它们带来的不是证明，而是那个名字与那个分量：GraphOf 把载荷的类型写了出来，不交给推断；两种读法都占据一个变元环境的变元位，故消费方是去实例化它们，而不是与它们作转换。

命名是本节的全部代价，这个数字值得留存，因为对它的第一次诊断是错的。若把图以它那个闭句别名来称呼，同样两行占掉了本章 130 秒中的 98 秒。当初被怪罪的是那两个分量，而它们是清白的：下一章一次隔离测量把「读式落在完全具体的位上」量到十五毫秒，把「同一条读式对着一个别名」量到五十一秒。真正耗时的是「判定别名的满足关系与它展开式的满足关系相等」，而 Agda 解决它的办法，是把一个内部装着整条可定义幂集描述的满足关系正规化。落在变元位上，诸读式根本不会遇到这个问题，而那个闭句只差一次展开。

小结

所得集合编码图记录直到某个序数界为止的逐次可构造层，其中步骤关系已经由后续内部描述所需的可定义幂集公式表达。

LsetGraph 是对象语言中「取值是实参处的层」这个句子，写下来时不点名任何层、任何塔、任何序数。StepAt 是一次 extAt 罩住三个相邻的存在量词，即那个实参、在其处所记录的取值，以及它的可定义幂集；ApproxAt 是两个合取项，即定义域与那条步进条件，再无其他。

此处没有任何东西被证两遍。可定义幂集以「落在一位上的描述」的形式来自上一章，并按既有形式直接使用；函数机器从 appAt 与 domAt 上读出；而那一步的两种读法就是 extAt 自己的那两个。本章所贡献的是形状：一个查阅逼近而非查阅塔的图，而那是一个图被允许拥有的唯一形状。

有两条裁定被记录在读者与之相遇之处。那一步是一条成员关系等价，而非一个单向的收集，这使即将到来的那场归纳的动机保持为命题，并把一条内部的函数外延性引理整个从证明路线中省去。此外，没有单值性合取项，因为步进条件已经唯一确定了「在一个实参处记录的每个取值」，故单值性是一条推论，不是一条假设。

一次测量，而紧随本章的下一章更正了它的诊断。本章曾经花掉的每一秒，都是「同一样东西的两种写法」之间的一次转换，而 Agda 每一次都以「把一个内部装着整条可定义幂集描述的满足关系正规化」来应对：两条读法对着图的那个闭句别名而取，98 秒；每一处「假设把环境写开，而应用把它藏在一个缩写背后」，各 15 秒。具体位不涉及那个机制，几乎不耗时。写成两侧是同一个表达式之后，本章在两秒之内、而不是 130 秒检查完毕，数学分毫未改。前几章据以写下的那条规矩，即充分性在变元实参处解除，对一条陈述成立，与它对一次代换成立完全一样。