---
title: "名字比较的充分性"
module: L.Choice.NameComparisonAdequacy
lang: zh
site: "Bedrock"
description: "名字比较的充分性"
stage: "典范良序与选择公理"
reading_order: 80
canonical: https://bedrock.institute/zh/L.Choice.NameComparisonAdequacy.html
html: L.Choice.NameComparisonAdequacy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/NameComparisonAdequacy.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.Coding.Environment, L.Coding.Model, L.Coding.Expressions, L.Coding.EnvironmentSet, L.Coding.SatisfactionGraph, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Choice.CanonicalNames, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.NameComparisonAdequacy.md, https://bedrock.institute/ja/L.Choice.NameComparisonAdequacy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 名字比较的充分性

同一个可定义子集可能有不止一条名字。因此，内部比较不能只辨认一条公式及其参数，还必须把每个给定集合接到指称它的名字，表达它在所有同指称名字中的最小性，再比较所得的最小名字。本章证明对象语言描述恰好完成这些任务；在反向读取中，恢复出的名字始终保留在命题截断之下。

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

共用前奏给出全书关于宇宙、命题、有穷索引与向量的约定。本章明列的唯一经典假设是排中律。它作为普通类型导入，并将显式传给需要它的构造；因此，后文使用满足关系表或名字序时，所依赖的假设边界始终可以核查。

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

因此，模块始终携带后继宇宙层级上的 `lem`。它经命名、有限语法码上的序与一致满足关系传入论证，却不许可从命题截断中任意取出见证。下文证明的充分性有意保持不对称：给定具体名字，可以把它们填入公式；反向读取一个满足赋值时，只得到命题截断下合适名字的存在性。

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

这次语义比较需要一套语法与两个紧密相关的结构。`Formula` 是共用的对象语言，而常元改名把公式搬过空常元域、载体成员与外围集合宇宙。`V` 上的结构给出外围解释；其外延性原理稍后把成员命题的逐点一致化为两种呈现所指称集合的相等。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp; embed )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
```

名字是解释于可构造载体之上的有限语法数据，因此证明必须把编码与 `L` 接起来。公式码是由数码与对组装出的集合；无参公式的码已经落在极限层中，因而可由 `limitOrder` 比较。在语义一侧，可构造性及其传递性把外围集合包装成 `L` 上结构的元素；内部数码、空可构造集与环境图则给出名字公式实际谈及的对象。

```agda
open import V.Coding {ℓ} using ( pr; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Ordinal {ℓ} using ( #∈ω; ω-ord )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ; LsetS )
open import L.Coding.Environment {ℓ} using ( env )
```

模型一侧的词汇先表达名字的数据，尚不从中恢复名字。`envOverAt` 断言一个候选集合是单值图，具有指定定义域，取值落在载体中，并且不含非对形式的冗余成员；其搬运引理允许沿槽位等式替换这三个指定集合。`consAtL` 描述环境如何添入候选成员，`domAt` 记录其长度，`extAt` 则由成员刻画指称。反向论证中，恢复模块至关重要，因为环境图的这些条件唯一决定每个参数值。

```agda
open import L.Coding.Model {ℓ} using ( envOverAt; envOverAt-transport; domAt )
open import L.Coding.Expressions {ℓ} using ( extAt-in; extAt-out; numL; consAtL )
open import L.Coding.EnvironmentSet {ℓ} lem using ( module Recover; envS; envOver )
open import L.Coding.SatisfactionGraph {ℓ} lem using ( satGraphAt )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

下一座桥说明载体层公式如何成为一致满足关系表中的一个取值。指名载体成员的常元被常元改名后进入模型，其赋值同时表示为环境与内部图，而公式由载体码集中的真实键寻址。要求该键属于 `AllCodes` 不可省略：只有在这样的键处，图的读式才迫使所记录的取值与实际满足关系一致。

```agda
open import L.Coding.SatisfactionBridge {ℓ} lem
  using ( consAtL-in; consAtL-out; asConst; values; envFor; envFor-graph )
  renaming ( graph to envGraph )
open import L.Coding.CodeSet {ℓ} lem using ( keyS; AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem
```

数学接口至此显出全貌。`CanonicalNames` 给出元语言名字、它的码、参数向量、指称及三键名字序；`FiniteStageOrders` 给出第一键所用的序；`NameComparison` 则给出有待证明充分性的对象语言描述。尤其要注意，`NameAt` 恰有四个概念性合取项：无参骨架、属于 `ω` 的元数数码、该元数之上取值于载体的参数图，以及对指称的外延刻画。

```agda
  using ( val-at; val-sat; keyIn; keyIn≡; keyIn∈; module Table )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming; limitCode )
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; limitOrder )
open import L.Choice.NameComparison {ℓ} lem
  using ( NameAt; NameAt-in; LeastNameAt; ≺At; StepAt; StepOf; StepAt-in; StepAt-out; DenoteOf; DenoteBody; DenoteBody-in; DenoteBody-out
```

余下的导入接口把三项不可混同的工作分开。码、图与定义域的读式恢复槽位所表示的数据；`Adequacy` 模块按码、元数与参数比较两条已经给定的名字；本章则补上缺失的一步，证明任意满足槽位数据来自名字，并且恢复出的名字具有所述最小性。所得名字依然留在命题截断之下，所以这里的读取引理都不选出见证。只有到了下游，`InternalWellOrder` 才在填充方向使用由既有良序构造的 `leastNameOf`，取得具体最小名字。

```agda
        ; FreeAt; codeFree-in; codeFree-out
        ; graphAt-value; graphAt-only
        ; domAt-numeral; domAt-fill; module Adequacy )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
```

证明中反复出现三种表示转换。由 `Fin k` 索引的族被列表化为长度受索引的向量，也可以逐项读回。成员命题之间的逻辑等价被转成集合外延性所需的路径。最后，带证明载体之间的路径负责搬运类型依赖于载体的公式码与满足关系集。经这些比较判定为不可能的分支则由空类型消去。

```agda
open import Cubical.Data.Vec.Properties using ( FinVec→Vec; FinVec→Vec→FinVec )
open import Cubical.Data.Vec using ( map )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
import Cubical.Data.Empty as Empty
```

命题截断精确记录反向读式的强度：它保留见证存在这一事实，却忘去见证是哪一个；当目标本身是命题时，才可从中消去。层级操作与这套纪律相辅相成：`⟪ A ⟫` 是索引集合 `A` 之成员的小类型，其嵌入把索引送到相应成员，而 `∈-asFiber` 从成员关系恢复这样的索引。因此，环境中由单值性唯一确定的条目可以作为数据恢复，却不能据此把仅仅存在的公式或名字变成选定的数据。这里用到的是命题截断，不是命题降级。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
```

元数经 von Neumann 自然数跨过语义边界。元语言自然数 `k` 由集合论数码 `# k` 表示，而 `ω` 恰好包含这些数码。因此，名字的元数条款可以双向读取；名字比较的中间键也可在内部直接写成一个数码属于另一个数码，无须再添一个关系参数。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_; ω )
```

打开 `L` 上的命题值结构，便固定模型元素类型 `S` 以及后续每条公式采用的集合论词汇。`S` 的一个元素由外围集合及其可构造性证据组成。因此，环境存放带证明的可构造集合，而公式中的成员关系与等词则经该结构考察其底层外围集合。

```agda
open hPropStructure 𝒮ʟ
```

绝对性模块把 `V` 上的外围结构与以可构造集合为元素的结构联系起来。下文的记号 `γ ⊨ φ` 表示公式 `φ` 在这个可构造结构中于环境 `γ` 下得到满足。因此，`γ` 的每个条目同时携带底层集合及其可构造性证明，而既有的充分性与绝对性引理把公式满足关系接到这些底层集合的隶属与相等。

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

最小性引入另一种局部语境。为检验当前名字是否最小，对象语言全称绑定一条竞争者的骨架码、元数数码与参数图。此前已有的每个槽位因而向外退后三位，`sh3` 正是把那些引用完整保留在竞争者三项数据之下的统一嵌入。

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

经满足关系图读取指称时，会形成该论证使用的最深局部语境。原环境之前依次压入五个新值：候选成员、扩张环境、环境长度、公式键，以及该键处的表取值。`sh5` 把外层槽位越过这五项，使图条款仍能回指原来的载体。

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

步进公式在作任何比较之前，先绑定两套完整的名字数据。每套包含骨架码、元数数码与参数图，合计六个新条目。`sh6` 把每个外层槽位嵌入这层框架之下，使两条最小名字子句与最后的名字比较仍谈论同一载体、码集、关系槽位及被比较对象。

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

六个固定索引为这层局部框架中的条目命名。由于相继引入的存在见证都压到环境前端，第一个名字的骨架码、元数与参数图最终位于索引 5、4、3，而第二个名字的骨架码位于索引 2。一次记下这些位置，便可保证后文每次引用都与见证的引入顺序对齐。

```agda
  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 = suc (suc zero)
```

索引 1 与 0 存放第二个名字的元数与参数图，于是局部环境从近到远呈 `p₂, k₂, s₂, p₁, k₁, s₁` 的次序。这里六个绑定是 `StepAt` 内两条名字的数据，必须与 `InternalWellOrder.Stp` 稍后绑定的六个外围见证区分。后者依次描述层塔、其可定义幂集、一个表取值、一个码集、码序与空字母表码集。内层公式只为该使用者提供局部名字比较，此处尚未断言内部良序。

```agda
  a6b = suc zero
  e6b = zero
```

第一条向量引理规范化逐项映射后的查表。从 `map f v` 的索引 `i` 处读出的，恰是把 `f` 施于 `v` 在 `i` 处的条目。对向量归纳时，首项情形由自反性成立，尾项情形化归到归纳假设。后文借此等式，可在载体索引及其作为模型元素的像之间无歧义地转换。

```agda
lookup-map : {ℓ' ℓ'' : Level} {X : Type ℓ'} {Y : Type ℓ''} (f : X → Y)
             {k : ℕ} (v : Vec X k) (i : Fin k)
           → lookup i (map f v) ≡ f (lookup i v)
lookup-map f (x ∷ v) zero    = refl
lookup-map f (x ∷ v) (suc i) = lookup-map f v i
```

第二条向量引理规范化恢复过程采用的另一种呈现。把族 `g : Fin k → X` 列表化为 `FinVec→Vec g`，再查索引 `i`，所得就是 `g i`。这并非 `lookup-map` 的反向；两条引理分别消去两种不同的表示层：一条透过逐项映射显露条目，另一条透过列表化显露条目。合用时，它们把恢复出的有穷族接到名字所存的参数向量上。

```agda
lookup-tab : {ℓ' : Level} {X : Type ℓ'} {k : ℕ} (g : Fin k → X) (i : Fin k)
           → lookup i (FinVec→Vec g) ≡ g i
lookup-tab g i j = FinVec→Vec→FinVec g j i
```

## 本章的框架

局部模块现在固定后续每次读式采用的数学环境。外围集合 `A` 配上 `pA` 后成为可构造结构的元素 `Aʟ`，而 `w` 是索引其成员的小类型 `⟪ A ⟫` 上的良序。涉及载体的槽位等式使用带证明的元素 `Aʟ`，因为后续公式与搬运依赖完整模型元素，并非只依赖其第一投影。

```agda
module At (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where
  private
    Aʟ : S
    Aʟ = A , pA
```

打开 `Naming A w`，便固定充分性所要对照的元语言对象。一条名字是依值三元组：元数 `k`、具有 `suc k` 个变量位置的无参公式，以及恰由 `A` 的 `k` 个成员组成的向量。名字的码取自该公式，名字的指称则是该公式在这些参数下从 `A` 中界定出的子集。名字序先由 `limitOrder` 比较公式码，再按自然数序比较元数，最后在元数相等时按 `w` 对参数向量作字典序比较。本章余下部分将在命题层证明槽位描述恰好恢复这次比较，同时保留命题截断与所陈述的最小性条件。

```agda
    module NM = Naming A w
```

固定可构造载体及其良序后，两套互补的接口便并列在一起。`Adequacy` 给出载体成员的嵌入、名字的参数族及比较模块 `Keys`；`Naming` 给出名字，以及名字的元数、无参公式、参数向量，还有由这些数据导出的码、扩张环境与指称。关系 `_≺ₙ_` 按三个键比较这样的名字。

这一区分也固定了本章结论的逻辑强度。`NameAt` 恰有四个概念性合取项，分别刻画骨架、元数、参数图与指称。充分性的填充方向从给定名字证明这四项，读取方向却只得到命题截断下名字的存在性。最小性稍后是恢复所得名字的一项性质，选出某个具体最小名字则发生在下游。`InternalWellOrder` 使用本章结论时，`StepAt` 内部的六个绑定是两组三项名字资料，与 `Stp` 外围的六个基础设施见证属于不同的环境。

```agda
  open Adequacy A pA w using ( ix; pfam; module Keys )
  open NM using
    ( Name; arity; formula; params; codeOf; denote; environment
    ; _≺ₙ_ )
```

## 参数序列，填进去

参数向量首先要从元语言数据跨入对象语言环境。族 `g : Fin k → ⟪ A ⟫` 在 `k` 个序号中的每一处给出一个载体成员。若位置 `e`、`a`、`B` 依次持有这些成员嵌入后的图、数码 `# k` 与载体 `A`，则 `envOverAt e a B` 得到满足。它的四项条件分别说明该图单值、定义域恰为这个有穷数码、取值落在载体中，并且只含有序对。

```agda
  paramSeq-in : ∀ {n} (e a B : Fin n) (γ : S ^ n) (k : ℕ) (g : Fin k → ⟪ A ⟫)
              → fst (lookup e γ) ≡ env (λ i → ix (g i))
              → fst (lookup a γ) ≡ # k
              → fst (lookup B γ) ≡ A
              → ⟨ γ ⊨ envOverAt e a B ⟩
```

把这三个集合放入任意位置后，无须重新证明那四项图性质。由 `Aʟ`、`# k` 与 `envS Aʟ g` 组成的典范环境，已经在序号二、一、零处满足这些性质。`envOverAt-transport` 沿三条给定等式把这份满足关系搬到 `γ`。等式在调用中取反，是因为搬运从典范集合出发，抵达指定位置中存放的集合。

```agda
  paramSeq-in e a B γ k g qe qa qB =
    envOverAt-transport (Aʟ ∷ (# k , numL k) ∷ envS Aʟ g ∷ []) γ
      (suc (suc zero)) (suc zero) zero e a B
      (sym qe) (sym qa) (sym qB) (envOver Aʟ g)
```

## 又被读回成一个向量

在反向读取中，等式 `qa` 与 `qB` 固定元数位和载体位，而 `h` 断言位置 `e` 中的集合满足环境条件。这里并未预先假定 `e` 的某种图表示；找出这样的表示正是任务所在。以这些数据打开 `Recover` 后，便得到一个由 `Fin k` 索引的族，以及其典范图就是原集合的证明。

```agda
  module _ {n : ℕ} (e a B : Fin n) (γ : S ^ n) (k : ℕ)
           (qa : fst (lookup a γ) ≡ # k) (qB : fst (lookup B γ) ≡ A)
           (h : ⟨ γ ⊨ envOverAt e a B ⟩) where
    private
      module R = Recover Aʟ k γ e a B qa qB h
```

恢复出的族是真正的数据，因而可以列表化为长度为 `k` 的向量。这里并未借助选择来解除截断。对每个序号，定义域条件只给出某个条目的仅仅存在，但单值性使条目类型成为命题；因此，可以把命题截断消去到这个命题中，取得唯一条目。该条目的值属于 `A`，而载体的成员纤维无截断地给出 `⟪ A ⟫` 中相应的元素。对这些元素应用 `FinVec→Vec`，便得到 `paramSeq-out`。这里使用的是命题截断，不是命题降级。

```agda
    paramSeq-out : Vec ⟪ A ⟫ k
    paramSeq-out = FinVec→Vec R.g
```

列表化改变了族的呈现方式，因而还要用图等式闭合这次往返。`R.recovers` 把位置 `e` 中的集合认作恢复所得有穷族的图。`FinVec→Vec` 的查取律再把列表化向量的每个条目认作相应的族值；函数外延性与 `env` 的同余把这些逐点路径提升为图的相等。因此，恢复所得向量精确呈现原环境集合，其中也没有「只由有序对构成」条件所排除的多余成员。

```agda
    paramSeq-graph : fst (lookup e γ)
                   ≡ env (λ i → ix (lookup i paramSeq-out))
    paramSeq-graph = R.recovers
                   ∙ cong env (funExt (λ i → cong ix (sym (lookup-tab R.g i))))
```

## 四个元素，在造出之处封印

指称条款自身含有四个存在见证，它们不同于 `NameAt` 的四个概念性合取项。第一个见证由名字 `t` 与候选载体成员 `m` 构成：把 `m` 放到 `t` 的参数向量之前，再把这个扩张赋值表示成模型元素。构造 `envFor Aʟ` 同时携带所需的可构造性证明，因此 `envAt t m` 可以占据一个对象语言位置。

```agda
  opaque
    envAt : Name → ⟪ A ⟫ → S
    envAt t m = envFor Aʟ (environment t m)
```

对象语言公式考察的是该模型元素的底层集合。等式 `envAt-fst` 把它认作 `envGraph Aʟ (environment t m)`，即候选元素置于诸参数之前所得的典范图。这一呈现恰好同时服务于两条公式：一条把候选元素添到原参数环境中，另一条检查扩张环境的定义域。

```agda
    envAt-fst : (t : Name) (m : ⟪ A ⟫)
              → fst (envAt t m) ≡ envGraph Aʟ (environment t m)
    envAt-fst t m = envFor-graph Aʟ (environment t m)
```

第二个见证在可构造模型内部表示一个自然数。`numAt j` 把 von Neumann 数码 `# j` 与其可构造性证明 `numL j` 配成模型元素。在指称论证中，将取 `j = suc (arity t)`，因为扩张环境除 `arity t` 个参数外还含有候选元素。

```agda
    numAt : ℕ → S
    numAt j = # j , numL j
```

投影 `numAt j` 的底层集合按定义便得到 `# j`，所以 `numAt-fst` 由自反性证明。这条简单等式把扩张向量的元语言长度与 `domAt` 所见的集合论数码连接起来；在这个填充方向无须解码数码。

```agda
    numAt-fst : (j : ℕ) → fst (numAt j) ≡ # j
    numAt-fst j = refl
```

第三个见证是统一满足关系存放名字公式的键。由于 `formula t` 没有常元，`embed (formula t)` 只是把它看成常元字母表为 `A` 的成员类型的公式，并未实际引入任何常元。`keyIn Aʟ` 把所得公式键包装成可构造模型元素，得到 `keyAt t`。

```agda
    keyAt : Name → S
    keyAt t = keyIn Aʟ (embed (formula t))
```

包装后的键与码集接口所用的键具有同一底层集合。等式 `keyAt-fst` 精确断言 `fst (keyAt t)` 等于 `fst (keyS Aʟ (embed (formula t)))`。因此，后续隶属与图的论证可以把抽象模型元素放入位置，同时用 `keyS` 给出的具体有序对码进行推理。

```agda
    keyAt-fst : (t : Name)
              → fst (keyAt t) ≡ fst (keyS Aʟ (embed (formula t)))
    keyAt-fst t = keyIn≡ Aʟ (embed (formula t))
```

同一个键还被证明属于 `AllCodes Aʟ`。这项隶属是语义条件，并非多余的簿记：满足关系图只在真实公式键处必须具有预期取值，而它在码域之外如何取值并不重要。因此，正是 `keyAt-∈` 使表在 `keyAt t` 处的取值可以被读成名字 `t` 的公式之满足关系。

```agda
    keyAt-∈ : (t : Name) → ⟨ keyAt t ∈ˢ AllCodes Aʟ ⟩
    keyAt-∈ t = keyIn∈ Aʟ (embed (formula t))
```

第四个见证是统一满足关系表在这个真实键处选定的取值。`Table.val Aʟ Aʟ` 同时接受该键及其属于码域的证明，并返回一个可构造模型元素。稍后，`val-sat` 将把它的底层集合认作所有满足 `embed (formula t)` 的 `A` 上编码环境之集；此处的 `valAt` 记录这次认同所需的表查询。

```agda
    valAt : Name → S
    valAt t = Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t)
```

由于 `valAt t` 就由这次表查询定义，`valAt-val` 以自反性成立。把这条等式显式列出，使指称论证可以在第四个具名见证与关于 `Table.val` 的一般定理之间直接转换。至此，四个构造恰好给出 `DenoteOf` 所绑定的见证：扩张环境、其长度数码、一个真实公式键，以及表在该键处的取值。

```agda
    valAt-val : (t : Name) → valAt t ≡ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t)
    valAt-val t = refl
```

## 一个名字的公式之键是什么

为了比较描述所造的键与表所用的键，先考察常元改名对无参公式的作用。公式 `χ` 的常元取自空类型。把它直接嵌入外围宇宙，与先嵌入载体、再把载体成员映入宇宙，所用的都是以空类型为定义域的函数。函数外延性使这两个函数相等，`mapFo` 的复合律随即给出 `sameEmbed χ`。这是关于空常元字母表的事实，并不是说任意公式经任意常元改名后都不变。

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

一条具有 `m` 个变元位置的公式，其表键是一个有序对：数码 `# m` 与常元映入外围宇宙后所得公式的码。由 `sameEmbed`，这条改名后的公式就是 `χ` 的直接嵌入，而其码正是 `limitCode χ` 的底层集合。对编码操作使用同余，便得到 `keyCode`。对名字而言，`m = suc (arity t)`；因此，这条等式恰好把表键与「扩张环境的长度、骨架码」组成的对对齐。

```agda
    keyCode : ∀ {m} (χ : Formula (⊥* {ℓ}) m)
            → fst (keyS Aʟ (embed χ)) ≡ pr (# m) (fst (limitCode χ))
    keyCode χ = cong (λ u → pr (# _) VCode.⌜ u ⌝) (sameEmbed χ)
```

指称证明还需要参数环境的两种等价呈现。族 `pfam t` 把每个有穷序号送到相应参数的底层外围集合。另一种呈现先把命名模块的嵌入 `NM.DA.ι` 逐项作用于 `params t`，得到模型元素向量，再取其典范图 `envGraph Aʟ`。向量映射的查取律逐点认同两边的取值；函数外延性与 `env` 的同余随即给出 `valuesOf t`，即两张环境图的相等。

```agda
    valuesOf : (t : Name)
             → env (pfam t) ≡ envGraph Aʟ (map NM.DA.ι (params t))
    valuesOf t = cong env (funExt (λ i →
      sym (cong fst (lookup-map NM.DA.ι (params t) i))))
```

扩张环境的每个条目都可构造。序号 `i : Fin (suc (arity t))` 选中候选元素或某个参数；无论哪种情形，`lookup i (environment t m)` 都已携带其底层集合属于 `A` 的证明。由于 `A` 可构造，可构造性的传递性给出 `valuesL t m i`。`domAt` 检查扩张环境的定义域时，所需的逐点可构造性前提正由这项事实提供。

```agda
    valuesL : (t : Name) (m : ⟪ A ⟫) (i : Fin (suc (arity t)))
            → ⟨ isL (values Aʟ (environment t m) i) ⟩
    valuesL t m i =
      isL-trans (snd (lookup i (environment t m))) pA
```

## 指称，两个方向

在把指称隶属与对象语言条款相比较之前，先要知道 `denote t` 的每个成员都属于载体。属于这个指称，仅仅给出一个载体序号 `mm`，其扩张环境满足公式，并给出所表示的载体成员到外围集合 `y` 的一条路径。这个见证位于命题截断之下，但目标 `y ∈ A` 本身是命题，所以 `PT.rec` 可以使用该见证，而不选出或保留某个序号。这里同样没有命题降级。

```agda
  private
    denoteMem : (t : Name) (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ A ⟩
    denoteMem t y = PT.rec (snd (y ∈ A)) step
      where
      step : Σ[ p ∈ Σ[ mm ∈ ⟪ A ⟫ ] ⟨ NM.satAt t mm ⟩ ] (⟪ A ⟫↪ (p .fst) ≡ y)
```

在获准的截断消去内部，恢复所得资料是一对 `p` 与一条等式 `q`。`p` 的第一分量是 `A` 的一个具体成员序号，因而典范的小隶属见证经 `∈∈ₛ` 转换后，证明其嵌入像属于 `A`。沿 `q` 搬运这项隶属，即得 `y ∈ A`。论证只使用成员关系的呈现，以及目标为命题这一事实；它既不引入选择函数，也不增加新的经典步骤。

```agda
           → ⟨ y ∈ A ⟩
      step (p , q) = subst (λ u → ⟨ u ∈ A ⟩) q
        (∈∈ₛ {a = ⟪ A ⟫↪ (p .fst)} {b = A} .snd (∈ₛ⟪ A ⟫↪ (p .fst)))
```

模块 `Named` 现在固定若干位置，以便把 `NameAt` 的四项资料与一个元语言名字比较：载体 `B`、载体码集 `C`、空字母表码集 `C₀`、骨架 `s`、元数 `a`、参数图 `e` 及指称 `d`。载体等式 `qB` 是完整模型元素的相等，连同其可构造性证明；`qC` 与 `q₀` 则只认同底层集合。这一区别由后续用途决定：下面的公式以位置 `B` 中模型元素的成员类型为类型，而 `C` 与 `C₀` 中的码集隶属只考察底层集合。

```agda
  module Named {n : ℕ} (B C C₀ s a e d : Fin n) (γ : S ^ n)
               (qB : lookup B γ ≡ Aʟ)
               (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ))
               (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where
    private
```

缩写 `Fo` 把公式对载体的这项依赖单独列出。对模型元素 `X` 与元数 `j`，`Fo X j` 是常元取自小成员类型 `⟪ fst X ⟫` 的公式类型。因此，在位置所存载体上读取的公式，从语义比较开始之前就具有正确类型；事后只凭底层集合的相等，不能替换这一依值载体。

```agda
      Fo : S → ℕ → Type ℓ
      Fo X j = Formula ⟪ fst X ⟫ j
```

对名字 `t`，先把无参公式 `formula t` 嵌入常元可取自固定载体 `A` 之成员的公式；原常元域为空，所以这一步没有增加实际参数。随后沿 `sym qB` 把它的类型从 `Fo Aʟ` 搬到 `Fo (lookup B γ)`，得到 `ψAt t`。这次搬运之所以成立，是因为 `qB` 认同完整的载体元素。至此，这条相对于位置的公式，其键与满足关系取值便可同上文固定载体上的构造比较。

```agda
      ψAt : (t : Name) → Fo (lookup B γ) (suc (arity t))
      ψAt t = subst (λ X → Fo X (suc (arity t))) (sym qB) (embed (formula t))
```

描述所用的公式先从固定载体 `Aʟ` 搬运到位置 `B` 所存的载体。公式的类型本身依赖载体，所以 `qB` 必须认同完整的带证明载体，而不只认同其底层集合。对 `qB` 作路径归纳即可证明：形成码集之键与这次搬运相交换。因此，在位置载体处由 `ψAt t` 算出的键，与在 `Aʟ` 处由 `embed (formula t)` 算出的键，是同一个集合。

```agda
      keyψ : (t : Name)
           → fst (keyS (lookup B γ) (ψAt t))
           ≡ fst (keyS Aʟ (embed (formula t)))
      keyψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ)
        (λ X ψ → fst (keyS X ψ)) (sym qB) (embed (formula t)))
```

统一满足关系的取值也有同样的依赖。在位置载体处，所需集合是先把已搬运公式的常元改名到该载体，再对所得公式施用 `Sat`；在 `Aʟ` 处，则对相应改名后的嵌入公式施用 `Sat`。沿 `qB` 的代入与这整个构造相交换，所以两个满足关系集的底层集合相等。

```agda
      satψ : (t : Name)
           → fst (Sat (lookup B γ) (mapFo (asConst (lookup B γ)) (ψAt t)))
           ≡ fst (Sat Aʟ (mapFo (asConst Aʟ) (embed (formula t))))
      satψ t = sym (constSubstCommSlice (λ X → Fo X (suc (arity t))) (V ℓ)
        (λ X ψ → fst (Sat X (mapFo (asConst X) ψ)))
```

路径归纳原理的最后一个实参就是嵌入后的公式本身。由此 `satψ` 得证，过程中没有作任何独立的语义选择：这条等式只来自在依值构造中代入载体。`keyψ` 与 `satψ` 合在一起，使后面的指称论证可以在位置载体与 `Aʟ` 之间往返，同时保持公式键及其满足关系集对齐。

```agda
        (sym qB) (embed (formula t)))
```

对一条固定的元语言名字 `t`，`Data t` 记录表示它所需的四条位置等式：骨架位置含有 `codeOf t` 的底层集合，元数位置含有 `# (arity t)`，参数位置含有环境图 `env (pfam t)`，指称位置含有 `denote t`。这四条等式恰与 `NameAt` 的四个概念性合取项相呼应。它们只断言当前诸位置与这条特定名字对齐，并不断言具有同一指称的所有名字都是唯一的。

```agda
    Data : Name → Type (ℓ-suc ℓ)
    Data t = (fst (lookup s γ) ≡ fst (codeOf t))
           × ( (fst (lookup a γ) ≡ # (arity t))
             × ( (fst (lookup e γ) ≡ env (pfam t))
               × (fst (lookup d γ) ≡ denote t) ) )
```

为了比较指称条款与 `denote t`，模块 `Body` 固定 `t` 以及 `Data t` 的前三个分量。骨架等式 `qs` 对齐公式键，参数等式 `qe` 对齐参数图；元数等式 `qa` 则记录同一名字余下的位置对齐。名字 `t` 固定以后，指称论证直接以 `suc (arity t)` 取得扩张环境的长度。私有向量 `δp` 把参数呈现在满足关系桥所需的限制语义载体中。

```agda
    module Body (t : Name) (qs : fst (lookup s γ) ≡ fst (codeOf t))
                (qa : fst (lookup a γ) ≡ # (arity t))
                (qe : fst (lookup e γ) ≡ env (pfam t)) where
      private
        δp : Vec NM.DA.SM (arity t)
```

名字的参数本来就属于小成员类型 `⟪ A ⟫`。逐项施用 `NM.DA.ι` 并非只保留这些索引，而是把每个索引所表示的集合与其属于 `A` 的证明配在一起，形成限制模型载体 `NM.DA.SM` 的元素。所得向量 `δp` 的长度为 `arity t`，因而恰是名字公式求值时所用内层环境的尾部。

```agda
        δp = map NM.DA.ι (params t)
```

位置等式 `qe` 通过外围参数族 `pfam t` 描述同一组参数，而满足关系桥需要的是限制载体向量 `δp` 的图。等式 `valuesOf t` 逐项认同这两种表示；将它与 `qe` 复合便得到 `qd'`，即参数位置所含的正是 `envGraph Aʟ δp`。这一形式既用于构造扩张环境，也用于稍后识别任意给出的扩张环境。

```agda
        qd' : fst (lookup e γ) ≡ envGraph Aʟ δp
        qd' = qe ∙ valuesOf t
```

指称载荷的第四项条件用于认同其键。从封印元素 `keyAt t` 出发，`keyAt-fst` 暴露嵌入公式的码集之键，`keyCode` 再把该键算成 `# (suc (arity t))` 与公式极限层码的有序对。骨架等式 `qs` 把第二个分量替换成位置 `s` 中的集合。余下的一步，是通过封印的长度数码表示第一个分量。

```agda
        qkey : fst (keyAt t)
             ≡ pr (fst (numAt (suc (arity t)))) (fst (lookup s γ))
        qkey = keyAt-fst t ∙ keyCode (formula t)
             ∙ cong (pr (# (suc (arity t)))) (sym qs)
             ∙ cong (λ u → pr u (fst (lookup s γ)))
```

最后一次同余反向使用 `numAt-fst`，在有序对中把集合论数码替换成 `numAt (suc (arity t))` 的底层集合。完成后的 `qkey` 因而恰具 `DenoteOf` 所需的形式：所选的键是所选定义域数码与骨架位置组成的对。反向证明将从载荷自带的键等式重新构造同一次计算。

```agda
                 (sym (numAt-fst (suc (arity t))))
```

正向先给定一个实际成员 `m : ⟪ A ⟫`、一个与它表示同一底层集合的外围元素 `z`，以及该集合属于 `denote t` 的证明。随后按语义次序给出 `DenoteOf` 的四个见证：把 `m` 添到诸参数之前所得的环境、该环境的长度数码、公式键，以及表在该键处的取值。六项条件把这些见证连在一起。前五项说明它们的形状与对齐关系，第六项则把所设的指称成员资格转换成环境对表取值的成员资格。

```agda
      denote-fill : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z
                  → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩ → DenoteOf B C s e γ z
      denote-fill z m qm hz =
        envAt t m , (numAt (suc (arity t)) , (keyAt t , (valAt t
        , ( hcons , (hdom , (hkey , (qkey , (hgraph , hmem))))))))
```

第一项条件说明，所选环境由候选成员添入参数环境而得。`consAtL` 的向内读式接收三条等式：`qd'` 给出原参数图，`sym qm` 认同位置 `z` 中的候选集合，`envAt-fst t m` 给出新构造的环境图。由此即可证明对象语言中的扩张公式。这保证公式求值时，额外的变元位置由候选成员占据，其后依次是原有参数。

```agda
        where
        hcons : ⟨ (envAt t m ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
        hcons = consAtL-in Aʟ δp (NM.DA.ι m) (envAt t m ∷ z ∷ γ)
                  zero (suc zero) (sh2 e) qd' (sym qm) (envAt-fst t m)
```

第二项条件固定扩张环境的定义域。其长度为 `suc (arity t)`：一个位置留给候选成员，随后是 `arity t` 个参数位置。`domAt` 的向内充分性引理接收 `environment t m` 的底层取值，以及每个取值皆可构造的证明。后一事实来自这些值属于可构造载体，以及 `L` 的传递性。

```agda
        hdom : ⟨ (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ)
                 ⊨ domAt (suc zero) zero ⟩
        hdom = domAt-fill (suc zero) zero
                 (numAt (suc (arity t)) ∷ envAt t m ∷ z ∷ γ)
                 (suc (arity t)) (values Aʟ (environment t m)) (valuesL t m)
```

同一条定义域引理还必须把所选见证看成它要比较的底层集合。等式 `envAt-fst t m` 暴露 `envAt t m` 的环境图，而 `numAt-fst (suc (arity t))` 暴露长度见证之下预期的 von Neumann 数码。有了这两条投影等式，定义域公式所陈述的就恰是：该数码编码所选环境的长度。

```agda
                 (envAt-fst t m) (numAt-fst (suc (arity t)))
```

第三项条件把所选键放入真正的码定义域。构造 `keyAt` 已经给出该键属于 `AllCodes Aʟ`；位置等式 `qC` 再把这一成员资格搬运到位置 `C` 所存的集合中。这项假设不可省略：满足关系图在真实公式键处必须给出公式的语义取值，而在码定义域之外，它的行为无须确定这样的取值。

```agda
        hkey : ⟨ fst (keyAt t) ∈ fst (lookup C γ) ⟩
        hkey = subst (λ u → ⟨ fst (keyAt t) ∈ u ⟩) (sym qC) (keyAt-∈ t)
```

第五项条件说明，所选取值正是满足关系图在所选键处容许的取值。求值该图公式时，外围赋值之前已经依次压入五项：取值、键、长度数码、扩张环境与候选成员。第一条对齐假设把 `keyAt t` 的底层集合认同为位置载体处 `ψAt t` 的键；先前的 `keyψ` 正是在这里把键的计算沿 `qB` 搬过载体边界。

```agda
        hgraph : ⟨ (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m
                    ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
        hgraph = graphAt-value (sh5 B) (suc zero) zero
                   (valAt t ∷ keyAt t ∷ numAt (suc (arity t)) ∷ envAt t m
                    ∷ z ∷ γ) (ψAt t)
```

第二条对齐假设认同所选取值。首先，`valAt-val` 把它暴露为表在 `keyAt t` 处的取值；定律 `val-at` 把该表取值认同为嵌入公式在 `Aʟ` 上的 `Sat` 集；最后按所需方向读取 `satψ`，把这个集合搬运到位置载体。有了两条对齐等式，`graphAt-value` 便可证明图条件，同时保持公式键及其语义取值不变。

```agda
                   (keyAt-fst t ∙ sym (keyψ t))
                   ( cong fst (valAt-val t)
                   ∙ cong fst (val-at Aʟ Aʟ (embed (formula t))
                                 (keyAt t) (keyAt-∈ t) (keyAt-fst t))
                   ∙ sym (satψ t) )
```

第六项条件是决定性的成员关系：编码后的扩张环境必须属于所选的图取值。假设说由 `m` 表示的成员属于 `denote t`。刻画式 `NM.denote-mem t m` 把它化为内层满足关系，即 `environment t m` 满足 `embed (formula t)`。因此，指称成员资格恰好给出统一满足关系表所要记录的语义事实。

```agda
        hmem : ⟨ fst (envAt t m) ∈ fst (valAt t) ⟩
        hmem = subst (λ u → ⟨ envAt t m ∈ˢ u ⟩) (sym (valAt-val t)) inTable
          where
          inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩
          inner = subst ⟨_⟩ (NM.denote-mem t m) hz
```

定律 `val-sat` 把这项内层满足关系认同为 `envAt t m` 属于表在 `keyAt t` 处的取值；此处证明从满足关系出发，所以反向读取该定律。随后沿 `valAt-val` 搬运，把显式的表取值替换成封印见证 `valAt t`。第六项条件由此得证，`denote-fill` 也随之完成：四个见证及其间的六项关系，全都来自名字 `t` 的数据与所设的指称成员资格。

```agda
          inTable : ⟨ envAt t m ∈ˢ Table.val Aʟ Aʟ (keyAt t) (keyAt-∈ t) ⟩
          inTable = subst ⟨_⟩
            (sym (val-sat Aʟ (embed (formula t)) (keyAt t) (keyAt-∈ t)
                    (keyAt-fst t) (environment t m) (envAt t m)
                    (envAt-fst t m))) inner
```

反向设已经给出 `z` 处的一份显式 `DenoteOf` 载荷，即四个被绑定元素连同上述六项条件。目标是证明由 `z` 表示的成员 `m` 属于 `denote t`。按 `NM.denote-mem` 的反向读式，只需重建嵌入公式在 `environment t m` 处的内层满足关系。余下诸等式将依次识别载荷任意给出的环境、数码、键与取值。

```agda
      denote-read : (z : S) (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ≡ fst z
                  → DenoteOf B C s e γ z → ⟨ ⟪ A ⟫↪ m ∈ denote t ⟩
      denote-read z m qm (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
        = subst ⟨_⟩ (sym (NM.denote-mem t m)) inner
        where
```

首先读取扩张条件。它的向外充分性定理比较原图 `qd'`、候选成员等式 `sym qm` 与满足证明 `hc`，由此推出任意见证 `c` 的底层集合恰为 `envGraph Aʟ (environment t m)`。因此，第一个存在见证不只是参数图的某个扩张；它正是把 `m` 放在名字 `t` 的诸参数之前所得典范环境的图。

```agda
        qcg : fst c ≡ envGraph Aʟ (environment t m)
        qcg = consAtL-out Aʟ δp (NM.DA.ι m) (c ∷ z ∷ γ)
                zero (suc zero) (sh2 e) qd' (sym qm) hc
```

定义域条件继而确定数码见证。由于 `qcg` 已把 `c` 认同为 `environment t m` 的图，`domAt-numeral` 可把 `hk` 读成一条等式：`k` 的底层集合等于该环境长度的数码。此长度为 `suc (arity t)`，而 `valuesL` 提供定义域充分性定理所需的可构造性。因此得到 `fst k ≡ # (suc (arity t))`。

```agda
        qk : fst k ≡ # (suc (arity t))
        qk = domAt-numeral (suc zero) zero (k ∷ c ∷ z ∷ γ) (suc (arity t))
               (values Aʟ (environment t m)) (valuesL t m) qcg hk
```

载荷的第四项条件 `hp` 说明，它的键是自身定义域见证 `k` 与骨架位置组成的对。用 `qk` 改写第一个分量、用 `qs` 改写第二个分量，便得到 `# (suc (arity t))` 与公式码之对。最后反向读取 `keyCode (formula t)`，把这一对识别为 `embed (formula t)` 的码集之键。所得等式 `qkey'` 因而把载荷任意给出的键认同为真正的公式键。

```agda
        qkey' : fst key ≡ fst (keyS Aʟ (embed (formula t)))
        qkey' = hp ∙ cong (λ u → pr u (fst (lookup s γ))) qk
              ∙ cong (pr (# (suc (arity t)))) qs ∙ sym (keyCode (formula t))
```

成员条件 `hi` 说明这个已恢复的键属于位置 `C` 所存的集合。沿 `qC` 搬运后，它成为对 `AllCodes Aʟ` 的成员资格，即 `key∈`。这是一份成员证明，并非选择一个新键：该键早已由 `DenoteOf` 载荷给出，并经 `qkey'` 得到认同。它的作用是把这个键放入统一表与满足关系图具有语义规格的定义域中。

```agda
        key∈ : ⟨ key ∈ˢ AllCodes Aʟ ⟩
        key∈ = subst (λ u → ⟨ fst key ∈ u ⟩) qC hi
```

最后还须认同任意给出的取值见证 `v`。先用 `qkey'` 与 `keyψ` 把它的键同位置载体处 `ψAt t` 的键对齐，图证明 `hg` 便可交给唯一性读式 `graphAt-only`，从而先把 `fst v` 认同为相应的 `Sat` 集。搬运等式 `satψ` 把该集合送回 `Aʟ`，再反向读取 `val-at`，将它认同为 `Table.val Aʟ Aʟ key key∈`。于是 `qval` 恢复出所需的表取值，使下一步能够把末尾成员关系 `hm` 转成内层满足关系。

```agda
        qval : fst v ≡ fst (Table.val Aʟ Aʟ key key∈)
        qval = graphAt-only (sh5 B) (suc zero) zero
                 (v ∷ key ∷ k ∷ c ∷ z ∷ γ) (ψAt t) (qkey' ∙ sym (keyψ t)) hg
             ∙ satψ t
             ∙ sym (cong fst (val-at Aʟ Aʟ (embed (formula t)) key key∈ qkey'))
```

`DenoteOf` 的最后一个分量说，扩张环境 `c` 属于恢复出的取值 `v`。路径 `qval` 把这个取值认作统一满足表在恢复出的公式码键处的表值。沿该路径迁移隶属关系，便得到下一条语义读式所需的表隶属。

```agda
        inTable : ⟨ c ∈ˢ Table.val Aʟ Aʟ key key∈ ⟩
        inTable = subst (λ u → ⟨ fst c ∈ u ⟩) qval hm
```

充分性等式 `val-sat` 随即把对该表值的隶属读作对嵌入公式的满足。它的假设以 `qkey'` 认定恢复出的键，并以 `qcg` 把 `c` 认作扩张环境的图。因此，`inner` 断言 `environment t m` 满足名字 `t` 的公式；外层结果再反向使用 `denote-mem`，得到对 `denote t` 的隶属。

```agda
        inner : ⟨ NM.DA._⊨ᵐ_ (environment t m) (embed (formula t)) ⟩
        inner = subst ⟨_⟩
          (val-sat Aʟ (embed (formula t)) key key∈ qkey'
             (environment t m) c qcg) inTable
```

前面的读式以载体成员 `m` 为对象。引理 `member-fill` 把正向读式改写到任意可构造元素 `z` 上：若其底集属于 `denote t`，便可同时得到它对载体位置的隶属以及完整的见证组 `DenoteOf`。第一项结论先在集合 `A` 中取得，再沿位置等式 `qB` 迁移。

```agda
      member-fill : (z : S) → ⟨ fst z ∈ denote t ⟩
                  → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z
      member-fill z hz = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (cong fst qB)) hA
        , denote-fill z (fib .fst) (fib .snd)
            (subst (λ u → ⟨ u ∈ denote t ⟩) (sym (fib .snd)) hz)
```

要应用成员层面的引理，必须先恢复 `z` 所表示的载体成员。包含引理 `denoteMem` 先把对指称的隶属变成对 `A` 的隶属。随后，隶属关系的纤维表示给出 `m : ⟪ A ⟫` 以及等式 `⟪ A ⟫↪ m ≡ fst z`；这是普通的依赖数据，不涉及选择原理或命题截断的消去。

```agda
        where
        hA : ⟨ fst z ∈ A ⟩
        hA = denoteMem t (fst z) hz
        fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z)
        fib = ∈-asFiber {a = fst z} {b = A} hA
```

反向改写从 `z` 对载体位置的隶属以及一组 `DenoteOf` 数据出发。恢复出它所表示的载体成员之后，前面的引理 `denote-read` 把该数据组读成嵌入成员对 `denote t` 的隶属。最后沿纤维等式迁移，便得到 `fst z` 对该指称的隶属。

```agda
      member-read : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩
                  → DenoteOf B C s e γ z → ⟨ fst z ∈ denote t ⟩
      member-read z hz hDen = subst (λ u → ⟨ u ∈ denote t ⟩) (fib .snd)
        (denote-read z (fib .fst) (fib .snd) hDen)
        where
```

这里所需的纤维来自载体位置的隶属假设。等式 `qB` 把该位置的底集与 `A` 认同，所以迁移后先得到 `fst z ∈ A`；`∈-asFiber` 再给出 `⟪ A ⟫` 中对应的成员及其嵌入等式。因此，这两条成员引理适用于模型中满足相应隶属假设的每个元素，而不要求输入预先以小载体类型中的成员给出。

```agda
        fib : Σ[ mm ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ mm ≡ fst z)
        fib = ∈-asFiber {a = fst z} {b = A}
          (subst (λ u → ⟨ fst z ∈ u ⟩) (cong fst qB) hz)
```

## 一个名字，装配起来

对于固定名字 `t`，`Data t` 记录四条等式：骨架位置是其公式码，元数位置是其数码，环境位置是其参数图，指称位置是 `denote t`。`NameAt-fill` 用这些等式证明 `NameAt` 的四个概念合取项：公式无常元、元数属于 `ω`、参数满足环境条件，以及指称的外延刻画。最后一个合取项由成员关系的两个方向 `into` 与 `back` 给出。

```agda
    NameAt-fill : (t : Name) → Data t → ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩
    NameAt-fill t (qs , (qa , (qe , qd))) =
      NameAt-in B C C₀ s a e d γ hf ha he into back
      where
      module Bt = Body t qs qa qe
```

第一个合取项来自名字 `t` 所携带的实际无参公式。该公式有 `suc (arity t)` 个变量位置，而 `qs` 把它在极限层中的码与骨架位置认同。再用 `qa` 认定元数位置、用 `q₀` 认定空字母表的码集，`codeFree-in` 就把这条公式及其码等式转成对 `FreeAt` 的满足。

```agda
      hf : ⟨ γ ⊨ FreeAt C₀ s a ⟩
      hf = codeFree-in C₀ s a γ (arity t) q₀ qa (formula t) qs
```

元数合取项只要求对 `ω` 的隶属。典范事实 `#∈ω (arity t)` 给出该数码对 `ω` 的隶属，等式 `qa` 再把它迁移到元数位置所存的值上。这部分描述不使用任何比较关系。

```agda
      ha : ⟨ fst (lookup a γ) ∈ ω ⟩
      ha = subst (λ u → ⟨ u ∈ ω ⟩) (sym qa) (#∈ω (arity t))
```

对于环境合取项，把名字 `t` 的参数向量看作族 `i ↦ lookup i (params t)`。它的图等式是 `qe`，定义域数码的等式是 `qa`，而 `qB` 把余域载体认作 `Aʟ`。`paramSeq-in` 将这个族的标准环境性质迁移到三个位置上，从而得到对 `envOverAt` 的满足。

```agda
      he : ⟨ γ ⊨ envOverAt e a B ⟩
      he = paramSeq-in e a B γ (arity t) (λ i → lookup i (params t)) qe qa
             (cong fst qB)
```

指称外延合取项的正向从指称位置的一个成员出发。沿 `qd` 迁移后，它成为 `denote t` 的成员。随后，`Bt.member-fill` 恰好给出指称公式体的两部分：对载体位置的隶属以及见证组 `DenoteOf`。

```agda
      into : (z : S) → ⟨ fst z ∈ fst (lookup d γ) ⟩
           → ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z
      into z hz = Bt.member-fill z (subst (λ u → ⟨ fst z ∈ u ⟩) qd hz)
```

反过来，`Bt.member-read` 把载体隶属与 `DenoteOf` 合在一起读作对 `denote t` 的隶属。再沿 `qd` 的逆向迁移，便把该元素放回指称位置。这两个函数正是 `NameAt` 中同一个外延合取项所需的两个方向。

```agda
      back : (z : S) → ⟨ fst z ∈ fst (lookup B γ) ⟩ → DenoteOf B C s e γ z
           → ⟨ fst z ∈ fst (lookup d γ) ⟩
      back z hzB hDen = subst (λ u → ⟨ fst z ∈ u ⟩) (sym qd)
        (Bt.member-read z hzB hDen)
```

`NameAt` 的反向读式只返回「一个名字及其四条数据等式」的命题截断。元数合取项 `ha` 是对 `ω` 的隶属；其语义表示在命题截断下给出自然数 `k`，并给出把元数位置认作 `# k` 的等式。由于最终结果本身也是一个命题截断类型，`PT.rec` 可以在构造该结果时使用这个见证。

```agda
    NameAt-read : ⟨ γ ⊨ NameAt B C C₀ s a e d ⟩ → ∥ Σ[ t ∈ Name ] Data t ∥₁
    NameAt-read (hf , (ha , (he , hd))) =
      PT.rec squash₁ atArity ha
      where
      atCode : (k : ℕ) (qa : fst (lookup a γ) ≡ # k)
```

固定 `k` 与元数等式 `qa` 后，`codeFree-out` 读取无常元合取项。它仍在命题截断下给出公式 `χ : Formula ⊥* (suc k)`，以及从骨架位置到该公式极限层码的等式 `qs`。在这个分支内，`atCode` 装配名字及其数据，其中 `qs` 是第一条等式，`qa` 是第二条。

```agda
             → Σ[ χ ∈ Formula (⊥* {ℓ}) (suc k) ]
                 (fst (lookup s γ) ≡ fst (limitCode χ))
             → Σ[ t ∈ Name ] Data t
      atCode k qa (χ , qs) = t , (qs , (qa , (qe , qd)))
        where
```

元数确定后，参数分量可以直接恢复。`paramSeq-out` 以 `qa` 与载体等式 `qB` 读取 `he`，得到 `⟪ A ⟫` 中长度为 `k` 的向量；该向量与 `k`、`χ` 一起定义名字 `t`。向量层面的恢复不带命题截断，但整个构造仍处于元数读式与公式读式引入的截断之内。

```agda
        t : Name
        t = k , (χ , paramSeq-out e a B γ k qa (cong fst qB) he)
```

恢复出的向量还必须满足 `Data t` 所记录的环境等式。配套引理 `paramSeq-graph` 断言，原环境位置恰等于该向量的编码图 `env (pfam t)`。这条路径就是第三条数据等式 `qe`。

```agda
        qe : fst (lookup e γ) ≡ env (pfam t)
        qe = paramSeq-graph e a B γ k qa (cong fst qB) he
```

局部模块 `Bt` 在恢复出的名字及其前三条数据等式 `qs`、`qa`、`qe` 处实例化指称公式体的读式。因此，`Data t` 尚缺的分量是指称位置与 `denote t` 之间的集合等式。下面通过双向比较两者的成员来证明它。

```agda
        module Bt = Body t qs qa qe
```

先证正向包含。设 `y` 属于指称位置。该位置是模型元素，所以由 `L` 的传递性可知 `y` 可构造，从而能把它包装为 `z : S`。向外读取外延合取项 `hd`，得到载体隶属以及经过命题截断的 `DenoteOf` 见证。目标 `y ∈ denote t` 是命题，因此 `PT.rec` 可以对该见证的任一代表应用 `Bt.member-read`。

```agda
        fwd : (y : V ℓ) → ⟨ y ∈ fst (lookup d γ) ⟩ → ⟨ y ∈ denote t ⟩
        fwd y hy = PT.rec (snd (y ∈ denote t))
          (Bt.member-read z (body .fst)) (body .snd)
          where
          z : S
```

`body` 经过两步语义读取而得。首先，`extAt-out` 把对指称位置的隶属变成对 `DenoteBody` 的满足；随后，`DenoteBody-out` 读出其中的载体合取项，以及汇集在 `DenoteOf` 中的四个存在见证。按照存在量词的语义，这些见证仍处于命题截断之下，并且只在上面的命题值隶属证明内部使用。

```agda
          z = y , isL-trans hy (snd (lookup d γ))
          body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × ∥ DenoteOf B C s e γ z ∥₁
          body = DenoteBody-out B C s e γ z
                   (extAt-out d (DenoteBody B C s e) γ hd z hy)
```

反向包含从 `y ∈ denote t` 出发。证明先把 `y` 看作元素 `z : S`，再用 `Bt.member-fill` 构造 `z` 处的指称公式体。引入引理 `DenoteBody-in` 与 `extAt-in` 依次重建公式体的满足，最后得到对指称位置的隶属。

```agda
        bwd : (y : V ℓ) → ⟨ y ∈ denote t ⟩ → ⟨ y ∈ fst (lookup d γ) ⟩
        bwd y hy = extAt-in d (DenoteBody B C s e) γ hd z
          (DenoteBody-in B C s e γ z (body .fst) (body .snd))
          where
          z : S
```

`z` 的可构造性来自两项已有事实：`denoteMem` 把 `denote t` 的每个成员放入 `A`，而 `pA` 说明 `A` 可构造。对于这个 `z`，`Bt.member-fill` 给出载体隶属和一组未截断的 `DenoteOf` 数据。因此，反向包含不需要消去任何命题截断。

```agda
          z = y , isL-trans (denoteMem t y hy) pA
          body : ⟨ fst z ∈ fst (lookup B γ) ⟩ × DenoteOf B C s e γ z
          body = Bt.member-fill z hy
```

对于每个集合 `y`，函数 `fwd y` 与 `bwd y` 给出两个隶属命题之间的双向蕴涵。由于两边都是命题，`⇔toPath` 把这对蕴涵变成真值的相等。`V` 的外延性再把逐点的隶属相等变成 `fst (lookup d γ) ≡ denote t`，即第四条等式 `qd`。

```agda
        qd : fst (lookup d γ) ≡ denote t
        qd = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
```

分支 `atArity` 在不选择全局见证的前提下处理两层截断。它的输入把元数表示为一个提升后的自然数；反转 `qk` 后便得到 `atCode` 所需的等式。随后，`codeFree-out` 在命题截断下给出公式及其码等式，`PT.map` 则在该截断内部应用 `atCode`。所得结论仅仅断言存在一个满足全部四条数据等式的名字，这正是 `NameAt-read` 的余域。

```agda
      atArity : Σ[ lk ∈ Lift {ℓ-zero} {ℓ} ℕ ] (# (lower lk) ≡ fst (lookup a γ))
              → ∥ Σ[ t ∈ Name ] Data t ∥₁
      atArity (lk , qk) = PT.map (atCode (lower lk) (sym qk))
        (codeFree-out C₀ s a γ (lower lk) q₀ (sym qk) hf)
```

## 最小，描述出来与所指

最小名字公式量化一个竞争名字的三项描述数据。第一项包装元素 `codeEl t` 把名字 `t` 的公式码放入模型：`codeOf t` 属于极限层 `Lset ω`，而该层可构造，所以由 `L` 的传递性可知这个码也可构造。不透明定义只暴露底集等式 `codeEl-fst`；以后在某个具体竞争者处实例化全称子句时，满足关系的证明只需要这条等式。

```agda
  opaque
    codeEl : Name → S
    codeEl t = fst (codeOf t)
             , isL-trans (snd (codeOf t)) (snd (LsetS ω ω-ord))
```

元素 `codeEl t` 把名字的公式码带入模型。它的第一投影依定义就是`codeOf t` 的底层集合，因此实例化全称子句时所需的等式由自反性给出。第二投影中保存的可构造性证明不会改变这个码。

```agda
    codeEl-fst : (t : Name) → fst (codeEl t) ≡ fst (codeOf t)
    codeEl-fst t = refl
```

名字的参数资料由第二个模型元素表示。对 `t` 而言，族`i ↦ lookup i (params t)` 在它的 `arity t` 个位置逐一选出载体元素，`envS Aʟ` 再把这个族变成编码后的环境图。因此，`envEl t` 恰具有 `NameAt`的环境槽所要求的形式。

```agda
    envEl : Name → S
    envEl t = envS Aʟ (λ i → lookup i (params t))
```

展开环境包装便得到图 `env (pfam t)`，因为 `pfam t` 正是逐项读取`params t` 所得的族。因此 `envEl-fst` 同样由自反性证明。它与`codeEl-fst` 以及先前关于 `numAt` 的等式一起，给出把一条具体名字代入量化竞争者时所需的三条槽位等式。

```agda
    envEl-fst : (t : Name) → fst (envEl t) ≡ env (pfam t)
    envEl-fst t = refl
```

## 被描述的最小名字就是最小的名字

名字比较使用两个严格良序。记号 `_≺ˡ_` 表示公式码上的 `limitOrder`，`_≺ₚ_` 表示载体参数上给定的序 `w`。在 `_≺ₙ_` 中，先比较码，再比较元数，最后比较参数向量。只有第一键和第三键需要对象语言中的关系集；元数比较由数码隶属表达。

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

集合 `Rs` 与 `Ps` 在模型内部表示这两个序。对极限层元素 `u,v`，`Rrep`把有序对属于 `Rs` 读成 `u ≺ˡ v`，`Rfill` 则从该比较证明相应隶属。`Prep` 与 `Pfill` 对载体元素和 `Ps` 给出同样的两个方向。这四条表示律是充分性结果的假设。

```agda
  module Least (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 ⟩)
```

私有模块 `K` 把三键比较的充分性专门化到 `Rs`、`Ps` 及其表示律。它的 `order-in` 把元层名字比较的证明转成 `_≺At_` 的满足，`order-out`则在命题截断之下恢复该比较。下文会为所比较的具体名字提供码、数码和环境等式。

```agda
               where
    private
      module K = Keys Rs Ps Rrep Rfill Prep Pfill
```

模块 `Min` 固定最小名字公式使用的九个位置：两个关系 `R,P`、载体 `B`、两个码集 `C,C₀`、当前名字的码、元数与环境 `s,a,e`，以及它的指称 `d`。等式 `qR` 与 `qP` 认同关系的底层集合；`qB` 则是模型元素的等式，因为后续公式依赖于载体。等式 `qC` 认同载体上的码集之底层集合。

```agda
    module Min {n : ℕ} (R P B C C₀ s a e d : Fin n) (γ : S ^ n)
               (qR : fst (lookup R γ) ≡ fst Rs)
               (qP : fst (lookup P γ) ≡ fst Ps)
               (qB : lookup B γ ≡ Aʟ)
               (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ))
```

余下的等式 `q₀` 把 `C₀` 与空字母表上的码集之底层集合认同。固定 `qB`、`qC` 与 `q₀` 后，私有模块 `N` 在这里使用的各槽位上提供已经证明的 `NameAt`装填与读取原则。因此，最小名字的充分性可以把「当前资料构成一条名字」与附加的最小性断言分开处理。

```agda
               (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where
      private
        module N = Named B C C₀ s a e d γ qB qC q₀
```

对名字 `t`，`IsMin t` 断言没有更早的名字指称槽 `d` 中的集合。给定任意竞争者 `t'`，若有等式把该槽认作 `denote t'`，并有证明 `t' ≺ₙ t`，就必须导出矛盾。因此，只有指称同一给定集合的名字才是竞争者，而「更早」使用名字上的完整字典序。

```agda
      IsMin : Name → Type (ℓ-suc ℓ)
      IsMin t = (t' : Name) → fst (lookup d γ) ≡ denote t'
              → t' ≺ₙ t → Empty.⊥
```

谓词 `Least t` 把 `N.Data t` 与 `IsMin t` 配成一对。第一分量是四等式记录，把码、元数数码、参数环境和指称槽与 `t` 的资料认同；第二分量排除同一指称的每个更小名字。这正对应 `LeastNameAt` 的两个合取项：命名条件与全称最小性条件。

```agda
      Least : Name → Type (ℓ-suc ℓ)
      Least t = N.Data t × IsMin t
```

为装填 `LeastNameAt`，`N.NameAt-fill` 先从具体名字 `t` 与记录 `dt` 证明其命名合取项。余下的合取项是实现三层全称量词的函数。对任意集合 `s'`、`a'` 与`e'`，它假设三者描述一个指称同一 `d` 的竞争者，并假设该竞争者先于当前名字，然后必须导出矛盾。

```agda
      LeastAt-fill : (t : Name) → Least t
                   → ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩
      LeastAt-fill t (dt , mt) = N.NameAt-fill t dt , univ
        where
        univ : (s' a' e' : S)
```

加入竞争者的三项资料后，环境是 `e' ∷ a' ∷ s' ∷ γ`；因此三项分别位于零、一、二号槽，原有槽位都经 `sh3` 移位。第一个前提是竞争者的 `NameAt` 满足，并共享指称槽 `sh3 d`；第二个前提是从该竞争者到移位后当前三元组的 `_≺At_`满足。结果为 `Lift Empty.⊥`，即公式语义所需宇宙层级中的矛盾。

```agda
             → ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ NameAt (sh3 B) (sh3 C) (sh3 C₀)
                   (suc (suc zero)) (suc zero) zero (sh3 d) ⟩
             → ⟨ (e' ∷ a' ∷ s' ∷ γ) ⊨ ≺At (sh3 R) (sh3 P)
                   (suc (suc zero)) (suc zero) zero (sh3 s) (sh3 a) (sh3 e) ⟩
             → Lift {j = ℓ-suc ℓ} Empty.⊥
```

证明先把 `Named.NameAt-read` 施于竞争者的命名满足。所得结果是在命题截断之下的一条名字 `t'` 及其 `Named.Data` 记录中的四条等式。由于所需结果是作为命题的矛盾，`PT.rec` 可以消去该命题截断。这里没有选出或保留竞争者，恢复出的名字只在这次不可能性证明中使用。

```agda
        univ s' a' e' hn hlt = lift (PT.rec Empty.isProp⊥ step
          (Named.NameAt-read (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero))
             (suc zero) zero (sh3 d) (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ hn))
          where
          step : Σ[ t' ∈ Name ] Named.Data (sh3 B) (sh3 C) (sh3 C₀)
```

对恢复出的竞争者，四条资料等式依次命名为 `qs'`、`qa'`、`qe'` 与 `qd'`。最后一条说明共享的指称槽是 `denote t'`，所以 `mt t' qd'` 已可反驳任何`t' ≺ₙ t` 的证明。该比较本身也在命题截断之下取得；由于目标仍是矛盾，第二次`PT.rec` 可以消去这个命题截断。

```agda
                   (suc (suc zero)) (suc zero) zero (sh3 d)
                   (e' ∷ a' ∷ s' ∷ γ) qB qC q₀ t'
               → Empty.⊥
          step (t' , (qs' , (qa' , (qe' , qd')))) =
            PT.rec Empty.isProp⊥ (mt t' qd')
```

`K.order-out` 的调用给出被截断的比较。它使用关系等式 `qR,qP`、恢复出的竞争者之码、数码与环境等式、`dt` 中当前名字对应的三条等式，以及所设的满足 `hlt`。其结果是 `∥ t' ≺ₙ t ∥₁`；把它消去到 `mt t' qd'` 所给的矛盾，便完成全称最小性子句。

```agda
              (K.order-out (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
                 (sh3 s) (sh3 a) (sh3 e) (e' ∷ a' ∷ s' ∷ γ) t' t
                 qR qP qs' (dt .fst) qa' (dt .snd .fst)
                 qe' (dt .snd .snd .fst) hlt)
```

反过来，`LeastNameAt` 的满足分成命名证据 `hn` 与全称子句 `hu`。读取 `hn`得到 `∥ Σ[ t ∈ Name ] N.Data t ∥₁`。这里的映射保留外层命题截断，并为每个恢复出的 `t` 与 `dt` 补上 `IsMin t` 的证明。因此，`LeastAt-read` 只证明最小名字的命题截断存在。

```agda
      LeastAt-read : ⟨ γ ⊨ LeastNameAt R P B C C₀ s a e d ⟩
                   → ∥ Σ[ t ∈ Name ] Least t ∥₁
      LeastAt-read (hn , hu) = PT.map step (N.NameAt-read hn)
        where
        step : Σ[ t ∈ Name ] N.Data t → Σ[ t ∈ Name ] Least t
```

为证明 `IsMin t`，固定一个显式竞争者 `t'`、说明它指称槽 `d` 中集合的等式`qd'`，以及比较 `lt : t' ≺ₙ t`。全称子句 `hu` 在 `codeEl t'`、先前定义的`numAt (arity t')` 和 `envEl t'` 处实例化。因此，此处新定义的只有码与环境包装，数码包装是复用的。

```agda
        step (t , dt) = t , (dt , mt)
          where
          mt : IsMin t
          mt t' qd' lt = lower (hu (codeEl t') (numAt (arity t')) (envEl t')
            (Named.NameAt-fill (sh3 B) (sh3 C) (sh3 C₀) (suc (suc zero))
```

`hu` 的第一个前提由 `Named.NameAt-fill` 构造。等式 `codeEl-fst`、`numAt-fst` 与 `envEl-fst` 认同竞争者的三个资料槽，所设的 `qd'` 则认同共享的指称槽。第二个前提从 `K.order-in` 开始；它将把显式比较 `lt` 转成比较公式的满足。

```agda
               (suc zero) zero (sh3 d)
               (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) qB qC q₀ t'
               (codeEl-fst t' , (numAt-fst (arity t')
                              , (envEl-fst t' , qd'))))
            (K.order-in (sh3 R) (sh3 P) (suc (suc zero)) (suc zero) zero
```

`K.order-in` 的调用还接收 `dt` 中当前名字的三条等式以及关系等式 `qR,qP`，因而在扩张环境中证明 `hu` 所需的那条比较前提。施用 `hu` 得到被抬升的矛盾，`lower` 再把它带回 `IsMin` 所需的宇宙层级。这里的抬升与降位只处理宇宙安放，并不消去命题截断。

```agda
               (sh3 s) (sh3 a) (sh3 e)
               (envEl t' ∷ numAt (arity t') ∷ codeEl t' ∷ γ) t' t
               qR qP (codeEl-fst t') (dt .fst) (numAt-fst (arity t'))
               (dt .snd .fst) (envEl-fst t') (dt .snd .snd .fst) lt))
```

## 一步，描述出来与所指

模块 `Step` 保留同样的两个被表示关系、载体与码集，并加入被比较集合的槽 `x`与 `y`。五条等式的作用与 `Min` 中相同：`qR,qP` 解释两个关系槽，`qB` 以依值模型元素等式认同载体，`qC,q₀` 认同两个码集的底层集合。这里的局部陈述只比较`x` 与 `y` 的名字；它与层序的后续联系在本模块之外证明。

```agda
    module Step {n : ℕ} (R P B C C₀ x y : Fin n) (γ : S ^ n)
                (qR : fst (lookup R γ) ≡ fst Rs)
                (qP : fst (lookup P γ) ≡ fst Ps)
                (qB : lookup B γ ≡ Aʟ)
                (qC : fst (lookup C γ) ≡ fst (AllCodes Aʟ))
```

`LeastOf i t` 是步进任一端点所需的元层性质。第一分量说槽 `i` 含有`denote t`；第二分量说，任何指称也等于该槽的名字 `t'` 都不能先于 `t`。因此，它断言 `t` 是槽 `i` 中特定集合的一条最小名字；它本身不包含任何公式的满足证明。

```agda
                (q₀ : fst (lookup C₀ γ) ≡ fst (AllCodes ∅ʟ)) where
      LeastOf : Fin n → Name → Type (ℓ-suc ℓ)
      LeastOf i t = (fst (lookup i γ) ≡ denote t)
                  × ((t' : Name) → fst (lookup i γ) ≡ denote t'
                     → t' ≺ₙ t → Empty.⊥)
```

`StepAt-fill` 从显式名字 `t₁,t₂`、它们分别对 `x,y` 最小的证明，以及显式比较`t₁ ≺ₙ t₂` 出发。它按绑定次序向 `StepAt-in` 提供六个见证：`t₁` 的码、元数数码和参数环境，随后是 `t₂` 的对应三项资料。公式体继而要求两份最小名字满足与一份比较满足。此装填定理的输入没有处在命题截断之下。

```agda
      StepAt-fill : (t₁ t₂ : Name) → LeastOf x t₁ → LeastOf y t₂ → t₁ ≺ₙ t₂
                  → ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
      StepAt-fill t₁ t₂ l₁ l₂ lt = StepAt-in R P B C C₀ x y γ
        ( codeEl t₁ , (numAt (arity t₁) , (envEl t₁
        , ( codeEl t₂ , (numAt (arity t₂) , (envEl t₂
```

存在见证会被压入环境前端，所以六个见证在环境中按绑定次序反向出现：先是`envEl t₂`、它的数码与码，再是 `envEl t₁`、它的数码与码，最后接原环境 `γ`。在这个环境中，`s6a,a6a,e6a` 定位第一名字的码、数码与环境。证明 `ln₁` 把第一名字的三条资料等式、指称等式 `l₁ .fst` 和最小性证明 `l₁ .snd` 交给`LeastAt-fill`。

```agda
        , ( ln₁ , (ln₂ , cmp) )))))))
        where
        ln₁ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
                s6a a6a e6a (sh6 x)
                (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂
```

传给第一次 `LeastAt-fill` 的记录恰有预期的两个部分。其 `N.Data` 分量由`codeEl-fst`、`numAt-fst`、`envEl-fst` 以及把槽 `x` 与 `t₁` 的指称认同的等式 `l₁ .fst` 组成；其 `IsMin` 分量是 `l₁ .snd`。因此，`ln₁` 证明第一个被绑定三元组是 `x` 的一条最小名字。对 `t₂` 的同类构造与比较证明则给出`StepAt-in` 所需的其余分量。

```agda
                 ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ)
                qR qP qB qC q₀ t₁
                ( (codeEl-fst t₁ , (numAt-fst (arity t₁)
                                 , (envEl-fst t₁ , l₁ .fst)))
                , l₁ .snd )
```

第二个最小名字条件由与第一个相同的充分性映射填充，只是这次使用槽位 `s6b`、`a6b` 与 `e6b`。共享的六见证环境把这些槽位分别认同为 `t₂` 的码、元数数码与参数环境，而 `sh6 y` 指定 `t₂` 必须指称的集合。因此，余下的实参必须同时证明这项指称与 `t₂` 的最小性。

```agda
        ln₂ = Min.LeastAt-fill (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
                s6b a6b e6b (sh6 y)
                (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂
                 ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ)
                qR qP qB qC q₀ t₂
```

这组嵌套序对恰好具有 `LeastAt-fill` 所需的类型：先给出 `t₂` 的四条数据等式，再给出它的最小性证明。前三条等式来自封装好的码元素、数码元素与环境元素；`l₂ .fst` 把指称认同为槽位 `y` 中的值；`l₂ .snd` 则排除每个指称相同且满足 `t' ≺ₙ t₂` 的 `t'`。因此，最小性的方向是：没有更小的竞争名字先于 `t₂`。

```agda
                ( (codeEl-fst t₂ , (numAt-fst (arity t₂)
                                 , (envEl-fst t₂ , l₂ .fst)))
                , l₂ .snd )
```

比较条件只使用每个名字的三个排序键。对 `order-in` 的调用先取得解释两个关系槽位的 `qR` 与 `qP`，再给出两条码等式与两条元数数码等式。加上下行的两条环境等式，便是这次调用所需的八条等式。指称与最小性没有传入，因为 `_≺ₙ_` 只按这三个键比较名字。

```agda
        cmp = K.order-in (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b
                (envEl t₂ ∷ numAt (arity t₂) ∷ codeEl t₂
                 ∷ envEl t₁ ∷ numAt (arity t₁) ∷ codeEl t₁ ∷ γ) t₁ t₂
                qR qP (codeEl-fst t₁) (codeEl-fst t₂)
                (numAt-fst (arity t₁)) (numAt-fst (arity t₂))
```

两条环境等式补全槽位认同，最后的实参 `lt` 给出实际比较 `t₁ ≺ₙ t₂`。因此，`cmp` 是两个三元组之间对象语言比较公式的满足证明。它与 `ln₁`、`ln₂` 一同给出 `StepAt-in` 所装入的三个合取项。这个填充方向从指定的两个名字与一项指定的比较出发，因而可以直接引入六个存在见证。

```agda
                (envEl-fst t₁) (envEl-fst t₂) lt
```

反向定理精确标明见证的边界。从 `StepAt` 的满足关系出发，它只返回 `∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ] (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁`。外层依值和让 `t₁` 遍历全部名字；对每个这样的 `t₁`，内层依值和再让 `t₂` 遍历全部名字。其载荷精确断言：`t₁` 是槽 `x` 中取值的最小名字，`t₂` 是槽 `y` 中取值的最小名字，并且 `t₁ ≺ₙ t₂`。第一个 `PT.rec` 打开 `StepAt-out` 给出的六见证之命题截断，而消去目标仍是这条带有命题截断的结论。

```agda
      StepAt-read : ⟨ γ ⊨ StepAt R P B C C₀ x y ⟩
                  → ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ]
                      (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁
      StepAt-read h = PT.rec squash₁ atSix (StepAt-out R P B C C₀ x y γ h)
        where
```

`Goal` 为该陪域命名，使各次截断消去具有同一个目标。由于 `Goal` 本身就是命题截断，`squash₁` 证明它是命题。这正是外层六见证截断以及后续两次最小名字截断都可以被消去的理由，同时最终的一对名字仍由一道命题截断隐藏。

```agda
        Goal : Type (ℓ-suc ℓ)
        Goal = ∥ Σ[ t₁ ∈ Name ] Σ[ t₂ ∈ Name ]
                 (LeastOf x t₁ × (LeastOf y t₂ × (t₁ ≺ₙ t₂))) ∥₁
```

在这次获准的消去内部，`atSix` 取得普通的 `StepOf` 见证，并把它分成 `(s₁,k₁,p₁)` 与 `(s₂,k₂,p₂)` 两个三元组。由于存在见证逐个加入环境头部，公式体在反序环境 `p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ` 中求值。因此，第一次调用 `LeastAt-read` 时使用第一组三元数据的固定位置 `s6a`、`a6a` 与 `e6a`，读取槽位 `x` 中的值的一个最小名字。

```agda
        atSix : StepOf R P B C C₀ x y γ → Goal
        atSix (s₁ , (k₁ , (p₁ , (s₂ , (k₂ , (p₂ , hb)))))) =
          PT.rec squash₁ atFirst
            (Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
               s6a a6a e6a (sh6 x)
```

公式体证明 `hb` 含有三个合取项。各投影依次把它们命名为 `h₁`、`h₂` 与 `hc`：前两项分别是第一、第二组三元数据对 `LeastNameAt` 的满足，第三项是从第一组三元数据到第二组三元数据的 `≺At` 满足。证明先把 `h₁` 交给 `LeastAt-read`。另外两项保留到两个元语言名字都恢复以后，因为只有到那时，`hc` 才能解释为这两个名字之间的比较。

```agda
               (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₁)
          where
          h₁ = hb .fst
          h₂ = hb .snd .fst
          hc = hb .snd .snd
```

`atSecond` 记录读出第一个最小名字后尚需完成的工作。它先取得一个特定的 `t₁` 及其完整 `Min.Least` 记录，再取得一个特定的 `t₂` 及相应记录，最后必须构造 `Goal`。每份记录都含有四条数据等式，以及方向正确的最小性断言。因此，这个后续函数既有足够信息恢复两项 `LeastOf` 事实，也能解释仍处于对象语言层面的比较 `hc`。

```agda
          atSecond : (t₁ : Name)
                   → Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
                       s6a a6a e6a (sh6 x)
               (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁
                   → Σ[ t₂ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C)
```

两份记录就绪后，最终陈述只缺一项证明 `lt : t₁ ≺ₙ t₂`。映射到该比较之上的函数，从每份数据记录中只保留指称等式 `dᵢ .snd .snd .snd`，并将它与最小性证明 `mᵢ` 配对；这两项恰好组成 `LeastOf`。随后，它把所得的两项最小名字事实与 `lt` 合并，并把完整的名字对放入 `Goal`，全程不移除外围的命题截断。

```agda
                       (sh6 C₀) s6b a6b e6b (sh6 y)
               (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₂
                   → Goal
          atSecond t₁ (d₁ , m₁) (t₂ , (d₂ , m₂)) =
            PT.map (λ lt → t₁ , (t₂ , ( (d₁ .snd .snd .snd , m₁)
```

此时，`order-out` 解释 `hc`。除 `qR` 与 `qP` 外，它还从 `d₁`、`d₂` 取得两个已恢复名字各自的码等式、元数数码等式与参数环境等式。三键比较不需要指称等式。所得结果只有 `∥ t₁ ≺ₙ t₂ ∥₁`；`PT.map` 把这道命题截断内的每项比较变换成 `Goal` 所需的完整见证。

```agda
                                      , ( (d₂ .snd .snd .snd , m₂) , lt ))))
              (K.order-out (sh6 R) (sh6 P) s6a a6a e6a s6b a6b e6b
                 (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) t₁ t₂
                 qR qP (d₁ .fst) (d₂ .fst) (d₁ .snd .fst) (d₂ .snd .fst)
                 (d₁ .snd .snd .fst) (d₂ .snd .snd .fst) hc)
```

`atFirst` 是读取第一个最小名字时使用的后续函数。取得已恢复的 `(t₁,l₁)` 后，它在第二组三元数据的槽位处对 `h₂` 应用 `LeastAt-read`，而第二个名字及其记录仍只在命题截断下得到。随后，`PT.rec` 可以把这对数据交给 `atSecond t₁ l₁`，因为消去目标是命题 `Goal`。因此，第二道截断只在构造最终的截断存在陈述时被消去。

```agda
          atFirst : Σ[ t₁ ∈ Name ] Min.Least (sh6 R) (sh6 P) (sh6 B) (sh6 C)
                      (sh6 C₀) s6a a6a e6a (sh6 x)
               (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ t₁
                  → Goal
          atFirst (t₁ , l₁) = PT.rec squash₁ (atSecond t₁ l₁)
```

最后一次调用传入第二组三元数据的固定槽位、同一个反序六见证环境以及 `h₂`。它完成了四个截断接口的复合：`StepAt-out`、两次 `LeastAt-read` 与 `order-out`。这个复合精确证明：`StepAt` 的满足关系蕴含命题截断下的名字 `t₁,t₂` 的存在性，其中 `t₁` 是 `x` 的最小名字，`t₂` 是 `y` 的最小名字，并且 `t₁ ≺ₙ t₂`。任何特定的名字对都不会被导出这道截断。

```agda
            (Min.LeastAt-read (sh6 R) (sh6 P) (sh6 B) (sh6 C) (sh6 C₀)
               s6b a6b e6b (sh6 y)
               (p₂ ∷ k₂ ∷ s₂ ∷ p₁ ∷ k₁ ∷ s₁ ∷ γ) qR qP qB qC q₀ h₂)
```

## 小结

本章建立了名字之语义对应的两个方向。在充分性方向，一条具体名字凭其公式码、元数、参数环境与指称装填 `NameAt`；再给出它在同指称名字中最小的证明，便装填 `LeastNameAt`；两条这样的最小名字连同 `t₁ ≺ₙ t₂` 则装填 `StepAt`。在完备性方向，从满足关系反向恢复的正是这些资料。因此，比较两条最小描述的公式与元语言比较一致：先比较公式码，码相同时比较元数，前两项都相同时再比较参数向量。

这些完备性陈述保留命题截断。唯一性使参数图能够无截断地决定其向量，但读取整条名字、最小名字或一对已比较的最小名字时，只证明合适见证的存在性。每次截断消去都只以命题为目标，不会导出某条特定名字或某对特定名字；这里也没有实施命题降级。下游正是在这个边界上把 `StepAt` 接到宿主层的步序。