---
title: "后继层成员的典范名字"
module: L.Choice.CanonicalNames
lang: zh
site: "Bedrock"
description: "后继层成员的典范名字"
stage: "典范良序与选择公理"
reading_order: 75
canonical: https://bedrock.institute/zh/L.Choice.CanonicalNames.html
html: L.Choice.CanonicalNames.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/CanonicalNames.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Manipulation.ConstantOccurrences, FOL.Manipulation.ParameterAbstraction, V.Hierarchy, V.Coding, V.Model, L.Constructible, L.Definability, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Choice.FiniteStageOrders, L.WellOrder.Base]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.Choice.CanonicalNames.md, https://bedrock.institute/ja/L.Choice.CanonicalNames.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 后继层成员的典范名字

后继层的成员由一条公式及前一层中的有限多个参数确定。本章把这些数据封装成名字，证明每个成员都有名字，再良序化所有名字，以便选出最小代表。

后继层的成员就是下面那一层的可定义子集，而前面的章节已经把这句话说了两遍：一遍在 `L.Definability` 中，说成带参数的公式，参数取自那一层；另一遍在 `FOL.Manipulation.ParameterAbstraction` 中，在参数离开语法之后，说成**一条无参公式配上一个参数向量**。可比较的是后一种形式。它的公式是一段有穷的语法，故它的码是遗传有穷集，早已现身于极限层 `Lset ω`，而 `L.Choice.FiniteStageOrders` 恰把那里良序化；它的参数是下面那一层的成员，而在外围构造调用本章时，那一层已被良序化。**名字**就是这样一对，中间夹着元数；本章造出它，证明后继层的每个成员都有一个，并把诸名字良序化。

那个序是一次写开了的三键字典序比较。此处没有任何东西是「依值和上的一般序」的实例，而这是有意为之：那样一件东西得携带一族以第一个键为索引的序，并在那种一般性下证出它的四条定律，而这比所要的定理更大，却只用一次。三个键各有其名，而每个键都由一个已然存在的序来比较。

显式的经典输入是 `lem : LEM (ℓ-suc ℓ)`。它既供给公式码所用的有限层极限序，也供给结尾的极小元搜索。把它保留为模块参数，便准确记录两项构造共同需要的强度；中间的编码、抽象、字典序定律与可及性论证不再加入其他公理。

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

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

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

名字赖以书写的词汇来自集合论的一阶语言。这里的公式带有一个常元符号域和固定数目的自由变量槽位，构造子覆盖了隶属、相等、联结词、假，以及两类量词，其中受限形式也一并列出。这套语法早已存在；本章只需对一种特殊形状的公式，即常元域为空的那些公式，加以命名和比较。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
```

几项既有的公式操作承担了「把带常元的定义变成名字」的实质工作。把词项与公式编码为集合的操作给出将成为第一个键的码；改名引理说，经常元域的嵌入去读一条公式时满足关系不变；出现计数与参数抽象一起，把常元换成新变量和一个参数向量。在宇宙一侧，结构 `𝒮ᵥ` 在 `V` 之内解释这套语言，而配对构造 `pr` 正是把码的片段包装成集合的东西。

```agda
open import FOL.Manipulation.ConstantMapping using ( mapTm; embed )
open import FOL.Manipulation.Relabelling using ( embed-⊨ )
open import FOL.Manipulation.ConstantOccurrences using ( countFo; constantsFo )
open import FOL.Manipulation.ParameterAbstraction using ( absFo; ⊨-abs₁ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

可构造一侧贡献的是被命名的对象。`Lset` 是 `V` 之内可构造层级的一层，而 `𝒟ₒ` 是可定义幂集算子：它取一个集合，返回其中由「带该集合常元的单变量公式」可定义的子集所成之集。关键在于，`𝒟ₒ` 交还的只是「存在这样一条公式」这一截断的见证，因此命名的完备性将继承这种截断，而非一条被选定的公式。模块 `DefOf` 载有内层满足关系及其小性事实，指称正是由它们造出的。

```agda
open import V.Coding {ℓ} using ( pr; module VCode )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( Lset; Lset-mono; 𝒟ₒ; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
```

第一个键需要一个既有序可及的安身之处。该语言的数码，即 von Neumann 自然数，是 `L` 之内的序数，且每个数码落在其后一层之中；层成员的配对则在两阶之后出现。极限层 `Lset ω` 收拢了到某个有穷层为止出现的对象，而 `Limit` 就是它的成员连同隶属的凭证。在这一层上，`limitOrder` 把一切良序化；`Tri-map` 则沿等价搬运三歧判决，第三键的三歧将复用这一工具。

```agda
open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Axioms.Basic {ℓ} using ( pr∈Lset-suc )
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Limit; inSome; limitOrder; Tri-map )
open import L.WellOrder.Base {ℓ-suc ℓ}
```

序的抽象概念被打包成记录的严格良序：一个严格比较、三歧性、非自反性、传递性与良基性，连同使用这种记录的最小元搜索 `leastOf`。名字将被证明恰好满足这四条定律。在类型论一侧，导入的工具处理因名字的公式与参数向量以元数为索引而产生的依值类型中的等式处理：向依值对中造路径的办法、替换沿路径与常值函数的交换、等价的两个方向，以及从嵌入提取的单射性。

```agda
  using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf )

open import Cubical.Foundations.Prelude using ( toPathP )
open import Cubical.Foundations.Transport using ( constSubstCommSlice )
open import Cubical.Foundations.Equiv using ( equivFun; invEq )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
```

自然数供出诸元数，而自然数上的序供出中间那个键。它的三歧在此是可判定的，故名字的比较可以直接在 `arity a ≟ arity b` 上分岔；`_<_` 的传递性与良基性进入相应的定律。`⇔toPath` 把命题双条件的证明变成路径，指称的隶属刻画正因此才被陈述为命题的等式，而非两个蕴涵；`toℕ` 则把一个有界索引读成普通的数码。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Nat using ( _+_; +-comm )
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Data.FinData using ( toℕ )
```

字典序比较将写成和类型：每个键的判决要么严格在前，要么相等，相等时再由下一个键决定。因此本章需要带构造子的二元和、带 `map` 的参数向量，以及良基归纳的工具箱：`Acc` 表达「从任一元素出发的严格下降都会终止」，`acc` 打包这样一份证明，`WFI` 把它变成归纳原理。这里的向量以其长度为索引，正是这一点引出后文要研究的元数转换问题。

```agda
open import Cubical.Data.Sigma using ( ΣPathP )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Data.Vec using ( map )
open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; module WFI )
```

两种消去的靶类型由数学本身固定。空类型的消去子处理不可能的情形，比如一条含常元的无参公式。命题截断把被选定的见证变成单纯的存在主张：只要 `A` 有元素，`∥ A ∥₁` 就有元素，而它只能消去到取值为命题的靶子。累积集合的层级贡献了 `sett`，即由小索引类型组装出的一个集合，以及嵌入 `⟪_⟫`，它把小类型中的元素看作宇宙的成员。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
```

最后一组固定了诸名字被解读于其中的具体解释。`#` 把自然数变成宇宙之内对应的数码，而 `ω` 是无穷集，于是极限层那类数码隶属凭证便可制造。这里的真值与联结词直接取自 `hProp (ℓ-suc ℓ)` 上的逻辑运算；再在结构 `𝒮ᵥ` 处打开 `ZFStructure` 的语义，便固定了一条公式在 `V` 之内意味着什么。下文的每一个满足判断都是这个内层判断，而正是它把名字的指称与可定义幂集自己的可定义性概念扣在一起。

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

最后这些声明固定了全章采用的解释：公式在 `V` 上的集合论结构中读取，真值取命题。

```agda
open hPropStructure 𝒮ᵥ
```

## 无参的码是遗传有穷的

名字的第一个键是其无参公式的码。这样的有限语法码是遗传有穷的，因此早已属于极限层，可以由既有良序比较。

第一个键要把公式当作 `Lset ω` 的成员，故首先要立的就是「它的码是这样一个成员」。读一遍 `V.Coding` 的诸编码子句便知别无他物：一个数码作标签，一个数码作 de Bruijn 序号，以及装着各部分的 Kuratowski 对。唯一可能走出有穷世界的构造是常元那一条，它把一个任意集合放进码里，而无参公式压根没有常元。

于是两条封闭性事实就够了，而两条都是引用既有结果、并非重新证明：`L.Choice.FiniteStageOrders` 的 `inSome` 说 `Lset ω` 的成员到某个有穷层为止已经现身，而 `L.Axioms.Basic` 的 `pr∈Lset-suc` 说两层成员的 Kuratowski 对在两阶之后现身。至于从一个有穷层推进到更晚的层，只需沿数码的后继逐级施用单调性，这也是本节唯一的递归。

极限层的隶属凭证难以直接使用，因为它只说该元素处在某个有穷层之中。辅助谓词 `AtStage` 记录的是哪个有穷层：一个自然数 `k`，连同该元素属于 `Lset (# k)` 的证明。一旦把元素固定在某一层上，`raiseTo` 便能前移这份凭证，从层 `# k` 推进到层 `# (d + k)`，对 `d` 递归：每一步后继都通过 `self∈sucV` 观察到该层包含界定它的那个数码，而 `Lset-mono` 把这一点转成层的单调性。

```agda
private
  AtStage : S → Type (ℓ-suc ℓ)
  AtStage x = Σ[ k ∈ ℕ ] ⟨ x ∈ˢ Lset (# k) ⟩

  raiseTo : (x : S) (d k : ℕ) → ⟨ x ∈ˢ Lset (# k) ⟩ → ⟨ x ∈ˢ Lset (# (d + k)) ⟩
  raiseTo x zero    k h = h
```

数码是整个论证的原子，故先安置它们。由 `numeral-ord`，`# k` 是 `L` 中的序数，`ord∈Lset-suc` 把它放入自身层的后继。证明 `#∈ω` 说明作为界的数码属于 `ω`，故单调性把该数码提升到极限层。相伴的封闭性陈述则说明，只要 `x` 与 `y` 都在极限层，`pr x y` 也在那里；复合语法的编码恰好需要这一点。

```agda
  raiseTo x (suc d) k h = Lset-mono (self∈sucV (# (d + k))) (raiseTo x d k h)

numeral∈limit : (k : ℕ) → ⟨ (# k) ∈ˢ Lset ω ⟩
numeral∈limit k = Lset-mono (#∈ω (suc k)) (ord∈Lset-suc (# k) (numeral-ord k))

pr∈limit : (x y : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ y ∈ˢ Lset ω ⟩
         → ⟨ pr x y ∈ˢ Lset ω ⟩
```

配对这条陈述的证明有一处波折：`inSome` 把层见证交在命题截断之内，故那些层编号无法作为数据被选出。但目标本身是一个隶属命题，而截断的见证允许消去到取值为命题的靶子。外层的 `PT.rec` 拆开 `x` 的见证，内层的拆开 `y` 的见证，然后把两者交给真正干活的辅助引理 `both`。

```agda
pr∈limit x y hx hy = PT.rec (snd (pr x y ∈ˢ Lset ω))
  (λ atX → PT.rec (snd (pr x y ∈ˢ Lset ω)) (both atX) (inSome y hy))
  (inSome x hx)
  where
  both : AtStage x → AtStage y → ⟨ pr x y ∈ˢ Lset ω ⟩
```

设 `x` 的层号为 `j`，`y` 的为 `k`，先把两个元素抬到公共层 `# (k + j)`，使 `pr∈Lset-suc` 得以适用，把这一对放进两阶之后、由 `# (suc (suc (k + j)))` 在 `ω` 中界定的层；公共层的两个加数顺序相反，一次沿 `+-comm` 的替换把它修正。既然数码与对都对极限层封闭，而带标签的码不过是数码与载荷组成的对，`tag∈limit` 便也给出封闭性。这三条事实就是接下来那场语法归纳的全部负担。

```agda
  both (j , hj) (k , hk) = Lset-mono (#∈ω (suc (suc (k + j))))
    (pr∈Lset-suc (# (k + j)) x y (raiseTo x k j hj)
      (subst (λ n → ⟨ y ∈ˢ Lset (# n) ⟩) (+-comm j k) (raiseTo y j k hk)))

tag∈limit : (k : ℕ) (x : S) → ⟨ x ∈ˢ Lset ω ⟩ → ⟨ VCode.mkTag k x ∈ˢ Lset ω ⟩
tag∈limit k x h = pr∈limit (# k) x (numeral∈limit k) h
```

数码、配对与标签齐备之后，每条无参码的安置便由语法上的结构归纳给出。这条归纳很短，因为上面三条封闭性事实承担了全部工作；各构造子情形只是把它们重新拼装，而唯一可能逃出有穷世界的常元情形是空的，因为常元域是空类型。标签数字全程以字面量出现，除「是数码」之外没有用到它们的任何值。

先处理词项，其归纳只有两条子句。变量不含常元内容，故其码是包在标签 `1` 里的 de Bruijn 序号的数码，`tag∈limit` 当即适用。无参词项的常元子句是矛盾：常元域 `⊥*` 没有元素，不可能情形由空类型的消去子打发。陈述中的 `mapTm` 是把无参词项嵌入工作语法的操作，它把常元换成宿主值；对 `⊥*` 而言无物可换。

```agda
codeTm∈limit : ∀ {n} (t : Term (⊥* {ℓ}) n)
             → ⟨ VCode.⌜ mapTm Empty.rec* t ⌝ᵗ ∈ˢ Lset ω ⟩
codeTm∈limit (con c) = Empty.rec* c
codeTm∈limit (var i) = tag∈limit 1 (# (toℕ i)) (numeral∈limit (toℕ i))

code∈limit : ∀ {n} (χ : Formula (⊥* {ℓ}) n) → ⟨ VCode.⌜ embed χ ⌝ ∈ˢ Lset ω ⟩
```

公式遵循同一模式，每个构造子一个标签。每个二元子句把两条直接子公式或子词项的码在一个标签下配成对，联结词与量词子句包装单一的子码，而假就是零的裸数码。每种情形的结果都是对归纳假设施用一次 `tag∈limit` 或 `pr∈limit`，故各子句体都只有一行。

```agda
code∈limit (t ∈̇ u)  = tag∈limit 0 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u))
code∈limit (t ≐ u)  = tag∈limit 1 _ (pr∈limit _ _ (codeTm∈limit t) (codeTm∈limit u))
code∈limit (φ ∧̇ ψ)  = tag∈limit 2 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
code∈limit (φ ∨̇ ψ)  = tag∈limit 3 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
code∈limit (φ ⇒̇ ψ)  = tag∈limit 4 _ (pr∈limit _ _ (code∈limit φ) (code∈limit ψ))
```

最后四条子句覆盖量词及其受限形式，标签为 `6` 到 `9`；受限形式还额外把辖域词项的码配进对中。对本章要紧的只是最终结果：每条无参公式都有一个落在极限层中的码，随时可被该层既带的序去比较。标签编号只是编码约定，不属于任何数学主张。

```agda
code∈limit ⊥̇        = tag∈limit 5 _ (numeral∈limit 0)
code∈limit (∃̇ φ)    = tag∈limit 6 _ (code∈limit φ)
code∈limit (∀̇ φ)    = tag∈limit 7 _ (code∈limit φ)
code∈limit (∀̇∈ t φ) = tag∈limit 8 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
code∈limit (∃̇∈ t φ) = tag∈limit 9 _ (pr∈limit _ _ (codeTm∈limit t) (code∈limit φ))
```

极限层的成员带有隶属凭证，故第一个键不是光秃秃的码，而是码连同那张凭证。本小节把二者打包，并记录一项关于沿元数等式传输的辅助事实，比较时将用到它。

`limitCode` 把无参公式送到「码与刚造好的隶属证明」组成的对；这一对恰是 `Limit` 的元素，即极限层序所作用的对象。第二条陈述涉及依值语法的一处微妙：公式的类型提及它的元数，故当发现两个名字的元数相等之后，必须先把一条公式沿该等式替换，才能与另一条比较。`code-shift` 说这次替换对码不可见：把元数为 `suc i` 的公式沿路径 `i ≡ j` 传输，得到的公式具有相同的码。

```agda
limitCode : ∀ {n} → Formula (⊥* {ℓ}) n → Limit
limitCode χ = VCode.⌜ embed χ ⌝ , code∈limit χ

code-shift : {i j : ℕ} (e : i ≡ j) (χ : Formula (⊥* {ℓ}) (suc i))
           → VCode.⌜ embed (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e χ) ⌝
           ≡ VCode.⌜ embed χ ⌝
```

证明援引一条一般事实：结果类型不依赖索引的函数，与沿该索引的替换可交换。公式的编码落在固定的集合类型 `S` 中，与公式所处的元数无关，故由 `constSubstCommSlice`，传输后的公式的码等于原来的码；陈述用 `sym` 排布成从被替换的公式指回原公式的方向。

```agda
code-shift e χ = sym (constSubstCommSlice
  (λ k → Formula (⊥* {ℓ}) (suc k)) S (λ _ ψ → VCode.⌜ embed ψ ⌝) e χ)
```

## 无参公式可从它的像还原

在固定元数下，编码不会把两条不同的无参公式等同起来。先从遗传有穷的像解码，再用语法编码的单射性，即得这一单射性。

码与元数都相同的两个名字，其公式必须相同，否则那次比较就会把两个不同的名字判为「互不更小、又不与任何东西相等」。`V.Coding` 证过它自己的单射性，但它是对工作语法证的，那里的常元域是载体；此处所需的是无参公式的单射性，而无参公式经 `embed` 映入那套语法。

上述缺口由一个反向的**抹除**补上，而抹除可以粗糙，因为它只需在无参公式上作左逆。常元被送到序号为零的变量，那个槽位总在，因为视野中的每条公式至少有一个自由变量槽位；其余每条子句都是构造子上的恒等。对一条本来就没有常元的公式，抹除逐条子句什么也没改，于是单射性就是三次路径复合。

词项的抹除是唯一有创造性的工作。常元 (在工作语法中取值为任意集合) 被换成序号为零的变量；变量保持原样。这之所以合法，只因目标限定在元数为 `suc n` 的公式，故零号槽位总在。公式的抹除随后按同态方式声明：每个构造子映到自身，各部分取抹除。

```agda
private
  eraseTm : ∀ {n} → Term S (suc n) → Term (⊥* {ℓ}) (suc n)
  eraseTm (con x) = var zero
  eraseTm (var i) = var i

  eraseFo : ∀ {n} → Formula S (suc n) → Formula (⊥* {ℓ}) (suc n)
```

前五条子句覆盖原子公式与命题联结词：两条原子关系对各自的词项实参作抹除，三个二元联结词对两条子公式递归。这里发生的不过是把抹除沿构造子分发；常元信息已在词项一层被丢弃。

```agda
  eraseFo (t ∈̇ u)  = eraseTm t ∈̇ eraseTm u
  eraseFo (t ≐ u)  = eraseTm t ≐ eraseTm u
  eraseFo (φ ∧̇ ψ)  = eraseFo φ ∧̇ eraseFo ψ
  eraseFo (φ ∨̇ ψ)  = eraseFo φ ∨̇ eraseFo ψ
  eraseFo (φ ⇒̇ ψ)  = eraseFo φ ⇒̇ eraseFo ψ
```

余下五条子句就是字面上的恒等：假没有部件，而每个量词围着被抹除的主体重建自身。每条子句都是被迫的；公式如何被抹除没有选择余地，这正是下面左逆计算可以预期的原因。

```agda
  eraseFo ⊥̇        = ⊥̇
  eraseFo (∃̇ φ)    = ∃̇ eraseFo φ
  eraseFo (∀̇ φ)    = ∀̇ eraseFo φ
  eraseFo (∀̇∈ t φ) = ∀̇∈ (eraseTm t) (eraseFo φ)
  eraseFo (∃̇∈ t φ) = ∃̇∈ (eraseTm t) (eraseFo φ)
```

左逆性质逐层陈述、逐层证明。对词项而言，`mapTm Empty.rec*` 之后再作 `eraseTm` 得回原词项：常元情形是空的，因为无参词项本无常元；变量情形是 `refl`，因为两种复合都重建同一个变量。公式层面的陈述随后主张：抹除一条无参公式的嵌入，沿一条路径得回原公式。

```agda
  eraseTm-embed : ∀ {n} (t : Term (⊥* {ℓ}) (suc n))
                → eraseTm (mapTm Empty.rec* t) ≡ t
  eraseTm-embed (con c) = Empty.rec* c
  eraseTm-embed (var i) = refl

  eraseFo-embed : ∀ {n} (χ : Formula (⊥* {ℓ}) (suc n)) → eraseFo (embed χ) ≡ χ
```

证明对公式归纳，凡词项出现处复用词项层的事实。原子与二元联结词的子句对两个递归结果施用二元同余 `cong₂`，由各部分的路径造出复合体的路径。

```agda
  eraseFo-embed (t ∈̇ u)  = cong₂ _∈̇_ (eraseTm-embed t) (eraseTm-embed u)
  eraseFo-embed (t ≐ u)  = cong₂ _≐_ (eraseTm-embed t) (eraseTm-embed u)
  eraseFo-embed (φ ∧̇ ψ)  = cong₂ _∧̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
  eraseFo-embed (φ ∨̇ ψ)  = cong₂ _∨̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
  eraseFo-embed (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (eraseFo-embed φ) (eraseFo-embed ψ)
```

假只需 `refl`，因为没有东西被嵌入其中；四个量词子句施用一元同余，受限形式还带词项，故用 `cong₂`。至此，每条无参公式都有一条从被抹除的像指回自身的显式路径。

```agda
  eraseFo-embed ⊥̇        = refl
  eraseFo-embed (∃̇ φ)    = cong ∃̇_ (eraseFo-embed φ)
  eraseFo-embed (∀̇ φ)    = cong ∀̇_ (eraseFo-embed φ)
  eraseFo-embed (∀̇∈ t φ) = cong₂ ∀̇∈ (eraseTm-embed t) (eraseFo-embed φ)
  eraseFo-embed (∃̇∈ t φ) = cong₂ ∃̇∈ (eraseTm-embed t) (eraseFo-embed φ)
```

单射性如今只是一句话。设两条同元数无参公式的嵌入码相同。编码自身的单射性把它变成两条嵌入公式的相等；对两侧作抹除仍保持相等，因为抹除是一个函数；而左逆路径把两侧各自化归到原公式。复合出的路径就是想要的 `χ ≡ ψ`，故在固定元数下，两条不同的无参公式不可能具有相同的码。

```agda
code-inj : ∀ {n} (χ ψ : Formula (⊥* {ℓ}) (suc n))
         → VCode.⌜ embed χ ⌝ ≡ VCode.⌜ embed ψ ⌝ → χ ≡ ψ
code-inj χ ψ e = sym (eraseFo-embed χ)
               ∙ cong eraseFo (VCode.⌜⌝-inj (embed χ) (embed ψ) e)
               ∙ eraseFo-embed ψ
```

## 命名数据

一个名字记录元数、一条多出一个输出变量的无参公式，以及相应长度的参数向量。它所指称的，是该公式在这个环境下从层中界定出的子集。

本章余下的一切都相对于一个集合 `A`，即诸名字据以写出的那一层，也相对于该层成员上的一个严格良序，故工作在模块 `Naming A w` 之内进行。一个**名字**由三部分组成：一个元数、一条比该元数多一个自由变量槽位的无参公式，以及一个由 `A` 的小成员类型取出、长度等于该元数的参数向量。多出的那个槽位正是用于选出子集的；其余槽位接收诸参数，而第一个键当即从那条公式读出。

模块取层 `A`，以及关键的、其成员上的一个严格良序作为参数，因为第三个键将按这个序比较参数，而本章不会在任意层上构造一个序。类型 `Name` 是一个依值三元组：自然数 `k`、有 `suc k` 个自由变量槽位的无参公式、以及由 `k` 个 `A` 载体成员组成的向量。向量长度被强制等于元数，故名字不可能把公式与错误数目的参数配对。

```agda
module Naming (A : S) (w : SWO ⟪ A ⟫) where
  module DA = DefOf A
  open DA using ( _⊨ᵐ_ )

  Name : Type ℓ
  Name = Σ[ k ∈ ℕ ] (Formula (⊥* {ℓ}) (suc k) × Vec ⟪ A ⟫ k)
```

诸投影标出三个键的来源：`arity` 返回那个数，`formula` 返回恰好多一个变量槽位的无参公式，`params` 返回那个向量。它们的类型依值于名字自身，故 `formula a` 处在元数 `suc (arity a)` 上，`params a` 处在 `arity a` 上；这份依值正是后文比较中每个传输问题的来源。

```agda
  arity : Name → ℕ
  arity a = a .fst

  formula : (a : Name) → Formula (⊥* {ℓ}) (suc (arity a))
  formula a = a .snd .fst

  params : (a : Name) → Vec ⟪ A ⟫ (arity a)
```

第一个键同样是一个投影：`codeOf` 对公式施用 `limitCode`，交付它的码连同极限层中的隶属凭证，随时可由 `limitOrder` 比较。

```agda
  params a = a .snd .snd

  codeOf : Name → Limit
  codeOf a = limitCode (formula a)
```

一个名字所**指称**的，是当参数由**环境**给出时，它的公式所选中的 `A` 的子集，次序与参数抽象定理一致。环境由一个成员后接诸参数组成，全部经可定义幂集所用的常元解释读入限制载体，而满足关系取内层版本；因此，指称正是由「`Def A` 据以定义的那个概念」选出的 `A` 的子集，与定义完全一致。小性直接继承：任何公式在任何环境处的内层满足皆小，故该子集是小索引类型上的一个 `sett`，降至小索引类型无须额外工作。

由一条谓词从 `A` 中刻出的子集可直接呈现：`subsetOf` 接受 `A` 的小成员类型上的一个命题族，构造一个 `sett`，其索引类型是「成员 `m` 连同谓词在 `m` 处成立的证明」的依值和，并把这个对子送到集合 `⟪ A ⟫↪ m`。于是一个索引就是一位见证连同其证书，而所得集合的隶属只断言这样的对子仅仅存在。这与 `defSet` 的构造形状相同，故两种形式写出的谓词呈现的是同一类对象。

```agda
  private
    module SemM = FOL.Semantics DA.𝒮M
    open SemM using ( _^_ )

    subsetOf : (⟪ A ⟫ → hProp ℓ) → S
    subsetOf P = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ P m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))
```

在指称本身之前，有两个呈现细节要交代。辅助事实 `⟪⟫↪-inj` 记录映射 `⟪ A ⟫↪` 是嵌入，故其两个值之间的路径来自底层索引之间的路径；这将恢复 `m' ≡ m`，并在隶属规格的正向中使用。环境随即拼装而成：对标记自由变量的成员 `m`，环境是 `DA.ι m` 后接逐个经 `DA.ι` 解码的诸参数。头一项填入界定子集的那个额外槽位，其余各项填入参数槽位，且环境的长度按定义就是 `suc (arity a)`，恰为该名字公式的元数。

```agda
    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  environment : (a : Name) → ⟪ A ⟫ → DA.SM ^ (suc (arity a))
  environment a m = DA.ι m ∷ map DA.ι (params a)

  satAt : (a : Name) → ⟪ A ⟫ → hProp ℓ
```

定义一个名字指称的谓词是 `satAt a m`：内层语义在该拼装环境中满足嵌入后公式这一陈述的等价小命题。经 `subsetOf` 之后，`denote a` 就是层级中的一个集合，恰由内层语义从 `A` 中选出的子集。这里没有再作任何尺寸上的决定：小性经 `⊨ᵐ-small` 一次进入，全部花费在 `sett` 的索引类型上。

```agda
  satAt a m = DA.⊨ᵐ-small (embed (formula a)) (environment a m) .fst

  denote : Name → S
  denote a = subsetOf (satAt a)
```

下面把「指称」的规格逐字写出：`A` 的一个成员属于该指称，当且仅当内层世界在该名字所规定的环境处满足它的公式。压缩成小命题只是编码上的安排，而那个等价把它原样送回。

该定理是命题之间的路径，与 `defSet-mem` 的陈述形式一致，并由两个蕴含经 `⇔toPath` 证明。辅助定义 `decode` 把 `satAt a m` 重新展开成 `⊨ᵐ-small` 返回的完整对子，于是两个方向都能使用其第二分量中的等价，即连接小命题与内层满足陈述的那一个。

```agda
  denote-mem : (a : Name) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ denote a) ≡ (environment a m ⊨ᵐ embed (formula a))
  denote-mem a m = ⇔toPath fwd bwd
    where
    decode = DA.⊨ᵐ-small (embed (formula a)) (environment a m)
```

`sett` 的隶属只给出索引的截断存在，故正向把截断消入一个命题，得到索引 `(m' , h)` 连同从 `⟪ A ⟫↪ m'` 到 `⟪ A ⟫↪ m` 的路径 `q`。嵌入的单射性把 `q` 变为 `m' ≡ m`，沿它搬运 `h` 得到 `satAt a m` 的证明，`decode` 的等价再把这个证明转换为满足陈述。每一步都只在需要命题之处花费证明，因此没有选取任何见证。

```agda
    fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩ → ⟨ environment a m ⊨ᵐ embed (formula a) ⟩
    fwd = PT.rec (snd (environment a m ⊨ᵐ embed (formula a)))
      (λ { ((m' , h) , q) →
        invEq (decode .snd) (subst (λ v → ⟨ satAt a v ⟩) (⟪⟫↪-inj q) h) })
    bwd : ⟨ environment a m ⊨ᵐ embed (formula a) ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ denote a ⟩
```

反向把同一等价反向使用：一个满足的证明经等价变成 `satAt a m` 的证明，取作带平凡路径的索引 `(m , 证明)`，再以 `∣_∣₁` 截断。两个方向合起来把隶属与内层满足毫无剩余地等同起来，这正是「指称」一词被要求表达的含义。

```agda
    bwd h = ∣ (m , equivFun (decode .snd) h) , refl ∣₁
```

## 后继层的每个成员都有名字

可定义幂集的规格为后继层的每个成员给出一条带常元的公式。把这些常元抽象出去，就得到构成其名字的无参公式与参数向量。

按那个算子自己的规格，`𝒟ₒ A` 的成员仅仅是「由带 `A` 中常元的单变量公式可定义的子集」；参数抽象把这样一条公式变成元数更高的无参公式，并给出其中出现的常元列表。从前者读出后者，就是命名的全部，而且它是一个函数。

函数 `nameOf` 一举拼装三个键。`countFo φ` 逐次计数每个常元出现，给出元数，于是抽象 `absFo φ` 落在 `1 + countFo φ` 个自由槽位上，恰为元数的后继；`constantsFo φ` 按同一顺序列出诸常元，是 `⟪ A ⟫` 中长度恰合的向量。注意 `nameOf` 接受的是带常元的公式，而非名字的无参分量：抽象发生在定义内部，每个构造子一条子句。

```agda
  nameOf : Formula ⟪ A ⟫ 1 → Name
  nameOf φ = countFo φ , (absFo φ , constantsFo φ)
```

其充分性来自参数抽象定理 `⊨-abs₁`，使用前须先认同空常元域的两种解释。这里有两种读一条无参公式的方式，必须先把二者认同：名字的指称经 `embed` 在常元域 `⟪ A ⟫` 之内读它，而抽象定理在空常元域处读它。两个解释都是从空类型出发的函数，故它们相符；把这个相符说出来，便是这次认同所需的全部验证。

抽象定理 `⊨-abs₁` 谈的是空常元域上的满足，而名字的语义读的是 `⟪ A ⟫` 上的满足。要逐项比较两个陈述，`emptySat` 把「在任意常元解释 `f : ⊥* → DA.SM` 处的满足陈述」固定为一个形状，使改动 `f` 成为把一个函数应用于函数的事。公式本身从不提及常元，正是这一点使这种一致性可用。

```agda
  private
    emptySat : (f : ⊥* {ℓ} → DA.SM) {n : ℕ}
             → DA.SM ^ n → Formula (⊥* {ℓ}) n → hProp (ℓ-suc ℓ)
    emptySat f γ χ = γ ⊨ᶠ χ
      where open SemM.At (⊥* {ℓ}) f using () renaming ( _⊨_ to _⊨ᶠ_ )
```

无参公式的两个常元解释都有类型 `⊥* → DA.SM`：工作语义所用的那个，把每个常元送到 `DA.ι (Empty.rec* b)`；以及消去子 `Empty.rec*` 本身。由于 `⊥*` 没有元素，`funExt` 加上消去子便证得这两个函数相等，即 `sameReading`，无须检视任何东西。随后，`absSat` 陈述的是：指称所用的、经 `embed` 的环境读法，与抽象定理所用的空域读法，在同一个成员 `m` 与同一条抽象公式处相符。

```agda
    sameReading : (λ (b : ⊥* {ℓ}) → DA.ι (Empty.rec* b)) ≡ Empty.rec*
    sameReading = funExt (λ b → Empty.rec* b)

    absSat : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
           → (environment (nameOf φ) m ⊨ᵐ embed (formula (nameOf φ)))
           ≡ ((DA.ι m ∷ []) ⊨ᵐ φ)
```

证明是一条三步的路径。改名引理 `embed-⊨` 说把无参公式嵌入更丰富的常元域不改变它所说的话，这一步把左边搬到带 `Empty.rec*` 标记的读法；`sameReading` 再把指称自己的读法代入其中；最后反着读 `⊨-abs₁`，恰好就是抽象定理对「抽象后的公式在单个参数处的满足」与「原公式的满足」的认同。每一步都是此前某章的定理，只作连接，不作重证。

```agda
    absSat φ m =
        embed-⊨ DA.𝒮M DA.ι (absFo φ)
          (environment (nameOf φ) m)
      ∙ cong (λ f → emptySat f (environment (nameOf φ) m) (absFo φ)) sameReading
      ∙ sym (⊨-abs₁ DA.𝒮M DA.ι φ (DA.ι m))
```

把两种读法在命题层面认同之后，`satAt-abs` 把这一认同从满足陈述提升到集合据以构造的小命题上。它比较 `satAt (nameOf φ) m`，即名字指称背后的小命题，与 `DA.smallSat φ m`，即 `defSet φ` 背后的小命题。两个辅助名 `big` 与 `small` 展开各自的 `⊨ᵐ-small` 对子，使每个方向都能使用两份打包好的等价。

```agda
    satAt-abs : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
              → satAt (nameOf φ) m ≡ DA.smallSat φ m
    satAt-abs φ m = ⇔toPath fwd bwd
      where
      big = DA.⊨ᵐ-small (embed (formula (nameOf φ))) (environment (nameOf φ) m)
```

正向把三次转换复合，全部施加于证明：先把大的等价反向运行，抵达嵌入后的满足陈述；沿路径 `absSat φ m` 把证明搬运到空域陈述；再把小的等价正向运行，抵达 `DA.smallSat φ m`。路径 `absSat φ m` 认同了两个满足类型，普通的传输便可沿所需方向移动证明。命题性用于把满足类型打包成 `hProp`；传输本身只需要这条路径。

```agda
      small = DA.⊨ᵐ-small φ (DA.ι m ∷ [])
      fwd : ⟨ satAt (nameOf φ) m ⟩ → ⟨ DA.smallSat φ m ⟩
      fwd h = equivFun (small .snd) (subst ⟨_⟩ (absSat φ m) (invEq (big .snd) h))
      bwd : ⟨ DA.smallSat φ m ⟩ → ⟨ satAt (nameOf φ) m ⟩
      bwd h = equivFun (big .snd)
```

反向是同一复合、路径取反：`sym (absSat φ m)` 把证明向另一方向搬运，两个等价也以相反次序应用。这里没有证明任何新东西；要点在于，对每个 `m`，`satAt (nameOf φ) m` 与 `DA.smallSat φ m` 是同一个小命题，这正是下一步两个集合得以相等的原因。

```agda
        (subst ⟨_⟩ (sym (absSat φ m)) (invEq (small .snd) h))
```

两个子集都是由 `A` 的成员上的一条小谓词从 `A` 中选出的，故两条谓词一旦相等，两个集合便由一次同余而相等，无须援引外延性。完备性沿那条等式即可得到，而它陈述为截断形式，因为可定义幂集本来就是这样给出一条公式的。

等式 `denote-defSet` 把谓词的相符 `satAt-abs` 变成集合的相等：`funExt` 把逐点相等聚成谓词族的相等，`cong subsetOf` 再把它带到所呈现的集合上。完备性于是取证书 `h : ⟨ x ∈ˢ 𝒟ₒ A ⟩`，用 `𝒟ₒ-inv` 反演，它仅仅给出一条满足 `defSet φ ≡ x` 的公式 `φ`；相应地，结论也是「存在一个名字与一个等式」的截断形式，而非被选定的名字。

```agda
  denote-defSet : (φ : Formula ⟪ A ⟫ 1) → denote (nameOf φ) ≡ DA.defSet φ
  denote-defSet φ = cong subsetOf (funExt (satAt-abs φ))

  names-complete : (x : S) → ⟨ x ∈ˢ 𝒟ₒ A ⟩
                 → ∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁
  names-complete x h = PT.map named (𝒟ₒ-inv A x h)
```

在截断之内，从反演数据到目标对的步骤是平凡的：公式 `φ` 由 `nameOf φ` 命名，所需的等式是 `denote-defSet φ ∙ q`，即从名字的指称到 `defSet φ` 的路径再接上给定的到 `x` 的路径。由于目标 `∥ Σ[ a ∈ Name ] (denote a ≡ x) ∥₁` 是命题，`PT.map` 可以在截断之下工作，把仅仅给出的公式映为仅仅给出的名字，而无须检视它究竟是哪一条。

```agda
    where
    named : Σ[ φ ∈ Formula ⟪ A ⟫ 1 ] (DA.defSet φ ≡ x)
          → Σ[ a ∈ Name ] (denote a ≡ x)
    named (φ , q) = nameOf φ , (denote-defSet φ ∙ q)
```

## 参数向量上的序

参数向量按 `A` 的成员上的既定良序作字典序比较。该关系接受两个可能不同的长度：任一向量先耗尽的混合长度情形都没有前驱；两个非空向量先比较首项，只有首项相等时才继续比较尾部。这样，传递性可以直接用于三个向量各自的实际长度；三歧性则要等元数路径把一个向量传到另一长度后才使用。

这里有两个良序在起作用，且都以短名一次性固定。极限层的序 `limitOrder` 比较公式码，改记为 `_≺_`；模块参数 `w`，即 `A` 的成员上的良序，比较参数，改记为 `_≺ₚ_`。每次开启同时改名了三歧、非自反、传递与良基四条定律，故后文的证明调用任一序的定律时不必写长长的限定名。

```agda
  open SWO limitOrder using () renaming
    ( _<∙_ to _≺_ ; tri∙ to ≺-tri ; irr∙ to ≺-irr
    ; trans∙ to ≺-trans ; wf∙ to ≺-wf )
  open SWO w using () renaming
    ( _<∙_ to _≺ₚ_ ; tri∙ to ≺ₚ-tri ; irr∙ to ≺ₚ-irr
```

比较本身按两个向量的模式匹配定义，向量各带长度索引 `j` 与 `k`。只要有一个向量为空，就不可能再下降，结果类型是空类型：走完的向量在任何位置都无物可低于它。这些情形毫无代价，而它们可反驳这一事实，正是传递性与非自反性的证明所要消耗的。

```agda
    ; trans∙ to ≺ₚ-trans ; wf∙ to ≺ₚ-wf )

  infix 20 _≺ᵥ_
  _≺ᵥ_ : ∀ {j k} → Vec ⟪ A ⟫ j → Vec ⟪ A ⟫ k → Type (ℓ-suc ℓ)
  []      ≺ᵥ []      = ⊥*
  []      ≺ᵥ (y ∷ q) = ⊥*
```

两个非空向量在头部比较：要么头部 `x` 按参数序低于 `y`，要么两条头部经一个路径相等而下降继续进入尾部。严格情形是和的左支，等头情形是右支，故后文的证明可以按「首次判定发生在哪个位置」来分支。注意头部的相等是路径 `x ≡ y`，混合的传递情形将把它代入比较之中。

```agda
  (x ∷ p) ≺ᵥ []      = ⊥*
  (x ∷ p) ≺ᵥ (y ∷ q) = (x ≺ₚ y) ⊎ ((x ≡ y) × (p ≺ᵥ q))
```

四条定律里有三条是当即的归纳。非自反与三歧要求长度相等，因为只有在那里，一个向量才谈得上与另一个相等；传递性则不要求，它拿到三个长度各异的向量，而除「三者皆非空」之外的每个情形都由空类型反驳。

非自反性对向量作归纳证明：一个向量永不可能低于它自己。该陈述只在单一长度处有意义，因为 `p ≺ᵥ p` 要求两次出现的长度相同，而归纳沿尾部消耗短一格处的陈述。接着是传递性的陈述，它同时对三个长度陈述。

```agda
  ≺ᵥ-irr : ∀ {k} (p : Vec ⟪ A ⟫ k) → p ≺ᵥ p → Empty.⊥
  ≺ᵥ-irr []      h             = Empty.rec* h
  ≺ᵥ-irr (x ∷ p) (inl h)       = ≺ₚ-irr x h
  ≺ᵥ-irr (x ∷ p) (inr (_ , h)) = ≺ᵥ-irr p h

  ≺ᵥ-trans : ∀ {i j k} (p : Vec ⟪ A ⟫ i) (q : Vec ⟪ A ⟫ j) (r : Vec ⟪ A ⟫ k)
```

传递性对三个向量同时作情形分析。若第一次下降始于走完的向量，其比较类型已是空类型；中间向量走完时同理；第三个向量走完时，第二个比较可反驳。每种情形的证明都是空类型的消去子，自身不携带任何数学内容。

```agda
           → p ≺ᵥ q → q ≺ᵥ r → p ≺ᵥ r
  ≺ᵥ-trans []      []      r       h k = Empty.rec* h
  ≺ᵥ-trans []      (y ∷ q) r       h k = Empty.rec* h
  ≺ᵥ-trans (x ∷ p) []      r       h k = Empty.rec* h
  ≺ᵥ-trans (x ∷ p) (y ∷ q) []      h k = Empty.rec* k
```

当三个向量都非空时，比较从头部读出，而前两个混合情形是有趣的。若 `x` 低于 `y` 而 `y` 与 `z` 相等，把该路径代入第一个比较即得 `x` 低于 `z`；对称地，先有 `x ≡ y` 再有 `y` 低于 `z`，则沿该路径把第二个比较反方向搬运。二者是同一动作的实例：元素的路径通过搬运作用于比较。

```agda
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inl k) = inl (≺ₚ-trans x y z h k)
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inl h) (inr (e , k)) =
    inl (subst (λ v → x ≺ₚ v) e h)
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inl k) =
    inl (subst (λ v → v ≺ₚ z) (sym e) k)
```

传递性的最后一个情形让两个头部原地不动：两条路径拼接成 `x ≡ z`，递归下降进入尾部，长度随它们各自所带。传递性完成后，三歧性对同一长度的两个向量陈述，因为只有在那里两个向量才谈得上重合；空向量经 `refl` 相等。

```agda
  ≺ᵥ-trans (x ∷ p) (y ∷ q) (z ∷ r) (inr (e , h)) (inr (e' , k)) =
    inr (e ∙ e' , ≺ᵥ-trans p q r h k)

  ≺ᵥ-tri : ∀ {k} (p q : Vec ⟪ A ⟫ k) → Tri (p ≺ᵥ q) (p ≡ q) (q ≺ᵥ p)
  ≺ᵥ-tri []      []      = eq refl
  ≺ᵥ-tri (x ∷ p) (y ∷ q) = decide (≺ₚ-tri x y)
```

非空向量的头部由参数序的三歧性比较，辅助函数 `decide` 把判定从头部搬运到整个向量。无论哪一方的严格判定都变成左支：头部已定，尾部根本不参与。相等情形是唯一必须考察尾部的情形，下一处处理。

```agda
    where
    decide : Tri (x ≺ₚ y) (x ≡ y) (y ≺ₚ x)
           → Tri ((x ∷ p) ≺ᵥ (y ∷ q)) ((x ∷ p) ≡ (y ∷ q)) ((y ∷ q) ≺ᵥ (x ∷ p))
    decide (lt h) = lt (inl h)
    decide (gt h) = gt (inl h)
```

当头部经路径 `e` 相等时，向量比较归结为尾部的比较，`Tri-map` 把三种结果重新标记。尾部严格更低变成右支 `e , h`；尾部相等在 `cong₂ _∷_` 之下变成整个向量的相等；镜像的判定则附上 `sym e`。递归在尾部上是结构的，归纳就此闭合。

```agda
    decide (eq e) =
      Tri-map (λ h → inr (e , h)) (cong₂ _∷_ e) (λ h → inr (sym e , h))
        (≺ᵥ-tri p q)
```

需要谋划的是良基性。从一个向量向下走，头部或者按给定的序下降，此时尾部被换成同长的任意一个；或者头部不动而尾部下降。故这次下降是两层嵌套的归纳：头部用给定序的良基性，尾部用尾部的可及性，而那些任意的尾部由「短一格的那条陈述」供给。正是这第三样配料使整件事也对长度递归，也正因如此，头部的归纳取作归纳原理而非取作第二个递归实参：若三副胃口都在同一场递归里伺候，那次下降就交不出单一的递减尺度。

辅助函数 `consAcc` 把可及性从长度 `k` 提升到长度 `suc k`：在「长度 `k` 的每个向量都可及」的前提下，它为 `y ∷ q` 构造可及性。输入 `prev` 正是前一长度处的陈述，这使得严格情形能把尾部换成同长的任意 `r`。证明随后对头部运行给定序的良基归纳，于是头部的下降是引擎，尾部的可及性在其内部被消耗。

```agda
  private
    consAcc : (k : ℕ) → ((r : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) r)
            → (y : ⟪ A ⟫) (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
            → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
    consAcc k prev = WFI.induction ≺ₚ-wf onHead
```

归纳假设 `ih` 的陈述很讲究：对每个严格低于 `y` 的 `z`，在给定尾部自身可及性的前提下，`z ∷ q` 的可及性对**每个**长度为 `k` 的尾部 `q` 都成立。对 `q` 的全称量化使严格情形无须对被考察的向量作递归即可工作，而这恰恰因为 `≺ₚ-wf` 是被当作归纳原理使用，而不是被递归地调用。

```agda
      where
      onHead : (y : ⟪ A ⟫)
             → ((z : ⟪ A ⟫) → z ≺ₚ y → (q : Vec ⟪ A ⟫ k)
                  → Acc (_≺ᵥ_ {k} {k}) q → Acc (_≺ᵥ_ {suc k} {suc k}) (z ∷ q))
             → (q : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) q
```

可及性是被构造的数据：`acc` 把一个元素与一个函数配对，该函数把每个严格更低的元素送到它自身的可及性。于是 `y ∷ q` 的目标由 `acc` 给出，应用于一个必须处理「从 `y ∷ q` 出发的严格下降」的两种形状的步进函数，证明的余下部分就是这个步进函数的主体。

```agda
             → Acc (_≺ᵥ_ {suc k} {suc k}) (y ∷ q)
      onHead y ih q (acc rq) = acc step
        where
        step : (r : Vec ⟪ A ⟫ (suc k)) → r ≺ᵥ (y ∷ q)
             → Acc (_≺ᵥ_ {suc k} {suc k}) r
```

严格情形中头部 `z` 低于 `y`，尾部 `r` 是任意的，这里归纳假设完成全部工作：它由 `z ≺ₚ y` 与 `prev r`，即 `r` 在长度 `k` 处的可及性，供给 `z ∷ r` 的 `Acc`。相等情形保留头部：路径把 `z` 与 `y` 认同，故沿 `sym e` 把 `y ∷ r` 的可及性反向搬运，得到 `z ∷ r` 的可及性。沿头部路径的这一搬运是跨长度比较的代价，在此一次性付清。

```agda
        step (z ∷ r) (inl h)       = ih z h r (prev r)
        step (z ∷ r) (inr (e , h)) =
          subst (λ v → Acc (_≺ᵥ_ {suc k} {suc k}) (v ∷ r)) (sym e)
            (onHead y ih r (rq r h))

  ≺ᵥ-wf : (k : ℕ) (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
```

主定理对长度作归纳。空向量的可及性是当即的：它唯一的准前驱是空向量自身，而那个比较是空类型。对 `x ∷ p`，应用 `consAcc`，以 `≺ᵥ-wf k` 供给前一长度处对任意尾部的陈述，以 `≺ᵥ-wf k p` 供给本向量自身尾部的可及性；二者都来自对 `k` 的一次结构递归。

```agda
  ≺ᵥ-wf zero    []      = acc (λ { [] h → Empty.rec* h })
  ≺ᵥ-wf (suc k) (x ∷ p) = consAcc k (≺ᵥ-wf k) x p (≺ᵥ-wf k p)
```

还有一件派生的事实随这次比较同行，并由一次路径归纳证出：把一个向量沿长度的等式搬过去，不改变它在谁之下、在谁之上。需要它的有两处，即三歧与下降，二者遇到的都是「长度相等但并非同一」的两个向量。

左边的引理说：比较 `subst (Vec ⟪ A ⟫) e p ≺ᵥ q` 与 `p ≺ᵥ q` 之间是一条路径，即沿长度等式 `e` 搬运被比较的向量不改变比较命题本身。证明完全不展开向量的情形。一般引理 `constSubstCommSlice` 说，沿 `e` 的搬运与「不使用该索引的类型族」可交换，而对固定的 `q` 作比较恰是这样的类型族；`sym` 把等式调到后文证明所需的方向。

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

右边的引理是镜像：把**另一个**向量沿它自己的长度等式搬过去，不改变在它之下的东西。两个方向都需要，因为名字比较在 `lt` 情形把第一个名字的参数搬到第二个的长度，在 `gt` 情形方向相反，而后文的良基性证明两边都要搬。两个朝向一次证完，此后的证明就不必再对向量上的 `subst` 说理。

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

## 三个键，依次

名字依次按公式码、元数与参数向量作字典序比较。比较写成三个明确情形，因而三歧性与传递性都可逐键证明。

这个比较是从定义直接读出的类型族。其外侧的和支是公式码在极限序下的严格比较：若一个名字的码低于另一个的，码即判定，其余一概不问。右侧的和支携带路径 `codeOf b ≡ codeOf a`，即允许进入下一个键的码相等，并把它与第二个键的比较打包，即自然数元数的严格不等。

```agda
  infix 20 _≺ₙ_
  _≺ₙ_ : Name → Name → Type (ℓ-suc ℓ)
  a ≺ₙ b = (codeOf a ≺ codeOf b)
         ⊎ ( (codeOf b ≡ codeOf a)
           × ( (arity a < arity b)
```

最内侧的和支完成下降：在码相等且元数相等之下 (后者同样以路径 `arity b ≡ arity a` 携带)，参数向量由 `_≺ᵥ_` 比较。因此嵌套的每一层都是「前一个键的相等」与「下一个键的严格比较」的对，四条定律的情形分析正是沿这一形状逐键进行。

```agda
             ⊎ ((arity b ≡ arity a) × (params a ≺ᵥ params b)) ) )
```

于是非自反与传递就是三个键各自的定律，按情形归类。传递性的混合情形把一个键上的等式代入另一个键的比较，所需的验证仅此而已；参数那一情形援引三个长度上的向量比较，而这正是当初把那一条跨长度证出的原因。

一个名字永不可能严格低于它自己，三个子句各道其由：无论哪个和支见证 `a ≺ₙ a`，都等于见证三个键中某键从自身到自身的严格下降。码的情形与极限序的非自反性矛盾；元数的情形是自然数严格小于自身，由 `¬m<m` 反驳；参数的情形与 `params a` 自身长度处的向量非自反性矛盾。

```agda
  ≺ₙ-irr : (a : Name) → a ≺ₙ a → Empty.⊥
  ≺ₙ-irr a (inl h)                 = ≺-irr (codeOf a) h
  ≺ₙ-irr a (inr (_ , inl h))       = ¬m<m h
  ≺ₙ-irr a (inr (_ , inr (_ , h))) = ≺ᵥ-irr (params a) h

  ≺ₙ-trans : (a b c : Name) → a ≺ₙ b → b ≺ₙ c → a ≺ₙ c
```

传递性对三个名字陈述，按两次比较各自在何处判定作情形分析。当二者都在码处判定时，直接援引极限序的传递性。第一个混合情形中，`a` 在码处严格低于 `b`，而第二次比较只知道 `codeOf c ≡ codeOf b`；把该等式反向代入，即得 `codeOf a` 低于 `codeOf c`；对称的情形是同一次代入正向读出。每个混合情形只是一次搬运，别无其他。

```agda
  ≺ₙ-trans a b c (inl h) (inl k) =
    inl (≺-trans (codeOf a) (codeOf b) (codeOf c) h k)
  ≺ₙ-trans a b c (inl h) (inr (q , _)) =
    inl (subst (λ v → codeOf a ≺ v) (sym q) h)
  ≺ₙ-trans a b c (inr (q , _)) (inl k) =
```

在元数键处判定的诸情形以自然数重复同一模式。两条严格的元数不等经 `<-trans` 复合；严格不等与元数相等并列时，代换相应的端点即被搬运成严格不等。注意所携路径的方向：比较记录的是 `codeOf b ≡ codeOf a` 与 `arity b ≡ arity a`，即陈述在更大的名字处的相等，故拼接与代换都逆着这一朝向进行。

```agda
    inl (subst (λ v → v ≺ codeOf c) q k)
  ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inl k)) =
    inr (q' ∙ q , inl (<-trans h k))
  ≺ₙ-trans a b c (inr (q , inl h)) (inr (q' , inr (e , _))) =
    inr (q' ∙ q , inl (subst (λ j → arity a < j) (sym e) h))
```

最后的情形是三个键直到参数处都相符，而这里恰需第三个键在三个可能不同的长度上的传递性：`≺ᵥ-trans` 接受各带其长度的 `params a ≺ᵥ params b` 与 `params b ≺ᵥ params c`，返回 `params a ≺ᵥ params c`。两条元数路径拼接成 `arity a ≡ arity c`，右支的三个分量就此齐备。

```agda
  ≺ₙ-trans a b c (inr (q , inr (e , _))) (inr (q' , inl k)) =
    inr (q' ∙ q , inl (subst (λ j → j < arity c) e k))
  ≺ₙ-trans a b c (inr (q , inr (e , h))) (inr (q' , inr (e' , k))) =
    inr (q' ∙ q , inr (e' ∙ e , ≺ᵥ-trans (params a) (params b) (params c) h k))
```

三歧性是第三条定律，也是逐字读出比较本身而非组合前两条定律的那一条。证明沿诸键依次下降：若码已经判定，结论立即给出；若码相等，则由元数判定；若元数也相等，则由参数向量判定。只有最后一步需要用心。相等的元数由一条路径相连而非被等同，因此 `params a` 与 `params b` 处在不同的长度上；必须先把前者传输到后者的长度，向量比较才能进行，而比较返回的严格判决也要传回原类型，才算原有两个名字之间的比较。相等情形还需要更多：两个名字要作为相等的依值三元组呈现出来，故两条公式本身必须一致，而这正是码的单射性所给出的，因为 `code-shift` 表明沿元数路径的传输不改变码，而码上的判定说明码本来就已相等。

结论的类型是 `Tri`，即三选一的判定，携带或是 `a ≺ₙ b` 的证明、路径 `a ≡ b`、或是 `b ≺ₙ a` 的证明。证明把整个问题交给码上的序：`≺-tri` 已经对两个码给出这样的判定，局部辅助函数 `byCodes` 再把码层面的判定转换为名字层面的判定。先以类型引入这个辅助函数，使转换的形状在各子句之前就可看见。

```agda
  ≺ₙ-tri : (a b : Name) → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
  ≺ₙ-tri a b = byCodes (≺-tri (codeOf a) (codeOf b))
    where
    byCodes : Tri (codeOf a ≺ codeOf b) (codeOf a ≡ codeOf b) (codeOf b ≺ codeOf a)
            → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
```

严格情形是直接的：无论偏向哪一方，码上的严格比较正是名字序和类型的左支。相等的情形则打开第二个键，交给 `byArities`，它对元数做的事正如 `byCodes` 对码做的事。

```agda
    byCodes (lt h) = lt (inl h)
    byCodes (gt h) = gt (inl h)
    byCodes (eq ec) = byArities (arity a ≟ arity b)
      where
      byArities : NatOrder.Trichotomy (arity a) (arity b)
```

这里的判定取和的右支，并携带码等式本身。请注意方向：比较记录的是在较大名字处陈述的 `codeOf b ≡ codeOf a`，所以这一侧的严格情形需要 `sym ec`，而对偶情形需要照原样的 `ec`。当元数也相等时，由 `≺ᵥ-tri` 比较向量；但 `params a` 位于长度 `arity a`，`params b` 位于 `arity b`，所以第一个向量要沿元数路径 `e` 传输之后才能比较。

```agda
                → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
      byArities (NatOrder.lt h) = lt (inr (sym ec , inl h))
      byArities (NatOrder.gt h) = gt (inr (ec , inl h))
      byArities (NatOrder.eq e) =
        byParams (≺ᵥ-tri (subst (Vec ⟪ A ⟫) e (params a)) (params b))
```

被传输的向量得到一个名字 `shifted`，使下面的陈述能在各自真实的长度上保持可读。相等情形需要的还不止向量：要直接得出 `a ≡ b`，两条公式也必须一致，`sameFormula` 就是在被传输的公式处陈述这一点，后者的类型正是元数为 `arity b` 的名字的公式的类型。若没有这样一条等式，两个名字可能在两个已判定的键与参数上都相符，语法上却仍不相同。

```agda
        where
        shifted : Vec ⟪ A ⟫ (arity b)
        shifted = subst (Vec ⟪ A ⟫) e (params a)

        sameFormula : subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a)
                    ≡ formula b
```

两条公式为何一致：由 `code-shift`，把 `formula a` 沿 `e` 传输不改变它的码，而 `ec` 的第一个分量说明 `formula a` 的码等于 `formula b` 的码。串接二者即得相同的码，再由 `code-inj` 把相同的码还原为相等的无参公式。这正是本章前面证过的那条单射性，在此完成它的陈述所预示的工作。备好 `shifted` 与 `sameFormula` 之后，`byParams` 便把向量层面的判定转换为名字层面的判定。

```agda
        sameFormula =
          code-inj (subst (λ k → Formula (⊥* {ℓ}) (suc k)) e (formula a))
            (formula b)
            (code-shift e (formula a) ∙ cong fst ec)

        byParams : Tri (shifted ≺ᵥ params b) (shifted ≡ params b)
```

严格判决是在被传输的长度处得到的，所以它们的陈述要传回。`≺ᵥ-subst-left` 说：把 `subst (Vec ⟪ A ⟫) e p` 与 `q` 相比，作为命题与把 `p` 与 `q` 相比相同；把 `h` 沿这条等式传输，就把对 `shifted` 的比较换成对 `params a` 的比较。每个判决还要携带码等式与元数等式，方向按和的要求放置。对偶情形对称，在比较的另一侧使用 `≺ᵥ-subst-right`。

```agda
                       (params b ≺ᵥ shifted)
                 → Tri (a ≺ₙ b) (a ≡ b) (b ≺ₙ a)
        byParams (lt h) = lt (inr (sym ec , inr (sym e ,
          transport (≺ᵥ-subst-left e (params a) (params b)) h)))
        byParams (gt h) = gt (inr (ec , inr (e ,
```

相等判定是 `Name` 中两个元素之间的路径，而 `Name` 本身是个三元组。`ΣPathP` 把元数路径 `e` 与其余分量之间的路径配对：`toPathP sameFormula` 把公式等式沿类型族 `Formula (⊥*) (suc k)` 提升，`toPathP ep` 对向量等式做同样的事。这正是 `sameFormula` 的用武之地：在两个已判定的键相等、参数也相等之后，缺的只是公式等式，而它一旦补上，两个名字作为数据便完全相同。

```agda
          transport (≺ᵥ-subst-right e (params b) (params a)) h)))
        byParams (eq ep) =
          eq (ΣPathP (e , ΣPathP (toPathP sameFormula , toPathP ep)))
```

## 沿三个键下降

良基性来自嵌套下降，一个键一层。最内层，码与元数固定，诸参数下降，递减的实参是向量的可及性；中间一层，码固定，元数下降；最外层，码下降。每一层各是一个函数，把外层的诸归纳假设当实参收进来，于是每一层恰对一份可及性证明递归，且处处都是结构递归。一切陈述都落在名字自身上，连同说明各键位置所在的等式；这正是三歧处同一条规矩的再现：陈述在名字诸投影上的内容，必须与陈述在名字上的内容对得上。

最内层是一个函数，其参数序列把整幅下降图景一次记录完毕。它拿到的有：一个固定的码 `c`；覆盖所有码小于 `c` 的名字的外层归纳假设 `ihC`；一个界 `k`；覆盖码为 `c` 且元数小于 `k` 的名字的中层归纳假设 `ihK`；一个参数向量 `p` 连同它自身的向量可及性；以及所研究的名字 `a`，并带三条等式：`qc` 把码固定在 `c`，`ek` 把元数固定在 `k`，`qp` 把传输后的参数认同为 `p`。结论只是：`a` 可及。

```agda
  private
    accAtParam : (c : Limit)
               → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
               → (k : ℕ)
               → ((b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b)
```

向量可及性参数的类型陈述在单一长度 `k` 上，与 `p` 相配；这正是参数要经等式 `qp` 传输到 `p` 的长度、而非就地比较的原因。`a` 的可及性由构造子 `acc` 连同一个步进函数给出：要证每个名字可及，只需对每个 `a` 展示一个函数，它接收任一位于 `a` 之下的 `b` 并返回 `b` 的可及性。

```agda
               → (p : Vec ⟪ A ⟫ k) → Acc (_≺ᵥ_ {k} {k}) p
               → (a : Name) → codeOf a ≡ c → (ek : arity a ≡ k)
               → subst (Vec ⟪ A ⟫) ek (params a) ≡ p
               → Acc _≺ₙ_ a
    accAtParam c ihC k ihK p (acc rp) a qc ek qp = acc step
```

步进函数按哪个键判定 `b ≺ₙ a` 分情形。若码下降，`qc` 把 `codeOf b ≺ codeOf a` 传成 `codeOf b ≺ c`，外层归纳假设即告完成。若元数判定，这个前驱判断携带 `q : codeOf a ≡ codeOf b`，故有 `sym q ∙ qc : codeOf b ≡ c`。再沿 `ek : arity a ≡ k` 把 `arity b < arity a` 传成 `arity b < k`，中层归纳假设便可应用。

```agda
      where
      step : (b : Name) → b ≺ₙ a → Acc _≺ₙ_ b
      step b (inl h)           = ihC b (subst (λ v → codeOf b ≺ v) qc h)
      step b (inr (q , inl h)) = ihK b (sym q ∙ qc) (subst (λ j → arity b < j) ek h)
      step b (inr (q , inr (e , h))) =
```

剩下的是参数键，也是最内层中唯一递归的情形。对前驱判断 `b ≺ₙ a`，这一分支给出 `e : arity a ≡ arity b`，而 `ek : arity a ≡ k` 把当前名字固定到元数 `k`。因此 `eb = sym e ∙ ek` 的类型是 `arity b ≡ k`；沿它传输 `params b`，便得到固定长度处的前驱向量 `pb`。码等式则独立地由 `sym q ∙ qc` 对齐。

```agda
        accAtParam c ihC k ihK pb (rp pb hb) b (sym q ∙ qc) eb refl
        where
        eb : arity b ≡ k
        eb = sym e ∙ ek
        pb : Vec ⟪ A ⟫ k
```

严格比较 `h` 是在各自长度上于 `params b` 与 `params a` 之间作出的，而所用的可及性属于 `p`。两步即可弥合差距：`≺ᵥ-subst-left` 与 `≺ᵥ-subst-right` 说沿长度等式的传输不改变向量在谁之下，故先把 `h` 改写成界长度处的比较；再由 `qp` 把右端点从 `params a` 传到 `p`，得 `hb : pb ≺ᵥ p`。递归调用把 `hb` 交给 `rp`，即 `p` 的可及性，并返回 `b` 的可及性。

```agda
        pb = subst (Vec ⟪ A ⟫) eb (params b)
        hb : pb ≺ᵥ p
        hb = subst (λ v → pb ≺ᵥ v) qp
          (transport (sym (≺ᵥ-subst-right ek pb (params a)))
            (transport (sym (≺ᵥ-subst-left eb (params b) (params a))) h))
```

中间一层固定一个码，沿元数下降。它的参数序列更短：码的归纳假设 `ihC`、带自身自然数序可及性的界 `k`、以及码固定在 `c`、元数固定在 `k` 的那个名字。接替向量可及性的正是自然数可及性 `rk`，因为元数键在 ℕ 中下降。

```agda
    accAtArity : (c : Limit)
               → ((b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b)
               → (k : ℕ) → Acc _<_ k
               → (a : Name) → codeOf a ≡ c → arity a ≡ k → Acc _≺ₙ_ a
    accAtArity c ihC k (acc rk) a qc ek =
```

主体把一切交给最内层：参数被传输到 `k`，而其向量可及性由 `≺ᵥ-wf` 直接给出，后者对每个长度上的每个向量都成立，此处不需要递归。真正的归纳只在元数上进行：局部的 `ihK` 拆开自然数可及性 `rk`，于是码为 `c` 且元数严格更小的名字由在那个更小界处的递归调用处理。这一层把「任一名字的严格更小的元数」变成「更小的界」。

```agda
      accAtParam c ihC k ihK (subst (Vec ⟪ A ⟫) ek (params a))
        (≺ᵥ-wf k (subst (Vec ⟪ A ⟫) ek (params a))) a qc ek refl
      where
      ihK : (b : Name) → codeOf b ≡ c → arity b < k → Acc _≺ₙ_ b
      ihK b q h = accAtArity c ihC (arity b) (rk (arity b) h) b q refl
```

最外层沿码下降，根本不需要关于元数的等式。给定码 `c` 的可及性以及码为 `c` 的名字，它在界 `arity a` 处调用中间层，并直接供给那个无条件成立的自然数可及性。局部的 `ihC` 拆开码的可及性：码严格更小的名字在它自己的码处得到一次递归调用。这与中间一层完全镜像，只是再往外一层。

```agda
    accAtCode : (c : Limit) → Acc _≺_ c → (a : Name) → codeOf a ≡ c → Acc _≺ₙ_ a
    accAtCode c (acc rc) a qc =
      accAtArity c ihC (arity a) (<-wellfounded (arity a)) a qc refl
      where
      ihC : (b : Name) → codeOf b ≺ c → Acc _≺ₙ_ b
```

最后的定理是三层的一行复合。给定名字 `a`，码序自身的良基性给出 `codeOf a` 的可及性，最外层把它转换成 `a` 的可及性，其中码等式由反身性成立。于是每个名字在三键比较之下都可及，这正是严格良序的良基性定律。

```agda
      ihC b h = accAtCode (codeOf b) (rc (codeOf b) h) b refl

  ≺ₙ-wf : WellFounded _≺ₙ_
  ≺ₙ-wf a = accAtCode (codeOf a) (≺-wf (codeOf a)) a refl
```

## 束，与最小的名字

四条定律说明诸名字带有严格良序，而把它们打包进该结构的记录，就能把这个序交给一般的极小元搜索。把这个序交给搜索，一族仅仅非空的名字就变成一个确定的极小元：构造诸名字的目的正在于此，因为单一层之上的一族集合成为一族名字，而一族名字有极小元。

记录 `nameOrder` 把已证的四条定律逐场收拢：比较本身、三歧性、非自反性、传递性与良基性。这里没有证明任何新东西；打包的意义在于，后续构造可以直接使用一个严格良序，而无须知道这一个是如何拼装的。

```agda
  nameOrder : SWO (Name)
  nameOrder = record
    { _<∙_   = _≺ₙ_
    ; tri∙   = ≺ₙ-tri
    ; irr∙   = ≺ₙ-irr
```

极小元搜索照字面兑现这份记录。它的族实参是映入 `hProp` 的函数，性质陈述在每个名字上；假设是截断 `∥ Σ ... ∥₁`，即仅仅非空，不携带任何被选出的见证；结论则是一对显式的名字与它的最小性，终究是被选出的见证，由 `leastOf` 借助模块的经典假设 `lem` 抽出。截断之所以能消去，是因为极小见证的整个类型 `Σ[ a ∈ Name ] IsLeast nameOrder P a` 是命题：任意两个极小见证由三歧性得到相等。因此经典下降把名字族的仅仅非空转化为一个确定的极小名字。

```agda
    ; trans∙ = ≺ₙ-trans
    ; wf∙    = ≺ₙ-wf }

  leastName : (P : Name → hProp (ℓ-suc ℓ))
            → ∥ Σ[ a ∈ Name ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ Name ] IsLeast nameOrder P a
  leastName = leastOf nameOrder lem
```

## 小结

现在，后继层的每个成员都有名字，而诸名字带有严格良序，因而可以选出最小代表。一个 `Name` 由一个元数、一条多一个变量的无参公式，以及一个取自该层的参数向量组成；`denote` 是它所界定的子集，而 `denote-mem` 在可定义幂集据以定义的内层语义中陈述这一点。`names-complete` 说明后继层的每个成员都由某个名字指称；该存在结论是截断的，因为可定义幂集本来就是这样给出它的公式的。

`code∈limit` 把第一个键放到极限层那个序可以比较它的地方，而 `code-inj` 在元数对齐后保证编码单射：此时相等的码还原出相等的无参公式。`_≺ᵥ_` 跨长度地为第三个键排序，而 `_≺ₙ_` 就是三键比较本身，连同严格良序的全部四条定律，以及 `leastName`，即非空族的最小名字。两者的组合正是后续选择构造所消费的：单一层之上的一族子集成为一族名字，而 `leastName` 选出一个典范代表，自始至终不必从截断的完备性陈述里挑选公式。