---
title: "L 内部的可构造层级"
module: L.Hierarchy
lang: zh
site: "Bedrock"
description: "L 内部的可构造层级"
stage: "内部编码：表与统一满足关系"
reading_order: 71
canonical: https://bedrock.institute/zh/L.Hierarchy.html
html: L.Hierarchy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Hierarchy.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.HierarchySequence]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Hierarchy.md, https://bedrock.institute/ja/L.Hierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 内部的可构造层级

`L` 内的一阶图记录外部的可构造层级，直至给定序数。表中的值与外部层级逐一对照，被证明具有函数性且精确；随后这些对被收集成一个可构造集合，其成员恰是此前各层。

本章构造内部层级。对层级中的序数 `α`，`hierL` 在 `α` 处是 `L` 的一个元素，其成员恰是有序对「低于 `α` 的序数 `β` 与塔在该处的取值 `Lset β`」。全章重复同一个模式。**表**是有序对之集；说它在集合 `B` 上**正确**，指它在 `B` 以下记录的每个取值都是元层面的塔在那里的取值；说它**完备**，指它在以下的每个实参处都记录了取值。正确且完备的表，恰是图的步进条件所读出的内容，也恰是步进条件据以写下的内容；因此连接步进与塔的那对引理同时服务于消去与引入。

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

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

module L.Hierarchy {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

本章在模型自身层级的后继处取一份排中律实例并在其下运行；以下每个构造都陈述于本模块之内，只在公理章传递之处携带这一假设。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
```

这里有两个结构。环境层级贡献其结构 `𝒮ᵥ`，本章将使用它的隶属归纳与外延性；可构造结构 `𝒮ʟ` 贡献载体 `S`，其元素是层级中的集合连同「其可构造」的证明，故每个载体元素 `x` 都有底层集合 `fst x`。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV )
open import V.Coding {ℓ} using ( pr; pr-inj )
```

层级给出全章使用的三件工具：沿隶属的归纳、集合的外延性，以及有序对 `pr` 连同找回其分量的单射性。这个对住在层级那一层，而表的被记录条目也住在那里。

```agda
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; Lset; Lset-in; Lset-out; IsOrd )
```

可构造一侧给出塔 `Lset`，它把层级的一个序数送到该处的可构造层；可定义幂集 `𝒟ₒ`；两条隶属读式 `Lset-in` 与 `Lset-out`；序数性 `IsOrd`；以及「可构造性沿隶属传递」这一事实。塔由序数索引，序数是层级的集合；从不由宇宙层级索引，后者是类型的大小指标。

```agda
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`。

```agda
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst; domAt-intro )
```

前一编码章贡献本章要组装的词汇：带见证与三条读式的步进条件，带定义域、取值与步进子句的逼近，有两条读式的塔之图，以及有序对图。

```agda
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 )
```

命题机制是常用的那一套：截断的存在、其注入与消去、「第二分量为命题的序对在第一分量相等时即相等」，以及把隶属的逐点等价转成集合路径的操作。

```agda
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-集合性使两个被制表集合的相等成为命题。

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

在可构造结构内部，`S` 是载体，`⊨` 是满足判断；`SetOf` 把候选集合与「它实现一个类」的断言配成对，record 的各字段正是以这种形式陈述其公理。

```agda
open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

满足关系最终在可构造结构处读取：全章的记号 `γ ⊨ φ` 都是在载体元素的环境处、以取自 `L` 的常元判断对象语言公式。

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

一个私有辅助把变元槽后移两位：当一步要在「先加取值、再加实参」而扩展的环境中判读时，所有旧槽都后移两位。凡从表自身的条目内部判读该表的步进时，它都会出现。

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

## 表记录什么

**表**是有序对之集，这里总是取层级配对所成的对：一个实参连同一个取值。三个条件刻画表在界集 `B` 上的样子，它们是互补的条件，而不是同一句陈述的三种读法。`Values` 要求：在 `B` 以下记录的每个取值都是塔在那里的取值。`Entries` 要求：`B` 以下的每个实参处都记录了正準条目。`Domain` 要求：`B` 以外的东西完全没有被记录。

```agda
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` 是它呈现的那个集合。

```agda
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` 以下记录的恰是那些典范条目，没有任何走样。

```agda
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` 把步进见证变成塔的成员。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) where
  private
```

三个槽位命名取值、实参与表，全部从同一环境 `γ` 的载体元素读出。

```agda
    ok : IsOrd (fst (lookup b γ)) → Values (lookup f γ) (fst (lookup b γ))
       → PowOK b f γ
```

旁条件被一次性解除，同时服务两个方向。`PowOK` 要求：每个被记录取值的可定义幂集是 `L` 的元素；而被记录取值是塔在 `B` 以下某个实参处的取值，该实参因 `B` 是序数而是序数，且以序数为索引的层，其可定义幂集可构造。故那一步所需的全部，就是正确性加上单独一条序数性假设，而两种读法的陈述里都不带该条件。两个方向分开命名，因为它们分开使用。向上是「被记录取值的可定义幂集落在 `B` 处的塔里面」，即 `Lset-in`。向下是塔自身的分解 `Lset-out`，随后把分解给出的序数记为模型的元素，这一步由类的传递性供给。

```agda
    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 把两条事实对齐到同一个取值上。

```agda
    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` 的被记录取值。

```agda
    below ob ents z (δ , (δ∈ , hz)) =
      d , (LsetS δ oδ , ((δ∈ , ents d δ∈) , hz))
```

见证在实参 `d`，即 `δ` 的载体元素处给出：由完备性，表在该处记录典范条目。那里的被记录取值是 `δ` 处的层 (呈现为 `L` 的元素)，而由分解，`z` 落在其可定义幂集中。

```agda
      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` 把集合与这份证书打包在一起。

```agda
    above : Values (lookup f γ) (fst (lookup b γ)) → (z : S) → StepOf b f γ z
          → ⟨ fst z ∈ Lset (fst (lookup b γ)) ⟩
```

`above` 是镜像：步进见证把一个成员放进塔里。见证指名低于实参的实参 `c`、其处被记录的取值 `w`，以及 `z` 属于 `w` 之可定义幂集的成员资格。

```agda
    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` 处的塔里。

```agda
  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 γ))
```

向上引理读作：若步进条件在该环境处成立、实参是序数、且表在其上正确而完备，则在取值槽位记录的取值就是塔在实参处的取值。

```agda
  step-Lset h ob vals ents =
    extensionalV {a = fst (lookup v γ)} {b = Lset (fst (lookup b γ))} pt
    where
```

层级中成员相同的两个集合相等，这是环境层级的外延性。证明给出逐点等价 `pt`，把路径的组装交给外延性。

```agda
    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` 由见证证明这条命题。

```agda
      where
      z : S
      z = x , isL-trans {x = fst (lookup v γ)} {y = x} hx (lookup v γ .snd)
```

要应用 `above`，须把 `x` 视为载体元素；其可构造性由被记录取值的可构造性而来，因为 `x` 是它的成员。

```agda
    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` 属于被记录取值」这条命题中。

```agda
      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`。

```agda
      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` 把见证变成对被记录取值的隶属。

```agda
    pt : (x : V ℓ) → (x ∈ fst (lookup v γ)) ≡ (x ∈ Lset (fst (lookup b γ)))
    pt x = ⇔toPath (fwd x) (bwd x)
```

对每个成员而言，属于被记录取值与属于塔是同一命题；两个方向给出等价，外延性再逐成员把它提升为集合的相等。

```agda
  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 ⟩
```

向下引理把方向反过来：给定实参的序数性、正确性、完备性，以及「被记录取值就是塔」这一事实，步进条件即告成立。

```agda
  step-table ob vals ents q = StepAt-in v b f γ (ok ob vals) into back
    where
```

步进条件由它的两个方向引入：每个成员都有见证，且每个见证都可靠；旁条件由 `ok` 一并供给。

```agda
    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` 把分解变成见证；见证只需存在即可。

```agda
    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` 施于被记录的那个取值。实参以下的正确性**就是**归纳假设，一字不差。实参以下的完备性则是逼近的取值子句被花掉之处：比这个实参更低的实参落在逼近的定义域以下，因为定义域是序数、而序数传递；逼近于是在那里有取值；而归纳假设把它与塔的取值认同。那个取值只是「仅仅」被拿出来的，而这已经够了，因为要对它证的是一条隶属关系。

```agda
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` 可构造」这一前提之所以被携带，是因为表的条目是载体元素，其第一分量是可构造集合；归纳将从某个序数中的隶属供给这一前提。

```agda
  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` 的序数性假设将在归纳步内被消耗。

```agda
    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` 处的取值。

```agda
      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`，归纳之所以能够到达这一步，全凭于此。

```agda
      ou : IsOrd u
      ou = mem-ord {A = fst (lookup a γ)} oa u u∈a
```

`u` 的序数性由 `a` 的序数性而来，因为 `u` 是 `a` 的成员；这正是该步所需要的关于其所处实参的全部。

```agda
      vals : Values (lookup f γ) u
      vals c y c∈ q = IH (fst c) c∈ (snd c) y q
```

`u` 以下的正确性就是归纳假设，按原样使用：对 `u` 的成员 `c`，第一分量为 `c` 的被记录对所记录的是塔在 `c` 处的取值。`c` 的可构造性随归纳而来，归纳由隶属供给它。

```agda
      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`，逼近在该处记录了某个取值；该条目只是「仅仅」存在，而消去的目标是「典范条目被记录」这条命题。

```agda
        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`，就把被记录取值同认于塔。因此图**确定**它的取值：凡在某个序数处满足它的对象，都是元层面的塔在该处的取值。

这条读式以变元槽形式陈述，这并非装饰。它的各处实例化住在不同的具体环境中；若在某一处陈述，就得通过一个内部装着整条塔描述的满足关系，把它运到另一处。

```agda
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 γ))
```

陈述取塔之图在取值槽与实参槽处的满足、实参的序数性，结论是被记录取值就是塔。除了图成立之外，不假设关于图的任何东西。

```agda
  Lset-only h ob = PT.rec
    (setIsSet (fst (lookup w γ)) (Lset (fst (lookup b γ)))) read
    (LsetGraph-out w b γ h)
    where
```

图展开为一个单纯见证：一个逼近，连同其满足与其在取值处的步进。消去是合法的，因为目标是两个 h-集合的相等，即一条命题；而见证本身也只在这条命题内部被需要。

```agda
    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` 扩展的环境中施用：逼近占据新增的零号槽，取值与实参各上移一位。

```agda
      where
      vals : Values f (fst (lookup b γ))
      vals c z _ p = approx-val zero (suc b) (f ∷ γ) ha ob c z p
```

步进引理所需的正确性，就是把上一节的归纳施于逼近 `ha`：`f` 在实参以下记录的每个取值都是塔在该处的取值。

```agda
      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∈)
```

完备性来自逼近的取值子句：在以下的每个实参处，都「仅仅」记录了某条目。消去的目标是「典范条目被记录」这条命题，因此那个缺席的见证永远不会被需要。

```agda
        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`、实参的序数性、表在实参上的三个条件，以及「被记录取值就是塔」的断言。

```agda
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 γ))
```

结论是塔之图在取值槽与实参槽处成立。

```agda
              → ⟨ γ ⊨ 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`，其正确性、完备性与对塔的同认恰是手头的假设。

```agda
    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` 低于实参。两个方向都需要，因为逼近的定义域条件会以相反的次序使用它们。

```agda
    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` 放到实参以下。

```agda
      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` 低于实参。其内容就是表的第三个条件的一次应用。

```agda
    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)` 由正确性在该被记录对处供给。

```agda
      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` 的两件事实从被记录对读出：其底层集合低于实参，由定义域条件；它是序数，由实参的序数性。

```agda
      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` 的实参低于实参」。这是本章对该传递性的第二次、也是最后一次使用。

```agda
    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` 满足，因为某个实参处的取值是一个构造。

```agda
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-集合的相等本身就是命题，因此这是一个命题上的析取聚合。

```agda
IsHier : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
IsHier B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z)
```

`IsHier B h` 说 `h` 所呈现的集合逐成员地实现被记录的类：在每个 `z` 处，属于该集合与被记录是同一命题。两个方向都不丢弃，因为各有其用：只有隶属而无被记录，会放进陌生者；只有被记录而无隶属，会漏掉应有的对。

```agda
HierOf : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
HierOf B = Σ[ h ∈ S ] IsHier B h
```

`HierOf B` 把实现集合连同其规格收集为一对。这对正是归纳要在每个序数处构造的东西；它的两个分量分别回答对任何构造都要问的两个问题：它是什么，以及它为何合格。

```agda
module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsHier B h) where
```

两条读式对一个带规格的变元实现集合陈述，这样即将到来的构造就可以把它们应用于自己正在建造的集合，无论归纳当前站在哪个层。

```agda
  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` 处的取值。两个结论都由规格施加于该成员而来。

```agda
  hier-out c z p = PT.rec
    (isProp× (snd (fst c ∈ B)) (setIsSet (fst z) (Lset (fst c)))) read
    (subst ⟨_⟩ (sp k) p)
    where
```

该成员的隶属沿规格被运进被记录命题，而那是一条截断的存在；消去的目标是一对命题构成的命题，因此可以在这里消耗见证。

```agda
    k : S
    k = pr (fst c) (fst z)
      , isL-trans {x = fst h} {y = pr (fst c) (fst z)} p (h .snd)
```

成员自身也须被命名为载体元素：底层集合的有序对可构造，因为它属于 `h` 所呈现的可构造集合。

```agda
    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` 处的取值。

```agda
      , (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` 本身为实参)；条目与模型之对相等，则由该对的定义读式给出。

```agda
    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` 的元素，而这正是模型的配对所需要的第二分量。

```agda
opaque
  hierAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → HierOf α
  hierAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → HierOf α}
    (build (PairGraphAt zero (suc zero)) refl)
    where
```

归纳的步进函数把成对的那个图保持为**随身携带自己等式的变元句子**，而不写出它将被实例化成的闭句子。等式随句子同行，因此下面的每条读式都在调用处以 `refl` 施用。

```agda
    build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero)
          → (α : V ℓ)
          → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → HierOf δ)
          → ⟨ isL α ⟩ → IsOrd α → HierOf α
```

步进接收句子及其等式、序数 `α`、它的两张证书，以及归纳假设：`α` 的每个成员处的层级均已建成。它须返回 `α` 处的层级及其规格。

```agda
    build φ qφ α IH hα oα = r .fst .fst , spec
      where
      A : S
      A = α , hα
```

`α` 处的层级是实现者的第一分量，在替换产出之后一次提取；`A` 是呈现为载体元素的 `α`，正是替换消费定义域时所用的形式。

```agda
      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` 与其取值」的有序对，正是被记录类所要求的形式。

```agda
      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` 所要的。环境中载着取值、给图自身量词留的新槽，以及实参。

```agda
        (λ 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` 是有序对图自己的等式。

```agda
        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` 上的纤维被给出，其中包括被绑定的塔值、把条目与模型之对等同的等式，以及塔之图在取值与实参处的满足。见证是纤维的一个元素，即图陈述所断言「仅仅存在」的那个类型的元素。

```agda
      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)` 处成立的塔之图；塔之图确定其取值，配对的单射性等同两条目，而该等式是这些路径的复合。

```agda
      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` 把目标化归于此。

```agda
        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` 的序数性取自 `α` 的序数性。

```agda
          ∙ 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` 把以「仅仅存在」形式呈现的两半，装配成恰为该可缩纤维的居留。

```agda
      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` 的集合而存在的时刻，就是此刻。

```agda
      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
```

余下的是验证：收集所得的集合确实实现被记录的类。规格逐成员比较「属于收集集合」与「是被记录的对」；比较的两个方向分别证明，再合并为逐点等价。

```agda
        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` 处满足有序对图。消去是合法的，因为被记录的类是命题。

```agda
          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` 处取值」之对；底层集合随之而来，这正是「被记录」所要求的。

```agda
        fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst (r .fst .fst) ⟩
        fromRec hz = subst ⟨_⟩ (sym (r .fst .snd z)) (PT.map conv hz)
          where
```

向内读：一条被记录的对给出低于 `α` 的实参连同塔在该处的取值；有序对图在该实参的典范条目处成立，而收集集合含有这条条目。

```agda
          conv : Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩
                   × (fst z ≡ pr (fst c) (Lset (fst c))))
               → Σ[ c ∈ S ] (⟨ fst c ∈ α ⟩ × ⟨ (z ∷ c ∷ []) ⊨ φ ⟩)
```

见证从被记录的呈现转换成图的呈现：实参保持不变，而「底层集合等于典范对」的等式变成有序对图在该处的满足。

```agda
          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` 处的满足。

```agda
              (eq ∙ sym (prʟ-fst c (value c c∈)))

hierL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
hierL α hα oα = hierAt α hα oα .fst
```

某个序数处的内部层级，就是归纳所得的实现集合，呈现为 `L` 的元素。它对每个可构造序数都存在；也就是说：模型如今为它的每个序数准备了一个集合，其成员恰是「低于该序数的序数与塔在该处取值」组成的有序对。

```agda
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` 说别无其他满足者。于是内部之图与元层面的塔在每个可构造序数处、在两个方向上一致。

```agda
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 ⟩
```

陈述取实参的序数性与「被记录取值就是塔在该处的取值」的断言，结论是塔之图成立。这是上一节的向内读式，之所以在每个可构造序数处都可用，是因为内部层级在每个可构造序数处都存在。

```agda
  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` 所消费的。

```agda
    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` 的一个元素；其成员恰是「低于该序数的序数与塔在该处取值」组成的有序对。其规格是归纳所证明的隶属等价。

此处制表的层由序数索引，序数是层级的集合；宿主的宇宙层级是类型的大小指标，从不为塔索引。