---
title: "名字比较的公式"
module: L.Choice.NameComparison
lang: zh
site: "Bedrock"
description: "名字比较的公式"
stage: "典范良序与选择公理"
reading_order: 77
canonical: https://bedrock.institute/zh/L.Choice.NameComparison.html
html: L.Choice.NameComparison.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparison.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.Satisfaction, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.SatisfactionGraph, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.PinnedRecursion, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.NameComparison.md, https://bedrock.institute/ja/L.Choice.NameComparison.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 名字比较的公式

同一个可定义子集可能有许多名字。在元语言中，一个名字由三份数据组成：元数 `k`、具有 `suc k` 个变元位的无参公式，以及取自载体的 `k` 个参数所成的向量。名字的指称由这三份数据派生：多出的那个变元表示待判断的元素，其余变元接收参数向量。因此，指称不是名字的第四个分量。

为了在 `L` 内表达这些数据，本章把参数向量表示为有穷环境图，并用满足关系图表示公式的读取。在真实的公式键处，`satGraphAt` 把该键关联到所有满足该公式的环境所成的集合。因此，它的输出恰是这个满足环境集。`NameAt` 把元数、无参公式码和参数环境与派生的指称联系起来；后文量化竞争名字时，它们都要具有同一个指称。

名字按字典序比较：先由极限层上的序比较公式码，再比较元数，最后依载体上给定的序比较参数向量。公式 `≺At` 表达这三种情形。`LeastNameAt` 只陈述当前名字没有同指称而更小的名字；真正选出最小名字的是前文的 `CanonicalNames.leastName`。`StepAt` 在局部量化两条最小名字并比较它们。本章完成的充分性恰好止于 `≺At` 与元语言关系 `_≺ₙ_` 的对应；`NameAt`、`LeastNameAt` 与 `StepAt` 的完整充分性由后续发展给出。

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

底层语言供给宇宙层级、有穷指标、向量与取值为命题的陈述。经典推理只经一个显式假设 `LEM (ℓ-suc ℓ)` 进入；它的层级足以承载下文使用的满足关系构造与良序。保留这个显式假设，有助于区分「只陈述一项性质」与「真正选出一个见证」这两类步骤。

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

现在固定宇宙层级 `ℓ`，并在所需的更高层级上假设排中律。这是本章沿用的经典逻辑接口。下面的公式构造器只组合语法，但它们使用的自然数对象、满足关系图、极限层码序和典范名字理论都在同一假设下构造。因此，本模块如实记录这些语义依赖，而不再次作选择。`LeastNameAt` 表达最小性；实际选出最小名字的构造仍是 `CanonicalNames.leastName`。

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

对象语言能够陈述隶属与相等，组合命题，并在整个载体或某个集合上量化；它的语义在取值为命题的结构中读取。常元映射连接后文所需的三种呈现：真正的无参公式、空字母表上的公式，以及在可构造载体上解释的同一语法。这些映射保持公式结构，因此后文可以在内部辨认一个无参骨架的码。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )
```

公式码、有序对与数码本身都是累积层级中的集合。可构造子结构提供读取这些公式的载体；传递性则使码集中的隶属事实能够供给其分量所需的可构造性。配对编码与数码编码的单射性将在后文从相等的键中恢复元数与骨架码。诸 `Lset` 层为极限层码序提供背景。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; Lset )
open import L.Ordinal {ℓ} using ( ∈#-elim; #∈#-elim )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; extensionalL )
```

元数由内部自然数集中的数码表示，参数向量则由有穷环境的图表示。对象语言公式能够检查有序对、应用与定义域，把一个待判断的元素加入环境，并以外延方式定义子集。对于载体上的一条公式，`Sat` 是所有满足该公式的环境所成的集合。后文从满足关系图恢复的正是这个集合值。

```agda
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Coding.Environment {ℓ} using ( env; lookup-spec )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; appAt; appAt-adequate; domAt; domAt-in; domAt-out; domAt-intro; envOverAt )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in-both; numL; sucAtL; sucAtL-adequate; consAtL )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

满足关系已经被组织成一张表，其中每个条目把子公式键与递归确定的满足环境集配成一对。槽位闭包与全性保证递归所需的每个真实键都有条目，满足关系桥则把公式中的常元认作所选载体的元素。因此，本章可以读取某个键处已经存下的集合值，而无须重新运行满足关系递归。

```agda
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.CodeSet {ℓ} lem
```

对每个载体，`AllCodes` 恰好收集该载体上所有真实的公式键；它的两个方向把成员关系与相应公式联系起来。统一满足关系桥由此支持关系公式 `satGraphAt B x y`：当 `x` 是槽位 `B` 所持载体上的真实键时，`y` 就是相应的满足环境集。`GraphWitAt` 与两条图读式揭示这项集合值关系，而无须启动新的递归。

```agda
  using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge )
open import L.Coding.SatisfactionGraph {ℓ} lem using
  ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
  ; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
```

环境塔与带标签的递归数据证明满足关系图的读法对每种语法构造都成立。与这套内部机制相对照，典范名字理论供给名字比较所遵循的元语言标准。元语言的 `Name` 存储元数、无参公式与参数向量；`limitCode` 从公式派生第一个比较键，而指称则另由满足关系派生。后文的槽位公式必须保持这一区分。

```agda
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )
```

名字的码是极限层的成员，并由 `limitOrder` 比较。第三个键来自载体上任意给定的严格良序。典范命名理论已经把这两项与自然数元数组合成 `_≺ₙ_`，证明该关系良基，并在 `leastName` 中使用它。本章让两个非数值的序经带有表示律的关系槽位出现，因而只描述它们所决定的比较，而不重新构造其中任何一个序。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
```

自然数序供给第二个比较键：当元数表示为数码时，一个数码隶属于另一个数码正好表达严格小于。有穷指标用于定位参数向量的分量，以及两个向量最早出现差异的位置。后文的充分性论证对共同长度作归纳，证明这种「首次相异」描述与 `_≺ₙ_` 所用的递归向量序一致。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )
```

证明数据遵循字典序的形状。依值对携带某个位置及其证据，余积则区分码、元数与参数三种情形。前面诸键的相等性允许把依值公式与向量运输到共同元数，再比较下一个键。空类型给出无常元公式所需的唯一常元解释。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )
```

存在式与析取式的满足语义带有命题截断：它保留「见证存在」，却忘掉给出的是哪个见证。因此，从公式码或名字比较向外读取时，结论仍是经过命题截断的存在性，而消去也只进入命题。这里发生的是命题截断；命题降级并未在此出现。累积层级则供给集合值的隶属关系，以及这些读式之后所需的外延相等原则。

```agda
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

层级集合的小成员能够嵌入外围层级；该嵌入的单射性将在后文把已表示参数的相等恢复为载体中的相等。空集充当空字母表：它没有常元，因此从它出发的映射唯一确定，无参公式在所需的重标记下保持同一个码。冯·诺伊曼数码 `# k`、它们的后继与 `ω` 则提供环境定义域和名字比较所用的内部元数。

```agda
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )
```

下文的公式都解释在可构造宇宙中。打开 `hPropStructure 𝒮ʟ` 便固定了它们的载体 `S`：载体的一个元素是环境宇宙中的一个集合，连同它可构造的证据。这个操作也把该结构中取命题值的等词与隶属关系带入作用域。因此，自由变元与常元都在可构造集合中取值；证明需要使用某条等词或隶属命题的证据时，`⟨_⟩` 则取出该命题的底层类型。

```agda
open hPropStructure 𝒮ʟ
```

同一套句法有两种彼此相容的读法。这个绝对性实例从环境宇宙结构 `𝒮ᵥ` 出发，把它限制到传递类 `isL`。在外层读法中，一个可构造集合经其底层的环境集合来读取；在内层读法中，常元指称为它命名的那个可构造集合，而等词与隶属由限制后的结构解释。本章把内层满足关系改名为 `⊨`。因此，对 `γ : S ^ n`，判断 `γ ⊨ F` 表示公式 `F` 在 `L` 内部、有限环境 `γ` 下成立。这正是 `L` 自身识别并比较名字时所需的读法。

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

这些公式用环境中的位置指向先前给定的数据。每进入一层新的约束，原有位置都必须越过新绑定的取值；经过两层约束后，位置 `i` 因而变成 `suc (suc i)`。缩写 `sh2` 记录的正是这次移动。`FreeAt` 先绑定后继元数及其码键，再读取骨架与空字母表码集时会用到它；指称条件先绑定候选元素及其扩展环境，再读取原参数环境时也会用到它。

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

在指称条件内部，须等四个取值进入环境之后，才会读取骨架与载体的码集。这四个取值依次是候选元素 `z`、扩展环境 `c`、它的定义域 `k`，以及正在考察的键。因此，原来的位置必须连续提升四次。`sh4` 恰好执行这次移位，使公式既能要求该键属于载体的码集，也能要求它等于由 `k` 与骨架组成的对。

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

再有一层存在量词绑定与该键相配的取值 `v`，所以调用 `satGraphAt` 时，载体的位置已隔着五个新取值。这里的 `v` 是满足被编码公式的诸环境所成的集合，并不是真值；紧接着的隶属原子询问扩展环境是否属于这个集合。同一档移位还出现在 `LexAt` 中：依次绑定一个序号、两个环境在该处的取值、一个更早的序号，以及见证两边相符的共同取值后，原参数环境也恰好隔着五个位置。`sh5` 统一记录了两处的下标计算。

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

## 同一个码，落在空字母表上

空字母表是空集成员的小表示 `⟪ ∅ ⟫`。如果 `m` 是其中一个符号，那么嵌入 `⟪ ∅ ⟫↪` 会给出一个环境集合，而表示定律会断言这个集合属于 `∅`。定理 `∅-empty` 恰好排除了这种证据，由此得到 `noAlpha m`。所以，这个字母表上的公式不可能含有常元节点。它们给出了无参公式的一种句法呈现；要把它与元层面名字所用的空常元域 `⊥*` 联系起来，只须关联这两个空类型。

```agda
private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → Empty.⊥
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)
```

`Fo∅ n` 是公式族 `Formula ⟪ ∅ ⟫ n` 的简称，也就是空字母表上具有 `n` 个可用变元位置的公式。它们不含常元，这是由常元符号的类型保证的，并非另有一个作用于公式的谓词。元层面名字使用与之平行的公式族 `Formula ⊥* n`。更确切地说，一个 `Name` 存储元数、在这个公式族中多出一个变元位置的无参公式，以及具有该元数的参数向量；指称由这三份数据派生，并不是另一个存储分量。

```agda
  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫
```

映射 `ε` 把空字母表 `⟪ ∅ ⟫` 送到空常元域 `⊥*`。给定一个假想的源符号 `m`，`noAlpha m` 导出矛盾，再由空型消去得到所需的目标。因此，`mapFo ε` 把 `⟪ ∅ ⟫` 上的公式改名为 `⊥*` 上的公式；反方向则可把 `embed` 特化为从 `⊥*` 到 `⟪ ∅ ⟫` 的改名。两种操作都不会改变任何常元出现，因为本来就没有常元。改名的复合法则因而给出空字母表刻画所需的精确公式码等式。

```agda
  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = Empty.rec (noAlpha m)
```

要在模型内部识别无参公式的码，首先必须联系「没有常元」的两种表示。以`⟪ ∅ ⟫` 为常元域的公式 `ψ`，其常元来自空集的成员；而 `mapFo ε ψ` 把同一份语法表示在空类型 `⊥*` 上。若假定空集有一个成员便会得到矛盾，所以映射 `ε`得以定义。于是，直接把 `ψ` 读入宇宙，与先沿 `ε` 改名再嵌入宇宙，两者的差别只在于从空类型出发的映射。函数外延性判定这些映射相等，`mapFo-comp` 再判定复合改名相等。因此，`sameCode` 首先证明所得宇宙公式本身相等；稍后对这条等式施用编码映射，便得到相应码的等式。

```agda
  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → Empty.rec (noAlpha m)))
             ∙ sym (mapFo-comp ε Empty.rec* ψ)
```

反向的比较从无参公式 `χ : Formula ⊥* n` 出发。可以先把它嵌入以 `⟪ ∅ ⟫`为常元域的公式，再沿该字母表到宇宙的包含映射改名；也可以把它直接嵌入宇宙上的公式。由 `mapFo-comp`，第一条路线就是一次从 `⊥*` 出发的改名；而从 `⊥*`出发的任意两个函数都相等，所以这次改名正是直接嵌入所用的改名。`sameCode'`给出的等式方向，恰好能把 `AllCodes ∅ʟ` 赋予嵌入公式的键，转换成 `χ` 通常的宇宙公式码所组成的键。

```agda
  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp Empty.rec* ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → Empty.rec* b))
```

这里还有一个依值类型问题。元数属于公式类型的一部分，所以等式 `e : i ≡ j`会把 `ψ : Fo∅ i` 移到 `subst Fo∅ e ψ : Fo∅ j`。然而完成这次迁移后，键中的公式码应当保持不变。读取并编码公式的函数以固定的宇宙 `V ℓ` 为值域，而该值域不依赖元数索引。因此，一般的替换计算 `constSubstCommSlice` 表明，沿元数等式迁移公式不会改变其码。`codeShift` 把这条等式排成从迁移后公式的码指回原公式之码的方向，以便解码论证随后调整元数。

```agda
  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)
```

现在可以证明码集桥接中较直接的一向。对任意无参 `k` 元公式 `χ`，先把它嵌入 `⟪ ∅ ⟫` 上，所得公式的键由 `key∈AllCodes` 属于 `AllCodes ∅ʟ`。这个键由数码 `# k` 与「经空字母表读入所得的嵌入公式之码」组成。等式 `sameCode'` 把该公式等同于 `χ` 直接嵌入宇宙所得的公式，而后者的码正是 `fst (limitCode χ)`。沿这条等式迁移隶属证明，便得到 `freeCode-in`：码集包含每条无参公式的「元数与码」之键。

```agda
freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) (fst (limitCode χ)) ∈ fst (AllCodes ∅ʟ) ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ fst (AllCodes ∅ʟ) ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))
```

反向则设 `pr (# k) c` 属于 `AllCodes ∅ʟ`。消去定理 `AllCodes-out` 只在命题截断下解码一个成员，而且它接收的是 `S` 的元素，也就是一个集合连同其可构造性证明。所需输入的底层集合已经是 `pr (# k) c`，还须补上它的可构造性证明。完成这一步以后，`PT.map read` 会把命题截断中的每一份可能解码载荷变成所需的 `k` 元无参载荷，始终不消去命题截断。

```agda
freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ fst (AllCodes ∅ʟ) ⟩
             → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ)) ∥₁
freeCode-out k c h = PT.map read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩
```

这张缺少的证书来自可构造性的传递性。`AllCodes ∅ʟ .snd` 说明码集可构造，`h`则说明该键属于码集，故 `isL-trans h (AllCodes ∅ʟ .snd)` 证明键本身可构造。把这张证书与 `pr (# k) c` 配对，就得到 `AllCodes-out` 所要求的 `S` 元素；此处没有额外的解码，也没有发生选择。

```agda
  cL = isL-trans h (AllCodes ∅ʟ .snd)
```

在命题截断内部，`AllCodes-out` 给出一个元数 `n`、一条公式 `ψ : Fo∅ n`，以及一条说明「给定的键就是 `ψ` 的键」的等式。局部函数 `read` 把每份这样的载荷变成所需元数 `k` 处的一条无参公式，并附上 `c` 等于其码的证明。它先把 `ψ` 迁移为 `ψ' : Fo∅ k`，再沿 `ε` 改名其不可能出现的常元。因此，所构造的见证是 `mapFo ε ψ'`。有序对的等式同时给出迁移所需的元数等式，以及返回依值对时所需的码等式。

```agda
  read : Σ[ n ∈ ℕ ] Σ[ ψ ∈ Fo∅ n ] (pr (# k) c ≡ fst (keyS ∅ʟ ψ))
       → Σ[ χ ∈ Formula (⊥* {ℓ}) k ] (c ≡ fst (limitCode χ))
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k
```

键等式的两个分量完成这一构造。第一分量的类型是 `# k ≡ # n`；数码的单射性再配合对称性，给出 `e : n ≡ k`，公式 `ψ` 沿它迁移为 `ψ'`。第二分量说明 `c`等于从原公式 `ψ` 得到的宇宙公式码。由 `codeShift`，该码等于迁移后 `ψ'` 的码；再由 `sameCode`，后者等于 `embed (mapFo ε ψ')` 的码。复合这些等式，恰好得到与见证配对的证明。由于 `read` 只通过 `PT.map` 使用，`freeCode-out` 的结论只是在命题截断下存在这样一条无参公式，并未从码集中选择出一条公式。

```agda
    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')
```

## 无参性，说成一个原子

码集把一条公式存放在由其元数与骨架组成的键之下。为了用一个隶属原子表达此事，`FreeAt` 先绑定元数位置之取值的后继，再绑定这个后继与骨架组成的对，最后询问该对是否属于码集位置。因此，用元语言记号看，它具有 `∃[ z ] ∃[ y ]` 的形状：`z` 是后继元数，`y` 是键。各次移位只记录穿过一层或两层绑定之后仍要读取哪个原位置。此时公式本身只描述对 `C₀` 所给集合的隶属；待该位置被认作空字母表的码集后，它才得到无参性的含义。

```agda
FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )
```

第一对读式在任意环境 `γ` 上成立。外部等式 `qa` 把元数位置的取值认作数码 `# k`；它是语义读式的假设，并不是 `FreeAt` 内部的另一个子句。骨架位置与码集位置仍可任意取值，所以这些引理先单独说明两层绑定的逻辑内容，尚不指定所用的码集。

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (qa : fst (lookup a γ) ≡ # k) where
```

正向构造从预期的键 `pr (# (suc k)) (fst (lookup s γ))` 已属于 `C₀` 位置上的集合这一假设出发。这个键恰好给出 `FreeAt` 所需的两个存在见证：先取数码 `# (suc k)`，再取它与骨架组成的对。余下工作只是核实这两个见证分别满足后继描述与配对描述；最末的原子正是起初假设的隶属。

```agda
  FreeAt-in : ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
            → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
    where
    numAt : S
```

内部语言的存在见证是 `S` 的元素，因此其底层集合必须连同一份可构造性证明给出。第一个见证 `numAt` 的证明来自每个数码都属于 `L`。对于第二个见证 `keyAt`，隶属假设把该键放进 `C₀` 位置所持有的可构造集中，再由 `L` 的传递性得到键本身可构造。这两份证明只是使数码与键能够充当绑定取值，并未给 `FreeAt` 增添新的数学条件。

```agda
    numAt = # (suc k) , numL (suc k)
    keyAt : S
    keyAt = pr (# (suc k)) (fst (lookup s γ)) , isL-trans h (lookup C₀ γ .snd)
    hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
    hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))
```

两条辅助公式的充分性等式现在完成所需核实。对于 `hsuc`，等式 `qa` 把元数位置的取值换成 `# k`，而这个数码的后继就是 `# (suc k)`。对于 `hpr`，`prAtL` 的充分性把对该公式的满足化为「该取值等于两个分量位置所指定的有序对」；`keyAt` 的定义恰是这个对。因此，这两条语义事实把所选见证接到了最后那条隶属原子上。

```agda
      (cong sucV (sym qa))
    hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
    hpr = subst ⟨_⟩
      (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl
```

反向读式从对 `FreeAt` 的满足关系中恢复隶属。存在公式的满足关系只在命题截断内给出见证，所以证明把外层截断消去到目标隶属命题中。外层存在量词的一个代表包含后继见证，以及对内层存在公式的满足关系；后者仍有自己的一层命题截断，随后还要再消去一次。

```agda
  FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
  FreeAt-out = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
                            ∈ fst (lookup C₀ γ))) atNum
    where
```

两次截断消去具有同一个余域，所以证明把它命名为 `Target`：预期的键属于 `C₀` 位置上的集合。该类型是命题，因为集合的隶属关系取命题值。正是这一事实允许两次使用截断消去；证明并没有从存在见证中选出一个特定代表。

```agda
    Target : Type (ℓ-suc ℓ)
    Target = ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ fst (lookup C₀ γ) ⟩
```

分支 `atKey` 处理内层存在量词的一个代表。它取得外层见证 `z` 以及「`z` 是元数取值之后继」的等式，还取得内层见证 `y` 和两条事实：`y` 满足配对公式，且其底层集合属于 `C₀` 位置上的集合。内层存在量词原本带有命题截断，但在这个消去分支内部，可以使用其代表来证明命题 `Target`。

```agda
    atKey : (z : S) → fst z ≡ sucV (fst (lookup a γ))
          → Σ[ y ∈ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                       × ⟨ fst y ∈ fst (lookup C₀ γ) ⟩ )
          → Target
    atKey z qz (y , (hp , hy)) =
```

`prAtL` 的充分性把 `y` 的底层集合认作一个对，其第一分量是 `z` 的底层集合，第二分量是骨架。先用关于 `z` 的等式，再接上 `qa`，便把第一分量认作 `# (suc k)`。因此，`y` 正是预期的键。沿此等式迁移已知的 `y` 的隶属，就得到 `pr (# (suc k)) (fst (lookup s γ))` 的隶属，也就是 `Target`。

```agda
      subst (λ u → ⟨ u ∈ fst (lookup C₀ γ) ⟩)
        (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
         ∙ cong (λ u → pr u (fst (lookup s γ))) (qz ∙ cong sucV qa)) hy
```

外层消去分支 `atNum` 取得一个代表 `z` 和两份证据。第一份说 `z` 满足后继公式；第二份 `hk` 是仍带命题截断的内层存在公式之满足关系。因此，`atNum` 已能确定键的预期第一分量，同时把内层见证留到消去进 `Target` 时再使用。

```agda
    atNum : Σ[ z ∈ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                       × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                       ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
          → Target
    atNum (z , (hs , hk)) = PT.rec (snd (pr (# (suc k)) (fst (lookup s γ))
```

`sucAtL` 的充分性把第一份证据解码成 `atKey` 所需的等式：`z` 是元数位置之取值的后继。随后，证明把 `hk` 消去到命题 `Target`，并对每个代表应用 `atKey`。连同 `FreeAt-out` 外层已有的消去，这恰好处理了两层存在量词，同时守住命题截断的边界。

```agda
                                         ∈ fst (lookup C₀ γ)))
      (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk
```

接下来的读式把此前任意的两个位置具体化。等式 `q₀` 把 `C₀` 位置上的集合认作 `AllCodes ∅ʟ`，其元素是空字母表上诸公式的键；`qa` 则再次把元数取值认作 `# k`。在这两项假设下，`FreeAt-in` 与 `FreeAt-out` 所刻画的隶属便能转换为关于元数为 `suc k` 的无参公式的实际陈述。

```agda
module _ {n : ℕ} (C₀ s a : Fin n) (γ : S ^ n) (k : ℕ)
         (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ))
         (qa : fst (lookup a γ) ≡ # k) where
```

从对 `FreeAt` 的满足关系出发，`FreeAt-out` 得到该键属于 `C₀` 位置当前所持有的集合。沿 `q₀` 迁移后，这条隶属落入 `AllCodes ∅ʟ`。先前的解码引理 `freeCode-out` 随即在命题截断内给出一条元数为 `suc k` 的无参公式 `χ`，其极限层码正是骨架位置的取值。这就是那个隶属原子的向外语义读式。

```agda
  codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
               → ∥ Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                     (fst (lookup s γ) ≡ fst (limitCode χ)) ∥₁
  codeFree-out h = freeCode-out (suc k) (fst (lookup s γ))
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) q₀
```

这里的元数是 `suc k`，因为定义子集所用的名字公式除了 `k` 个参数位置之外，还要留一个变元位置给候选元素。`codeFree-out` 中的公式见证仍处于命题截断内。`FreeAt-out` 可以把自己的绑定见证局部消去到隶属命题中，但最后的解码步骤 `freeCode-out` 又给出一个带命题截断的公式见证。因此，结论只断言这样的公式存在，并不从中选出一条公式。

```agda
      (FreeAt-out C₀ s a γ k qa h))
```

反过来，`codeFree-in` 从一条给定的元数为 `suc k` 的无参公式 `χ` 出发，并假设它的极限层码与骨架位置的取值相等。引理 `freeCode-in` 先把相应的键放入 `AllCodes ∅ʟ`；再沿码等式以及 `q₀` 的反向迁移，便把这条隶属移到实际的骨架位置与码集位置。最后，`FreeAt-in` 用两个存在见证包装所得隶属。这个方向无须产生带命题截断的公式见证，因为 `χ` 本来就是输入数据。

```agda
  codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
              → fst (lookup s γ) ≡ fst (limitCode χ) → ⟨ γ ⊨ FreeAt C₀ s a ⟩
  codeFree-in χ q = FreeAt-in C₀ s a γ k qa
    (subst (λ u → ⟨ pr (# (suc k)) (fst (lookup s γ)) ∈ u ⟩) (sym q₀)
      (subst (λ u → ⟨ pr (# (suc k)) u ∈ fst (AllCodes ∅ʟ) ⟩) (sym q)
```

一旦元数位置与空字母表码集位置得到确定，`codeFree-out` 与 `codeFree-in` 便共同给出 `FreeAt` 所承诺的读法。向外方向在命题截断内断言：骨架是一条具有 `suc k` 个变元的无参公式之码。向内方向从一条给定公式出发，因而不需要这样的截断。名字公式的识别至此完成；下一个问题是，它的有穷参数环境怎样记录数 `k`。

```agda
        (freeCode-in (suc k) χ)))
```

## 一个序列有多长

先刻画集合编码图中的任意隶属。若 `g` 以 `Fin k` 为索引，并且`pr x y` 属于 `env g`，那么仅仅存在一个索引 `i`，使`x ≡ # (toℕ i)` 且 `y ≡ g i`。结果仍处于命题截断内，因为层级集合中的隶属只记录某个生成条目的仅仅存在。因此，`memberOf` 揭示所有可能的索引，却不从中选择一个。

```agda
private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = PT.map
    (λ { (li , e) → lower li
```

隶属见证携带一条等式，把图中存放的条目与所查询的有序对联系起来。有序对构造子的单射性把这一条等式拆成两个分量各自的等式。见证中的等式先写存入的条目，故两个分量的路径都要反向，才能得到 `memberOf` 所需的方向：从 `x`、`y` 分别指向数码键与 `g` 给出的取值。

```agda
       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })
```

反过来，每个给定索引都产生一个条目。对 `i : Fin k`，有序对`pr (# (toℕ i)) (g i)` 属于 `env g`；提升后的索引就是隶属见证，而条目等式由自反性给出。因此，`memberOf` 与 `entryOf` 提供识别这个有穷图之横坐标所需的两个方向。

```agda
  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁
```

定义域的正向包含从如下仅仅存在出发：存在一个模型元素 `y`，使`pr x (fst y)` 位于图中。目标是隶属命题 `x ∈ # k`，所以外层命题截断可以消去到这个目标中。固定其中一个代表 `y` 后，只须从图的隶属中恢复一个索引，并证明该索引的数码属于 `# k`。

```agda
  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = PT.rec (snd (x ∈ # k)) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∈ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))
```

对一个明确的索引 `i`，定义域只用到第一分量的等式。由于`toℕ i < k`，数码引理 `#mono` 给出 `# (toℕ i)` 属于 `# k`；再沿`x ≡ # (toℕ i)` 迁移，便得到 `x` 属于 `# k`。第二分量的等式识别图中的取值，却与这一包含无关。辅助函数 `atEntry` 先固定取值 `y`，然后才消去余下的截断索引信息。

```agda
            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = PT.rec (snd (x ∈ # k)) (atIndex (fst y))
```

对图的隶属应用 `memberOf`，恰好得到所需的索引信息，但它仍在命题截断内。由于 `x ∈ # k` 是命题，`PT.rec` 可以把每个代表交给 `atIndex`。正向包含由此完成，整个过程没有把某个索引提取成普通数据。

```agda
      (memberOf k g x (fst y) p)
```

反向包含设 `x ∈ # k`。冯·诺伊曼数码的消去表明，在命题截断内，存在一个自然数 `m < k`，使 `x ≡ # m`。这样的 `m` 决定 `Fin k` 中的一个索引。结论本身也是「图中有取值」的命题截断存在，所以 `PT.map` 可以逐一变换数码见证，而无须选择其中一个。假设 `cg` 随后提供把该取值呈现为模型元素所需的可构造性证明。

```agda
  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (fst y) ∈ env g ⟩
  dom-from k g cg x h = PT.map atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∈ ℕ ] ((m < k) × (x ≡ # m))
```

对一个代表 `m < k`，令 `i` 为相应的有穷索引。存在量词的见证是模型元素`(g i , cg i)`，即该索引处的取值及其可构造性证明。图中的事实来自`entryOf`：以标准第一分量 `# (toℕ i)` 为键的有序对是一个条目。把这个第一分量迁移为 `x`，便得到所需的 `pr x (g i)` 属于图。

```agda
              → Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k
```

转换 `fromℕ' k m p` 把界限证明 `p : m < k` 化为索引 `i`。其往返律`toFromId'` 证明 `toℕ i ≡ m`。把 `x ≡ # m` 与这条往返等式之反向在数码下的像复合起来，便得到 `qi : x ≡ # (toℕ i)`；这正是把标准条目搬到所查询第一分量所需的路径。定义域的反向包含至此完成。

```agda
      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))
```

现在可以把这两个集合层面的包含与对象语言的定义域公式对应起来。固定环境`γ`、族 `g : Fin k → V ℓ`，以及等式 `qe`；后者把 `e` 位置的底集认作`env g`，而 `d` 位置仍是候选定义域。每个 `cg i` 都证明 `g i` 是可构造模型的元素，这正是反向包含构造存在见证时所需的条件。在这个语境中，接下来的两个引理分别读出与填充 `domAt e d`。

```agda
module _ {n : ℕ} (e d : Fin n) (γ : S ^ n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : fst (lookup e γ) ≡ env g) where
```

设 `γ` 满足 `domAt e d`。为了证明 `d` 位置的底集就是 `# k`，`domAt-numeral` 对模型元素 `lookup d γ` 与 `(# k , numL k)` 应用 `L` 内部的外延性，再把所得等式投影到底集。因此，只须对每个可构造的测试元素 `x` 证明：属于候选定义域与属于该数码是同一个命题。正向蕴含先用 `domAt-in` 读取定义域隶属。

```agda
  domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → fst (lookup d γ) ≡ # k
  domAt-numeral h = cong fst (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
    where
    fwd : (x : S) → ⟨ fst x ∈ fst (lookup d γ) ⟩ → ⟨ fst x ∈ # k ⟩
    fwd x hx = dom-into k g (fst x)
```

在正向蕴含中，`domAt-in` 把 `d` 位置中的隶属化为如下仅仅存在：某个取值与`x` 配成的对位于 `e` 位置的集合中。沿 `qe` 迁移后，该条目落入 `env g`，`dom-into` 随即给出 `x ∈ # k`。反过来，`dom-from` 把 `x ∈ # k` 化为`env g` 中某个条目的仅仅存在。由于属于候选定义域是命题，可以消去这一截断；局部函数 `put` 处理每个呈现出来的条目。

```agda
      (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe
        (domAt-in e d γ h x hx))
    bwd : (x : S) → ⟨ fst x ∈ # k ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
    bwd x hx = PT.rec (snd (fst x ∈ fst (lookup d γ))) put (dom-from k g cg (fst x) hx)
      where
```

对一个呈现出来的条目，`put` 先沿 `qe` 的反向把其隶属搬回 `e` 位置所存的图，再由 `domAt-out` 得到它的第一分量属于 `d` 位置。于是，两条蕴含经`⇔toPath` 在每个 `x` 处形成两条隶属命题之间的路径；外延性把这些逐点路径组装成候选定义域与 `# k` 的相等。截断的图见证只用于证明隶属，并未从中选择任何取值。

```agda
      put : Σ[ y ∈ S ] ⟨ pr (fst x) (fst y) ∈ env g ⟩ → ⟨ fst x ∈ fst (lookup d γ) ⟩
      put (y , p) = domAt-out e d γ h x y
        (subst (λ u → ⟨ pr (fst x) (fst y) ∈ u ⟩) (sym qe) p)
    pt : (x : S) → (fst x ∈ fst (lookup d γ)) ≡ (fst x ∈ # k)
    pt x = ⇔toPath (fwd x) (bwd x)
```

反向从一条等式开始，它断言 `d` 位置的集合确实是 `# k`。为了证明`domAt e d`，`domAt-intro` 要求对每个元素给出定义域的两条蕴含：图中仅仅存在一个取值蕴含该元素属于 `d`，而属于 `d` 又蕴含图中仅仅存在一个取值。等式 `qe` 与 `qd` 分别把这两项化为 `dom-into` 与 `dom-from`。因此，填充公式使用的仍是读出公式时那两个集合层面的包含，只是方向相反。

```agda
  domAt-fill : fst (lookup d γ) ≡ # k → ⟨ γ ⊨ domAt e d ⟩
  domAt-fill qd = domAt-intro e d γ step
    where
    step : (x : S)
         → (⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩
```

为了填充定义域公式，只须证明逐点的两个蕴含。先设某个取值与 `fst x` 配成的对属于位置 `e` 所存的图。沿 `qe` 搬运后，这个条目属于 `env g`，于是 `dom-into` 证明 `fst x` 属于数码 `# k`。再沿 `qd` 的反向搬运，便得到它属于位置 `d` 所存的候选定义域。

```agda
            → ⟨ fst x ∈ fst (lookup d γ) ⟩)
         × (⟨ fst x ∈ fst (lookup d γ) ⟩
            → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ fst (lookup e γ) ⟩)
    step x =
        (λ hy → subst (λ u → ⟨ fst x ∈ u ⟩) (sym qd) (dom-into k g (fst x)
```

反向蕴含沿同一路径倒行。先用 `qd` 把位置 `d` 中的隶属搬到 `# k` 中；`dom-from` 随后在命题截断内给出一个取值，使它与 `fst x` 配成的对属于 `env g`；最后沿 `qe` 的反向把该条目送回位置 `e`。两个方向由此完成 `domAt-fill`，过程中没有从有穷图中选出一个取值。

```agda
          (subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) qe hy)))
      , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (fst x) (fst y) ∈ u ⟩) (sym qe)
          (dom-from k g cg (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qd hx)))
```

## 满足关系的图所指派的取值

现在考察满足关系图在真实公式键处指派什么。固定周围环境 `γ`：位置 `B` 给出载体，`x` 与 `y` 则给出候选键和候选取值。缩写 `Bs = lookup B γ` 使随后证明对这三个位置保持统一。因此，以下公式的常元由底集 `fst Bs` 的成员索引。

```agda
module _ {n : ℕ} (B x y : Fin n) (γ : S ^ n) where
  private
    Bs : S
    Bs = lookup B γ
```

图公式通过十四个受界位置封装满足关系递归。对模型语言公式 `φ`，`fr φ` 在这些位置依次放入载体 `Bs`、它的典范满足关系表、由子公式键组成的槽、环境塔以及十个构造子标签的数码，随后接上周围环境 `γ`。每个分量都是此前已经为该载体与公式构造好的典范对象。

```agda
    fr : ∀ {m} (φ : Formula S m) → S ^ (14 + n)
    fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

这十个数码并不为码域编制索引，而是标记表规格中从零到九的十条构造子子句。`tgs φ` 记录 `fr φ` 中每个指定的标签位置都含有与其构造子相应的数码。凭借这份对齐，打包后的表公式才能为每种语法形状选中正确子句。

```agda
    tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
    tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ
```

满足关系表还需要为每个元数配备正确的环境族。`htow φ` 把既有的塔定理应用于 `fr φ` 的各分量：塔位置的取值是 `Tower.tower Bs`，载体位置是 `Bs`，零号标签位置则含有所需数码。因此，`towerAt` 在扩展环境中成立，此处无须重新证明关于塔的论证。

```agda
    htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
    htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl
```

典范表的定义域恰是公式键所成的槽。一个方向从表条目出发，用 `inSlot` 证明其键属于 `slot Bs φ`；由于条目是在命题截断下取得的，这次消去落入隶属命题。另一个方向用 `total` 证明槽中的每个键都仅仅存在一个表取值。`domAt-intro` 把这两个蕴含组合成 `hdom φ`。

```agda
    hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
    hdom φ = domAt-intro Ti Ci (fr φ)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot Bs φ)))
                 (λ { (w , hw) → inSlot Bs φ (fst z) (fst w) hw }) h)
           , (λ h → total Bs φ (fst z) h))
```

现在可以准确陈述正向读式。设 `ψ` 的常元取自 `fst Bs` 的成员。若位置 `x` 含有它的真实键 `keyS Bs ψ`，位置 `y` 含有翻译后的模型语言公式 `mapFo (asConst Bs) ψ` 的满足集合，那么 `satGraphAt B x y` 成立。这里的取值是满足该公式的环境所成的集合，并非单个真值。`graphAt-value` 向 `graphAt-in` 提供典范递归见证，从而证明这一结论。

```agda
  graphAt-value : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
                → fst (lookup x γ) ≡ fst (keyS Bs ψ)
                → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
                → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-value {m} ψ qx qy = graphAt-in B x y γ
```

存在见证按 `GraphWitAt` 所需的次序由五个典范分量装配：数码指派 `numν`、塔、槽、满足关系表与载体。随后把整份见证包入命题截断，以配合图公式中存在量词的语义。余下任务是证明这些选定分量满足载体、标签、塔、闭包、定义域、条目与表规格的要求。

```agda
    ∣ numν
    , (Tower.tower Bs
    , (slot Bs φ
    , (satTable Bs φ
    , (Bs
```

载体等式由自反性给出。接下来的三份证明分别断言：十个标签位置含有预定数码，环境位置确实是 `Bs` 上的塔，并且 `slot Bs φ` 对带有直接子公式的构造子闭合。最后一项保证递归表在复合公式键处施用子句时，能够查阅直接子公式键处的表条目。

```agda
    , (refl
    , (tgs φ
    , (htow φ
    , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
```

最后三项要求分别确定表的定义域、选定条目与子句规格。先前证明的 `hdom φ` 给出定义域公式。对表条目，`keyBridge Bs ψ` 关联载体语言公式与 `φ` 的键，而 `qx`、`qy` 把典范条目搬到位置 `x`、`y` 所存的键和值上。最后，`SlotHolds.holds` 从同一载体、标签、塔、槽与表证明该典范表满足 `tableAt`。装配好的见证因而证明图公式成立。

```agda
    , (hdom φ
    , (subst2 (λ u v → ⟨ pr u v ∈ fst (satTable Bs φ) ⟩)
         (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
    , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
    where
```

这里的 `φ` 是 `ψ` 在模型语言中的版本。`ψ` 的一个常元是底层载体的成员；`asConst Bs` 为它配上作为 `S` 中元素所需的可构造性证明，`mapFo` 再把这个常元映射施于整条公式。上文另行使用的 `keyBridge` 保证：翻译前直接编码与翻译后在模型内部编码所得的底层键相同。

```agda
    φ : Formula S m
    φ = mapFo (asConst Bs) ψ
```

反向读式设 `satGraphAt B x y` 成立，且位置 `x` 是 `ψ` 的真实键。`graphAt-out` 只能在命题截断内给出十四个存在分量。所求结论是累积层级 `V` 中的一条相等，而 `setIsSet` 说明这种相等所成的类型是命题。因此，`PT.rec` 可以在局部逐一考察呈现出的图见证，而不从中作全局选择。

```agda
  graphAt-only : ∀ {m} (ψ : Formula ⟪ fst Bs ⟫ m)
               → fst (lookup x γ) ≡ fst (keyS Bs ψ)
               → ⟨ γ ⊨ satGraphAt B x y ⟩
               → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
  graphAt-only {m} ψ qx h = PT.rec (setIsSet _ _) read (graphAt-out B x y γ h)
```

拆开一个图见证，可得候选表 `T`、码域 `C`、环境塔 `E`、载体 `b` 及其全部证明。这里的 `C` 不必是典范槽；关键在于它对子码闭合，`T` 满足打包后的表子句，而且真实键属于 `C`。最后一项由表条目 `ha` 经 `domAt-out` 得到。把这份键隶属与同一个表条目交给 `SatSoundC.pinned`，便可将 `ψ` 在表中记录的取值确定为典范满足集合。

```agda
    where
    read : GraphWitAt B x y γ → fst (lookup y γ) ≡ fst (Sat Bs (mapFo (asConst Bs) ψ))
    read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
      SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
        ψ (subst (λ u → ⟨ u ∈ fst C ⟩) qx
```

钉定定理所需的两个前提起初都在周围环境的位置 `x` 处读取。沿 `qx` 搬运，一方面把由 `hd` 与 `ha` 得到的定义域隶属化为 `keyS Bs ψ` 属于 `C`，另一方面把 `ha` 本身化为 `T` 在该键与位置 `y` 所存取值处的条目。钉定定理随即交回所需相等：在真实公式键处，图所容许的任何取值都等于翻译后公式的满足集合。

```agda
             (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
        (lookup y γ)
        (subst (λ u → ⟨ pr u (fst (lookup y γ)) ∈ fst T ⟩) qx ha)
```

## 名字，描述在诸位上

指称公式体一次检验一个候选元素 `z`。首个合取项 `z ∈ B` 把所描述的集合限制在载体之内。随后公式体绑定环境 `c`，并要求 `c` 是把 `z` 添到参数环境 `e` 前端所得的编码环境。此时 `c` 与 `z` 都位于周遭赋值之前，故对 `e` 的引用须穿过两层绑定。

```agda
DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero
```

其余三个见证决定如何解释骨架。首先要求 `k` 是扩展环境 `c` 的定义域；接着要求 `key` 属于位置 `C` 中的码集，并等于 `k` 与骨架码 `s` 组成的对；最后，`v` 是满足关系图在载体 `B` 与该键处容许的取值，末尾的隶属断言则是 `c ∈ v`。当 `C` 填入载体的真实码集时，这些条件表达的是扩展环境满足骨架，而非仅在任意键处查询图。

```agda
            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )
```

元语言名字由元数、无参公式与参数向量组成。`NameAt` 分别以元数位置 `a`、骨架码位置 `s` 与环境位置 `e` 表示这三项，并以指称位置 `d` 记录由它们导出的集合。第一个合取项检查由 `a` 的后继与 `s` 组成的对是否属于空字母表码集。这里的后继不可省略：具有 `a` 个参数的名字还需要一个变元来放置候选成员。下一个合取项要求 `a` 属于模型的自然数之集。

```agda
NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)
```

第三个合取项要求 `e` 是定义域恰为 `a`、取值落在 `B` 中的环境，从而把参数向量与前一位置记录的元数联系起来。最后一个合取项以外延方式刻画 `d`：对每个候选元素，属于 `d` 当且仅当它满足 `DenoteBody`，而该公式体的首项已经把候选元素限制在 `B` 中。因此，`d` 是由名字的三项数据导出的，并非元语言名字额外存储的分量。

```agda
    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )
```

`DenoteOf z` 是与 `DenoteBody` 四层存在量词相应的元语言载荷。它记录扩展环境 `c`、其候选定义域 `k`、一个公式键和图取值 `v`，并带上联系这些对象的全部条件。把这些数据放进一个依值元组，既显露出装配对象语言公式所需的见证，也保留了后续条件对先前选择的依赖。

```agda
module _ {n : ℕ} (B C s e : Fin n) (γ : S ^ n) where
  DenoteOf : (z : S) → Type (ℓ-suc ℓ)
  DenoteOf z = Σ[ c ∈ S ] Σ[ k ∈ S ] Σ[ key ∈ S ] Σ[ v ∈ S ]
    ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
    × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩
```

这份载荷严格沿着语义链展开。前两份满足证明分别断言 `c` 扩展旧环境，以及 `k` 是它的定义域。当 `C` 实例化为 `AllCodes B` 时，`key` 对 `C` 的隶属保证随后是在真实公式码处查询图。接着的显式等式把该键确定为 `k` 与 `s` 组成的对。末两份证明则断言 `v` 是图在该键处的取值，并且 `c` 属于 `v`。这里的 `v` 是满足该公式的环境之集，并非布尔真值。

```agda
      × ( ⟨ fst key ∈ fst (lookup C γ) ⟩
        × ( (fst key ≡ pr (fst k) (fst (lookup s γ)))
          × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
            × ⟨ fst c ∈ fst v ⟩ ) ) ) ) )
```

`DenoteBody-in` 把这份显式载荷变成对公式体的满足。载体隶属保留为最外层合取项，而见证 `c`、`k`、`key` 与 `v` 按四层存在绑定的同一次序引入。多数条件本来就以满足证明陈述。例外是定义 `key` 的等式：配对公式的充分性路径把这条集合论等式转换为对 `prAtL` 的满足。

```agda
  DenoteBody-in : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf z
                → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
  DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
    = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
    , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp
```

对象语言的每个存在量词都以命题截断解释，因此构造在结束证明前把四个见证逐层包入截断。最后一行从图取值向外直至扩展环境，依次闭合这四层。所得满足因而只记录适当数据存在；未截断的见证只保留在用来构造它的输入 `DenoteOf z` 中。

```agda
      , ∣ v , (hg , hm) ∣₁ )) ∣₁) ∣₁) ∣₁
```

`DenoteBody-out` 在反向读取时保留同一边界。载体隶属位于所有存在量词之外，因此可以直接取得；四个见证则只能在嵌套的命题截断中显露。每次截断消去的目标都是 `∥ DenoteOf z ∥₁`，仍为一个命题，故证明可以变换每一份局部见证，却不会从中全局选出一个元组。

```agda
  DenoteBody-out : (z : S) → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
                 → ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf z ∥₁
  DenoteBody-out z (hz , hc) = hz , PT.rec squash₁
    (λ { (c , (hc , hk)) → PT.rec squash₁
      (λ { (k , (hk , hkey)) → PT.rec squash₁
```

在键这一层，公式体给出对配对公式的满足，而 `DenoteOf` 要求解码后的等式 `fst key ≡ pr (fst k) (fst (lookup s γ))`。沿配对公式的充分性路径正向读取，恰好得到这条等式。最内层的映射随后把图证明与隶属证明连同见证 `v` 一并保留，外围的消去再于一层命题截断之下重建整份载荷。

```agda
        (λ { (key , (hi , (hp , hv))) → PT.map
          (λ { (v , (hg , hm)) → c , (k , (key , (v , (hc , (hk , (hi
            , ( subst ⟨_⟩
                  (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ)) hp
              , (hg , hm) ))))))) }) hv }) hkey }) hk }) hc
```

`NameAt-in` 接受五份输入。前三份建立固定的合取项：骨架在给定元数处为无参公式，元数属于模型的自然数之集，参数图是载体上的环境。余下两份输入给出刻画指称所需的逐点双向蕴含。第一向从 `z ∈ d` 得到 `z ∈ B` 与一份显式的 `DenoteOf z`；反向则把 `z ∈ B` 和一份显式的 `DenoteOf z` 变成 `z ∈ d`。

```agda
module _ {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n) where
  NameAt-in : ⟨ γ ⊨ FreeAt C₀ s a ⟩
            → ⟨ fst (lookup a γ) ∈ ω ⟩
            → ⟨ γ ⊨ envOverAt e a B ⟩
            → ((z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
```

两个方向都对每个候选元素分别陈述，因为 `extAt` 通过逐点隶属表达集合相等。它们有意使用未截断的 `DenoteOf z`：本引理是一条引入规则，调用方要提供可用来构造公式体满足的具体数据。从 `NameAt` 的任意满足中恢复这些数据属于另一项充分性论证；下一章给出的恢复结果仍保留在命题截断之下。

```agda
               → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z)
            → ((z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
               → ⟨ fst z ∈ fst (lookup d γ) ⟩)
            → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
  NameAt-in hf ha he into back =
```

证明把这两个方向交给 `extAt` 的引入规则。由 `z ∈ d`，第一向给出载体隶属与载荷，`DenoteBody-in` 再把它们转换为对公式体的满足。反过来，`DenoteBody-out` 把公式体的满足读成载体隶属与经过命题截断的载荷。由于目标 `z ∈ d` 是命题，可以消去该截断并应用第二份输入。把所得外延刻画与前三份输入组合起来，便得到整条名字公式的满足。

```agda
    hf , (ha , (he , extAt-in-both d (DenoteBody B C s e) γ
      (λ z hz → DenoteBody-in B C s e γ z (into z hz .fst) (into z hz .snd))
      (λ z h → PT.rec (snd (fst z ∈ fst (lookup d γ)))
                 (back z (DenoteBody-out B C s e γ z h .fst))
                 (DenoteBody-out B C s e γ z h .snd))))
```

## 那个序，不跑自己的递归

随后的比较公式成组绑定数据，因此对周遭赋值的引用须作统一移位。`sh3` 把一个周遭位置移过三层新绑定。在 `LexAt` 中，这三层分别存放序号 `i` 以及两个参数环境在 `i` 处的取值，使原有的两个环境位置与参数序位置仍可引用。稍后的 `LeastNameAt` 也使用同一移位，把周遭位置移过一个竞争名字的骨架、元数与环境。

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

`sh6` 相应地把引用移过六层绑定。`StepBody` 绑定两个名字时会使用它，每个名字都由骨架、元数与参数环境表示。完全扩展后的赋值因而把六个新取值置于原赋值之前，而载体、两个序关系、两个码集以及待比较的两个指称仍保留为周遭位置。这些移位只保持引用所指，不增添任何序假设，也不亲自执行比较。

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

参数键要找两个参数环境首次相异的位置。`LexAt` 先绑定元数位置所持集合的一个成员 `i`。当该位置存放一个元数的数码时，它的成员恰是各个更小位置的数码；因此，这个有界存在量词已经遍历全部可能的序号，无须另行引入序号之序。

```agda
LexAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
LexAt P a e₁ e₂ =
  ∃̇∈ (var a) (
    ∃̇ ( ∃̇ ( appAt (sh3 e₁) (suc (suc zero)) (suc zero)
           ∧̇ ( appAt (sh3 e₂) (suc (suc zero)) zero
```

选定 `i` 后，两层存在量词给出取值 `u` 与 `v`，使 `e₁(i)=u`、`e₂(i)=v`；第三次应用则断言 `u` 与 `v` 组成的有序对属于参数关系 `P`。随后的有界全称量词考察每个 `j ∈ i`，并对每个这样的 `j` 要求仅仅存在一个取值 `x`，使两张环境图在 `j` 处都取到 `x`。所以整条公式说的是「此处严格有序，而每个更早位置都有共同取值」。只有把两个环境认作单值图之后，共同取值才蕴涵相应参数相等；后面的充分性论证正是用图的查表性质与载体嵌入的单射性得到这一步。公式本身不执行递归。

```agda
             ∧̇ ( appAt (sh3 P) (suc zero) zero
               ∧̇ ∀̇∈ (var (suc (suc zero))) (
                    ∃̇ ( appAt (sh5 e₁) (suc zero) zero
                      ∧̇ appAt (sh5 e₂) (suc zero) zero ) ) ) ) ) ) )
```

完整的名字比较现在按字典序的优先次序组合三个键：骨架码、元数与参数环境。第一个析取支把关系位置 `R` 应用于 `s₁` 与 `s₂`。由取值公式的充分性，这表示两个骨架码组成的有序对属于 `R`。把 `R` 保留为一个位置，使同一条公式可以通用于不同赋值；后面的充分性定理会在这里填入表示极限层码序的关系。

```agda
≺At : ∀ {n} → Fin n → Fin n
    → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Formula S n
≺At R P s₁ a₁ e₁ s₂ a₂ e₂ =
      appAt R s₁ s₂
  ∨̇ ( (var s₂ ≐ var s₁)
```

第二个析取支处理骨架码相等的情形。它先按 `s₂ = s₁` 的方向记录等式，再给出余下两个字典序分支：若两个元数位置都存放数码，则 `a₁ ∈ a₂` 表示第一元数更小；另一分支要求 `a₂ = a₁`，再由 `LexAt P a₁ e₁ e₂` 在参数首次相异处决定次序。`s₂ = s₁` 与 `a₂ = a₁` 的方向正好配合后面的迁移，把第二个名字的码与参数向量移到第一个名字的数据上。

```agda
    ∧̇ ( (var a₁ ∈̇ var a₂)
      ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) )
```

为了给 `LexAt` 证明一条可复用的读式，先单独命名相符存在量词之下的公式体。在先前位置 `j` 处，`Body` 要求同一个取值 `x` 满足两次应用，也就是让两张环境图在 `j` 处都含有取值 `x`。扩张赋值中新添的五项依次是 `x`、`j`、`v`、`u`、`i`，所以对周遭环境位置的引用都须穿过五层绑定。

```agda
module _ {n : ℕ} (P a e₁ e₂ : Fin n) (γ : S ^ n) where
  private
    Body : Formula S (suc (suc (suc (suc (suc n)))))
    Body = appAt (sh5 e₁) (suc zero) zero ∧̇ appAt (sh5 e₂) (suc zero) zero
```

固定 `i`、`u`、`v` 后，`Inner i u v` 记录前三层存在绑定之后剩下的公式体。前两个分量说图 `e₁` 与 `e₂` 分别含有对 `(i,u)` 与 `(i,v)`；第三个分量说对 `(u,v)` 属于关系 `P`。这些分量仍是关于 `appAt` 的满足关系陈述；稍后另行记录它们解码后的隶属形态，便可显式联系这两种呈现。

```agda
    Inner : (i u v : S) → Type (ℓ-suc ℓ)
    Inner i u v =
      ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₁) (suc (suc zero)) (suc zero) ⟩
      × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 e₂) (suc (suc zero)) zero ⟩
        × ( ⟨ (v ∷ u ∷ i ∷ γ) ⊨ appAt (sh3 P) (suc zero) zero ⟩
```

`Inner` 的第四个分量是在 `i` 之下相符。对每个属于 `i` 的模型元素 `j`，它给出语义存在式 `∃[ x ∶ S ]`，断言某个 `x` 满足 `Body`。这个存在式是命题截断：它保留「在 `j` 处有共同取值」这一事实，却不把选定的取值作为数据暴露出来。因此，有界全称量词被读成一个函数，为每个 `j ∈ i` 给出这样一份经过命题截断的存在。

```agda
          × ((j : S) → ⟨ fst j ∈ fst i ⟩
             → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩) ) )
```

`Agrees i` 以两次应用解码后的形态陈述同一项相符：对每个 `j ∈ i`，仅仅存在一个元素 `x : S`，使 `j` 与 `x` 的底集组成的对同时属于图 `e₁` 与 `e₂`。当 `i` 是元数的数码时，它的成员恰好表示所有更早位置。这个定义只记录共同的图取值；相应元层参数的相等要到后面才从已知的环境图与载体嵌入的单射性导出。

```agda
  Agrees : (i : S) → Type (ℓ-suc ℓ)
  Agrees i = (j : S) → ⟨ fst j ∈ fst i ⟩
           → ∥ Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                          × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ ) ∥₁
```

`Differs` 汇集首次相异见证的完整解码形态。它包含序号 `i`、取值 `u` 与 `v`、`i` 对元数位置所持集合的隶属、对 `(i,u)` 与 `(i,v)` 的两份图隶属、该位置上的严格参数比较，以及 `Agrees i`。当元数位置存放数码，且两个图位置存放该元数的参数环境时，这些字段恰好组成字典序首次相异所需的数据。

```agda
  Differs : Type (ℓ-suc ℓ)
  Differs = Σ[ i ∈ S ] Σ[ u ∈ S ] Σ[ v ∈ S ]
    ( ⟨ fst i ∈ fst (lookup a γ) ⟩
    × ( ⟨ pr (fst i) (fst u) ∈ fst (lookup e₁ γ) ⟩
      × ( ⟨ pr (fst i) (fst v) ∈ fst (lookup e₂ γ) ⟩
```

严格比较字段与 `≺At` 的码分支采用相同的关系形态：`u` 与 `v` 的底层值组成的有序对属于位置 `P` 所持的集合。末尾的 `Agrees i` 记录每个更早位置上的共同取值；对预期的单值环境图而言，这便保证更早参数没有相异。因此，`Differs` 把首次相异见证的数学内容与表达它的对象语言绑定结构分开记录。

```agda
        × ( ⟨ pr (fst u) (fst v) ∈ fst (lookup P γ) ⟩ × Agrees i ) ) ) )
```

映射 `pack` 只把 `Inner` 的相符分量转换为 `Agrees`，前三个分量与这次局部转换无关。固定 `j ∈ i` 后，语义存在式的一个见证 `x` 带有两份对 `appAt` 的满足证明。分别应用 `appAt-adequate`，即可把它们变成 `Agrees` 所需的两份图隶属，同时保持同一个见证 `x`。

```agda
  private
    pack : (i u v : S) → Inner i u v → Agrees i
    pack i u v (_ , (_ , (_ , hj))) j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
         , ( subst ⟨_⟩
```

这次转换在已有的命题截断之内完成。`PT.map` 把每个可能的见证及其两份应用证明，映成同一个见证及其两份隶属证明。由于目标仍是经过命题截断的存在，过程中既不取出任何代表，也不使用选择原理。逐点映射便足以对每个更早位置得到 `Agrees i` 所需的结论。

```agda
               (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₁
           , subst ⟨_⟩
               (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ)) p₂ ) })
      (hj j hj')
```

`unpack` 给出满足原公式所需的反向转换。由 `Agrees i` 与一个位置 `j ∈ i`，它取得一份经过命题截断的共同取值见证。对其中每个可能的代表 `x`，它保留该见证，并把两份图隶属转换回 `Body` 中两次应用的满足证明。

```agda
    unpack : (i u v : S) → Agrees i
           → (j : S) → ⟨ fst j ∈ fst i ⟩
           → ⟨ ∃[ x ∶ S ] (x ∷ j ∷ v ∷ u ∷ i ∷ γ) ⊨ Body ⟩
    unpack i u v hj j hj' = PT.map
      (λ { (x , (p₁ , p₂)) → x
```

这里沿反方向使用同一些充分性路径。每份隶属证明都沿 `appAt-adequate` 的对称路径迁移，从而得到 `Body` 中相应的合取项。`PT.map` 再次使整个构造留在经过命题截断的存在之内，所以 `unpack` 无须在全局选定共同取值，便能证明所需的语义存在。

```agda
         , ( subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₁) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₁
           , subst ⟨_⟩
               (sym (appAt-adequate (sh5 e₂) (suc zero) zero (x ∷ j ∷ v ∷ u ∷ i ∷ γ))) p₂ ) })
      (hj j hj')
```

`LexAt-in` 从 `Differs` 中的明确数据出发。序号 `i` 与取值 `u`、`v` 分别成为有界存在量词及随后两层存在量词的见证，`hi` 则证明 `i` 确实落在界内。在扩张赋值 `γ₃ = v ∷ u ∷ i ∷ γ` 中，前两份图隶属沿 `appAt-adequate` 反向迁移，得到对 `e₁(i)=u` 与 `e₂(i)=v` 两次应用的满足证明。关系字段与相符字段随后进入同一个合取结构，其中有界全称分量由 `unpack` 给出。

```agda
  LexAt-in : Differs → ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩
  LexAt-in (i , (u , (v , (hi , (h₁ , (h₂ , (hp , hj)))))))
    = ∣ i , (hi , ∣ u , ∣ v
    , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) γ₃)) h₁
      , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 e₂) (suc (suc zero)) zero γ₃)) h₂
```

`Differs` 的最后两个字段完成引入证明。对 `(u,v)` 属于 `P` 的证明沿`appAt-adequate` 反向迁移，成为对第三次应用的满足关系证明；`unpack` 则把`i` 以下的相符变成有界全称量词所需的语义形态。赋值`γ₃ = v ∷ u ∷ i ∷ γ` 明确记录三层绑定的次序，外围的构造子再由内向外依次闭合 `v`、`u` 与 `i` 的存在量词。

```agda
        , ( subst ⟨_⟩ (sym (appAt-adequate (sh3 P) (suc zero) zero γ₃)) hp
          , unpack i u v hj ) ) ) ∣₁ ∣₁) ∣₁
    where
    γ₃ : S ^ (suc (suc (suc n)))
    γ₃ = v ∷ u ∷ i ∷ γ
```

从 `LexAt` 向外读取时，必须保留其存在量词所设下的见证边界。因此，`LexAt-out` 的目标是命题 `∥ Differs ∥₁`，并且只把外层截断消去到这个目标中。局部函数 `atValue` 承担实际的数学解码：一旦在各次消去的局部范围内取得具体的`i`、`u`、`v`、界限证明和余下的满足关系数据，它便构造一份未截断的`Differs` 记录。这样的记录不会被选出到这些局部范围之外。

```agda
  LexAt-out : ⟨ γ ⊨ LexAt P a e₁ e₂ ⟩ → ∥ Differs ∥₁
  LexAt-out = PT.rec squash₁ atIndex
    where
    atValue : (i u v : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩ → Inner i u v → Differs
    atValue i u v hi h@(h₁ , (h₂ , (hp , _))) = i , (u , (v
```

`atValue` 的前半段恢复序号与两次图查取。界限证明 `hi` 已经具有 `Differs`要求的形态。正向读取两条充分性路径，便把两次应用的满足关系分别变成`(i,u)` 对 `e₁` 的隶属，以及 `(i,v)` 对 `e₂` 的隶属。因此，两个取值仍与公式找到它们时的同一个序号相联系。

```agda
      , ( hi
        , ( subst ⟨_⟩
              (appAt-adequate (sh3 e₁) (suc (suc zero)) (suc zero) (v ∷ u ∷ i ∷ γ)) h₁
          , ( subst ⟨_⟩
                (appAt-adequate (sh3 e₂) (suc (suc zero)) zero (v ∷ u ∷ i ∷ γ)) h₂
```

第三次应用以同样方式解码，得到 `(u,v)` 对参数关系 `P` 的隶属。函数 `pack`把有界范围内以应用陈述的相符翻译成 `Agrees i` 所要求的两份图隶属，从而给出最后一个字段。这些数据在 `atValue` 内组成一份明确的 `Differs` 记录；外围的各次消去最终只保留它的命题截断。

```agda
            , ( subst ⟨_⟩
                  (appAt-adequate (sh3 P) (suc zero) zero (v ∷ u ∷ i ∷ γ)) hp
              , pack i u v h ) ) ) ) ))
```

最内层存在量词给出第二个取值 `v` 及 `Inner i u v`，但二者只在该存在量词的截断内部可用。处理函数 `atSecond` 对每一份局部可用的 `(v,h)` 调用 `atValue`构造 `Differs`，并立即把结果放入 `∥ Differs ∥₁`。这正是命题截断所容许的消去：见证被用于证明一个命题，却不会由结果暴露出来。

```agda
    atSecond : (i u : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
             → Σ[ v ∈ S ] Inner i u v → ∥ Differs ∥₁
    atSecond i u hi (v , h) = ∣ atValue i u v hi h ∣₁
```

向外一层，`atFirst` 取得具体的第一个取值 `u`，以及第二个取值之存在的截断。它用 `atSecond` 消去这层内部截断，而 `atSecond` 的结果仍是`∥ Differs ∥₁`。所以论证可以从第一个取值走到完整的首次相异记录，而始终无须取得一个全局可用的 `v`。

```agda
    atFirst : (i : S) → ⟨ fst i ∈ fst (lookup a γ) ⟩
            → Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ → ∥ Differs ∥₁
    atFirst i hi (u , h) = PT.rec squash₁ (atSecond i u hi) h
```

最后，`atIndex` 取得序号 `i`、证明它低于元数的 `hi`，以及从 `u` 开始的余项之截断。用 `atFirst` 消去这份余项，就完成了向外读取。三个处理函数合起来依`i`、`u`、`v` 的次序跟随存在量词的嵌套，而每次消去都有同一个命题目标。因此，`LexAt-out` 只证明首次相异记录仅仅存在，并未选择其中的序号或取值。

```agda
    atIndex : Σ[ i ∈ S ] ( ⟨ fst i ∈ fst (lookup a γ) ⟩
                         × ∥ Σ[ u ∈ S ] ∥ Σ[ v ∈ S ] Inner i u v ∥₁ ∥₁ )
            → ∥ Differs ∥₁
    atIndex (i , (hi , h)) = PT.rec squash₁ (atFirst i hi) h
```

## 读那次比较，以及族的一步

元语言载荷 `Below` 依照 `≺At` 的同一优先次序排列三个比较键。最外层的和类型表示：或者骨架码组成的有序对 `(s₁,s₂)` 属于位置 `R` 中的关系，或者两码相等，由后面的键决定。这个和类型的一个元素会明确指出所取分支并携带相应证据；定义本身并未断言对任意位置取值都能判定应取哪一支。这一区别很要紧，因为对象语言析取的语义带有命题截断。

```agda
module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) where
  Below : Type (ℓ-suc ℓ)
  Below = ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ fst (lookup R γ) ⟩
        ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          × ( ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

在骨架码相等的前提下，内层和类型首先给出元数比较 `a₁ ∈ a₂`。当这两个位置存放元数的数码时，这条隶属表示第一元数较小。若两元数转而相等，则由`Differs` 给出参数键的首次相异证据。两条等式特意取 `s₂ = s₁` 与`a₂ = a₁` 的方向，以配合后文把第二个名字的数据迁移到第一个名字的类型中。

```agda
            ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
              × Differs P a₁ e₁ e₂ γ ) ) )
```

`≺At-in` 把一份明确的 `Below` 数据翻译成对比较公式的满足关系。在码分支中，关系隶属沿 `appAt-adequate` 反向迁移，并作为最外层的左析取支引入。在元数分支中，码等式随最外层右析取支进入，而元数隶属进入内层左析取支。这里所做的全是引入：已给出的分支证据被包装进各对象语言析取带命题截断的语义中。

```agda
  ≺At-in : Below → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
  ≺At-in (inl h) =
    ∣ inl (subst ⟨_⟩ (sym (appAt-adequate R s₁ s₂ γ)) h) ∣₁
  ≺At-in (inr (q , inl h)) = ∣ inr (q , ∣ inl h ∣₁) ∣₁
  ≺At-in (inr (q , inr (q' , h))) =
```

参数分支沿两层析取各自的右支进入。它把码等式与元数等式带入相应的右支，再把给定的 `Differs` 记录交给 `LexAt-in`。于是，前文已经解码的首次相异数据便成为参数子句的满足关系。这样，`Below` 的三个情形都能直接引入 `≺At`，无需搜索分支，也无需从存在量词中取出见证。

```agda
    ∣ inr (q , ∣ inr (q' , LexAt-in P a₁ e₁ e₂ γ h) ∣₁) ∣₁
```

反向读式的目标必然较弱：`≺At-out` 返回 `∥ Below ∥₁`。最外层对象语言析取的满足关系本身带有截断，所以 `PT.rec` 只能在构造这个命题时局部查看其分支。局部函数 `outer` 把码分支与码相等分支分开；在后一情形中，它保留等式`s₂ = s₁`，并把尚未归类的内层析取交给 `inner`。

```agda
  ≺At-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ Below ∥₁
  ≺At-out = PT.rec squash₁ outer
    where
    inner : (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
          → ⟨ fst (lookup a₁ γ) ∈ fst (lookup a₂ γ) ⟩
```

在给定码等式后，`inner` 读取余下两个键。若取得元数隶属，便立即得到 `Below`的中间情形；否则，载荷包含元数等式 `a₂ = a₁` 以及对 `LexAt` 的满足关系，只剩首次相异分量尚待解码。函数签名把这两个选项明确列出，同时固定二者共同使用的码等式。

```agda
          ⊎ ( (fst (lookup a₂ γ) ≡ fst (lookup a₁ γ))
            × ⟨ γ ⊨ LexAt P a₁ e₁ e₂ ⟩ )
          → ∥ Below ∥₁
    inner q (inl h) = ∣ inr (q , inl h) ∣₁
    inner q (inr (q' , h)) =
```

在参数分支中，`LexAt-out` 只给出 `∥ Differs ∥₁`，恰好保留存在语义所要求的边界。`PT.map` 把其中每一份局部出现的 `Differs` 记录映到 `Below` 的第三种情形，并附上已经取得的码等式与元数等式。结果仍处于一层命题截断之下，因此这次转换只是把存在带到存在，从不要求选定一份首次相异见证。

```agda
      PT.map (λ u → inr (q , inr (q' , u))) (LexAt-out P a₁ e₁ e₂ γ h)
```

`outer` 的类型正是第一个比较键处的语义分支。左侧是关系 `R` 对两个骨架位置之应用的满足关系；右侧则保留等式 `s₂ = s₁`，并带有余下「元数或参数」析取的满足关系。解码左侧便得到 `Below` 的码分支，消去内层析取则调用 `inner`。这两阶段读取与 `≺At` 的嵌套结构相互对应，并始终把最终结果留在 `∥ Below ∥₁` 中，不把任何一层析取变成被选定的分支。

```agda
    outer : ⟨ γ ⊨ appAt R s₁ s₂ ⟩
          ⊎ ( (fst (lookup s₂ γ) ≡ fst (lookup s₁ γ))
            × ⟨ γ ⊨ ( (var a₁ ∈̇ var a₂)
                    ∨̇ ( (var a₂ ≐ var a₁) ∧̇ LexAt P a₁ e₁ e₂ ) ) ⟩ )
          → ∥ Below ∥₁
```

最后两个分支完成对比较的向外读取。在码分支中，`appAt-adequate` 把关系应用的满足关系转换成「两个骨架码组成的有序对属于 `R`」，从而得到 `Below` 的第一种情形。在码相等的分支中，内层对象语言析取仍处于命题截断之下，因此只能将它消去到 `∥ Below ∥₁` 中。这样，三个比较键中的任一情形都能被读回，但在截断之外，公式不会显露究竟是哪一个键决定了比较。

```agda
    outer (inl h) = ∣ inl (subst ⟨_⟩ (appAt-adequate R s₁ s₂ γ) h) ∣₁
    outer (inr (q , h)) = PT.rec squash₁ (inner q) h
```

为了描述两个最小名字之间的比较，步进的公式体需要六个新槽位。这里先固定前三个索引：`s6a`、`a6a` 与 `e6a` 分别指向第一个名字的骨架码、元数数码与参数环境。进入全部六层绑定以后，这三项数据位于 de Bruijn 的第五、第四与第三位。为这些位置命名，使后面的最小性公式和比较公式保持可读，也把绑定位置的计算集中在一处。

```agda
private
  s6a a6a e6a s6b a6b e6b : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n))))))
  s6a = suc (suc (suc (suc (suc zero))))
  a6a = suc (suc (suc (suc zero)))
  e6a = suc (suc (suc zero))
```

余下的索引 `s6b`、`a6b` 与 `e6b` 指向第二、第一与第零位，第二个名字的数据将落在这里。这种反转来自 de Bruijn 表示的通常规律：见证按 `s₁,a₁,e₁,s₂,a₂,e₂` 的次序绑定，而每个新见证都添加在环境的最前端。因此，完全扩张后的环境是 `e₂ ∷ a₂ ∷ s₂ ∷ e₁ ∷ a₁ ∷ s₁ ∷ γ`，六个索引恰好分别选中预定的两个三元组。

```agda
  s6b = suc (suc zero)
  a6b = suc zero
  e6b = zero
```

最小名字被表达为已经占据 `s`、`a` 与 `e` 三个槽位的一组名字数据所具有的性质。第一个合取项要求这组数据满足 `NameAt`，因而指称 `d`。第二个合取项全称量化一个竞争者的骨架码、元数数码与参数环境。三层全称量词把该竞争者放在第二、第一与第零位，而 `sh3` 使载体、两个码集以及指称 `d` 仍指向原来的槽位。

```agda
LeastNameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n
            → Fin n → Fin n → Fin n → Fin n → Formula S n
LeastNameAt R P B C C₀ s a e d =
  NameAt B C C₀ s a e d
  ∧̇ ∀̇ (∀̇ (∀̇ ( NameAt (sh3 B) (sh3 C) (sh3 C₀)
```

蕴涵的前件把范围限制在同样指称 `d` 的竞争名字上；指称其他集合的名字与这里的最小性无关。其后件否定 `≺At competitor current`，所以 `d` 的任何竞争名字都不会在三键序中严格先于当前名字。这个公式只陈述最小性，既不搜索名字，也不通过消去命题截断来选出名字。明确的最小名字构造属于元语言中的命名理论，并使用其中的排中律假设。

```agda
                      (suc (suc zero)) (suc zero) zero (sh3 d)
             ⇒̇ ¬̇ (≺At (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                        (sh3 s) (sh3 a) (sh3 e)) )))
```

反复消去存在量词时，需要改变见证所携带的性质，却不能在全局选出这个见证。辅助函数 `exists-map` 恰好概括这一操作。若每个 `B x` 都仅仅给出一个 `C x`，那么 `(x , B x)` 的仅仅存在便推出 `(x , C x)` 的仅仅存在。外层 `PT.rec` 把原来的命题截断消去到另一个命题截断类型中，内层 `PT.map` 则保留同一个 `x`，同时改造其第二分量。整个结果始终不会暴露 `A` 中的某个特定见证。

```agda
private
  exists-map : {A : Type (ℓ-suc ℓ)} {B C : A → Type (ℓ-suc ℓ)}
             → ((x : A) → B x → ∥ C x ∥₁)
             → ∥ Σ A B ∥₁ → ∥ Σ A C ∥₁
  exists-map f = PT.rec squash₁ (λ { (x , h) → PT.map (x ,_) (f x h) })
```

算子 `∃₆` 在任意公式体外依次绑定六个对象语言变元。它将用于提供两个名字所需的两组三元数据，但算子本身并不提及名字、最小性或序。把这层绑定框架单独定义，就能对任何多出六个自由位置的公式统一给出语义上的引入与消去读法；见证必须满足的数学条件随后由 `StepBody` 提供。

```agda
∃₆ : ∀ {n} → Formula S (suc (suc (suc (suc (suc (suc n)))))) → Formula S n
∃₆ φ = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ φ)))))
```

给定公式体 `φ` 与环境 `γ`，`Six` 记录能够引入六层存在量词的未截断数据：六个见证 `s₁,k₁,p₁,s₂,k₂,p₂`，以及 `φ` 的满足关系。字母 `k` 与 `p` 预示它们稍后将分别充当元数数码和参数环境；在这个通用定义中，它们还只是载体 `S` 的元素。由于每层绑定都把新见证添加到环境前端，满足关系所用的环境以相反次序列出它们，即在原环境 `γ` 前依次放置 `p₂,k₂,s₂,p₁,k₁,s₁`。

```agda
module _ {n : ℕ} (φ : Formula S (suc (suc (suc (suc (suc (suc n))))))) (γ : S ^ n)
         where
  Six : Type (ℓ-suc ℓ)
  Six = Σ[ s₁ ∈ S ] Σ[ k₁ ∈ S ] Σ[ p₁ ∈ S ] Σ[ s₂ ∈ S ] Σ[ k₂ ∈ S ] Σ[ p₂ ∈ S ]
          ⟨ (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) ⊨ φ ⟩
```

引入读法从 `Six` 的一个值出发，其中六个见证都已明确给出。它依绑定次序把这些见证交给六层存在量词，并逐层将余下的满足关系证明放入相应存在量词带来的命题截断中。这里不需要搜索或选择，因为见证本来就是输入数据。嵌套的构造子也说明了为何公式体所见的环境具有 `Six` 定义中记录的反向次序。

```agda
  ∃₆-in : Six → ⟨ γ ⊨ ∃₆ φ ⟩
  ∃₆-in (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , h)))))) =
    ∣ s₁ , ∣ k₁ , ∣ p₁ , ∣ s₂ , ∣ k₂ , ∣ p₂ , h ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁
```

向外读式从六重存在公式的满足关系出发，其终点必须是 `∥ Six ∥₁`，而不能是暴露在截断之外的六元组。每次调用 `exists-map` 都跨过一层存在量词，并把该层局部可用的见证保留在共同的命题目标中。这条链依次处理 `s₁`、`k₁`、`p₁`、`s₂` 与 `k₂`；到最内层时，`PT.map` 把由 `p₂` 与公式体满足关系证明组成的那一对送入同一个最终截断载荷。

```agda
  ∃₆-out : ⟨ γ ⊨ ∃₆ φ ⟩ → ∥ Six ∥₁
  ∃₆-out = exists-map (λ s₁ →
    exists-map (λ k₁ →
      exists-map (λ p₁ →
        exists-map (λ s₂ →
```

第五次应用 `exists-map` 之后，最内层存在量词已经具有最后一个分量所需的形状，因此恒等映射便已足够。`∃₆-in` 与 `∃₆-out` 合起来，以正确的不对称方式刻画这层绑定框架的语义内容：包含六个明确见证的数据可以引入公式，而从公式的满足关系向外读取时，只能得到这种数据的仅仅存在。下面可把这一通用结论用于具体公式体，无须重新打开任何一层截断。

```agda
          exists-map (λ k₂ → PT.map (λ p → p))))))
```

具体的公式体对六个索引选出的两组三元数据施加三个条件。第一组三元数据必须满足关于 `x` 的 `LeastNameAt`，第二组必须满足关于 `y` 的 `LeastNameAt`。两者使用同一个载体与同一对码集，而 `R` 和 `P` 提供名字比较所需的两个关系槽位。公式体要越过六个新绑定的见证读取外围七个槽位，因此这些槽位都经 `sh6` 移位。

```agda
StepBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
         → Formula S (suc (suc (suc (suc (suc (suc n))))))
StepBody R P B C C₀ x y =
    LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6a a6a e6a (sh6 x)
  ∧̇ ( LeastNameAt (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀) s6b a6b e6b (sh6 y)
```

第三个条件用 `≺At` 比较两组三元数据，使 `x` 的名字在三键名字序中严格先于 `y` 的名字。因此，`StepBody` 所说的恰是：在同一个载体上已经给出两个最小名字，且第一个先于第二个。它不比较 `x` 与 `y` 的诞生层，不包含外层递归表，也不主张所表示的关系具有良基性；这些内容属于使用这条单步描述的更大构造。

```agda
    ∧̇ ≺At (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b )
```

`StepAt` 用六层存在量词封闭 `StepBody`。作为一条对象语言公式，它断言的只是：存在 `x` 的一个最小名字的数据、`y` 的一个最小名字的数据，以及使前者先于后者的比较。公式描述这一种比较情形；它本身不产生任何一个最小名字，不执行外围的层递归，也不证明良基性。存在量词的语义还意味着，从一个已满足的 `StepAt` 向外读取时必须保留命题截断。

```agda
StepAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
StepAt R P B C C₀ x y = ∃₆ (StepBody R P B C C₀ x y)
```

固定各槽位与环境以后，`StepOf` 把通用类型 `Six` 特化到 `StepBody`。因此，它的一个元素包含六个明确的载体元素，以及一份证明，说明它们在反向扩张的环境中满足两个最小名字条件与名字比较。为这份未截断载荷取名，也把它同 `StepAt` 所表达的命题区分开来：随后的引入读法可以直接使用一个 `StepOf`，而向外读式只能返回 `∥ StepOf ∥₁`。这正是六重绑定步进公式的见证边界。

```agda
module _ {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n) where
  StepOf : Type (ℓ-suc ℓ)
  StepOf = Six (StepBody R P B C C₀ x y) γ
```

`StepOf` 已经给出六个见证以及公式体的证明，因此引入方向可以直接完成。各见证依绑定次序放入相应的存在量词之下，所得赋值便满足 `StepAt`。这里使用已经给出的两项最小名字条件及比较的证明，并不构造任何名字。

```agda
  StepAt-in : StepOf → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
  StepAt-in = ∃₆-in (StepBody R P B C C₀ x y) γ
```

反向读取时，`StepAt` 的满足关系只能拆成 `∥ StepOf ∥₁`。因此所得结论是：仅仅存在两组三元数据，分别满足两项最小名字公式，并且从前者到后者的比较公式得到满足。命题截断保留这项存在事实，却不暴露六个具体见证，这正符合存在量词的语义。

```agda
  StepAt-out : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩ → ∥ StepOf ∥₁
  StepAt-out = ∃₆-out (StepBody R P B C C₀ x y) γ
```

## 对着元语言造出的诸名字

为了把公式同预期的元层关系比较，固定一个可构造集 `A`，并在其载体 `⟪ A ⟫` 上固定严格良序 `w`。`A` 上名字的每个参数都取自这个载体，因此 `w` 恰好给出参数向量所需的序。以下充分性论证相对于这些数据成立，故适用于任何在自身载体上配有这种序的可构造集。

```agda
module Adequacy (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where
  private
    module NM = Naming A w
```

命名构造给出类型 `Name` 以及此处要对照的比较。元数为 `k` 的名字包含一条有 `suc k` 个变元位置的无参公式，以及一个恰有 `k` 个参数的向量。公式码由该公式派生，而 `_≺ₙ_` 依次比较名字的码、元数与参数向量。把 `w` 的关系改记为 `_≺ₚ_`，只是标明它在这里充当参数序。

```agda
  open NM using ( Name; arity; params; codeOf; _≺ᵥ_; _≺ₙ_ )
  open SWO w using () renaming ( _<∙_ to _≺ₚ_ )
```

为了同递归定义的向量序比较，先写出显式的首次相异关系 `Lex`。对两个等长向量，`Lex p q` 选取一个序号 `i`，要求 `p` 在该处的条目按 `_≺ₚ_` 先于 `q` 的条目，并要求每个 `j<i` 处的条目相等。不同于对象语言中的相符公式，这个元层关系可以直接陈述条目相等，无须以共同的图取值为中介。

```agda
  Lex : ∀ {k} → Vec ⟪ A ⟫ k → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
  Lex {k} p q = Σ[ i ∈ Fin k ]
    ( (lookup i p ≺ₚ lookup i q)
    × ((j : Fin k) → toℕ j < toℕ i → lookup j p ≡ lookup j q) )
```

从 `Lex` 到递归向量序的方向依首次相异所在的位置展开。序号为零时，头部的严格比较正是 `_≺ᵥ_` 的第一种情形。序号为后继时，相异位置以下的相等先给出两个头部相等；再把同一个见证的序号减一，便得到尾部之间的比较。这是对向量的结构递归，不使用任何经典原理。

```agda
  lex-vec : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Lex p q → p ≺ᵥ q
  lex-vec (x ∷ p) (y ∷ q) (zero  , (h , _)) = inl h
  lex-vec (x ∷ p) (y ∷ q) (suc i , (h , ag)) =
    inr (ag zero (suc-≤-suc zero-≤) , lex-vec p q (i , (h , λ j hj → ag (suc j) (suc-≤-suc hj))))
```

反向映射沿 `_≺ᵥ_` 的两种情形展开。两个空向量之间的序关系不可能成立。若两个非空向量因头部严格有序而被比较，序号零便见证 `Lex`；零以下没有序号，所以相等条件自动成立。

```agda
  vec-lex : ∀ {k} (p q : Vec ⟪ A ⟫ k) → p ≺ᵥ q → Lex p q
  vec-lex []      []      h = Empty.rec* h
  vec-lex (x ∷ p) (y ∷ q) (inl h) = zero , (h , λ j hj → Empty.rec (¬-<-zero hj))
  vec-lex (x ∷ p) (y ∷ q) (inr (e , h)) = suc (vec-lex p q h .fst)
    , ( vec-lex p q h .snd .fst
```

余下的情形给出头部相等以及尾部的递归序关系。对尾部应用归纳假设，得到尾部首次相异的序号；把它提升为后继，就得到原向量中的对应序号。已有的头部等式证明位置零处相等，而位置零正是这个提升后序号以下的第一个位置。

```agda
      , step )
    where
    step : (j : Fin (suc _)) → toℕ j < suc (toℕ (vec-lex p q h .fst))
         → lookup j (x ∷ p) ≡ lookup j (y ∷ q)
    step zero    _  = e
```

对提升后序号以下的其余每个位置，从数值不等式两边各去掉一个后继，所需结论便化为尾部自身的相等条件。反向证明由此完成。因此，显式的首次相异关系与递归向量序相互等价，参数论证可以在这两种表述之间转换，而不改变所比较的关系。

```agda
    step (suc j) hj = vec-lex p q h .snd .snd j (pred-≤-pred hj)
```

## 参数，两边各说一遍

公式码由另一个已有的序比较。每个 `codeOf t` 都属于极限层，而该层上的严格良序是 `limitOrder`；把它的关系记为 `_≺ˡ_`，便可与参数键 `_≺ₚ_` 并列辨认码键。这里不定义新的序；三键名字比较所使用的正是这两个序在模型内的表示。

```agda
  open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )
```

参数是小载体 `⟪ A ⟫` 的元素，因而同时含有一个底层集合以及该集合属于 `A` 的证据。映射 `ix` 忘去这份隶属证据，只保留 `V` 中的底层集合。参数值出现在环境图中，或出现在表示参数序的关系所含有序对中时，都采用这个典范嵌入像。

```agda
  ix : ⟪ A ⟫ → V ℓ
  ix m = ⟪ A ⟫↪ m
```

同一个底层集合也可以视为可构造模型的元素。由于 `A` 可构造且 `ix m` 属于 `A`，可构造性的传递性说明 `ix m` 也可构造。把这个集合与该证明配对，便得到 `ixL m : S`，也就是参数充当对象语言取值时所需的形式。

```agda
  ixL : ⟪ A ⟫ → S
  ixL m = ix m , isL-trans (∈∈ₛ {a = ix m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) pA
```

对一个名字 `t`，族 `pfam t` 逐项读取其参数向量。它的定义域是 `Fin (arity t)`，在序号 `i` 处的值是该处参数的底层 `V` 集合。因此，元数依定义确定这个族的定义域，而图 `env (pfam t)` 恰好给出该参数向量在模型内的环境表示。

```agda
  pfam : (t : Name) → Fin (arity t) → V ℓ
  pfam t i = ix (lookup i (params t))
```

把载体元素送到底层集合时不会丢失辨认该元素所需的信息。典范映射 `⟪ A ⟫↪` 是嵌入，因此 `ix u ≡ ix v` 蕴涵 `u ≡ v`。这项单射性是反向参数论证的关键：若两张环境图在较早序号处具有共同取值，就能把底层 `V` 集合的相等读回为两个参数向量相应条目的相等。

```agda
  ix-inj : (u v : ⟪ A ⟫) → ix u ≡ ix v → u ≡ v
  ix-inj u v = isEmbedding→Inj isEmb⟪ A ⟫↪ u v
```

还须明确两个模型内关系集各自表示什么。对码而言，`Rrep` 把 `u` 与 `v` 的有序对属于 `Rs` 读为 `u ≺ˡ v`，`Rfill` 则从这项比较证明相应隶属。对参数而言，`Prep` 与 `Pfill` 同样在「两个 `ix` 像组成的有序对属于 `Ps`」与 `u ≺ₚ v` 之间给出两个方向。这四条表示律都是假设。在这些假设下，只要两个可构造关系集具有相应表示，三键公式便满足充分性；这里不构造其中任何一个关系。

```agda
  module Keys (Rs Ps : S)
              (Rrep : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩ → u ≺ˡ v)
              (Rfill : (u v : Limit) → u ≺ˡ v → ⟨ pr (fst u) (fst v) ∈ fst Rs ⟩)
              (Prep : (u v : ⟪ A ⟫) → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩ → u ≺ₚ v)
              (Pfill : (u v : ⟪ A ⟫) → u ≺ₚ v → ⟨ pr (ix u) (ix v) ∈ fst Ps ⟩)
```

为了把四条表示律用于一次具体的参数比较，固定两个名字，以及对象语言读取其数据的各个槽位。这个局部论证受五项等同支配：一项识别参数关系，一项识别第一个元数，一项等同两个元数，另有两项分别识别参数环境。在这些假设下，论证将在显式首次相异 `Lex` 与基于图的记录 `Differs` 之间作双向翻译。

```agda
              where
```

前四项等同建立共同的比较框架。槽位 `P` 持有关系集 `Ps`；槽位 `a₁` 持有 `t₁` 的元数之数码；`qk : arity t₂ ≡ arity t₁` 则使两个参数向量能在同一个长度上比较。最后，`e₁` 持有 `pfam t₁` 的图，该族在每个序号处的值就是第一个名字的相应参数之嵌入像。须注意，`qk` 是两个自然数元数之间的等同，并不是某个对象语言槽位的等式。

```agda
    module _ {n : ℕ} (P a₁ e₁ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qP : fst (lookup P γ) ≡ fst Ps)
             (qa : fst (lookup a₁ γ) ≡ # (arity t₁))
             (qk : arity t₂ ≡ arity t₁)
             (q₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
```

第五项等同使第二个环境具有同一个定义域。先沿 `qk` 把 `params t₂` 从长度 `arity t₂` 搬运到长度 `arity t₁`，再把搬运后的每个条目嵌入 `V` 并取所得的图。这样，两张环境图都能用 `Fin (arity t₁)` 中的序号查取。接下来定义的私有族为搬运前后的条目取名，首先是第一个向量的 `pr₁`。

```agda
             (q₂ : fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) qk (params t₂)))))
             where
      private
        pr₁ : Fin (arity t₁) → ⟪ A ⟫
```

在共同长度的序号 `i` 处，`pr₁ i` 就是 `t₁` 的参数向量在该处的条目。它仍是小载体 `⟪ A ⟫` 的元素；只有当这个参数被放入环境图或模型中的有序对时，才施用嵌入 `ix`。把这两个层次分开，参数序便能直接作用于载体元素。

```agda
        pr₁ i = lookup i (params t₁)
```

配套的族 `pr₂` 读取 `t₂` 搬运后的向量。它与 `pr₁` 具有相同定义域，但其值仍是属于第二个名字的载体元素。因此，在每个共同序号处，`pr₁ i ≺ₚ pr₂ i` 与 `pr₁ j ≡ pr₂ j` 都是类型正确的陈述，恰好分别给出 `Lex` 所要求的严格比较与先前相符。

```agda
        pr₂ : Fin (arity t₁) → ⟪ A ⟫
        pr₂ i = lookup i (subst (Vec ⟪ A ⟫) qk (params t₂))
```

现在可以在一个确定序号处读取第一张图。假设以 `# (toℕ i)` 为键、以 `fst u` 为值的对属于槽位 `e₁` 中的集合。沿 `q₁` 搬运这项隶属，便把它放进 `env (pfam t₁)`；`lookup-spec` 再把其第二分量认定为该图在此处的唯一取值。这个取值就是 `ix (pr₁ i)`，故 `at₁` 恢复等式 `fst u ≡ ix (pr₁ i)`。

```agda
        at₁ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₁ γ) ⟩ → fst u ≡ ix (pr₁ i)
        at₁ i u h = subst ⟨_⟩ (lookup-spec (pfam t₁) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₁ h)
```

第二张图以搬运后的族代替 `pfam t₁`，采用完全相同的读法。先沿 `q₂` 搬运键 `# (toℕ i)` 处那一有序对的隶属，再由 `lookup-spec` 得到 `fst u ≡ ix (pr₂ i)`。因此，`at₁` 与 `at₂` 给出这里所需的单值性结论：它们把每个有效序号处读出的值精确认定为那里所表示的参数条目。

```agda
        at₂ : (i : Fin (arity t₁)) (u : S)
            → ⟨ pr (# (toℕ i)) (fst u) ∈ fst (lookup e₂ γ) ⟩ → fst u ≡ ix (pr₂ i)
        at₂ i u h = subst ⟨_⟩ (lookup-spec (λ j → ix (pr₂ j)) i (fst u))
          (subst (λ z → ⟨ pr (# (toℕ i)) (fst u) ∈ z ⟩) q₂ h)
```

反向使用 `lookup-spec`，便得到第一张图的典范条目。自反性说明 `ix (pr₁ i)` 正是 `pfam t₁` 在 `i` 处规定的值；逆向读取查表等式，就把这项相等变成对 `env (pfam t₁)` 的隶属。再沿 `q₁` 的反向搬运，即可把同一个有序对放进槽位 `e₁` 实际持有的集合。这就是见证 `put₁ i`。

```agda
        put₁ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ fst (lookup e₁ γ) ⟩
        put₁ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₁ i)) ∈ z ⟩) (sym q₁)
          (subst ⟨_⟩ (sym (lookup-spec (pfam t₁) i (ix (pr₁ i)))) refl)
```

见证 `put₂ i` 对搬运后的第二个族与槽位 `e₂` 作同样构造。于是，这四条引理为两个名字各自给出图查取的两个方向：`at₁` 与 `at₂` 识别任意给出的候选值，`put₁` 与 `put₂` 则展示图所规定的值。正向翻译将用后两者构造 `Differs`，反向翻译将用前两者恢复 `Lex`。

```agda
        put₂ : (i : Fin (arity t₁))
             → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ fst (lookup e₂ γ) ⟩
        put₂ i = subst (λ z → ⟨ pr (# (toℕ i)) (ix (pr₂ i)) ∈ z ⟩) (sym q₂)
          (subst ⟨_⟩ (sym (lookup-spec (λ j → ix (pr₂ j)) i (ix (pr₂ i)))) refl)
```

`Lex` 使用的序号是一个有穷数，而 `Differs` 携带的序号必须是可构造模型的元素。辅助定义 `numAt` 跨过这道小边界：它把 von Neumann 数码 `# m` 与其可构造性证明 `numL m` 配成一对。它本身并不断言这个数码低于某个元数；相应的隶属稍后由有穷序号自带的界限另行给出。

```agda
        numAt : (m : ℕ) → S
        numAt m = # m , numL m
```

正向翻译从 `Lex` 的一个元素取得有穷序号 `i`、该处的严格比较 `hlt`，以及每个更早序号处的相等 `agree`。所得 `Differs` 记录首先放入模型元素 `numAt (toℕ i)`，随后放入两个取值 `ixL (pr₁ i)` 与 `ixL (pr₂ i)`。有穷序号必小于其长度，故 `#mono` 把 `toℕ<n i` 化为该序号数码属于元数数码的证明；沿 `qa` 搬运以后，这项隶属便落在元数槽位中。

```agda
      lex-fill : Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
               → Differs P a₁ e₁ e₂ γ
      lex-fill (i , (hlt , agree)) = numAt (toℕ i)
        , ( ixL (pr₁ i) , ( ixL (pr₂ i)
        , ( subst (λ z → ⟨ # (toℕ i) ∈ z ⟩) (sym qa)
```

接下来的字段证明相异序号处发生了什么。见证 `put₁ i` 与 `put₂ i` 把两个嵌入后的参数值分别放进对应的环境图。表示律 `Pfill` 把 `hlt : pr₁ i ≺ₚ pr₂ i` 化为这两个值组成的有序对属于 `Ps`；再沿 `qP` 的反向搬运，这项隶属便进入槽位 `P` 所持有的关系集。因此，`Differs` 的三项隶属字段恰好表达两次查取与参数的严格比较。

```agda
              (#mono (toℕ i) (arity t₁) (toℕ<n i))
          , ( put₁ i
            , ( put₂ i
              , ( subst (λ z → ⟨ pr (ix (pr₁ i)) (ix (pr₂ i)) ∈ z ⟩) (sym qP)
                    (Pfill (pr₁ i) (pr₂ i) hlt)
```

还需构造所选序号以下的 `Agrees`。给定模型元素 `j` 及 `fst j ∈ # (toℕ i)`，数码消去定理在命题截断内说明：存在某个 `m < toℕ i`，使 `fst j` 等于 `# m`。把局部构造 `step` 映到这个结果上，就会在该较早位置为两张图给出一个共同取值。命题截断始终保留：从数码隶属中恢复的那个自然数不会暴露到 `Agrees` 所要求的命题之外。

```agda
                , agrees ) ) ) ) ) )
        where
        agrees : Agrees P a₁ e₁ e₂ γ (numAt (toℕ i))
        agrees j hj = PT.map step (∈#-elim (toℕ i) (fst j) hj)
          where
```

函数 `step` 精确陈述共同取值的要求。由 `m < toℕ i` 与把 `fst j` 认作 `# m` 的等式出发，它必须返回一个模型元素 `x`，使以 `fst j` 为键、以 `fst x` 为值的对同时属于两张环境图。给出的取值是第一族在相应有穷序号处的条目，包装为 `ixL (pr₁ jx)`。对第一张图，`put₁ jx` 已经给出典范数码键处的所需隶属；沿这个键的两种表示之间的等式搬运，即可把它改写到 `fst j` 处。

```agda
          step : Σ[ m ∈ ℕ ] ((m < toℕ i) × (fst j ≡ # m))
               → Σ[ x ∈ S ] ( ⟨ pr (fst j) (fst x) ∈ fst (lookup e₁ γ) ⟩
                            × ⟨ pr (fst j) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
          step (m , (hm , qj)) = ixL (pr₁ jx)
            , ( subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₁ γ) ⟩)
```

对第二张图，先前序号处的假设 `agree` 把 `pr₁ jx` 与 `pr₂ jx` 等同。沿这项等同的反向搬运 `put₂ jx`，便把其中的值从 `ix (pr₂ jx)` 改写为共同取值 `ix (pr₁ jx)`；再像前面那样搬运键，即得到 `fst j` 处的隶属。因此，在 `i` 以下的每个位置，两张图都含有同一个取值。这就完成了 `step` 的一个结果，进而完成 `Differs` 的 `Agrees` 字段。

```agda
                  (sym qjx) (put₁ jx)
              , subst (λ z → ⟨ pr z (ix (pr₁ jx)) ∈ fst (lookup e₂ γ) ⟩) (sym qjx)
                  (subst (λ y → ⟨ pr (# (toℕ jx)) (ix y) ∈ fst (lookup e₂ γ) ⟩)
                    (sym (agree jx (subst (_< toℕ i) (sym qm) hm))) (put₂ jx)) )
            where
```

剩下的认同关乎共同条目的键。由 `m < toℕ i`，再结合 `i` 本身小于`arity t₁`，传递性说明 `m` 给出一个合法元素 `jx : Fin (arity t₁)`。把`jx` 再转回自然数便得到 `m`；路径 `qm` 记录这次往返，使两项图隶属可以改写到各自的典范数码键上。

```agda
            jx : Fin (arity t₁)
            jx = fromℕ' (arity t₁) m (<-trans hm (toℕ<n i))
            qm : toℕ jx ≡ m
            qm = toFromId' (arity t₁) m (<-trans hm (toℕ<n i))
            qjx : fst j ≡ # (toℕ jx)
```

等式 `qj` 把原来的模型内键认作 `# m`，而 `qm` 又把 `m` 认作 `jx` 所对应的自然数。二者复合即得`qjx : fst j ≡ # (toℕ jx)`。这正是前文所用的换键等式：它把两张图的典范条目都传输到`j` 所指的位置。至此 `Agrees` 构造完成，正向桥 `lex-fill` 也随之闭合。

```agda
            qjx = qj ∙ cong #_ (sym qm)
```

反向桥从一份 `Differs` 记录出发，目标是恢复显式的首次相异。记录中的序号 `i` 属于元数数码，但数码隶属的消去定理只能在命题截断内恢复相应的较小自然数。因此，`lex-read` 返回 `Lex` 的命题截断：数码消去隐藏所选的自然数，`PT.map` 则在不解除这层截断的前提下完成其余显式构造。

```agda
      lex-read : Differs P a₁ e₁ e₂ γ
               → ∥ Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂)) ∥₁
      lex-read (i , (u , (v , (hi , (h₁ , (h₂ , (hp , ag))))))) =
        PT.map atIndex (∈#-elim (arity t₁) (fst i)
          (subst (λ z → ⟨ fst i ∈ z ⟩) qa hi))
```

进入映射后的构造时，隐藏见证已可作为具体自然数 `m` 使用，同时还有`m < arity t₁`，以及把模型内序号认作 `# m` 的等式。函数 `atIndex` 此时要直接构造`Lex`。它选取相应的有穷序号，并将在该处证明首次相异的两项要求：该序号处严格比较，所有更小序号处相符。

```agda
        where
        atIndex : Σ[ m ∈ ℕ ] ((m < arity t₁) × (fst i ≡ # m))
                → Lex (params t₁) (subst (Vec ⟪ A ⟫) qk (params t₂))
        atIndex (m , (hm , qi)) = ι , (below , agrees)
          where
```

`m` 的界给出 `ι : Fin (arity t₁)`。和正向一样，数码往返把关于 `# m` 的等式改写为`qι : fst i ≡ # (toℕ ι)`，于是记录在第一张环境图中的隶属可以在 `ι` 的典范键处读取。查取引理`at₁` 随即把记录的值 `fst u` 认作第一个参数的嵌入像 `ix (pr₁ ι)`。

```agda
          ι : Fin (arity t₁)
          ι = fromℕ' (arity t₁) m hm
          qι : fst i ≡ # (toℕ ι)
          qι = qi ∙ cong #_ (sym (toFromId' (arity t₁) m hm))
          qu : fst u ≡ ix (pr₁ ι)
```

对第二张图应用 `at₂`，同样得到 `fst v ≡ ix (pr₂ ι)`。`Differs` 的关系原子说：记录的两个值组成的有序对属于槽位`P` 中的集合。把该集合改写为 `Ps`，再把两个值改写为相应参数的嵌入像之后，表示律 `Prep` 便把这条原子读成所需的严格比较`pr₁ ι ≺ₚ pr₂ ι`。

```agda
          qu = at₁ ι u (subst (λ z → ⟨ pr z (fst u) ∈ fst (lookup e₁ γ) ⟩) qι h₁)
          qv : fst v ≡ ix (pr₂ ι)
          qv = at₂ ι v (subst (λ z → ⟨ pr z (fst v) ∈ fst (lookup e₂ γ) ⟩) qι h₂)
          below : pr₁ ι ≺ₚ pr₂ ι
          below = Prep (pr₁ ι) (pr₂ ι)
```

上述传输完成了名为 `below` 的证明。余下任务是恢复 `ι` 之前的相符。任取满足`toℕ j < toℕ ι` 的 `j`，有界子句 `ag` 仅仅地给出一个模型元素，其值在该位置同时出现于两张环境图。所求的两个参数嵌入像之相等是命题，因此可以把这份命题截断直接消去到该相等中。

```agda
            (subst2 (λ y z → ⟨ pr y z ∈ fst Ps ⟩) qu qv
              (subst (λ z → ⟨ pr (fst u) (fst v) ∈ z ⟩) qP hp))
          agrees : (j : Fin (arity t₁)) → toℕ j < toℕ ι → pr₁ j ≡ pr₂ j
          agrees j hj = ix-inj (pr₁ j) (pr₂ j)
            (PT.rec (setIsSet (ix (pr₁ j)) (ix (pr₂ j))) same
```

为了调用 `ag`，先由 `#mono` 把有穷不等式化为`# (toℕ j) ∈ # (toℕ ι)`，再沿 `qι` 传输到记录中的界。所得截断见证恰具有 `same` 所需的形状：一个元素`x`，以及有序对 `(# (toℕ j), fst x)` 分别属于两张环境图的证明。因此，这层截断含有所需相等的全部资料，却不让任何具体见证逸出。

```agda
              (ag (numAt (toℕ j))
                (subst (λ z → ⟨ # (toℕ j) ∈ z ⟩) (sym qι) (#mono (toℕ j) (toℕ ι) hj))))
            where
            same : Σ[ x ∈ S ] ( ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₁ γ) ⟩
                              × ⟨ pr (# (toℕ j)) (fst x) ∈ fst (lookup e₂ γ) ⟩ )
```

选定一个共同取值 `x` 后，`at₁` 把 `fst x` 认作 `ix (pr₁ j)`，`at₂` 则把同一个集合认作`ix (pr₂ j)`。反转第一条路径再与第二条复合，便得到两个参数嵌入像相等。`ix` 的单射性把这项相等反映回`pr₁ j ≡ pr₂ j`，恰好就是 `Lex` 在先前序号处要求的条件。反向桥至此完成。

```agda
                 → ix (pr₁ j) ≡ ix (pr₂ j)
            same (x , (k₁ , k₂)) = sym (at₁ j x k₁) ∙ at₂ j x k₂
```

## 两半

在 `Keys` 接受的四条表示律下，两个关系位置分别表示公式码上的 `limitOrder` 和载体参数上的给定次序。现在，两半证明比较的是同样三个键。`order-in` 把一份具体的 `t₁ ≺ₙ t₂` 证明送到 `≺At` 的满足关系；`order-out` 从这样的满足关系只能读回 `∥ t₁ ≺ₙ t₂ ∥₁`。向外一半保留析取与存在满足关系带来的命题截断。因此，本章至此只完成比较公式 `≺At` 自身的充分性，没有在这里得到关于其余公式的更强结论。

余下工作的边界是明确的。元语言的 `Name` 只存储元数、无参公式和参数向量，指称由它们派生。在模型内部，`NameAt` 为这些数据和派生的指称设置位置，并用 `satGraphAt` 返回的满足环境集检查指称。`LeastNameAt` 只陈述没有同指称而更小的名字，并不选择名字。`NameAt`、`LeastNameAt` 与 `StepAt` 的完整充分性，包括从满足关系中恢复见证，属于 `L.Choice.NameComparisonAdequacy`；实际的最小名字选择仍由 `CanonicalNames.leastName` 完成。

## 小结

接下来两条路径归纳引理清除完整三键比较中的类型层面障碍。第一条 `envShift` 处理元数等式`e : arity t ≡ k`。沿 `e` 传输 `params t`，逐项读取并组成环境图，所得图与在原长度上直接读取`params t` 的图相等。当 `e` 是自反路径时，结论立即化简；路径归纳遂覆盖任意等式。

```agda
    private
      envShift : (t : Name) {k : ℕ} (e : arity t ≡ k)
               → env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) e (params t))))
               ≡ env (pfam t)
      envShift t e = sym (constSubstCommSlice
```

这条等式从传输后向量的图指向原图 `env (pfam t)`。这个方向服务于最终证明：关于第二个环境的假设先把相应槽位认作原图，再接上`envShift` 的反向，便把同一槽位认作第一名字之元数上的图，恰好得到首次相异桥所要求的形式。

```agda
        (Vec ⟪ A ⟫) (V ℓ) (λ _ v → env (λ i → ix (lookup i v))) e (params t))
```

第二条引理 `vecShift` 对向量序作平行的化简。沿长度等式传输 `q` 后再拿它与 `p` 比较，所得命题与直接比较原向量相同。等式证明同样不引入新的数学情形：路径归纳把它化为自反路径。于是，元数一经认同，`envShift` 与`vecShift` 便使环境图的呈现和向量比较始终同步。

```agda
      vecShift : {i j k : ℕ} (e : i ≡ j) (p : Vec ⟪ A ⟫ k) (q : Vec ⟪ A ⟫ i)
               → (p ≺ᵥ subst (Vec ⟪ A ⟫) e q) ≡ (p ≺ᵥ q)
      vecShift e p q = sym (constSubstCommSlice
        (Vec ⟪ A ⟫) (Type (ℓ-suc ℓ)) (λ _ v → p ≺ᵥ v) e q)
```

最后的比较在任意环境的任意槽位上进行。两个槽位分别持有表示关系 `Rs` 与 `Ps`；对每个名字，另有三个槽位持有它的公式码、元数数码与参数图。八条等式`qR`、`qP`、`qs₁`、`qs₂`、`qa₁`、`qa₂`、`qe₁` 与 `qe₂` 把这些读法固定到两个具体名字`t₁`、`t₂` 上。恰在这些假设之下，内部公式才可与 `_≺ₙ_` 对照。

```agda
    module _ {n : ℕ} (R P s₁ a₁ e₁ s₂ a₂ e₂ : Fin n) (γ : S ^ n) (t₁ t₂ : Name)
             (qR : fst (lookup R γ) ≡ fst Rs) (qP : fst (lookup P γ) ≡ fst Ps)
             (qs₁ : fst (lookup s₁ γ) ≡ fst (codeOf t₁))
             (qs₂ : fst (lookup s₂ γ) ≡ fst (codeOf t₂))
             (qa₁ : fst (lookup a₁ γ) ≡ # (arity t₁))
```

最后四条槽位等式固定两个元数与两张环境图，因此定理并未把任何特定坐标写死。为了读取第二、第三个键，还须把槽位取值之间的相等提升回名字所携依值数据的相等。第一个辅助引理`codeSame` 处理码键：它从两个骨架槽位相等，重建类型 `Limit` 中的等式`codeOf t₂ ≡ codeOf t₁`。

```agda
             (qa₂ : fst (lookup a₂ γ) ≡ # (arity t₂))
             (qe₁ : fst (lookup e₁ γ) ≡ env (pfam t₁))
             (qe₂ : fst (lookup e₂ γ) ≡ env (pfam t₂)) where
      private
        codeSame : fst (lookup s₂ γ) ≡ fst (lookup s₁ γ) → codeOf t₂ ≡ codeOf t₁
```

`Limit` 的元素由一个底层集合及其属于 `Lset ω` 的证据组成。该证据取值于命题，因此 `Σ≡Prop` 说明：底层集合之间的一条路径就足以确定完整码之间的路径。这里所需的底层路径是复合`sym qs₂ ∙ q ∙ qs₁`：从第二个码走到它的槽位，经记录的骨架等式，再走到第一个码。这既说明证明分量无须另行比较，也说明所得等式为何具有名字序第二分支所需的方向。

```agda
        codeSame q = Σ≡Prop (λ x → snd (x ∈ Lset ω)) (sym qs₂ ∙ q ∙ qs₁)
```

反向转换从 `Limit` 中的等同出发；这里的码由底层集合及其属于极限层的证明组成。对这条等同施用 `fst`，便得到两个底层码集合的等同。再与两项槽位等同复合，就得到公式后两支所需的方向：第二个骨架槽等同于第一个。

```agda
        codeBack : codeOf t₂ ≡ codeOf t₁ → fst (lookup s₂ γ) ≡ fst (lookup s₁ γ)
        codeBack ec = qs₂ ∙ cong fst ec ∙ sym qs₁
```

参数支必须按第一个名字的元数读取第二张环境图。给定 `ek : arity t₂ ≡ arity t₁`，路径归纳把 `params t₂` 的图与先把该向量搬运到新长度再取图所得的集合等同起来。将这条图等同反向读取，并与槽位 `e₂` 的等同复合，便得到首次相异之桥所要求的搬运后环境。

```agda
        shiftEnv : (ek : arity t₂ ≡ arity t₁)
                 → fst (lookup e₂ γ)
                 ≡ env (λ i → ix (lookup i (subst (Vec ⟪ A ⟫) ek (params t₂))))
        shiftEnv ek = qe₂ ∙ sym (envShift t₂ ek)
```

正向定理现在依次处理一个名字先于另一个名字的三种缘由。在码支中，`Rfill` 把两个公式码在极限序下的严格比较化为其有序对属于 `Rs`。关于 `R`、`s₁` 与 `s₂` 的等同把这项隶属搬运到公式的三个槽位，`≺At-in` 再将所得见证放入 `≺At` 的第一支。

```agda
      order-in : t₁ ≺ₙ t₂ → ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩
      order-in (inl h) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inl (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
                (sym qR)
                (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) (sym qs₁) (sym qs₂)
```

在元数支中，码的等同先经 `codeBack` 给出两个骨架槽所需的等同。严格不等式 `arity t₁ < arity t₂` 由 von Neumann 数码律 `#mono` 化为隶属 `# (arity t₁) ∈ # (arity t₂)`，两项元数槽等同再把这项隶属搬运到公式中。因此，只有在第一个键已证相等之后，第二个键才参与比较。

```agda
                  (Rfill (codeOf t₁) (codeOf t₂) h))))
      order-in (inr (ec , inl h)) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inl
          (subst2 (λ y z → ⟨ y ∈ z ⟩) (sym qa₁) (sym qa₂)
            (#mono (arity t₁) (arity t₂) h))))
```

参数支从码相等且元数相等的情形开始。元数路径先把第二个参数向量搬运到第一个向量的长度，`vec-lex` 再把两者的递归向量比较化为一个显式的首次相异序号。`lex-fill` 随后把这份见证化为满足 `LexAt` 所用的 `Differs` 载荷：其中记录该序号、此处的严格比较以及此前各处的相等，并用 `shiftEnv` 识别搬运后的第二张图。这样便由比较证据直接构造出 `≺At` 的第三支，无须从命题截断中提取任何见证。

```agda
      order-in (inr (ec , inr (ek , hv))) = ≺At-in R P s₁ a₁ e₁ s₂ a₂ e₂ γ
        (inr (codeBack ec , inr (qa₂ ∙ cong #_ ek ∙ sym qa₁
          , lex-fill P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek)
              (vec-lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂))
                (transport (sym (vecShift ek (params t₁) (params t₂))) hv)))))
```

反向定理保留对象语言析取与存在量词所携带的命题截断。因此，`≺At-out` 只能在截断内给出三种情形；目标本身是命题 `∥ t₁ ≺ₙ t₂ ∥₁`，故 `PT.rec` 可以在其中作情形分析。在码支中，各槽位等同把公式记录的有序对隶属搬回 `Rs`，`Rrep` 再将它读成两个真实码在极限序下的严格比较，从而给出名字比较的第一支。

```agda
      order-out : ⟨ γ ⊨ ≺At R P s₁ a₁ e₁ s₂ a₂ e₂ ⟩ → ∥ t₁ ≺ₙ t₂ ∥₁
      order-out h = PT.rec squash₁ read (≺At-out R P s₁ a₁ e₁ s₂ a₂ e₂ γ h)
        where
        read : Below R P s₁ a₁ e₁ s₂ a₂ e₂ γ → ∥ t₁ ≺ₙ t₂ ∥₁
        read (inl k) = ∣ inl (Rrep (codeOf t₁) (codeOf t₂)
```

在元数情形中，公式先给出第二个骨架槽等同于第一个；`codeSame` 把这条底层等同提升为两个码在 `Limit` 中的等同。另一项前提经元数槽等同搬运后，成为第一个元数数码属于第二个元数数码。数码消去把这项隶属化为 `arity t₁ < arity t₂`，于是第一个键的相等与第二个键的严格比较共同组成 `_≺ₙ_` 的元数支。

```agda
          (subst2 (λ y z → ⟨ pr y z ∈ fst Rs ⟩) qs₁ qs₂
            (subst (λ z → ⟨ pr (fst (lookup s₁ γ)) (fst (lookup s₂ γ)) ∈ z ⟩)
              qR k))) ∣₁
        read (inr (q , inl k)) = ∣ inr (codeSame q , inl
          (#∈#-elim (arity t₁) (arity t₂)
```

参数情形必须先恢复一个共同长度。公式给出从第二个元数槽到第一个元数槽的等同；将它与两项槽位等同复合，便得到相应 von Neumann 数码的等同，`#-inj′` 再恢复 `ek : arity t₂ ≡ arity t₁`。这条路径使第二个向量具有可比较的类型以后，`lex-read` 依据两张环境图解释 `LexAt` 的记录。所得是仍处于命题截断内的显式首次相异 `Lex`，恰好保留了公式的存在见证边界。

```agda
            (subst2 (λ y z → ⟨ y ∈ z ⟩) qa₁ qa₂ k))) ∣₁
        read (inr (q , inr (q' , dif))) = PT.map atLex
          (lex-read P a₁ e₁ e₂ γ t₁ t₂ qP qa₁ ek qe₁ (shiftEnv ek) dif)
          where
          ek : arity t₂ ≡ arity t₁
```

在该截断内部，`atLex` 完成第三种情形。归纳 `lex-vec` 把显式首次相异化为第一个向量与搬运后第二个向量之间的递归向量序，`vecShift` 再从所得命题中消去这次搬运。把它与 `codeSame q` 及恢复出的元数路径 `ek` 合在一起，就得到 `_≺ₙ_` 的参数支；`PT.map` 则使整个结果仍处于截断内。因此，在两个序的表示律与各项槽位等同之下，`order-in` 从名字比较构造对 `≺At` 的满足，而 `order-out` 只恢复 `∥ t₁ ≺ₙ t₂ ∥₁`。这证明的是比较公式自身的充分性；`NameAt`、`LeastNameAt` 与 `StepAt` 的相应读式还需要另外的论证。

```agda
          ek = #-inj′ (sym qa₂ ∙ q' ∙ qa₁)
          atLex : Lex (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) → t₁ ≺ₙ t₂
          atLex lx = inr (codeSame q , inr (ek
            , transport (vecShift ek (params t₁) (params t₂))
                (lex-vec (params t₁) (subst (Vec ⟪ A ⟫) ek (params t₂)) lx)))
```