---
title: "最早分歧关系的内部族"
module: L.Choice.EarliestDisagreement
lang: zh
site: "Bedrock"
description: "最早分歧关系的内部族"
stage: "典范良序与选择公理"
reading_order: 82
canonical: https://bedrock.institute/zh/L.Choice.EarliestDisagreement.html
html: L.Choice.EarliestDisagreement.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/EarliestDisagreement.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full, L.Recursion, L.Axioms.Infinity, L.Choice.FiniteStageOrders, L.Choice.LimitStageOrder, L.Coding.HierarchySequence, L.Hierarchy, L.Coding.Model, L.Coding.Expressions, FOL.Absoluteness, FOL.ZFModel]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.EarliestDisagreement.md, https://bedrock.institute/ja/L.Choice.EarliestDisagreement.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 最早分歧关系的内部族

在每个有穷层，`before n` 按两个集合的最早分歧来比较它们。本章在 `L` 内用集合 `relAt n` 表示这条关系，再把这些集合组成以数码为索引的族，并用对象语言公式 `BeforeAt` 表达对该族的查找。以此公式实例化 `Described` 后得到 `codeOrder`，它将在后续名字比较中供应码的比较关系。本章本身既不比较名字，也不证明名字比较的良基性。

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

本构造只通过稍后附在模块上的显式假设使用排中律。因此，这一经典假设在本章导出的每项结果中都保持可见。

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

固定宇宙层级 `ℓ`，并假设 `LEM (ℓ-suc ℓ)`。下文的集合、公式与命题值关系都处在这一选择所确定的层级上。

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

我们将在累积层级上用一阶公式描述关系。有序对充当关系条目，稍后再借助其单射性从编码条目恢复两个被比较的集合。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ¬̇_; ∃̇_; ∀̇∈; ∃̇∈ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
```

第 `n` 个有穷层是 `Lset (# n)`，其中 `# n` 是层级内的冯·诺伊曼数码。关于它的序数性与可构造性的证明，使我们能把该层及其每个成员都视为 `L` 模型中的对象。

```agda
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; Lset-mono )
open import L.Ordinal {ℓ} using
  ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; mem-ord; boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
```

两种集合构造承担不同任务。分离从一个界中切出单层关系；替换要到后面才用于沿内部 `ω` 收集这些关系。有穷逼近本身则由 `finSet` 与 `finSetL` 构造。

```agda
open import L.Axioms.Basic {ℓ}
  using ( extensionalL; LsetS; ∅ʟ; finSet; finSet-in; finSet-out; module FinOf )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Recursion {ℓ} lem using ( smallDom; mereFunct )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
```

数学递归已经确定：`before zero` 为空；`before (suc n)` 用 `before n` 排列较早的点，并在 `finiteStage n` 上按最早分歧比较下一有穷层的成员。`PrecedesAt` 在对象语言中表达这个后继步，`RecShape` 则组织它的有穷逼近。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( before; precedes; Agrees; Witness; finiteStage )
open import L.Choice.LimitStageOrder {ℓ} lem
  using ( PrecedesAt; module Precedes; module Described )
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt; module RecShape )
```

对象语言中的应用与外延性，使公式能够断言某个集合是关系值表的一项取值。我们先用它们描述一个递归步，之后再用它们读取完整族在某个数码处的值。

```agda
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; appC; appC-adequate; domAt-intro )
open import L.Coding.Expressions {ℓ} using ( numL; extAt; extAt-out; extAt-in; extAt-in-both )
```

证明中会反复沿集合与有序对的等式作运输，还会对自然数严格序作归纳，以证明逼近所记录的每个取值都是唯一确定的。

```agda
import FOL.Absoluteness
import FOL.ZFModel
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Nat.Order using
```

这项归纳使用自然数 `<` 的良基性：先认定所有更小索引处的值，才能确定 `k` 处的值。这与 `before` 本身的任何良基性质是两回事。

```agda
  ( _<_; <-trans; <-asym; pred-≤-pred; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Induction.WellFounded using ( module WFI )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.FinData.Properties using ( toℕ<n; enum; toℕ∘enum )
```

下文若干见证只能在命题截断下取得。这种见证只保证存在，并不选出规范资料；只有当目标是命题时才能消去，例如隶属、`before`，或 `V` 中集合的等式。

```agda
open import Cubical.Data.FinData.Base using ( toℕ )
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 )
```

集合通过其成员的呈现来访问。借助这种呈现，我们可以遍历有穷层的所有成员并构造它们的有序对；内部 `ω` 则提供整个族最终的定义域。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω )
```

从现在起，公式都在可构造集合所承载的命题值结构中解释。

```agda
open hPropStructure 𝒮ʟ
```

载体 `S` 由一个集合及其属于 `L` 的证明组成。因此，构造内部关系既要给出底层集合，也要给出它的可构造性证明。

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

绝对性把这一结构中的满足关系与底层集合上的相应断言联系起来。记号 `γ ⊨ φ` 表示赋值 `γ` 满足对象语言公式 `φ`。

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

绑定两个新变元会使原有的每个 de Bruijn 位置后移两位。映射 `sh2` 记录这一变化，使每个自由变元在新增绑定之下仍指称原来的对象。

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

把二位移位应用两次得到 `sh4`，它用于穿过四个新增绑定。

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

同样，`sh6` 在新增六个绑定时保持原有引用。这些移位只改变 de Bruijn 位置，不改变公式的数学内容。

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

对象 `stageS n` 把有穷层 `Lset (# n)` 封装为可构造载体的一个元素。保持这一封装不透明，可使后续论证不依赖其中可构造性证明的具体写法。

```agda
opaque
  stageS : ℕ → S
  stageS n = LsetS (# n) (numeral-ord n)
```

等式 `stageS-fst` 恰好揭示该封装所携带的数学集合：它的第一分量是 `finiteStage n`。

```agda
  stageS-fst : (n : ℕ) → fst (stageS n) ≡ finiteStage n
  stageS-fst n = refl
```

对象 `numS k` 类似地把冯·诺伊曼数码 `# k` 与其可构造性证明封装在一起。

```agda
  numS : ℕ → S
  numS k = # k , numL k
```

等式 `numS-fst` 让后面的公式读取底层数码，而无须展开与它一同保存的证明。

```agda
  numS-fst : (k : ℕ) → fst (numS k) ≡ # k
  numS-fst k = refl
```

若 `z` 属于可构造集合 `A`，则 `L` 的传递性说明 `z` 也可构造。封装 `memS A z h` 记录这一结论，使 `z` 能作为模型元素使用。

```agda
  memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S
  memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A)
```

`memS A z h` 的第一分量仍是原集合 `z`；新增分量只提供它属于 `L` 的证明。

```agda
  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z
  memS-fst A z h = refl
```

对模型元素 `a` 与 `b`，`prS a b` 在 `L` 内构造它们的有序对。下文的关系集合正以这种对象为成员。

```agda
  prS : S → S → S
  prS a b = prʟ a b
```

忘掉可构造性证明后，就恢复普通有序对 `pr (fst a) (fst b)`。这条等式把内部隶属断言与底层集合上的关系 `before` 联系起来。

```agda
  prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b)
  prS-fst a b = prʟ-fst a b
```

特别地，`finiteStage n` 的每个成员 `x` 都能提升到载体 `S`；该层本身提供这项提升所需的可构造性证明。

```agda
stageEl : (n : ℕ) (x : V ℓ) → ⟨ x ∈ finiteStage n ⟩ → S
stageEl n x h = x , Lset→isL (# n) (numeral-ord n) x h
```

## 每层的关系，作为 `L` 的一个元素

要用分离表示一条关系，首先需要一个包含所有可能条目的集合。因此，`pairsAt n` 给出可构造界 `D`：只要 `u,v` 都属于 `finiteStage n`，`D` 就包含 `pr u v`。

```agda
pairsAt : (n : ℕ)
        → Σ[ D ∈ S ] ((u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
                     → ⟨ pr u v ∈ fst D ⟩)
pairsAt n = d .fst , onPair
  where
```

有穷层中被呈现的成员已经携带自己的隶属证明。映射 `ixL` 再附上由此得到的可构造性证明，把每个被呈现成员变成 `S` 的元素。

```agda
  ixL : ⟪ finiteStage n ⟫ → S
  ixL m = ⟪ finiteStage n ⟫↪ m
        , Lset→isL (# n) (numeral-ord n) (⟪ finiteStage n ⟫↪ m)
            (∈∈ₛ {a = ⟪ finiteStage n ⟫↪ m} {b = finiteStage n} .snd
              (∈ₛ⟪ finiteStage n ⟫↪ m))
```

两个呈现的乘积索引了该层成员的每一对。对这些内部有序对应用 `smallDom`，便把整个索引族放入同一个可构造集合 `D` 中。

```agda
  d : Σ[ D ∈ S ] ((p : ⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
                  → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ finiteStage n ⟫ × ⟪ finiteStage n ⟫)
        (λ p → prʟ (ixL (fst p)) (ixL (snd p)))
```

给定任意 `u,v ∈ finiteStage n`，它们的隶属证明给出呈现索引 `fu` 与 `fv`。该界包含这两个索引处的有序对，再沿恢复出的分量等式运输，便得到 `pr u v` 本身属于该界。

```agda
  onPair : (u v : V ℓ) → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
         → ⟨ pr u v ∈ fst (d .fst) ⟩
  onPair u v hu hv = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩)
    (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd))
    (d .snd (fu .fst , fv .fst))
```

两个纤维 `fu` 与 `fv` 恰好记录呈现索引，以及把相应被呈现成员认同为 `u`、`v` 的等式。

```agda
    where
    fu = ∈-asFiber {a = u} {b = finiteStage n} hu
    fv = ∈-asFiber {a = v} {b = finiteStage n} hv
```

设在同一载体 `A` 上，每个 `R' w z` 都蕴含 `R w z`。那么，关于 `R` 的最早分歧见证也给出关于 `R'` 的见证。方向发生反转，是因为较早点上的关系出现在一致性子句的前件中。

```agda
precedes-map : (R R' : V ℓ → V ℓ → hProp (ℓ-suc ℓ)) (A x y : V ℓ)
             → ((w z : V ℓ) → ⟨ w ∈ A ⟩ → ⟨ z ∈ A ⟩ → ⟨ R' w z ⟩ → ⟨ R w z ⟩)
             → ⟨ precedes R A x y ⟩ → ⟨ precedes R' A x y ⟩
precedes-map R R' A x y f = PT.map step
  where
```

分歧点 `z`、它属于 `A` 与 `y` 的证明，以及它不属于 `x` 的证明都保持不变。需要转换的只有 `x` 与 `y` 在 `z` 之前一致的证明。

```agda
  step : Σ[ z ∈ V ℓ ] Witness R A x y z → Σ[ z ∈ V ℓ ] Witness R' A x y z
  step (z , (z∈A , (z∈y , (z∉x , ag)))) =
    z , (z∈A , (z∈y , (z∉x , ag')))
    where
    ag' : Agrees R' A x y z
```

在较早点 `w`，先把假设 `R' w z` 映到 `R w z`，再交给原有的一致性证明，由此得到相对于 `R'` 的一致性。

```agda
    ag' w w∈A hR' = ag w w∈A (f w z w∈A z∈A hR')
```

分离条件只把候选关系条目作为自由变元。它用存在量词绑定前一关系与前一层，以等式把它们固定为给定常元，并让两个端点在当前层中取值。

```agda
RelCond : (R A A' : S) → Formula S 1
RelCond R A A' =
  ∃̇ ( (var zero ≐ con R)
    ∧̇ ∃̇ ( (var zero ≐ con A)
         ∧̇ ∃̇∈ (con A') ( ∃̇∈ (con A')
```

余下的合取把候选条目认同为两个端点的有序对，并断言它们相对于给定的前一层与前一关系满足 `PrecedesAt`。这正是递归步骤稍后采用的后继比较；区别在于，此处的 `RelCond` 用常元固定前一层与前一关系，而递归公式从逼近中取得关系，并通过层级图识别相应的层。

```agda
              ( prAtL (sh2 (sh2 zero)) (suc zero) zero
              ∧̇ PrecedesAt (sh2 (suc zero)) (sh2 zero) (suc zero) zero ) ) ) )
```

现在递归定义表示关系的集合。零处关系为空；在后继处，分离从包含较大有穷层全部成员对的界开始。

```agda
opaque
  relAt : ℕ → S
  relAt zero    = ∅ʟ
  relAt (suc n) =
    hasSeparationL (pairsAt (suc n) .fst)
```

在这个界中，`RelCond (relAt n) (stageS n) (stageS (suc n))` 恰好选出那些按以前一关系为基础的后继子句进行比较的端点对。

```agda
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .fst
```

等式 `relAt-zero` 显式记录基例，使得以后能把所谓零层关系成员化为对空集的隶属，从而排除它。

```agda
  relAt-zero : relAt zero ≡ ∅ʟ
  relAt-zero = refl
```

在后继层，属于 `relAt (suc n)` 包含两部分：候选条目属于有序对之界，并且满足由 `relAt n`、前一层与当前层确定的分离公式。

```agda
  relAt-mem : (n : ℕ) (z : S)
            → (z ∈ˢ relAt (suc n))
            ≡ ( (z ∈ˢ pairsAt (suc n) .fst)
              ⊓ ((z ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n))) )
  relAt-mem n =
```

这条等价正是分离所给出的精确刻画。后续证明会双向使用它：或从隶属中取出公式，或由界证明与公式证明合成隶属。

```agda
    hasSeparationL (pairsAt (suc n) .fst)
      (RelCond (relAt n) (stageS n) (stageS (suc n))) .fst .snd
```

谓词 `Rel n a b` 是有序对 `pr a b` 属于表示集合 `relAt n` 的缩写。接下来的表示引理将证明，对该层成员而言，这一谓词等价于 `before n a b`。

```agda
Rel : ℕ → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Rel n a b = pr a b ∈ fst (relAt n)
```

这些引理的证明会在含五个条目的环境中解释 `PrecedesAt`。在外围绑定造成移位后，`s1` 与 `s2` 标出端点槽与层槽的位置。

```agda
private
  s1 : Fin 5
  s1 = suc zero
  s2 : Fin 5
  s2 = sh2 zero
```

其余位置 `s3` 与 `s4` 分别指向前一关系和编码后的有序对。统一命名这些位置，使语义论证始终与 `RelCond` 中的四种角色对齐。

```agda
  s3 : Fin 5
  s3 = sh2 (suc zero)
  s4 : Fin 5
  s4 = sh2 (sh2 zero)
```

要辨认关系集的任意成员，必须恢复它的两个分量。因此，`RelOf k zv` 要求给出 `finiteStage k` 中的 `x,y`、把 `zv` 认同为其有序对的等式，以及 `before k x y` 成立的证明。这个见证类型包含选定的分量，故其本身不一定是命题。

```agda
RelOf : (k : ℕ) → V ℓ → Type (ℓ-suc ℓ)
RelOf k zv = Σ[ x ∈ S ] Σ[ y ∈ S ]
  ( ⟨ fst x ∈ finiteStage k ⟩
  × ( ⟨ fst y ∈ finiteStage k ⟩
    × ( (zv ≡ pr (fst x) (fst y)) × ⟨ before k (fst x) (fst y) ⟩ ) ) )
```

从 `relAt k` 的隶属关系只能在命题截断下得到这样的分量：关系只记录合适的呈现存在，并不规范地选定一份呈现。反过来，显式给出的分量及其比较足以把该有序对写入关系。

```agda
relAt-out : (k : ℕ) (zv : V ℓ) → ⟨ zv ∈ fst (relAt k) ⟩ → ∥ RelOf k zv ∥₁
relAt-in  : (k : ℕ) (zv : V ℓ) → RelOf k zv → ⟨ zv ∈ fst (relAt k) ⟩
```

基例反映 `before zero`：`relAt zero` 为空，所以假定的成员会导出矛盾。在后继情形，隶属首先给出分离条件，而其中的存在见证只能经命题截断使用。

```agda
relAt-out zero zv h = Empty.rec
  (∅-empty zv (∈∈ₛ {a = zv} {b = ∅} .fst
    (subst (λ t → ⟨ zv ∈ fst t ⟩) relAt-zero h)))
relAt-out (suc n) zv h = PT.rec squash₁
  (λ { (r , (qr , ha)) → PT.rec squash₁
```

逐层打开被截断的见证后，可以看到候选的前一关系、相应有穷层及有序对的两个分量。证明在把这些资料交给最后的重构时始终保留命题截断，因此不会把某份特定呈现作为选定资料带出。

```agda
    (λ { (a , (qa , hx)) → PT.rec squash₁
      (λ { (x , (x∈ , hy)) → PT.map (atY r a x qr qa x∈) hy }) hx }) ha }) cond
  where
  zS : S
  zS = memS (relAt (suc n)) zv h
```

由 `zv ∈ relAt (suc n)` 及 `L` 的传递性，可以把底层集合 `zv` 封装成 `L` 的元素。这样便能在当前分析的这个成员上解释对象语言的分离条件。

```agda
  qz : fst zS ≡ zv
  qz = memS-fst (relAt (suc n)) zv h
```

分离的定义性质把所假定的隶属转成 `RelCond` 的满足关系。因此，后续论证可以使用该条件的数学内容，而不只停留在属于有界对集这一事实上。

```agda
  cond : ⟨ (zS ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = subst ⟨_⟩ (relAt-mem n zS)
    (subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (sym qz) h) .snd
```

对候选分量 `x,y`，剩余公式体陈述两件事：当前分析的成员是它们的有序对，并且 `x` 在前一层上按最早分歧先于 `y`。第二项仍使用 `r` 所表示的关系，因为外围见证还须把该关系认同为 `relAt n`。

```agda
  Body : (r a x y : S) → Type (ℓ-suc ℓ)
  Body r a x y =
      ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ prAtL s4 s1 zero ⟩
    × ⟨ (y ∷ x ∷ a ∷ r ∷ zS ∷ []) ⊨ PrecedesAt s3 s2 s1 zero ⟩
```

从后继层选定 `x` 后，`AtY` 记录从同一层选择 `y`，并附上配对与比较事实。把两个选择分开，正好对应 `RelCond` 中嵌套的存在结构。

```agda
  AtY : (r a x : S) → Type (ℓ-suc ℓ)
  AtY r a x = Σ[ y ∈ S ] (⟨ fst y ∈ fst (stageS (suc n)) ⟩ × Body r a x y)
```

所有见证齐备后，层等式把两个分量都放入 `finiteStage (suc n)`。余下工作是把当前成员认同为其有序对，并把依据所表示关系作出的比较转成 `before (suc n)`；随后两部分分别完成这两种转换。

```agda
  atY : (r a x : S) → fst r ≡ fst (relAt n) → fst a ≡ fst (stageS n)
      → ⟨ fst x ∈ fst (stageS (suc n)) ⟩ → AtY r a x → RelOf (suc n) zv
  atY r a x qr qa x∈ (y , (y∈ , (hpr , hprec))) =
    x , (y , ( subst (λ t → ⟨ fst x ∈ t ⟩) (stageS-fst (suc n)) x∈
             , ( subst (λ t → ⟨ fst y ∈ t ⟩) (stageS-fst (suc n)) y∈
```

供应关系与 `relAt n` 的等式，使其中记录的任意前驱对都能读成 `Rel n`。这是用本章构造的具体关系解释通用 `PrecedesAt` 陈述所需的一个方向。

```agda
               , (sym qz ∙ qpair , below) ) ) )
    where
    Rrep : (s t : S) → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
         → ⟨ Rel n (fst s) (fst t) ⟩
    Rrep s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) qr p
```

反向搬运把 `Rel n` 的证明写回所供应的关系。有了这两个方向，`PrecedesAt` 的充分性定理便能把两种呈现当作同一个基底关系处理。

```agda
    Rfill : (s t : S) → ⟨ Rel n (fst s) (fst t) ⟩
          → ⟨ pr (fst s) (fst t) ∈ fst (lookup s3 (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) ⟩
    Rfill s t p = subst (λ w → ⟨ pr (fst s) (fst t) ∈ w ⟩) (sym qr) p
```

固定这两条表示映射后，`Precedes` 模块提供对象语言公式与宿主谓词 `precedes` 之间的语义桥梁。这座桥只处理一次比较步骤，并不在这里证明任何序性质。

```agda
    module P = Precedes s3 s2 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])
                        (Rel n) Rrep Rfill
```

读出 `PrecedesAt` 得到在公式所供应之层上的 `precedes` 比较。层等式再把该载体认同为 `finiteStage n`，也就是 `before (suc n)` 的递归定义所使用的载体。

```agda
    onStage : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
    onStage = subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩)
      (qa ∙ stageS-fst n) (P.PrecedesAt-out hprec)
```

在一致性子句内部，每次使用基底关系时，都必须把 `before n` 转为 `relAt n` 中的隶属。归纳得到的写入引理完成这一转换，随后 `precedes-map` 恰好给出后继关系 `before (suc n)`。

```agda
    below : ⟨ before (suc n) (fst x) (fst y) ⟩
    below = precedes-map (Rel n) (before n) (finiteStage n) (fst x) (fst y)
      (λ w t hw ht hb → relAt-in n (pr w t)
        (stageEl n w hw , (stageEl n t ht , (hw , (ht , (refl , hb))))))
      onStage
```

配对公式的充分性把封装后的成员认同为 `pr (fst x) (fst y)`。再与封装等式复合，便得到原始 `zv` 所需的等式。

```agda
    qpair : fst zS ≡ pr (fst x) (fst y)
    qpair = subst ⟨_⟩ (prAtL-adequate s4 s1 zero (y ∷ x ∷ a ∷ r ∷ zS ∷ [])) hpr
```

当 `k = 0` 时，`RelOf` 见证已经包含不可能的 `before zero` 证明，所以写入方向由矛盾得出。在后继情形，目标有序对先被放入有界对集，再证明它满足分离条件。

```agda
relAt-in zero zv (x , (y , (x∈ , (y∈ , (qq , hb))))) = Empty.rec* hb
relAt-in (suc n) zv (x , (y , (x∈ , (y∈ , (qq , hb))))) =
  subst (λ t → ⟨ t ∈ fst (relAt (suc n)) ⟩) (prS-fst x y ∙ sym qq)
    (subst ⟨_⟩ (sym (relAt-mem n (prS x y))) (inBound , cond))
  where
```

两个层隶属假设把该有序对放入 `pairsAt (suc n)`。这是分离所需的界：只有有穷层成员组成的对才可能进入 `relAt (suc n)`。

```agda
  inBound : ⟨ prS x y ∈ˢ pairsAt (suc n) .fst ⟩
  inBound = subst (λ t → ⟨ t ∈ fst (pairsAt (suc n) .fst) ⟩) (sym (prS-fst x y))
    (pairsAt (suc n) .snd (fst x) (fst y) x∈ y∈)
```

在反向构造中，环境含有实际的前一关系 `relAt n`，故把它解释为 `Rel n` 只需恒等映射。于是可以使用同一座语义桥，从宿主层比较构造 `PrecedesAt`。

```agda
  module P = Precedes s3 s2 s1 zero
                      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
                      (Rel n) (λ _ _ p → p) (λ _ _ p → p)
```

假设 `before (suc n) x y` 展开为以 `before n` 为基底的最早分歧。为了用内部关系表达同一份一致性，每个已记录的前置有序对都经 `relAt-out` 读出；由于目标 `before n w t` 是命题，可以消去命题截断。

```agda
  held : ⟨ precedes (Rel n) (finiteStage n) (fst x) (fst y) ⟩
  held = precedes-map (before n) (Rel n) (finiteStage n) (fst x) (fst y)
    (λ w t hw ht hR → PT.rec (snd (before n w t)) (readBack w t)
      (relAt-out n (pr w t) hR))
    hb
```

读回的 `RelOf` 见证可能使用不同于 `w,t` 的分量，但其中的配对等式说明其有序对等于 `pr w t`。有序配对的单射性分别认同两个分量，随后所记录的 `before n` 证明便具有所需端点。

```agda
    where
    readBack : (w t : V ℓ) → RelOf n (pr w t) → ⟨ before n w t ⟩
    readBack w t (p , (q , (p∈ , (q∈ , (qq' , hbf))))) =
      subst2 (λ s u → ⟨ before n s u ⟩)
        (sym (pr-inj qq' .fst)) (sym (pr-inj qq' .snd)) hbf
```

转换后的宿主层比较已满足 `PrecedesAt-in` 的假设。它给出分离公式所需的比较子句，其中前一层与前一关系位于相应变元中。

```agda
  hprec : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ [])
          ⊨ PrecedesAt s3 s2 s1 zero ⟩
  hprec = P.PrecedesAt-in
    (subst (λ w → ⟨ precedes (Rel n) w (fst x) (fst y) ⟩) (sym (stageS-fst n))
      held)
```

候选成员本就是 `prS x y`，因此满足配对识别公式。其充分性等式把这一内部构造连接到公式所要求的底层有序对。

```agda
  hpr : ⟨ (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []) ⊨ prAtL s4 s1 zero ⟩
  hpr = subst ⟨_⟩
    (sym (prAtL-adequate s4 s1 zero
      (y ∷ x ∷ stageS n ∷ relAt n ∷ prS x y ∷ []))) (prS-fst x y)
```

`stageS (suc n)` 的呈现等式把 `finiteStage (suc n)` 的每个已知成员搬运到公式使用的层对象中。这里不需要额外的闭包性质。

```agda
  onStage : (w : V ℓ) → ⟨ w ∈ finiteStage (suc n) ⟩
          → ⟨ w ∈ fst (stageS (suc n)) ⟩
  onStage w hw = subst (λ t → ⟨ w ∈ t ⟩) (sym (stageS-fst (suc n))) hw
```

刚构造的见证满足完整的分离条件：它们认同前一关系与前一层，把 `x,y` 放入后继层，并建立配对与最早分歧。嵌套存在量词在命题截断下引入，只断言存在，并不选取规范见证。

```agda
  cond : ⟨ (prS x y ∷ []) ⊨ RelCond (relAt n) (stageS n) (stageS (suc n)) ⟩
  cond = ∣ relAt n , (refl
       , ∣ stageS n , (refl
       , ∣ x , (onStage (fst x) x∈
       , ∣ y , (onStage (fst y) y∈ , (hpr , hprec)) ∣₁) ∣₁) ∣₁) ∣₁
```

实用的读出接口从已知有序对 `pr u v` 出发，并预先假设两个端点都属于 `finiteStage n`。它只把截断呈现消去到命题 `before n u v`，因此没有规范呈现并不会造成损失。

```agda
relAt-rep : (n : ℕ) (u v : V ℓ)
          → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
          → ⟨ pr u v ∈ fst (relAt n) ⟩ → ⟨ before n u v ⟩
relAt-rep n u v hu hv h = PT.rec (snd (before n u v)) read (relAt-out n (pr u v) h)
  where
```

若读回的呈现使用分量 `p,q`，其有序对与 `pr u v` 相等便迫使 `p=u` 且 `q=v`。沿这两条等式搬运，就把所存比较转成目标比较。

```agda
  read : RelOf n (pr u v) → ⟨ before n u v ⟩
  read (p , (q , (p∈ , (q∈ , (qq , hbf))))) =
    subst2 (λ s t → ⟨ before n s t ⟩)
      (sym (pr-inj qq .fst)) (sym (pr-inj qq .snd)) hbf
```

反过来，`u,v` 的层隶属与 `before n u v` 的证明组成 `pr u v` 的显式 `RelOf` 见证。写入引理随后把该对记录进 `relAt n`，完成逐对表示的另一个方向。

```agda
relAt-fill : (n : ℕ) (u v : V ℓ)
           → ⟨ u ∈ finiteStage n ⟩ → ⟨ v ∈ finiteStage n ⟩
           → ⟨ before n u v ⟩ → ⟨ pr u v ∈ fst (relAt n) ⟩
relAt-fill n u v hu hv h = relAt-in n (pr u v)
  (stageEl n u hu , (stageEl n v hv , (hu , (hv , (refl , h)))))
```

## 那一步，对它所查阅的一切保持通用

递归描述必须把关系当作资料接收，而不能直接指称 `relAt`。`Held r a b` 给出所需解释：当且仅当 `r` 含有 `a,b` 的有序对时，`r` 才把 `a` 关联到 `b`。

```agda
Held : S → V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Held r a b = pr a b ∈ fst r
```

一次递归步骤先寻找当前索引的一个 `∈`-极大成员 `c`。当该索引是后继数码 `# (suc n)` 时，这个成员就是其前驱 `# n`；在零处则不存在这样的成员。因此，该步骤所定义的关系在零处没有成员，而无须另写基例公式。

```agda
opaque
 RelBodyAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
 RelBodyAt z b f =
   ∃̇ ( (var zero ∈̇ var (suc b))
     ∧̇ ( ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero))
```

找到 `c` 后，公式从逼近中读取在 `c` 处记录的关系。层级图识别出 `Lset (fst c)` 以及当前索引所确定的 `Lset` 层，两个候选端点都在后一层中取值。只有当当前索引被认同为数码时，这些层才是有穷层。

```agda
       ∧̇ ∃̇ ( appAt (sh2 f) (suc zero) zero
            ∧̇ ∃̇ ( LsetGraphAt zero (suc (suc zero))
                 ∧̇ ∃̇ ( LsetGraphAt zero (sh4 b)
                      ∧̇ ∃̇∈ (var zero)
                           ( ∃̇∈ (var (suc zero))
```

最内层子句要求候选条目是两个端点的有序对，并使用从逼近读出的关系，在前一层上以 `PrecedesAt` 比较它们。因此，该公式无需指称任何特定的 `relAt n`，便描述了递归的后继步骤。

```agda
                               ( prAtL (sh6 z) (suc zero) zero
                               ∧̇ PrecedesAt (suc (suc (suc (suc zero))))
                                             (suc (suc (suc zero)))
                                             (suc zero) zero ) ) ) ) ) ) )
```

`StepOf` 是该公式在元层面的含义。它选择四个模型元素：当前索引的候选极大成员 `c`、在那里记录的关系值 `r`，以及端点 `x,y`；候选条目 `zv` 已经是谓词的参数。只有在当前索引被认同为数码后，`c` 才会被认同为它的前驱数码。

```agda
StepOf : ∀ {n} → Fin n → Fin n → S ^ n → V ℓ → Type (ℓ-suc ℓ)
StepOf b f γ zv =
  Σ[ c ∈ S ] Σ[ r ∈ S ] Σ[ x ∈ S ] Σ[ y ∈ S ]
    ( ⟨ fst c ∈ fst (lookup b γ) ⟩
    × ( ((d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩ → Empty.⊥)
```

附带条件断言：`c` 属于当前索引并且在其中为 `∈`-极大元；逼近在 `c` 处记录 `r`；两个端点都属于当前取值所索引的层级阶段；`zv` 是它们的有序对；并且 `precedes (Held r)` 在 `Lset (fst c)` 上比较它们。这些正是一次递归步骤所需的数学数据；有穷性要到后面才由数码等式给出。

```agda
      × ( ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        × ( ⟨ fst x ∈ Lset (fst (lookup b γ)) ⟩
          × ( ⟨ fst y ∈ Lset (fst (lookup b γ)) ⟩
            × ( (zv ≡ pr (fst x) (fst y))
              × ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩ ) ) ) ) ) )
```

下面对任意变元 `z,b,f` 与任意环境证明语义对应。关于 `lookup b γ` 的底层集合为序数这一假设，用于把层级图描述的各阶段认同为相应的 `Lset` 值。

```agda
module _ {n : ℕ} (z b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  private
    Body : (c r A A' x y : S) → Type (ℓ-suc ℓ)
    Body c r A A' x y =
```

六个存在见证扩展环境后，最内层公式体保留两项决定性事实：`z` 所指的值是 `x,y` 的有序对，并且这两个端点相对于已恢复的层与关系满足 `PrecedesAt`。

```agda
        ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
      × ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
          ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                       (suc zero) zero ⟩
```

固定第一个端点 `x` 后，`AtY` 封装余下端点 `y`、它属于当前层的证明，以及最内层的两项事实。这个类型对应公式嵌套存在读法中的一层。

```agda
    AtY : (c r A A' x : S) → Type (ℓ-suc ℓ)
    AtY c r A A' x = Σ[ y ∈ S ] (⟨ fst y ∈ fst A' ⟩ × Body c r A A' x y)
```

`MaxOf c` 用隶属序表达极大性：若 `d` 也属于当前索引，则 `c ∈ d` 不可能成立。再结合 `c` 属于该索引，便知 `c` 是隶属序下的极大元。对后继数码而言，它就是前驱；在零处，`c` 的隶属前提本身已经没有见证。

```agda
    MaxOf : (c : S) → Type (ℓ-suc ℓ)
    MaxOf c = (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩ → ⟨ fst c ∈ fst d ⟩
            → Empty.⊥
```

为了把公式见证转成 `StepOf`，该转换假设 `c` 的隶属与极大性、逼近条目 `(c,r)`、认同前一层与当前层的等式，以及 `x` 属于当前层。最后一份 `AtY` 见证供应 `y` 与两项内层事实。

```agda
    atY : (c r A A' x : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → ⟨ fst x ∈ fst A' ⟩
        → AtY c r A A' x → StepOf b f γ (fst (lookup z γ))
```

层等式把公式中 `x,y` 的隶属转换成 `Lset (lookup b γ)` 中的隶属，正好符合 `StepOf` 的要求。配对等式与宿主层 `precedes` 比较随后由下面两项充分性论证给出。

```agda
    atY c r A A' x c∈ cmax hf qA qA' x∈ (y , (y∈ , (hpr , hprec))) =
      c , (r , (x , (y , (c∈ , (cmax , (hf
        , ( subst (λ t → ⟨ fst x ∈ t ⟩) qA' x∈
          , ( subst (λ t → ⟨ fst y ∈ t ⟩) qA' y∈
            , (qpair , hprec') ) ) ) ) ) ) ) )
```

这里直接把关系变元解释为 `Held r`，所以两条表示映射都是恒等映射。于是 `Precedes` 桥梁可以读出对象语言比较，而无需诉诸已经构造的 `relAt` 族。

```agda
      where
      module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                          (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                          (Held r) (λ _ _ p → p) (λ _ _ p → p)
```

读出 `PrecedesAt` 得到在公式所绑定层对象上的比较。该层的认同等式把载体搬运到 `Lset (fst c)`，从而得到 `StepOf` 所要求的比较。

```agda
      hprec' : ⟨ precedes (Held r) (Lset (fst c)) (fst x) (fst y) ⟩
      hprec' = subst (λ t → ⟨ precedes (Held r) t (fst x) (fst y) ⟩) qA
        (P.PrecedesAt-out hprec)
```

`prAtL` 的充分性把 `z` 所指的值认同为所恢复两端点的有序对。这便给出元层面步骤见证中的配对等式。

```agda
      qpair : fst (lookup z γ) ≡ pr (fst x) (fst y)
      qpair = subst ⟨_⟩
        (prAtL-adequate (sh6 z) (suc zero) zero
          (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)) hpr
```

第一个端点 `x` 已经显露后，余下端点仍只在命题意义下存在。`AtX` 正好记录这一中间状态：`x` 的层隶属，以及经过命题截断的 `AtY` 见证。

```agda
    AtX : (c r A A' : S) → Type (ℓ-suc ℓ)
    AtX c r A A' = Σ[ x ∈ S ] (⟨ fst x ∈ fst A' ⟩ × ∥ AtY c r A A' x ∥₁)
```

由于目标结论本身也经过命题截断，可以使用隐藏的 `y` 见证，而不把它作为选定资料带出命题。把逐点转换映射过该截断，恰好保留公式所供应的存在强度。

```agda
    atX : (c r A A' : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → fst A ≡ Lset (fst c) → fst A' ≡ Lset (fst (lookup b γ))
        → AtX c r A A' → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atX c r A A' c∈ cmax hf qA qA' (x , (x∈ , hy)) =
```

内层转换由恢复出的资料装配一份显式 `StepOf` 见证，`PT.map` 再把它放回命题截断之下。由此完成向外的语义读法，同时不产生规范的前驱或端点见证。

```agda
      PT.map (atY c r A A' x c∈ cmax hf qA qA' x∈) hy
```

找回 `c` 所索引的层之后，余下的内层量词要识别当前索引所索引的层。`AtA'` 打包一个可构造集合 `A'`、它在该处满足层图的证据，以及更内层见证 `x` 与 `y` 的命题截断存在。命题截断保留见证存在这一事实，却不选出一对规范见证。

```agda
    AtA' : (c r A : S) → Type (ℓ-suc ℓ)
    AtA' c r A = Σ[ A' ∈ S ]
      ( ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
      × ∥ AtX c r A A' ∥₁ )
```

要从 `A'` 继续，论证保留已经得到的关于 `c` 的信息、表中的条目 `(c,r)`，以及 `A` 与 `c` 所索引之层的同一视。在把 `AtX` 中隐藏的见证解释为语义步进之前，还须把 `A'` 识别为当前序数索引所索引的层。

```agda
    atA' : (c r A : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
         → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
         → fst A ≡ Lset (fst c)
         → AtA' c r A → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA' c r A c∈ cmax hf qA (A' , (hg , hx)) =
```

层图恰好给出这一同一视。把它的函数性定理 `Lset-only` 用于索引的序数性假设，便得到 `fst A' ≡ Lset (fst (lookup b γ))`；于是可以把命题截断的 `AtX` 消去到命题截断的步进结论中。

```agda
      PT.rec squash₁ (atX c r A A' c∈ cmax hf qA qA') hx
      where
      qA' : fst A' ≡ Lset (fst (lookup b γ))
      qA' = Lset-only zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) hg ob
```

再向外一层量词，`AtA` 对 `c` 所索引的层完成同样的工作。它由一个满足相应层图的可构造集合 `A`，以及 `AtA'` 后续数据的命题截断存在组成。

```agda
    AtA : (c r : S) → Type (ℓ-suc ℓ)
    AtA c r = Σ[ A ∈ S ]
      ( ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
      × ∥ AtA' c r A ∥₁ )
```

解释这一层时，首先需要一个等式来说明 `A` 究竟是哪一层。得到该等式后，便可像处理内层时一样，把命题截断的后续数据消去到命题截断的步进中。

```agda
    atA : (c r : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
        → AtA c r → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atA c r c∈ cmax hf (A , (hg , hA')) =
      PT.rec squash₁ (atA' c r A c∈ cmax hf qA) hA'
```

由于 `c` 属于 `b` 所指的序数，`mem-ord` 表明 `c` 本身也是序数。层图在这个序数处的函数性随即给出 `fst A ≡ Lset (fst c)`。这一识别不使用层的单调性。

```agda
      where
      qA : fst A ≡ Lset (fst c)
      qA = Lset-only zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) hg
        (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈)
```

再外一层的见证是逼近表在 `c` 处记录的关系。`AtR` 记录一个可构造集合 `r`、应用公式的满足证据，此公式表示表中含有条目 `(c,r)`，以及用于重建所需两层的后续数据之命题截断。

```agda
    AtR : (c : S) → Type (ℓ-suc ℓ)
    AtR c = Σ[ r ∈ S ]
      ( ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩ × ∥ AtA c r ∥₁ )
```

`appAt` 的充分性把它的满足判断转换成有序对 `(c,r)` 的周遭隶属陈述。有了这个表中条目，就可以把命题截断的 `AtA` 后续数据消去到命题截断的语义步进中。

```agda
    atR : (c : S) → ⟨ fst c ∈ fst (lookup b γ) ⟩ → MaxOf c
        → AtR c → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atR c c∈ cmax (r , (happ , hA)) = PT.rec squash₁ (atA c r c∈ cmax hf) hA
      where
      hf : ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩
```

具体而言，恢复出的事实是 `pr (fst c) (fst r) ∈ fst (lookup f γ)`。这正是 `StepOf` 所需的元层面形式：`f` 所指的逼近把关系 `r` 赋给索引 `c`。

```agda
      hf = subst ⟨_⟩ (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ)) happ
```

在最外层，`AtC` 选取序数索引的一个成员 `c`，并断言该索引中不存在满足 `c ∈ d` 的成员 `d`。因此 `c` 是该索引在隶属关系下的极大元。当后文把索引识别为一个非零冯·诺伊曼数码时，这个条件将识别出它的前驱；余下的命题截断分量则提供关系与层的数据。

```agda
    AtC : Type (ℓ-suc ℓ)
    AtC = Σ[ c ∈ S ]
      ( ⟨ fst c ∈ fst (lookup b γ) ⟩
      × ( ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
        × ∥ AtR c ∥₁ ) )
```

公式中的有界否定在提升后的宇宙中解释。把它降下便得到普通函数 `MaxOf c`：任何声称既属于该索引又满足 `c ∈ d` 的 `d` 都会导出矛盾。随后可经由前述各层消去命题截断的关系见证。

```agda
    atC : AtC → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
    atC (c , (c∈ , (hmax , hr))) = PT.rec squash₁ (atR c c∈ cmax) hr
      where
      cmax : MaxOf c
      cmax d hd hc = lower (hmax d hd hc)
```

这些逐层解释给出了步进主体的读出方向。为了建立反向结论，同一个主体公式在局部展开，使一个显式的 `StepOf` 见证能够重新填入其中的存在子句与有界子句。

```agda
  opaque
   unfolding RelBodyAt
```

从 `RelBodyAt` 的满足证据出发，最外层存在量词只给出 `c` 的命题截断存在。逐层读式在同一限制下恢复余下数据，最终得到 `∥ StepOf b f γ (fst (lookup z γ)) ∥₁`。它们证明某个步进存在，却不为嵌套量词选择规范见证。

```agda
   RelBody-out : ⟨ γ ⊨ RelBodyAt z b f ⟩
               → ∥ StepOf b f γ (fst (lookup z γ)) ∥₁
   RelBody-out = PT.rec squash₁ atC
```

反过来，一个显式的 `StepOf` 见证已经包含 `c`、关系 `r`、被比较的对象 `x,y`、它们的层隶属、有序对等式与前驱层比较。`RelBody-in` 重建两个中间层，并把这些数据逐一填入嵌套公式。公式的存在子句经过命题截断，因此结论断言公式得到满足，而不保留一组规范的内部见证。

```agda
   RelBody-in : StepOf b f γ (fst (lookup z γ)) → ⟨ γ ⊨ RelBodyAt z b f ⟩
   RelBody-in (c , (r , (x , (y , (c∈ , (cmax , (hf , (x∈ , (y∈
              , (qpair , hprec))))))))))
     = ∣ c , (c∈ , (hmax , ∣ r , (happ , ∣ A , (hgA , ∣ A' , (hgA'
       , ∣ x , (x∈ , ∣ y , (y∈ , (hpr , hprec')) ∣₁) ∣₁) ∣₁) ∣₁) ∣₁)) ∣₁
```

首先要重建的事实是 `c` 为序数。序数的每个成员仍是序数，因此，这由 `c ∈ fst (lookup b γ)` 以及该集合的序数性假设得出；它也正是构造由 `c` 索引的可构造层所需的条件。

```agda
     where
     oc : IsOrd (fst c)
     oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
```

利用这一序数性，`LsetS` 把 `Lset (fst c)` 打包为模型元素 `A`。最早分歧比较正是在这个由前驱索引的层上求值。

```agda
     A : S
     A = LsetS (fst c) oc
```

当前索引的序数性假设同样把 `Lset (fst (lookup b γ))` 打包为 `A'`。第二个层提供集合界，容纳有序对将要成为当前关系成员的两个对象。

```agda
     A' : S
     A' = LsetS (fst (lookup b γ)) ob
```

接下来须用对象语言中的有界全称否定表达语义上的极大性函数。对索引中的每个 `d`，任何 `c ∈ d` 的证明都会被 `cmax` 送到矛盾，再提升到公式满足关系所在的宇宙。

```agda
     hmax : ⟨ (c ∷ γ) ⊨ ∀̇∈ (var (suc b)) (¬̇ (var (suc zero) ∈̇ var zero)) ⟩
     hmax d hd hc = lift (cmax d hd hc)
```

`StepOf` 中的表条目采用周遭形式 `pr (fst c) (fst r) ∈ fst (lookup f γ)`。沿 `appAt` 充分性路径的逆向搬运，便把这个事实转换为应用原子的满足证据，也就是主体公式所需的形式。

```agda
     happ : ⟨ (r ∷ c ∷ γ) ⊨ appAt (sh2 f) (suc zero) zero ⟩
     happ = subst ⟨_⟩
       (sym (appAt-adequate (sh2 f) (suc zero) zero (r ∷ c ∷ γ))) hf
```

所选的 `A` 按定义就是 `c` 所索引的层。因此，层级的呈现定理由 `c` 的序数性与被表示取值的自反等式证明相应的层图子句。

```agda
     hgA : ⟨ (A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (suc (suc zero)) ⟩
     hgA = Lset-defines zero (suc (suc zero)) (A ∷ r ∷ c ∷ γ) oc refl
```

同一个呈现定理在当前索引处证明 `A'` 的图子句。这里所需的序数性就是既定假设 `ob`，故公式把 `A'` 精确识别为容纳 `x` 与 `y` 的那一层。

```agda
     hgA' : ⟨ (A' ∷ A ∷ r ∷ c ∷ γ) ⊨ LsetGraphAt zero (sh4 b) ⟩
     hgA' = Lset-defines zero (sh4 b) (A' ∷ A ∷ r ∷ c ∷ γ) ob refl
```

`StepOf` 中的等式把 `z` 所指的候选取值认同为 `x` 与 `y` 的 Kuratowski 对。沿 `prAtL` 充分性路径的逆向搬运，把这个等式转换为对象语言配对子句的满足证据。

```agda
     hpr : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ) ⊨ prAtL (sh6 z) (suc zero) zero ⟩
     hpr = subst ⟨_⟩
       (sym (prAtL-adequate (sh6 z) (suc zero) zero
         (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ))) qpair
```

最后还须翻译前驱层上的比较。这里的 `Precedes` 实例把基底关系解释为 `Held r`，也就是有序对属于 `r`。由于这一解释已经与对象语言应用公式所要求的隶属命题完全相同，两个表示映射都取恒等函数。

```agda
     module P = Precedes (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                         (suc zero) zero (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
                         (Held r) (λ _ _ p → p) (λ _ _ p → p)
```

固定这一解释后，`PrecedesAt-in` 把 `StepOf` 携带的语义最早分歧比较转换为 `PrecedesAt` 的满足证据。至此 `RelBodyAt` 的每个子句都已完成，从语义步进返回对象语言公式的桥梁也随之建立。

```agda
     hprec' : ⟨ (y ∷ x ∷ A' ∷ A ∷ r ∷ c ∷ γ)
              ⊨ PrecedesAt (suc (suc (suc (suc zero)))) (suc (suc (suc zero)))
                           (suc zero) zero ⟩
     hprec' = P.PrecedesAt-in hprec
```

上述主体只判定一个候选有序对。一个关系取值必须恰好收集所有这样的候选者，因此下一构造把这个单步条件外延地扩展到整个集合。

## 逼近与那个图

`RelStepAt v b f` 断言 `v` 所指集合的成员恰好是满足 `RelBodyAt` 的对象，其中候选者绑定为新引入的零号变元，索引 `b,f` 则在该绑定之下相应移位。因此它同时给出两个包含方向：候选关系的每个成员都实现一个语义步骤，而每个实现这种步骤的对象都属于该关系。

```agda
opaque
  RelStepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  RelStepAt v b f = extAt v (RelBodyAt zero (suc b) (suc f))
```

只要 `fst (lookup b γ)` 是序数，这一外延描述的读式就成立。主体公式需要该假设来识别步骤见证中出现的两个可构造层。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
         (ob : IsOrd (fst (lookup b γ))) where
  opaque
   unfolding RelStepAt
```

正向包含从 `v` 所指集合的一个成员 `w` 出发，在 `w` 处读出主体公式，并得到 `∥ StepOf b f γ (fst w) ∥₁`。结果经过命题截断，因为主体通过存在量词找出前驱、所记录的关系与被比较的分量。

```agda
   RelStep-out : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S)
               → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
   RelStep-out h w hw = RelBody-out zero (suc b) (suc f) (w ∷ γ) ob
     (extAt-out v (RelBodyAt zero (suc b) (suc f)) γ h w hw)
```

反向包含从 `w` 的一个显式语义步骤出发。`RelBody-in` 把它转换为主体的满足证据，外延描述的反向蕴涵随即推出 `w` 属于 `v` 所指的集合。

```agda
   RelStep-back : ⟨ γ ⊨ RelStepAt v b f ⟩ → (w : S) → StepOf b f γ (fst w)
                → ⟨ fst w ∈ fst (lookup v γ) ⟩
   RelStep-back h w s = extAt-in v (RelBodyAt zero (suc b) (suc f)) γ h w
     (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob s)
```

引入原理陈述了精确的逆命题。要证明 `RelStepAt`，只须对拟议关系的每个成员给出一个命题截断的步进，并对每个显式步进见证给出一个隶属证明。这两个函数正是外延性的两个包含方向。

```agda
   RelStep-in : ((w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩
                 → ∥ StepOf b f γ (fst w) ∥₁)
              → ((w : S) → StepOf b f γ (fst w)
                 → ⟨ fst w ∈ fst (lookup v γ) ⟩)
              → ⟨ γ ⊨ RelStepAt v b f ⟩
```

对第一个包含方向，每个命题截断的步进先经 `RelBody-in` 映射，再消去到作为命题的满足判断中。对第二个方向，`RelBody-out` 产生一个命题截断的步进；在应用给定的反向函数之前，它被消去到作为命题的隶属判断中。这里能够消去命题截断，仅仅因为两个目标都是命题。

```agda
   RelStep-in into back = extAt-in-both v (RelBodyAt zero (suc b) (suc f)) γ
     (λ w hw → PT.rec (snd ((w ∷ γ) ⊨ RelBodyAt zero (suc b) (suc f)))
       (RelBody-in zero (suc b) (suc f) (w ∷ γ) ob) (into w hw))
     (λ w h → PT.rec (snd (fst w ∈ fst (lookup v γ))) (back w)
       (RelBody-out zero (suc b) (suc f) (w ∷ γ) ob h))
```

这个外延步进现在实例化通用的递归形状构造。所得 `ApproxAt` 描述一张初始段表，其定义域与逐点步进子句符合 `RelStepAt`；`RelGraphAt` 则描述当前索引处由此前这种逼近支撑的一个取值。后文把该索引识别为数码时，这张表才成为有穷表。

```agda
module A = RecShape RelStepAt
open A using ( ApproxAt; ApproxAt-value; ApproxAt-step
             ; ApproxAt-in; GraphOf; PairOf )
     renaming ( GraphAt to RelGraphAt; Graph-in to RelGraph-in
              ; Graph-out to RelGraph-out; PairGraphAt to PairRelGraphAt
```

同一构造还为逼近图及其成对形式提供引入与消去原理。局部名称 `RelGraphAt` 与 `PairRelGraphAt` 表明，这套通用机制在此专用于递归定义的关系取值。

```agda
              ; PairGraph-in to PairRelGraph-in
              ; PairGraph-out to PairRelGraph-out )
```

到目前为止，这些公式只描述递归的形状，尚未识别其取值。下一步要证明，任何满足这一形状的表所记录的恰是先前构造的集合 `relAt m`；为此，证明把已记录取值的正确性与标准条目的存在性分开处理。

## 那一步，对着这场递归

`Values g k` 是正确性条件。对每个 `m < k`，若 `g` 含有把 `# m` 与任意模型元素 `w` 配成的条目，则 `w` 的底层集合等于 `relAt m` 的底层集合。这说明一个已记录索引处的集合值唯一，却不选择唯一的证明或见证包。

```agda
Values : S → ℕ → Type (ℓ-suc ℓ)
Values g k = (m : ℕ) → m < k → (w : S)
           → ⟨ pr (# m) (fst w) ∈ fst g ⟩ → fst w ≡ fst (relAt m)
```

`Entries g k` 是与之配合的完备性条件。它要求每个 `m < k` 的标准条目 `(# m, relAt m)` 都出现在 `g` 中。`Values` 与 `Entries` 合起来表明：表含有所有更小索引，并且每个索引处只记录预期的集合值。

```agda
Entries : S → ℕ → Type (ℓ-suc ℓ)
Entries g k = (m : ℕ) → m < k → ⟨ pr (# m) (fst (relAt m)) ∈ fst g ⟩
```

任何比较 `before k x y` 都迫使 `k` 为后继数。在零处该关系为空，因此比较会导出矛盾；在 `suc m` 处，前驱 `m` 与所需等式立即可得。这个小引理稍后把 `relAt k` 的成员转换回 `StepOf` 所需的前驱数据。

```agda
before-suc : (k : ℕ) (x y : V ℓ) → ⟨ before k x y ⟩ → Σ[ m ∈ ℕ ] (k ≡ suc m)
before-suc zero    x y h = Empty.rec* h
before-suc (suc m) x y h = m , refl
```

固定 `v` 所指的候选关系、`b` 所指的索引与 `f` 所指的表。等式 `qb` 把索引认同为数码 `# k`，而 `vals` 与 `ents` 断言该表在 `k` 以下正确且完备。在这些假设下，索引处的语义步骤可以与 `relAt k` 中的隶属精确比较。

```agda
module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k)
         (vals : Values (lookup f γ) k) (ents : Entries (lookup f γ) k) where
  private
    ob : IsOrd (fst (lookup b γ))
```

数码 `# k` 是序数。沿 `qb : fst (lookup b γ) ≡ # k` 的反向搬运这一事实，便证明 `fst (lookup b γ)` 为序数，从而可以使用先前关于步骤主体的读式与填入引理。

```agda
    ob = subst IsOrd (sym qb) (numeral-ord k)
```

考虑候选取值 `x` 的一个显式 `StepOf` 见证。其中的极大元 `c` 属于该索引，`qb` 把这一点转化为 `fst c ∈ # k`。数码隶属的消去在命题截断下恢复一个自然数 `m < k` 与等式 `fst c ≡ # m`；这里可以消去命题截断，因为目标隶属 `x ∈ relAt k` 是命题。

```agda
    into : (x : V ℓ) → StepOf b f γ x → ⟨ x ∈ fst (relAt k) ⟩
    into x (c , (r , (xx , (yy , (c∈ , (cmax , (hf , (xx∈ , (yy∈
           , (qx , hprec)))))))))) =
      PT.rec (snd (x ∈ fst (relAt k))) atC
        (∈#-elim k (fst c) (subst (λ t → ⟨ fst c ∈ t ⟩) qb c∈))
```

对这样一个 `m`，可用 `relAt k` 的引入引理证明所需隶属。相应的 `RelOf k x` 见证沿用分量 `xx` 与 `yy`，并需要它们属于 `finiteStage k`、`x` 与其有序对的等式，以及比较 `before k xx yy`。余下工作因而是证明极大元 `c` 确实对应 `k` 的直接前驱，并据此翻译表中记录的比较。

```agda
      where
      atC : Σ[ m ∈ ℕ ] ((m < k) × (fst c ≡ # m)) → ⟨ x ∈ fst (relAt k) ⟩
      atC (m , (hm , qc)) = relAt-in k x
        (xx , (yy , (xxk , (yyk , (qx , below)))))
        where
```

由于 `c` 由 `# m` 编码，而它又是 `# k` 的成员中的极大元，应有 `k = suc m`。三歧性比较 `suc m` 与 `k`：相等情形给出所需等式，两个严格不等情形则分别与已有的 `m`、`k` 关系或极大性矛盾。

```agda
        ksuc : k ≡ suc m
        ksuc = decide (suc m ≟ k)
          where
          decide : NatOrder.Trichotomy (suc m) k → k ≡ suc m
          decide (NatOrder.lt hlt) = Empty.rec
```

若 `suc m < k`，则数码 `#(suc m)` 本身属于 `# k`。又因 `c = # m`，还有 `c ∈ #(suc m)`。这两个隶属事实在索引中给出了一个严格位于 `c` 之上的成员，与极大性子句矛盾。

```agda
            (cmax (numS (suc m))
              (subst (λ t → ⟨ fst (numS (suc m)) ∈ t ⟩) (sym qb)
                (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst (suc m)))
                  (#mono (suc m) k hlt)))
              (subst (λ t → ⟨ fst c ∈ t ⟩) (sym (numS-fst (suc m)))
```

反之，若 `k < suc m`，去掉后继便得到 `k ≤ m`，这与已知的 `m < k` 不相容。因此只余相等情形；把三歧性给出的等式反向，即得下文所需方向的 `k ≡ suc m`。

```agda
                (subst (λ t → ⟨ t ∈ # (suc m) ⟩) (sym qc)
                  (#mono m (suc m) NatOrder.≤-refl))))
          decide (NatOrder.eq e) = sym e
          decide (NatOrder.gt hgt) = Empty.rec (<-asym hm (pred-≤-pred hgt))
```

步进见证已经给出 `xx` 属于 `Lset (fst (lookup b γ))`。沿 `qb` 搬运，把这个集合识别为 `Lset (# k)`，也就是 `finiteStage k`，从而得到 `RelOf k x` 所需的第一个层隶属分量。

```agda
        xxk : ⟨ fst xx ∈ finiteStage k ⟩
        xxk = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) qb xx∈
```

有序对的两个端点都必须属于由 `k` 索引的层。对于第二个端点，界等于 `# k` 的等式把 `Lset (fst (lookup b γ))` 中的隶属关系化为 `finiteStage k` 中的隶属关系。

```agda
        yyk : ⟨ fst yy ∈ finiteStage k ⟩
        yyk = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) qb yy∈
```

以前驱数码为索引的表项记录了关系 `r`。把第一分量从 `fst c` 化为 `# m` 后，正确性假设 `vals` 便把 `r` 的底层集合认同为 `relAt m`。

```agda
        rval : fst r ≡ fst (relAt m)
        rval = vals m hm r
          (subst (λ t → ⟨ pr t (fst r) ∈ fst (lookup f γ) ⟩) qc hf)
```

步进见证起初在 `Lset (fst c)` 上用 `r` 所持的关系比较两个端点。等式 `fst c ≡ # m` 与 `fst r ≡ fst (relAt m)` 把它改写为 `precedes (Rel m) (finiteStage m)`。

```agda
        atM : ⟨ precedes (Rel m) (finiteStage m) (fst xx) (fst yy) ⟩
        atM = subst (λ t → ⟨ precedes (λ s u → pr s u ∈ t) (finiteStage m)
                              (fst xx) (fst yy) ⟩) rval
          (subst (λ t → ⟨ precedes (Held r) (Lset t) (fst xx) (fst yy) ⟩) qc
            hprec)
```

为了得到递归比较，`precedes-map` 把基底关系 `Rel m` 换成 `before m`。由于基底关系出现在一致性条件的前件中，它所需的假设方向相反，即从 `before m` 走向 `relAt m` 中的隶属。因此先得到 `before (suc m)`，再由等式 `k ≡ suc m` 得到 `before k`。

```agda
        below : ⟨ before k (fst xx) (fst yy) ⟩
        below = subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) (sym ksuc)
          (precedes-map (Rel m) (before m) (finiteStage m) (fst xx) (fst yy)
            (λ w t hw ht hbf → relAt-fill m w t hw ht hbf) atM)
```

在反方向上，要把由 `RelOf k` 描述的成员化为语义步进见证。两个端点已经给出；余下的任务是恢复前驱索引及其关系表项，并证明此前驱是界中的极大成员。

```agda
    from : (x : V ℓ) → RelOf k x → StepOf b f γ x
    from x (xx , (yy , (xx∈ , (yy∈ , (qx , hbf))))) =
      numS m , (relAt m , (xx , (yy , (c∈ , (cmax , (hf , (xxb , (yyb
        , (qx , hprec)))))))))
      where
```

当 `k` 为零时，`before k` 不可能有证明。因此，引理 `before-suc` 从现有比较中取出自然数 `m`，使该比较发生在后继层。

```agda
      m : ℕ
      m = before-suc k (fst xx) (fst yy) hbf .fst
```

同一次后继分析还给出等式 `k ≡ suc m`。该等式把第 `k` 层的比较与以第 `m` 层数据为基底的递归步联系起来。

```agda
      qk : k ≡ suc m
      qk = before-suc k (fst xx) (fst yy) hbf .snd
```

由于 `k` 等于 `suc m`，前驱满足 `m < k`。这个界使证明能够在索引 `m` 处同时使用逼近表的正确性与完备性假设。

```agda
      hm : m < k
      hm = subst (λ j → m < j) (sym qk) NatOrder.≤-refl
```

表示前驱的数码必须属于 `b` 中保存的界。不等式 `m < k` 给出 `# m ∈ # k`；关于 `numS m` 与界的等式再把这项隶属关系化为所需形式。

```agda
      c∈ : ⟨ fst (numS m) ∈ fst (lookup b γ) ⟩
      c∈ = subst (λ t → ⟨ fst (numS m) ∈ t ⟩) (sym qb)
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst m)) (#mono m k hm))
```

还需证明 `# m` 是 `# k` 的成员中的极大者。给定 `d ∈ # k` 与 `# m ∈ d`，数码消去只在命题截断中把 `d` 表成某个满足 `j < k` 的 `# j`；这两项隶属将同时迫使 `m < j` 与 `j ≤ m`。

```agda
      cmax : (d : S) → ⟨ fst d ∈ fst (lookup b γ) ⟩
           → ⟨ fst (numS m) ∈ fst d ⟩ → Empty.⊥
      cmax d hd hc = PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst d) (subst (λ t → ⟨ fst d ∈ t ⟩) qb hd))
        where
```

在 `d ≡ # j` 的分支中，`d` 属于 `# k = # (suc m)` 给出 `j ≤ m`。另一方面，`# m` 属于 `d` 给出严格不等式 `m < j`，自然数序的非对称性遂排除该分支。

```agda
        step : Σ[ j ∈ ℕ ] ((j < k) × (fst d ≡ # j)) → Empty.⊥
        step (j , (hj , qd)) = <-asym mj (pred-≤-pred (subst (λ i → j < i) qk hj))
          where
          mj : m < j
          mj = #∈#-elim m j
```

`m < j` 的推导使用冯·诺伊曼数码的隶属关系与严格序之间的准确对应。关于 `numS m` 的等式和 `d ≡ # j` 先把假设的隶属改写为 `# m ∈ # j`，随后即可解码数码隶属。

```agda
            (subst (λ t → ⟨ t ∈ # j ⟩) (numS-fst m)
              (subst (λ t → ⟨ fst (numS m) ∈ t ⟩) qd hc))
```

由于 `m < k`，完备性 `ents` 给出标准表项 `(# m , relAt m)`。把 `# m` 改写为 `numS m` 的底层集合，便得到语义步进见证所需的表项。

```agda
      hf : ⟨ pr (fst (numS m)) (fst (relAt m)) ∈ fst (lookup f γ) ⟩
      hf = subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst (lookup f γ) ⟩)
        (sym (numS-fst m)) (ents m hm)
```

`RelOf k` 记录把第一个端点置于 `finiteStage k`，也就是 `Lset (# k)`。用界等式改写 `# k` 后，该端点便属于 `Lset (fst (lookup b γ))`，正好满足 `StepOf` 的要求。

```agda
      xxb : ⟨ fst xx ∈ Lset (fst (lookup b γ)) ⟩
      xxb = subst (λ t → ⟨ fst xx ∈ Lset t ⟩) (sym qb) xx∈
```

同样的运输把第二个端点置于由界确定的层中。这两个端点条件保证重建出的步仍是有界关系，而不是任意集合上的比较。

```agda
      yyb : ⟨ fst yy ∈ Lset (fst (lookup b γ)) ⟩
      yyb = subst (λ t → ⟨ fst yy ∈ Lset t ⟩) (sym qb) yy∈
```

`RelOf k` 中保存的比较先沿 `k ≡ suc m` 改写，从而显出递归子句 `precedes (before m) (finiteStage m)`。为了得到语义步进，还须把其基底关系从 `before m` 换成 `relAt m` 中的隶属。

```agda
      hprec : ⟨ precedes (Held (relAt m)) (Lset (fst (numS m)))
                 (fst xx) (fst yy) ⟩
      hprec = subst (λ t → ⟨ precedes (Held (relAt m)) (Lset t)
                              (fst xx) (fst yy) ⟩) (sym (numS-fst m))
        (precedes-map (before m) (Rel m) (finiteStage m) (fst xx) (fst yy)
```

这里，`precedes-map` 使用方向从 `relAt m` 中的隶属回到 `before m` 的 `relAt-rep`；一致性前件中的反变性于是给出以 `Rel m` 为基底的比较。最后，数码等式把该层改写为 `Lset (fst (numS m))`，从而得到 `StepOf` 的最后一个字段。

```agda
          (λ w t hw ht hR → relAt-rep m w t hw ht hR)
          (subst (λ j → ⟨ before j (fst xx) (fst yy) ⟩) qk hbf))
```

引理 `step-rel` 证明：在索引 `k` 处满足步进公式的任意集合都等于 `relAt k`。外延性把这个集合等式化为两个隶属蕴涵。在正向蕴涵中，`RelStep-out` 给出命题截断的步进见证，而 `into` 把其中任意见证送到 `relAt k` 的隶属关系。

```agda
  step-rel : ⟨ γ ⊨ RelStepAt v b f ⟩ → fst (lookup v γ) ≡ fst (relAt k)
  step-rel h = cong fst (extensionalL {a = lookup v γ} {b = relAt k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup v γ) ⟩ → ⟨ fst x ∈ fst (relAt k) ⟩
    fwd x hx = PT.rec (snd (fst x ∈ fst (relAt k))) (into (fst x))
```

这里可以消去命题截断，因为属于 `relAt k` 是一个命题。证明并不选择特定的前驱或有序对见证，只保留原成员属于已实现关系这一事实。

```agda
      (RelStep-out v b f γ ob h x hx)
```

对于反向的隶属蕴涵，`relAt-out` 给出该成员的命题截断的 `RelOf k` 描述。映射 `from` 据此重建 `StepOf` 见证，随后 `RelStep-back` 把该成员放入满足步进公式的集合。

```agda
    bwd : (x : S) → ⟨ fst x ∈ fst (relAt k) ⟩ → ⟨ fst x ∈ fst (lookup v γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup v γ)))
      (λ ro → RelStep-back v b f γ ob h x (from (fst x) ro))
      (relAt-out k (fst x) hx)
```

对于每个可构造元素，两个蕴涵给出两项隶属命题之间的等价。命题外延性把该等价化为路径，集合外延性再把这些逐点路径装配成所需的底层集合等式。

```agda
    pt : (x : S) → (fst x ∈ fst (lookup v γ)) ≡ (fst x ∈ fst (relAt k))
    pt x = ⇔toPath (fwd x) (bwd x)
```

反向引理 `rel-step` 从候选取值与 `relAt k` 的等式出发，证明步进公式。引入规则要求给出两个隶属方向；在第一个方向中，`toStep` 要为候选取值的每个成员配上一个命题截断的语义步进。

```agda
  rel-step : fst (lookup v γ) ≡ fst (relAt k) → ⟨ γ ⊨ RelStepAt v b f ⟩
  rel-step q = RelStep-in v b f γ ob toStep backStep
    where
    toStep : (w : S) → ⟨ fst w ∈ fst (lookup v γ) ⟩ → ∥ StepOf b f γ (fst w) ∥₁
    toStep w hw = PT.map (from (fst w))
```

该等式先把候选成员运入 `relAt k`。`relAt k` 的向外表示只给出命题截断的 `RelOf k` 记录，而 `PT.map from` 在把其中可能的元素化为步进见证时保留这层命题截断。

```agda
      (relAt-out k (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) q hw))
```

第二个隶属方向从显式的 `StepOf` 见证开始。映射 `into` 证明其属于 `relAt k`，再沿所设等式的反方向把这项隶属运回候选取值。

```agda
    backStep : (w : S) → StepOf b f γ (fst w) → ⟨ fst w ∈ fst (lookup v γ) ⟩
    backStep w st = subst (λ t → ⟨ fst w ∈ t ⟩) (sym q) (into (fst w) st)
```

## 逼近所记录的每个取值

引理 `entryOf` 把取值正确性化为表项完备性。若 `j < k`，逼近就在 `# j` 处有某个取值；若那里记录的每个取值都等于 `relAt j`，则标准对 `(# j , relAt j)` 本身属于该逼近。

```agda
entryOf : ∀ {n} (f a : Fin n) (γ : S ^ n) (k : ℕ)
        → fst (lookup a γ) ≡ # k → ⟨ γ ⊨ ApproxAt f a ⟩
        → (j : ℕ) → j < k
        → ((u : S) → ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩
           → fst u ≡ fst (relAt j))
```

`ApproxAt` 中的定义域完备性在命题截断下给出数码 `# j` 处某个取值 `u` 的存在性。由于目标是标准对属于逼近这一命题，证明可以消去该命题截断，并使用所设的 `u` 的正确性。

```agda
        → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩
entryOf f a γ k qa h j hj vs =
  PT.rec (snd (pr (# j) (fst (relAt j)) ∈ fst (lookup f γ))) named
    (ApproxAt-value f a γ h (numS j)
      (subst (λ t → ⟨ fst (numS j) ∈ t ⟩) (sym qa)
```

定义域论证来自 `j < k`：数码的单调性给出 `# j ∈ # k`，关于 `numS j` 与界的等式再把这项隶属化为 `ApproxAt-value` 所需的形式。所得结论只在命题截断下断言某个记录取值存在，并不选定一个具体取值。

```agda
        (subst (λ t → ⟨ t ∈ # k ⟩) (sym (numS-fst j)) (#mono j k hj))))
  where
  named : Σ[ u ∈ S ] ⟨ pr (fst (numS j)) (fst u) ∈ fst (lookup f γ) ⟩
        → ⟨ pr (# j) (fst (relAt j)) ∈ fst (lookup f γ) ⟩
  named (u , p) =
```

在这样的取值分支中，数码等式先把记录的对规范为 `(# j , u)`。正确性假设给出 `fst u ≡ fst (relAt j)`，再在第二分量中作替换，就把原表项的隶属化为标准对的隶属。

```agda
    subst (λ t → ⟨ pr (# j) t ∈ fst (lookup f γ) ⟩) (vs u p') p'
    where
    p' : ⟨ pr (# j) (fst u) ∈ fst (lookup f γ) ⟩
    p' = subst (λ t → ⟨ pr t (fst u) ∈ fst (lookup f γ) ⟩) (numS-fst j) p
```

固定一个界为 `# k` 的逼近。归纳动机 `Val m` 断言：只要 `m < k`，在键 `# m` 处记录的每个可构造取值 `w`，其底层集合都与 `relAt m` 相等。

```agda
module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) (h : ⟨ γ ⊨ ApproxAt f a ⟩) where
  private
    Val : ℕ → Type (ℓ-suc ℓ)
    Val m = (m < k) → (w : S) → ⟨ pr (# m) (fst w) ∈ fst (lookup f γ) ⟩
```

这个动机量化所有可能的记录取值，而不选择其中一个。其结论是两个底层集合相等；这种形式既能用来改写表项，也能推出逼近的取值唯一性。

```agda
          → fst w ≡ fst (relAt m)
```

正确性通过自然数严格序上的良基归纳来证明。为了识别 `m` 处的取值，归纳假设先给出每个 `j < m` 处的正确性；随后，证明在加入 `w` 与表示 `m` 的数码所得的环境中，对候选取值 `w` 应用 `step-rel`。这里使用的是自然数 `<` 的良基性，而不是 `before` 的良基性。

```agda
  approx-val : (m : ℕ) → Val m
  approx-val = WFI.induction <-wellfounded go
    where
    go : (m : ℕ) → ((j : ℕ) → j < m → Val j) → Val m
    go m IH hm w hw = step-rel zero (suc zero) (sh2 f) (w ∷ numS m ∷ γ) m
```

`(# m , w)` 已被记录这一假设使 `ApproxAt-step` 给出 `w` 所满足的步进公式。为了用 `step-rel` 把这一步认同为 `relAt m`，还需提供关于所有更小索引的两项事实：记录的取值是正确的，并且每个标准表项都存在。

```agda
      (numS-fst m) vals ents
      (ApproxAt-step f a γ h (numS m) w
        (subst (λ t → ⟨ pr t (fst w) ∈ fst (lookup f γ) ⟩)
          (sym (numS-fst m)) hw))
      where
```

对于 `j < m`，正确性正是索引 `j` 处的归纳假设。该假设自身所需的界 `j < k`，由 `j < m` 与当前的 `m < k` 传递得到。

```agda
      vals : Values (lookup (sh2 f) (w ∷ numS m ∷ γ)) m
      vals j hj u hu = IH j hj (<-trans hj hm) u hu
```

`m` 以下的完备性由 `entryOf` 得到。对于每个 `j < m`，传递性再次给出 `j < k`，归纳假设则提供「在 `j` 处记录的每个取值都等于 `relAt j`」这一前提；因此索引 `j` 处的标准表项确实存在。

```agda
      ents : Entries (lookup (sh2 f) (w ∷ numS m ∷ γ)) m
      ents j hj = entryOf f a γ k qa h j (<-trans hj hm)
        (λ u p → IH j hj (<-trans hj hm) u p)
```

一旦证明了每个有界索引处的正确性，`entryOf` 就立即给出逼近的完备性。因此，`approx-ent` 断言每个 `m < k` 都使标准对 `(# m , relAt m)` 出现在记录表中。

```agda
  approx-ent : (m : ℕ) → m < k
             → ⟨ pr (# m) (fst (relAt m)) ∈ fst (lookup f γ) ⟩
  approx-ent m hm = entryOf f a γ k qa h m hm (approx-val m hm)
```

图公式在命题截断下隐藏了一个截至 `k` 的逼近及其最后一步。引理 `rel-only` 把该命题截断消去到集合等式这一命题中，并断言 `v` 中保存的取值必为 `relAt k`。

```agda
module _ {n : ℕ} (v b : Fin n) (γ : S ^ n) (k : ℕ)
         (qb : fst (lookup b γ) ≡ # k) where
  rel-only : ⟨ γ ⊨ RelGraphAt v b ⟩ → fst (lookup v γ) ≡ fst (relAt k)
  rel-only h = PT.rec (setIsSet (fst (lookup v γ)) (fst (relAt k))) read
    (RelGraph-out v b γ h)
```

在任一被表示的分支中，图给出逼近 `g`、`g` 满足 `ApproxAt` 的证明，以及索引 `k` 处步进成立的证明。前述良基归纳识别 `g` 在 `k` 以下记录的每个取值；`step-rel` 随即把最后的取值认同为 `relAt k`。

```agda
    where
    read : GraphOf v b γ → fst (lookup v γ) ≡ fst (relAt k)
    read (g , (ha , hs)) =
      step-rel (suc v) (suc b) zero (g ∷ γ) k qb
        (λ m hm w hw → approx-val zero (suc b) (g ∷ γ) k qb ha m hm w hw)
```

`step-rel` 的另一个输入是同一个逼近在 `k` 以下的完备性。该输入由 `approx-ent` 提供；后者使用取值定理，把每个仅知存在的表项替换为相应的标准表项。

```agda
        (λ m hm → approx-ent zero (suc b) (g ∷ γ) k qb ha m hm)
        hs
```

## 那个逼近的显式构造

为了用 `finSet` 收集下文的有限族，先要把它的所有成员放入同一个可构造层。更一般地，`smallStage` 对任意小族 `g : X → S` 的各个所在层作序数界定，得到序数 `σ`，使每个 `fst (g x)` 都属于 `Lset σ`。

```agda
smallStage : (X : Type ℓ) (g : X → S)
           → Σ[ σ ∈ V ℓ ] (IsOrd σ × ((x : X) → ⟨ fst (g x) ∈ Lset σ ⟩))
smallStage X g = bd .fst , (bd .snd .fst , mem)
  where
  bd = boundingOrd X (λ x → stage (fst (g x)) (g x .snd))
```

每个 `g x` 已经属于其诞生层。所取的界序数位于每个诞生层之上，因此 `Lset` 的单调性把每项隶属关系运入公共层 `Lset σ`。

```agda
         (λ x → stage-ord (fst (g x)) (g x .snd))
  mem : (x : X) → ⟨ fst (g x) ∈ Lset (bd .fst) ⟩
  mem x = Lset-mono {α = bd .fst} {β = stage (fst (g x)) (g x .snd)}
    (bd .snd .snd x) (stage-mem (fst (g x)) (g x .snd))
```

固定界 `k` 后，有限索引类型 `Fin k` 恰好枚举比 `k` 小的自然数。族 `famOf k` 把索引 `i` 映到一个可构造有序对，其两分量分别是数码 `# (toℕ i)` 与已实现关系 `relAt (toℕ i)`。

```agda
private
  famOf : (k : ℕ) → Fin k → S
  famOf k i = prS (numS (toℕ i)) (relAt (toℕ i))
```

提升后的 `Fin k` 把这个有限索引类型置于 `smallStage` 所需的宇宙中。对 `famOf k` 应用公共层引理，得到包含所有有序对的单个序数层；这正提供了稍后 `finSetL` 所需的可构造性前提。

```agda
  famBnd : (k : ℕ) → Σ[ σ ∈ V ℓ ] (IsOrd σ
         × ((i : Lift {ℓ-zero} {ℓ} (Fin k)) → ⟨ fst (famOf k (lower i)) ∈ Lset σ ⟩))
  famBnd k = smallStage (Lift {ℓ-zero} {ℓ} (Fin k)) (λ i → famOf k (lower i))
```

`famOf k i` 的底层集合是整个有序对，而不只是它的第一分量。等式 `famEq` 展开可构造配对与数码表示，把它认同为 `pr (# (toℕ i)) (fst (relAt (toℕ i)))`。

```agda
  famEq : (k : ℕ) (i : Fin k)
        → fst (famOf k i) ≡ pr (# (toℕ i)) (fst (relAt (toℕ i)))
  famEq k i = prS-fst (numS (toℕ i)) (relAt (toℕ i))
            ∙ cong (λ t → pr t (fst (relAt (toℕ i)))) (numS-fst (toℕ i))
```

逼近 `approxSet k` 由 `finSet` 构造，它把以 `Fin k` 为索引的底层有序对族收成一个有限集。证明 `finSetL` 利用这些有序对所在的公共层，说明该有限集是 `L` 的元素。这个构造不使用替换公理。

```agda
opaque
  approxSet : ℕ → S
  approxSet k = finSet k (λ i → fst (famOf k i))
    , FinOf.finSetL (famBnd k .fst) (famBnd k .snd .fst) k
        (λ i → fst (famOf k i)) (λ i → famBnd k .snd .snd (lift i))
```

投影等式表明，`approxSet k` 的底层集合恰好就是这个 `finSet`。因此，后续成员引理可以使用有限集的引入与消去规则，证明其表项恰为满足 `j < k` 的各对 `(# j , relAt j)`。

```agda
  approxSet-fst : (k : ℕ) → fst (approxSet k) ≡ finSet k (λ i → fst (famOf k i))
  approxSet-fst k = refl
```

有限逼近包含每个预期条目：若 `j < k`，则 `# j` 与 `relAt j` 的有序对属于 `approxSet k`。这是 `approxSet` 的有限集构造所具有的性质，并未使用替换。

```agda
approx-mem-in : (k j : ℕ) → j < k
              → ⟨ pr (# j) (fst (relAt j)) ∈ fst (approxSet k) ⟩
approx-mem-in k j hj =
  subst (λ t → ⟨ t ∈ fst (approxSet k) ⟩)
    (cong (λ i → pr (# i) (fst (relAt i))) (toℕ∘enum j hj))
```

不等式给出 `enum j hj : Fin k`。等式 `famEq` 把有限族中相应的成员认同为所需的有序对，`finSet-in` 再把它写入由 `finSet` 构造并由 `finSetL` 证明属于 `L` 的集合。

```agda
    (subst (λ t → ⟨ pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))) ∈ t ⟩)
      (sym (approxSet-fst k))
      (finSet-in k (λ i → fst (famOf k i))
        (pr (# (toℕ (enum j hj))) (fst (relAt (toℕ (enum j hj)))))
        ∣ enum j hj , famEq k (enum j hj) ∣₁))
```

反过来，属于 `approxSet k` 只给出一个经过命题截断的断言：该成员是由某个 `j < k` 索引的预期条目。因此，这条引理精确刻画了其中出现的有序对，却不选择规范的索引见证。

```agda
approx-mem-out : (k : ℕ) (y : V ℓ) → ⟨ y ∈ fst (approxSet k) ⟩
               → ∥ Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j)))) ∥₁
approx-mem-out k y h = PT.map named
  (finSet-out k (λ i → fst (famOf k i)) y
    (subst (λ t → ⟨ y ∈ t ⟩) (approxSet-fst k) h))
```

枚举索引 `i : Fin k` 被送到自然数 `toℕ i`，并同时带有 `toℕ<n i`。把成员等式反向后与 `famEq` 复合，便得到从原成员到标准有序对的所需等式。

```agda
  where
  named : Σ[ i ∈ Fin k ] (fst (famOf k i) ≡ y)
        → Σ[ j ∈ ℕ ] ((j < k) × (y ≡ pr (# j) (fst (relAt j))))
  named (i , q) = toℕ i , (toℕ<n i , (sym q ∙ famEq k i))
approxVals : (k : ℕ) → Values (approxSet k) k
```

上述成员刻画给出取值正确性。若首分量为 `# m` 的条目出现在 `k` 以下，则其第二分量就是 `relAt m` 的底层集合；由于 `V` 中集合之间的相等本身是命题，可以消去索引外层的命题截断。

```agda
approxVals k m hm u hu = PT.rec (setIsSet (fst u) (fst (relAt m))) named
  (approx-mem-out k (pr (# m) (fst u)) hu)
  where
  named : Σ[ j ∈ ℕ ] ((j < k) × (pr (# m) (fst u) ≡ pr (# j) (fst (relAt j))))
        → fst u ≡ fst (relAt m)
```

有序对的单射性把等式分成两个分量。数码的单射性继而把恢复出的索引认同为 `m`，于是第二分量的等式可从 `relAt j` 搬运到 `relAt m`。

```agda
  named (j , (hj , q)) = pr-inj q .snd
    ∙ cong (λ i → fst (relAt i)) (sym (#-inj′ (pr-inj q .fst)))
```

与取值正确性相配的是条目完备性：对每个 `m < k`，标准有序对 `(# m, relAt m)` 都在表中。这直接来自上面的有限集成员引理。

```agda
approxEnts : (k : ℕ) → Entries (approxSet k) k
approxEnts k m hm = approx-mem-in k m hm
```

固定一个环境，其中 `f` 表示 `approxSet k`，`a` 表示数码 `# k`。余下的任务是验证这张具体的有限表满足抽象的逼近公式。

```agda
module _ (k : ℕ) {n : ℕ} (f a : Fin n) (γ : S ^ n)
         (qf : fst (lookup f γ) ≡ fst (approxSet k))
         (qa : fst (lookup a γ) ≡ # k) where
  private
    onDom : (x : S)
```

定义域条件包含两个方向。表中出现的首分量必须属于 `# k`，而 `# k` 的每个成员都必须作为某个表条目的首分量出现。关于第二分量的存在断言按命题截断解释。

```agda
          → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
             → ⟨ fst x ∈ fst (lookup a γ) ⟩)
          × (⟨ fst x ∈ fst (lookup a γ) ⟩
             → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩)
    onDom x = fwd , bwd
```

先看第一个方向，只假设某个第二分量与 `x` 组成了表中条目。目标 `x ∈ # k` 是命题，因此可以先消去存在见证的命题截断，再用 `approx-mem-out` 分析该有序对。

```agda
      where
      fwd : ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
          → ⟨ fst x ∈ fst (lookup a γ) ⟩
      fwd = PT.rec (snd (fst x ∈ fst (lookup a γ))) atY
        where
```

把该条目搬运到 `approxSet k` 后，`approx-mem-out` 给出经过命题截断的 `j < k`，以及该条目与第 `j` 个标准有序对的等式。所求的索引成员关系是命题，故这里同样可以消去命题截断。

```agda
        atY : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
            → ⟨ fst x ∈ fst (lookup a γ) ⟩
        atY (y , p) = PT.rec (snd (fst x ∈ fst (lookup a γ))) named
          (approx-mem-out k (pr (fst x) (fst y))
            (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p))
```

首分量等式表明 `x` 的底层集合是 `# j`。再用把 `a` 解释为 `# k` 的等式，目标便化为证明这个集合属于 `# k`。

```agda
          where
          named : Σ[ j ∈ ℕ ]
                    ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j))))
                → ⟨ fst x ∈ fst (lookup a γ) ⟩
          named (j , (hj , q)) = subst (λ t → ⟨ fst x ∈ t ⟩) (sym qa)
```

数码单调性把 `j < k` 化为 `# j ∈ # k`。随后沿首分量等式搬运，即可证明原来的 `x` 属于所需定义域。

```agda
            (subst (λ t → ⟨ t ∈ # k ⟩) (sym (pr-inj q .fst)) (#mono j k hj))
```

反向证明把 `# k` 中的成员关系解码为经过命题截断的自然数 `j < k`，其数码就是给定元素。对这份截断数据作映射，便会得到所需的截断表条目。

```agda
      bwd : ⟨ fst x ∈ fst (lookup a γ) ⟩
          → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
      bwd hx = PT.map named
        (∈#-elim k (fst x) (subst (λ t → ⟨ fst x ∈ t ⟩) qa hx))
        where
```

对一个显式解码出的 `j`，取 `relAt j` 为第二分量。条目完备性把 `(# j, relAt j)` 放入 `approxSet k`，再沿有限表的解释等式和给定首分量的等式搬运，即得到原环境中的成员关系。

```agda
        named : Σ[ j ∈ ℕ ] ((j < k) × (fst x ≡ # j))
              → Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
        named (j , (hj , q)) = relAt j
          , subst (λ t → ⟨ pr (fst x) (fst (relAt j)) ∈ t ⟩) (sym qf)
              (subst (λ t → ⟨ pr t (fst (relAt j)) ∈ fst (approxSet k) ⟩)
```

最后一次搬运把解码得到的数码 `# j` 换回原来的首分量。因此，预期定义域中的每个元素都有相应条目，定义域条件的后一半由此完成。

```agda
                (sym q) (approx-mem-in k j hj))
```

还需验证逐点递归条件。有限表中出现的每个有序对都必须满足 `RelStepAt`，从而说明其第二分量确实是由首分量处的递归所确定的关系值。

```agda
    onStep : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩
           → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩
    onStep x y p = PT.rec (snd ((y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f)))
      named
      (approx-mem-out k (pr (fst x) (fst y))
```

先把表中的成员关系搬运到 `approxSet k`，再由 `approx-mem-out` 读取。所得标准形式带有命题截断；由于满足 `RelStepAt` 是命题，可以消去这层截断。

```agda
        (subst (λ t → ⟨ pr (fst x) (fst y) ∈ t ⟩) qf p))
      where
      named : Σ[ j ∈ ℕ ]
                ((j < k) × (pr (fst x) (fst y) ≡ pr (# j) (fst (relAt j))))
            → ⟨ (y ∷ x ∷ γ) ⊨ RelStepAt zero (suc zero) (sh2 f) ⟩
```

对恢复出的第 `j` 个条目，`rel-step` 重建递归步。它对每个 `i < j` 所需的假设来自 `approxSet k` 的取值正确性与条目完备性；`<` 的传递性把 `i < j < k` 化为这些引理所需的界。

```agda
      named (j , (hj , q)) =
        rel-step zero (suc zero) (sh2 f) (y ∷ x ∷ γ) j (pr-inj q .fst)
          (λ i hi u hu → approxVals k i (<-trans hi hj) u
            (subst (λ t → ⟨ pr (# i) (fst u) ∈ t ⟩) qf hu))
          (λ i hi → subst (λ t → ⟨ pr (# i) (fst (relAt i)) ∈ t ⟩) (sym qf)
```

有序对等式的首分量把实参认同为 `# j`，第二分量则把表中取值认同为 `relAt j`。这正是 `rel-step` 所需的两个端点等式。

```agda
            (approxEnts k i (<-trans hi hj)))
          (pr-inj q .snd)
```

这张具体的有限表现已满足 `ApproxAt`：`onDom` 证明其定义域恰为 `# k`，`onStep` 证明每个已记录实参都满足递归条件。由此得到的逼近没有使用替换。

```agda
  approxSet-approx : ⟨ γ ⊨ ApproxAt f a ⟩
  approxSet-approx = ApproxAt-in f a γ (domAt-intro f a γ onDom) onStep
```

因此，只要环境中表示索引与候选值的分量分别被认同为 `# k` 与 `relAt k`，`relAt k` 就在数码 `# k` 处满足递归图。存在量化的逼近由有限集合 `approxSet k` 见证。

```agda
relAt-graph : ∀ {n} (v b : Fin n) (γ : S ^ n) (k : ℕ)
            → fst (lookup b γ) ≡ # k → fst (lookup v γ) ≡ fst (relAt k)
            → ⟨ γ ⊨ RelGraphAt v b ⟩
relAt-graph v b γ k qb qv = RelGraph-in v b γ (approxSet k)
  (approxSet-approx k zero (suc b) (approxSet k ∷ γ) refl qb)
```

图的引入合并了两个事实：`approxSet-approx` 验证所有较小实参，`rel-step` 则借助 `approxVals` 与 `approxEnts` 验证 `k` 处的当前取值。因此，同一张有限表恰好提供了认证 `relAt k` 所需的全部先前信息。

```agda
  (rel-step (suc v) (suc b) zero (approxSet k ∷ γ) k qb
    (approxVals k) (approxEnts k) qv)
```

## 那一族，作为 `L` 的一个元素

至此，各个有限层关系已逐层得到验证。此前的唯一性论证使用自然数次序 `<` 上的良基归纳，既不建立也不使用 `before` 的良基性。下一项构造沿内部自然数使用替换，把所有 `(# k, relAt k)` 收集成一个属于 `L` 的集合图。

```agda
private
```

对任何已证明等于成对递归图的公式 `φ`，`famBuild` 都返回一个可构造集合 `h`，并带有两条精确性质。每个标准有序对都属于 `h`；而 `h` 中任何首分量已知为 `# k` 的成员，其第二分量都等于 `relAt k`。

```agda
  famBuild : (φ : Formula S 2) → φ ≡ PairRelGraphAt zero (suc zero)
           → Σ[ h ∈ S ]
               ( ((k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst h ⟩)
               × ((cS rS : S) (k : ℕ) → fst cS ≡ # k
                  → ⟨ pr (fst cS) (fst rS) ∈ fst h ⟩ → fst rS ≡ fst (relAt k)) )
```

替换要求每个 `c ∈ ωʟ` 上满足公式的输出纤维都是收缩类型。属于 `ωʟ` 只提供经过命题截断的数码表示；`PT.map` 逐个处理显式数码情形，`mereFunct` 再把截断存在性与取值唯一性合成为收缩性。

```agda
  famBuild φ qφ = r .fst .fst , (inFam , outFam)
    where
    fc : (c : S) → ⟨ c ∈ˢ ωʟ ⟩
       → isContr (Σ[ y ∈ S ] ⟨ (y ∷ c ∷ []) ⊨ φ ⟩)
    fc c c∈ = mereFunct φ c (PT.map atK c∈)
```

在显式的数码情形 `fst c = # j` 中，纤维的中心取为 `c` 与 `relAt j` 的可构造有序对。证明既给出它对 `φ` 的满足，也证明每个满足 `φ` 的其他输出都等于该中心；它并未从命题截断之外选择规范的 `j`。

```agda
      where
      atK : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst c)
          → Σ[ y ∈ S ] ( ⟨ (y ∷ c ∷ []) ⊨ φ ⟩
                       × ((y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ y) )
      atK (j , qj) = prS c (relAt (lower j)) , (holds , only)
```

数码解码器给出的等式方向相反。将其反向便得到 `fst c = # j`，这正是把递归图定理应用于 `j` 所需的形式。

```agda
        where
        qc : fst c ≡ # (lower j)
        qc = sym qj
```

为证明选定的有序对满足 `φ`，先用 `φ` 与成对图的等式把目标化为 `PairRelGraphAt`。有序对构造给出外层配对等式，`relAt-graph` 则给出 `relAt j` 的图断言。

```agda
        holds : ⟨ (prS c (relAt (lower j)) ∷ c ∷ []) ⊨ φ ⟩
        holds = PairRelGraph-in zero (suc zero)
          (prS c (relAt (lower j)) ∷ c ∷ []) φ qφ (relAt (lower j))
          (prS-fst c (relAt (lower j)))
          (relAt-graph zero (sh2 zero)
```

图断言在索引 `j` 处实例化：表示索引的分量由反向后的解码等式认同为 `# j`，候选关系按定义就是 `relAt j`。纤维证明的存在性部分由此完成。

```agda
            (relAt (lower j) ∷ prS c (relAt (lower j)) ∷ c ∷ [])
            (lower j) qc refl)
```

为证明唯一性，设 `y'` 是另一个满足 `φ` 的输出。读取成对图得到 `y'` 的一个经过命题截断的分解；由于 `S` 中的相等是命题，可以把该截断消去到目标 `y' = prS c (relAt j)` 中。

```agda
        only : (y' : S) → ⟨ (y' ∷ c ∷ []) ⊨ φ ⟩ → y' ≡ prS c (relAt (lower j))
        only y' h = PT.rec (isSetS y' (prS c (relAt (lower j)))) read
          (PairRelGraph-out zero (suc zero) (y' ∷ c ∷ []) φ qφ h)
          where
          read : PairOf zero (suc zero) (y' ∷ c ∷ []) φ qφ
```

一个显式分解把 `y'` 写成 `c` 与某个图取值 `z` 的有序对。定理 `rel-only` 把 `z` 的底层集合认同为 `relAt j`，而带有属于 `L` 之证明的元素的外延相等，把所得有序对等式提升到 `S` 中。

```agda
               → y' ≡ prS c (relAt (lower j))
          read (z , (q , hg)) = Σ≡Prop (λ t → snd (isL t))
            ( q
            ∙ cong (pr (fst c))
                (rel-only zero (sh2 zero) (z ∷ y' ∷ c ∷ []) (lower j) qc hg)
```

最后的等式把底层有序对与封装后的可构造有序对 `prS c (relAt j)` 比较。由此得到解码数码处集合取值的唯一性，并不声称图见证本身唯一。

```agda
            ∙ sym (prS-fst c (relAt (lower j))) )
```

现在沿 `ωʟ` 使用替换，得到一个收缩类型，其中的可构造集合恰好以这些 `y` 为成员：只需经过命题截断地存在 `c ∈ ωʟ`，使 `φ` 成立。收缩性保证所得集合唯一，而存在的数码数据仍处于命题截断之中。

```agda
    r : isContr (SetOf (λ y → ∃[ c ∶ S ] (c ∈ˢ ωʟ) ⊓ ((y ∷ c ∷ []) ⊨ φ)))
    r = hasReplacementL ωʟ φ fc
```

每个标准有序对都属于替换所得的集合。对替换的规格取见证 `numS k`，并给出它属于 `ωʟ` 以及 `relAt k` 满足成对图的证明；随后把封装的有序对搬运为它在 `V` 中的底层有序对。

```agda
    inFam : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst (r .fst .fst) ⟩
    inFam k = subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) qe
      (subst ⟨_⟩ (sym (r .fst .snd (prS (numS k) (relAt k))))
        ∣ numS k , (inω , holds) ∣₁)
      where
```

所需搬运等式只展开封装：`prS (numS k) (relAt k)` 的底层集合就是 `# k` 与 `relAt k` 的底层集合所成的有序对。`numS k` 的等式给出其中的首分量。

```agda
      qe : fst (prS (numS k) (relAt k)) ≡ pr (# k) (fst (relAt k))
      qe = prS-fst (numS k) (relAt k)
         ∙ cong (λ t → pr t (fst (relAt k))) (numS-fst k)
```

见证 `numS k` 属于内部自然数，因为它的底层集合是 `# k`，而每个数码都属于 `ω`。沿 `numS-fst` 搬运 `#∈ω k`，即可得到所需成员关系。

```agda
      inω : ⟨ numS k ∈ˢ ωʟ ⟩
      inω = subst (λ t → ⟨ t ∈ ω ⟩) (sym (numS-fst k)) (#∈ω k)
```

余下的见证证明封装后的标准有序对满足 `φ`。成对图的引入把目标化为有序对等式，以及 `relAt k` 在 `# k` 处满足递归图这一事实。

```agda
      holds : ⟨ (prS (numS k) (relAt k) ∷ numS k ∷ []) ⊨ φ ⟩
      holds = PairRelGraph-in zero (suc zero)
        (prS (numS k) (relAt k) ∷ numS k ∷ []) φ qφ (relAt k)
        (prS-fst (numS k) (relAt k))
        (relAt-graph zero (sh2 zero)
```

递归图定理直接在 `k` 处实例化。等式 `numS-fst k` 把输入认同为 `# k`，自反性把候选输出认同为 `relAt k`，从而完成标准条目的证明。

```agda
          (relAt k ∷ prS (numS k) (relAt k) ∷ numS k ∷ []) k (numS-fst k) refl)
```

对于反向规格，设一个有序对属于替换所得的集合，并且已知其首分量是 `# k`。目标只是证明其第二分量等于 `relAt k`；这是命题值结论，因此可以向其中消去替换成员关系所含的命题截断。

```agda
    outFam : (cS rS : S) (k : ℕ) → fst cS ≡ # k
           → ⟨ pr (fst cS) (fst rS) ∈ fst (r .fst .fst) ⟩
           → fst rS ≡ fst (relAt k)
    outFam cS rS k qc h =
      PT.rec (setIsSet (fst rS) (fst (relAt k))) atD
```

替换规格给出一个经过命题截断的内部自然数 `d`，使封装后的输入有序对在 `d` 上满足 `φ`。这里没有选择某个数码；稍后的有序对等式会把 `d` 的底层集合与已经指定的 `# k` 认同。

```agda
        (subst ⟨_⟩ (r .fst .snd (prS cS rS))
          (subst (λ t → ⟨ t ∈ fst (r .fst .fst) ⟩) (sym (prS-fst cS rS)) h))
      where
      atD : Σ[ d ∈ S ] ( ⟨ d ∈ˢ ωʟ ⟩ × ⟨ (prS cS rS ∷ d ∷ []) ⊨ φ ⟩ )
          → fst rS ≡ fst (relAt k)
```

读取成对图再次在命题截断下给出一个关系取值 `z`、把封装成员认同为有序对 `(d,z)` 的等式，以及 `z` 在 `d` 处满足递归图的证明。集合相等是命题，因此这层截断同样可以消去。

```agda
      atD (d , (d∈ , hp)) = PT.rec (setIsSet (fst rS) (fst (relAt k))) read
        (PairRelGraph-out zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ hp)
        where
        read : PairOf zero (suc zero) (prS cS rS ∷ d ∷ []) φ qφ
             → fst rS ≡ fst (relAt k)
```

去除封装等式后，有序对的单射性把所给第二分量认同为 `z`。一旦首分量等式表明图的索引是 `# k`，定理 `rel-only` 就进一步把 `z` 认同为 `relAt k`。

```agda
        read (z , (q , hg)) = pr-inj q' .snd
          ∙ rel-only zero (sh2 zero) (z ∷ prS cS rS ∷ d ∷ []) k qd hg
          where
          q' : pr (fst cS) (fst rS) ≡ pr (fst d) (fst z)
          q' = sym (prS-fst cS rS) ∙ q
```

所需的索引等式来自同一个有序对等式的首分量。将该分量反向后，`d` 被认同为原来的首分量；再与关于该首分量的假设复合，便得到 `fst d = # k`。

```agda
          qd : fst d ≡ # k
          qd = sym (pr-inj q' .fst) ∙ qc
```

把实际的成对递归图交给 `famBuild` 后，所得可构造集合被命名为 `beforeFam` 并保持不透明。紧随其后的规格引理将给出所有标准条目，以及每个已知数码处集合取值的唯一性；这一步提供的是内部关系族，尚未比较名字，也未证明最终良序。

```agda
opaque
  beforeFam : S
  beforeFam = famBuild (PairRelGraphAt zero (suc zero)) refl .fst
```

对每个自然数 `k`，内部图 `beforeFam` 都包含数码 `# k` 与已实现关系 `relAt k` 组成的有序对。这是该族的正向隶属律：它直接写入已经给定的数码与关系，并不从命题截断中选择数码解码见证。

```agda
  beforeFam-in : (k : ℕ) → ⟨ pr (# k) (fst (relAt k)) ∈ fst beforeFam ⟩
  beforeFam-in = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .fst
```

反过来，设 `beforeFam` 的一个条目的第一分量等于 `# k`，则其第二分量的底层集合等于 `relAt k` 的底层集合。因此，该图在指定数码处具有唯一的集合值；这既不提供规范的解码见证，也不声称构造所携带的每份证明都唯一。

```agda
  beforeFam-out : (cS rS : S) (k : ℕ) → fst cS ≡ # k
                → ⟨ pr (fst cS) (fst rS) ∈ fst beforeFam ⟩
                → fst rS ≡ fst (relAt k)
  beforeFam-out = famBuild (PairRelGraphAt zero (suc zero)) refl .snd .snd
```

## 某个槽位所持数码处的那个序

公式 `BeforeAt b x y` 分两步寻找关系 `r`。首先，`appC` 断言常元族 `beforeFam` 在 `b` 所指的值处取值为 `r`；随后，`appAt` 断言 `r` 包含 `x` 与 `y` 所指对象组成的有序对。下一条定理假设 `b` 所指的值为数码 `# m`，并在下文明确列出的层隶属条件下，把这一内部陈述认同为 `before m`。

```agda
opaque
  BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  BeforeAt b x y =
    ∃̇ ( appC beforeFam (suc b) zero ∧̇ appAt zero (suc x) (suc y) )
```

固定一个环境与自然数 `m`。关于 `b` 的等式说明其值是数码 `# m`，另两条隶属假设则把 `x` 与 `y` 所指的值放入 `finiteStage m`。这些假设把三个变元联系到同一个有限层比较；充分性定理只在这一受限语境中陈述。

```agda
module _ {n : ℕ} (b x y : Fin n) (γ : S ^ n) (m : ℕ)
         (qb : fst (lookup b γ) ≡ # m)
         (hx : ⟨ fst (lookup x γ) ∈ finiteStage m ⟩)
         (hy : ⟨ fst (lookup y γ) ∈ finiteStage m ⟩) where
  private
```

语义目标是一个元层面命题：按照 `before m`，`x` 所指的值先于 `y` 所指的值。此处的论证只建立一次有限层比较的表示，并不提出新的良基性结论。

```agda
    Goal : Type (ℓ-suc ℓ)
    Goal = ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
```

为了读出一个满足赋值，先暂时展开存在量词所隐藏的数据：一个关系 `r`、该族在 `b` 处取值为 `r` 的证据，以及 `r` 包含 `x,y` 处有序对的证据。这个类型描述的是一份显式数据包，但存在量词的语义只在命题截断下提供它，因而不会得到可保留或规范的见证。

```agda
    AtR : Type (ℓ-suc ℓ)
    AtR = Σ[ r ∈ S ]
      ( ⟨ (r ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩
      × ⟨ (r ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩ )
```

从任意一份这样的显式数据包出发，两条应用充分性律把公式满足读成通常的集合隶属。族的规律把 `r` 的底层集合识别为 `relAt m` 的底层集合；沿此等式运输有序对的隶属后，`relAt-rep` 再把它读回 `before m`。最后这一步恰好需要前述两条有限层隶属假设。

```agda
    atR : AtR → Goal
    atR (r , (happ , hmem)) =
      relAt-rep m (fst (lookup x γ)) (fst (lookup y γ)) hx hy
        (subst (λ t → ⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ t ⟩) qr
          (subst ⟨_⟩ (appAt-adequate zero (suc x) (suc y) (r ∷ γ)) hmem))
```

第一条应用事实在内部断言：`beforeFam` 在 `b` 所存条目处取值为 `r`。它的充分性律把这条陈述化为外部隶属事实，即该条目与 `r` 组成的有序对属于 `beforeFam`。

```agda
      where
      hf : ⟨ pr (fst (lookup b γ)) (fst r) ∈ fst beforeFam ⟩
      hf = subst ⟨_⟩ (appC-adequate beforeFam (suc b) zero (r ∷ γ)) happ
```

由于已经知道 `b` 处的条目等于 `# m`，族的反向规律便把 `r` 的底层集合识别为 `relAt m` 的底层集合。这里使用的是指定数码处集合值的唯一性，而不是对数码解码作全局选择。

```agda
      qr : fst r ≡ fst (relAt m)
      qr = beforeFam-out (lookup b γ) r m qb hf
```

现在可以证明精确语义对应的两个方向。局部展开 `BeforeAt` 会显露它的单个存在量词与两条应用事实，而关于 `b`、`x`、`y` 的假设始终保留在两个陈述中。

```agda
  opaque
    unfolding BeforeAt
```

在向外方向中，存在量词的满足只给出经过命题截断的关系数据包。证明把该命题截断直接消去到作为命题的 `Goal`：对每份假设中的显式数据包应用上面的转换即可。它并不会抽取并保留中间类型的元素。

```agda
    BeforeAt-out : ⟨ γ ⊨ BeforeAt b x y ⟩
                 → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
    BeforeAt-out h =
      PT.rec (snd (before m (fst (lookup x γ)) (fst (lookup y γ)))) atR h
```

在向内方向中，`before m` 的证明提供公式所需的关系隶属。我们取 `relAt m` 作为合适的关系，证明两条应用事实，再按存在量词的语义把整份数据包置于命题截断之下。这是为该方向构造的见证，并非从某个命题截断中恢复出的规范见证。

```agda
    BeforeAt-in : ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
                → ⟨ γ ⊨ BeforeAt b x y ⟩
    BeforeAt-in h = ∣ relAt m , (happ , hmem) ∣₁
      where
      happ : ⟨ (relAt m ∷ γ) ⊨ appC beforeFam (suc b) zero ⟩
```

族的应用来自 `beforeFam` 中已知的条目 `(# m, relAt m)`。先沿关于 `b` 的等式运输其第一分量，再反向使用应用的充分性，就得到所需的内部应用事实。

```agda
      happ = subst ⟨_⟩
        (sym (appC-adequate beforeFam (suc b) zero (relAt m ∷ γ)))
        (subst (λ t → ⟨ pr t (fst (relAt m)) ∈ fst beforeFam ⟩) (sym qb)
          (beforeFam-in m))
```

第二条应用事实来自 `relAt-fill`：两条有限层隶属假设与给定的 `before m` 比较共同说明，`x,y` 处两个值组成的有序对属于 `relAt m`。反向读取应用的充分性，便把这条隶属转成 `appAt` 的满足。

```agda
      hmem : ⟨ (relAt m ∷ γ) ⊨ appAt zero (suc x) (suc y) ⟩
      hmem = subst ⟨_⟩
        (sym (appAt-adequate zero (suc x) (suc y) (relAt m ∷ γ)))
        (relAt-fill m (fst (lookup x γ)) (fst (lookup y γ)) hx hy h)
```

## 那个框架，兑现

这两条充分性方向使 `BeforeAt` 满足先前 `Described` 框架的输入要求。该框架先比较两个极限层编码所在的有限层号；层号相同时，再使用本章所表示的层内 `before` 关系；随后由分离把这种比较实现为内部关系 `codeOrder`。这个实例只供应码序部分，尚未比较名字，也未证明最终的内部良序。

```agda
private
  module CodeOrder = Described BeforeAt BeforeAt-in BeforeAt-out
```

所得结论是关系集 `codeOrder` 及其两条表示律。`codeOrder-fill` 把元层面的 `limitOrder` 比较转成这个集合中的隶属，`codeOrder-rep` 则把这种隶属读回。后续的名字比较用这三项结果比较码，而参数的比较关系另行提供。

```agda
open CodeOrder public using ( codeOrder; codeOrder-fill; codeOrder-rep )
```

## 小结

对每个自然数 `n`，`L` 中的集合 `relAt n` 都在 `finiteStage n` 的成员上表示 `before n`。递归图验证这些取值，只有最后沿 `ωʟ` 把整族收集为 `beforeFam` 时才使用替换；有限逼近使用的是 `finSet` 与 `finSetL`。若 `b` 所指的值是 `# m`，且 `x,y` 所指的值属于 `finiteStage m`，则 `BeforeAt b x y` 等价于用 `before m` 比较这两个值。实例化 `Described` 后得到 `codeOrder`、`codeOrder-fill` 与 `codeOrder-rep`，它们将在后续供应码的比较关系，而本章尚不比较名字，也不证明最终的内部良序。