---
title: "有限层上的良序"
module: L.Choice.FiniteStageOrders
lang: zh
site: "Bedrock"
description: "有限层上的良序"
stage: "典范良序与选择公理"
reading_order: 74
canonical: https://bedrock.institute/zh/L.Choice.FiniteStageOrders.html
html: L.Choice.FiniteStageOrders.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/FiniteStageOrders.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal, L.Axioms.Basic, L.WellOrder.Base]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.Choice.FiniteStageOrders.md, https://bedrock.institute/ja/L.Choice.FiniteStageOrders.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 有限层上的良序

本章证明每个以数码为索引的层都是有穷的，并以最先分歧赋予其良序；随后结合层号与局部序来良序化极限层。

先前的选择构造为一个族的每一格定位了该格首次拥有成员的层，并证明了它是一个后继。于是该格中恰在那里现身的每个成员，都是同一个集合的可定义子集：一个写在单一层之上的名字。尚缺的是**比较**这些名字的办法，而本章要在塔的底部造出的正是这种比较。

本章依赖两个论断。第一，凡以数码为索引的层都是有穷的，其确切含义见下文：它附带一份有穷的集合清单，清单包含它的全部成员。第二，有穷层带有一个良序：比较两个成员时，看它们最先在何处出现分歧，并把较大的位置判给含有该处的那一个。

第二个论断才是数学内容所在，它本质上是关于**有穷**集合的论断。若把同一构造用于自然数的子集，就会出现无穷下降：先是全体自然数，然后是从一开始的全体，再是从二开始的全体，如此下去，每一步删去尚存者中最先的那一个，因而严格落到更低处。构造本身并不排除这种情形；在有穷基底上，只有有穷多个子集，因此寻找最小成员的过程会终止。下文据此证明良基性：一份有穷清单加上一个线序，可以为任何非空性质给出最小成员，方法是逐项检查清单，并在每一步保留截至该处最小的候选；而「每个非空性质都有最小成员」在经典意义下就是良基性。

有穷性能沿塔逐层推广，是因为有穷集合的可定义子集就是它的全部子集，而带清单的集合只有有穷多个子集，清单上的每个位向量对应其中一个。于是一层的清单给出下一层的清单，递归便足以推进整个构造。

极限层的构造无须假设或证明各有穷层序之间相容。它先比较元素首次出现的层号；层号相同，才使用该层自己的序。因此，不同层的元素由层号比较，同一层首次出现的元素由局部序比较。

讨论的舞台是建立在累积层级 $V$ 之上的可构造宇宙。排中律在这里作为显式假设出现：整个模块由一个参数 `lem` 给出，它对层级 `ℓ-suc ℓ` 上的每个命题作出判定。本章需要的正是这一个层级，下文的所有构造都可以使用这一固定判定；对于其他层级上的命题，除已证明的定理所述内容外，不作任何论断。

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

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

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

下文使用的名称都来自可构造层级：塔的层 `Lset α`、产生一层的全部可定义子集的算子 `𝒟ₒ`，以及数码 `# n` 是序数这一事实 `numeral-ord`。于是每个有限层 `Lset (# n)` 都是真正的层，这正是后续各节的递归能沿数码攀爬的原因。这里还引入了 `Lset-suc` 与 `FinOf` 相关工具，它们把一层与其内部的有穷集合联系起来。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-out; 𝒟ₒ; 𝒟ₒ∋⊆ )
open import L.Ordinal {ℓ} using ( numeral-ord )
open import L.Axioms.Basic {ℓ}
```

比较需要一个满足三分律的基底序。自然数上的序 `natOrder` 是一个严格强良基的线序，打包为 `SWO`，其三情形比较 `Tri` 分为 `lt`、`eq`、`gt` 三种。后面各节的搜索程序都针对这一接口编写，因此适用于任何 `SWO`；而自然数的实例正是用来给数码排序的那一个。

```agda
  using ( finSet; finSet-in; finSet-out; Lset-suc; module FinOf )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; leastOf; natOrder )

open import Cubical.Data.Bool using ( Bool; true; false; false≢true )
open import Cubical.Data.Nat using ( _+_ )
```

布尔值在这里作为掩码出现：要枚举带点名册的集合的子集，就把每个条目保留或丢弃，用 `Bool` 上的 `true` 或 `false` 记录，而 `false≢true` 保证二者可区分。在索引一侧，自然数用严格序 `_<_` 比较，它是传递且良基的，由 `¬m<m` 排除自环，并可用 `_≟_` 判定相等。这些恰好是找出见证某性质的最小下标所需的性质，也是扫描中作出逐步判定所需的性质。

```agda
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
```

这里的良基性由可达性谓词 `Acc` 表达：一个点是可达的，当且仅当它的每个前驱都可达，由构造子 `acc` 封装。当关系的一切点都可达时，称它具有 `WellFounded` 类型。`Acc` 上的证明义务都是命题，这一事实由 `isPropAcc` 记录，并在从「仅仅存在」的数据消去到可达性陈述时用到。模块 `WFI` 提供消费良基关系的递归原理。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; isPropAcc; module WFI )
```

对累积层级中的集合 `x`，`⟪ x ⟫` 是它的小呈现类型，`⟪ x ⟫↪` 把该类型嵌入层级。等价 `∈∈ₛ` 联系呈现中的成员关系与层级成员关系，`∈-asFiber` 则从成员证明恢复索引及其等同路径。空集给出第零层，冯·诺伊曼数码 `# n` 及其极限 `ω` 用来索引诸有穷层与极限。

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

下文的隶属陈述取命题为值。因此，`⟨ x ∈ˢ A ⟩` 是 `x` 属于 `A` 的证据类型；点名册用这一形式证明每个列出项确实属于集合，并陈述每个成员都被表示。

```agda
open InfinitySet using ( #_; ω )

open hPropStructure 𝒮ᵥ
```

## 点名册

`Tally` 用一个有穷索引族呈现集合的每个成员，允许重复，也不要求单射性或可判定相等。

有穷性以**点名册**的形式引入：取一个数和一个由相应多个集合组成的族，族中的每个集合都属于 `A`，并要求「`A` 的每个成员都仅仅等于其中某一个」。`onto` 表示该族列出了 `A` 的所有成员。

重复与不可判定的相等都不造成困难。扫描可以再次遇到同一元素，位向量也按位置记录取舍，即使两个位置名指同一集合亦然。因此，这种刻意保持较弱的有穷性概念能在下一层的构造中保持下去。

集合 `A` 的点名册有三个数据字段：数 `size` 决定列出的条目数，`item` 把每个合法位置 (即 `Fin size` 的元素) 映为集合 `item i`，而字段 `inside` 证明每个被列出的条目确实属于 `A`。没有这一条，更长的清单会平凡地覆盖较小的集合。注意同一元素完全可能出现在多个位置上：record 并不禁止这一点，也没有任何字段询问两个位置上的集合是否相同。

```agda
record Tally (A : S) : Type (ℓ-suc ℓ) where
  field
    size   : ℕ
    item   : Fin size → S
    inside : (i : Fin size) → ⟨ item i ∈ˢ A ⟩
```

第四个字段陈述覆盖性。给定 `x` 及其属于 `A` 的证明，`onto` 返回「索引 `i` 配路径 `item i ≡ x`」的命题截断。因此，只能得到某个索引仅仅存在，而不会暴露一个选定位置。后文只在目标为命题时消去这份截断见证。

```agda
    onto   : (x : S) → ⟨ x ∈ˢ A ⟩ → ∥ Σ[ i ∈ Fin size ] (item i ≡ x) ∥₁
```

## 劈开一个有穷索引

`splitFin` 与 `joinFin` 把小于和数的索引与某个加数中的索引对应起来，提供枚举掩码所需的算术。

为幂集清点需要枚举位向量，而长度为 `n + 1` 的向量个数是长度为 `n` 的两倍。因此需要一项索引算术：小于 `a + b` 的索引对应于小于 `a` 的索引或小于 `b` 的索引，反之亦然。后文只使用其中一个方向，所以这里只证明该方向；`bumpLeft` 是使沿 `a` 的递归通过类型检查所需的移位。

一个具体的图景有帮助。取 `a = 2`、`b = 3`，小于 `5` 的索引恰好等于「小于 `2` 的索引或小于 `3` 的索引」：`joinFin` 把左加数放进前两个位置、把右加数放进后三个位置，而 `splitFin` 询问一个索引落入哪个区域。这里与重复无关，因为这两张图关心的是位置，而不是日后放在位置上的条目。

第一张图处理左端增加一的和。`bumpLeft` 取一个属于 `a` 或 `b` 的索引，给出一个属于 `suc a` 或 `b` 的索引：左边的索引被外推一格，右边的原样保留。它本身没有内容，存在的原因只是 `splitFin` 的递归步会从左加数剥掉一格，需要一个移位把左索引放回正确的类型。注意 `joinFin` 只给出了从 `Fin a ⊎ Fin b` 到 `Fin (a + b)` 的方向，且 `a` 显式给出，以便递归能对它作模式匹配。

```agda
bumpLeft : {a b : ℕ} → Fin a ⊎ Fin b → Fin (suc a) ⊎ Fin b
bumpLeft (inl i) = inl (suc i)
bumpLeft (inr j) = inr j

joinFin : (a : ℕ) {b : ℕ} → Fin a ⊎ Fin b → Fin (a + b)
joinFin zero    (inr j)       = j
```

`joinFin` 与 `splitFin` 形状上互为逆映射，不过后文只证明一个方向的往返。`joinFin` 沿 `a` 递归：`a` 为零时，小于 `0 + b` 的索引就是小于 `b` 的索引；`a` 为后继时，第一个位置属于左加数，于是位置为零的左索引映到零号位置，其余一律上移一格。`splitFin` 沿同一递归倒着走：小于 `a + b` 的索引先问它是否小于 `a`，后继情形用 `bumpLeft` 恢复被剥掉的类型。

```agda
joinFin (suc a) (inl zero)    = zero
joinFin (suc a) (inl (suc i)) = suc (joinFin a (inl i))
joinFin (suc a) (inr j)       = suc (joinFin a (inr j))

splitFin : (a : ℕ) {b : ℕ} → Fin (a + b) → Fin a ⊎ Fin b
splitFin zero    j       = inr j
```

往返 `split-join` 说的是：对刚刚拼合的索引再作劈分，就回到原来的左或右索引。每条子句要么是 `refl`，要么是对递归路径施用 `cong`：`splitFin (joinFin x)` 的计算已经归约到对递归答案施加 `bumpLeft`，而 `cong bumpLeft` 把归纳假设穿过这一移位。相反的复合从未被断言，这里也没有任何关于「拼合是单射」的主张。

```agda
splitFin (suc a) zero    = inl zero
splitFin (suc a) (suc i) = bumpLeft (splitFin a i)

split-join : (a : ℕ) {b : ℕ} (x : Fin a ⊎ Fin b) → splitFin a (joinFin a x) ≡ x
split-join zero    (inr j)       = refl
split-join (suc a) (inl zero)    = refl
```

这一算术给掩码一节带来的是对规模的精确记账。当长度 `suc n` 的掩码枚举在 `maskCount n` 处把索引一分为二时，`splitFin` 判定首位是 `false` 还是 `true`，并把剩下的索引交给 `n` 处的递归；`mask-onto` 与 `split-join` 合起来证明每个位向量都被触及。

```agda
split-join (suc a) (inl (suc i)) = cong bumpLeft (split-join a (inl i))
split-join (suc a) (inr j)       = cong bumpLeft (split-join a (inr j))
```

## 枚举掩码

`maskAt` 枚举固定长度的全部布尔向量，而 `mask-onto` 证明每种选取模式都会出现。

长度为 `n` 的**掩码**是一个 `n` 位向量；对已经清点的集合，它指明保留哪些条目。共有 `maskCount n` 个掩码，即二的 `n` 次幂，这里写成反复加倍的形式。`maskAt` 把索引解释为掩码：按索引属于两个加数中的哪一支确定首位，再由该支中的剩余索引确定尾部。每个掩码都由某个索引得到，这就是 `mask-onto`，也是后文使用该枚举所需的唯一性质；该枚举不要求逐点单射。

取 `n = 2`，四个索引给出从 `false ∷ false ∷ []` 到 `true ∷ true ∷ []` 的四个掩码。这个构造事实上无重复地枚举它们；不过后面的点名册论证只使用已证明的覆盖性 `mask-onto`，并不依赖单射性。

掩码的计数按「将来枚举它的那个递归」来定义：长度为零恰有一个掩码；长度为 `suc n` 的掩码是一个首位加上一个长度为 `n` 的掩码，故计数为 `maskCount n + maskCount n`。这就是写成反复加倍形式的二的 `n` 次幂，而两个加数相同，恰好正是 `splitFin` 所期待的形状。

```agda
maskCount : ℕ → ℕ
maskCount zero    = 1
maskCount (suc n) = maskCount n + maskCount n

maskCons : (n : ℕ) → (Fin (maskCount n) → Vec Bool n)
         → Fin (maskCount n) ⊎ Fin (maskCount n) → Vec Bool (suc n)
```

`maskCons` 把一个首位接到从索引相应半支读出的尾部上：左加数取 `false`，右加数取 `true`。于是 `maskAt` 把索引读成掩码：长度为零时唯一的掩码是空向量；长度为 `suc n` 时，小于 `maskCount (suc n) = maskCount n + maskCount n` 的索引被一分为二，所在的半支给出首位，内层索引给出尾部。这个读法是一个定义而非定理：它只是按规则计算。

```agda
maskCons n r (inl j) = false ∷ r j
maskCons n r (inr j) = true  ∷ r j

maskAt : (n : ℕ) → Fin (maskCount n) → Vec Bool n
maskAt zero    j = []
maskAt (suc n) j = maskCons n (maskAt n) (splitFin (maskCount n) j)
```

覆盖性是 `mask-onto` 的内容，而它有意不带截断：给定一个向量 `v`，该陈述产生一个真实的索引，连同从该索引读出的掩码到 `v` 的路径。基情形中，空向量来自第零号索引。这是整个枚举中唯一必须交付数据而非仅仅存在性的地方，而它之所以能做到，是因为递归沿着向量本身进行。

```agda
mask-onto : (n : ℕ) (v : Vec Bool n) → Σ[ j ∈ Fin (maskCount n) ] (maskAt n j ≡ v)
mask-onto zero    []          = zero , refl
mask-onto (suc n) (false ∷ v) =
  joinFin (maskCount n) (inl (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inl (mask-onto n v .fst)))
```

后继情形由向量决定分支。首位为 `false` 时，尾部的索引经 `joinFin` 拼入左半支；路径分两步拼装：先用 `split-join` 证明对拼合索引的劈分确实还原出左半支，再用 `cong (false ∷_)` 把递归得到的路径带上首位。`true` 的情形逐字相同，只是换成右半支。结合计数，这说明已清点集合的掩码被 `Fin (maskCount size)` 覆盖，恰好是 `Tally` 字段所期待的形状。

```agda
     ∙ cong (false ∷_) (mask-onto n v .snd))
mask-onto (suc n) (true ∷ v)  =
  joinFin (maskCount n) (inr (mask-onto n v .fst))
  , (cong (maskCons n (maskAt n)) (split-join (maskCount n) (inr (mask-onto n v .fst)))
     ∙ cong (true ∷_) (mask-onto n v .snd))
```

## 选出一个子族

`select` 按布尔掩码筛选一个有穷族，其成员引理则把选中的条目与标为真的位置对应起来。

`select` 把掩码作用到一个族上：它保留那些位为 `true` 的条目，并把它们重新组成一个族，同时给出该族的长度。长度是**由递归产生**的，这正是关键：无须计数，也不需要任何算术把答案与掩码联系起来。

两条规格说明各自刻画结果包含什么，且都不带截断，因为二者都是同一次递归的直接推论。`marks` 的方向相反：它把对诸条目的一次判定变成记录该判定的掩码。

一个小例子显示了与重复的交互。取一个含重复条目的族，并取保留两个副本的掩码：选出的子族便两次含有该条目，两条副本各由引理以各自的原始位置回答。没有任何东西被丢失或合并，因为从来没有任何东西被要求唯一。

辅助函数 `selectStep` 完成筛选的一步：给定条目 `x` 与已选好的族，它把 `x` 排在最前并报告新长度 `suc k`。其结果类型把族与长度打包成一个依赖对，于是递归可以增长长度而不必对掩码做任何算术。

```agda
selectStep : {ℓ' : Level} {X : Type ℓ'} → X → Σ[ k ∈ ℕ ] (Fin k → X)
           → Σ[ k ∈ ℕ ] (Fin k → X)
selectStep {X = X} x (k , g) = suc k , h
  where
  h : Fin (suc k) → X
```

`select` 是沿掩码的递归。空掩码什么也不选，用荒谬模式表达：长度为零的族没有任何位置。首位为 `false` 时丢弃头部并沿右移后的族递归；首位为 `true` 时用 `selectStep` 保留头部。每一步族都右移一格，这正是全篇出现的 `λ i → f (suc i)` 所记录的内容。

```agda
  h zero    = x
  h (suc i) = g i

select : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → Vec Bool n
       → Σ[ k ∈ ℕ ] (Fin k → X)
select zero    f v           = zero , λ ()
```

第一条规格 `select-out` 顺向读出选取结果：被选族的每个位置 `j` 都来自某个位为 `true` 的原始位置 `i`，且该处的条目确实是原来的条目 `f i`。这一主张是数据而非仅仅的存在性：实际产生一个见证 `i`，位与等式都显式给出。

```agda
select (suc n) f (false ∷ v) = select n (λ i → f (suc i)) v
select (suc n) f (true ∷ v)  = selectStep (f zero) (select n (λ i → f (suc i)) v)

select-out : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
             (j : Fin (select n f v .fst))
           → Σ[ i ∈ Fin n ] ((lookup i v ≡ true) × (select n f v .snd j ≡ f i))
```

证明沿与定义相同的递归走。`false` 情形中头部已被丢弃，于是在尾部回答 `j` 的原始位置要上移成整向量中的 `suc i`；局部的 `step` 恰好完成对见证三元组的这一簿记。

```agda
select-out zero    f []          ()
select-out (suc n) f (false ∷ v) j       = step (select-out n (λ i → f (suc i)) v j)
  where
  step : Σ[ i ∈ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))
```

`true` 情形分两个子情形。若被选位置是第一个，答案就是头部本身，两条等式都因 `select` 把头部原封不动作为零号位置返回而由 `refl` 成立；否则递归回答尾部的位置，同样的上移照旧适用。

```agda
       → Σ[ i ∈ Fin (suc n) ] ((lookup i (false ∷ v) ≡ true)
           × (select (suc n) f (false ∷ v) .snd j ≡ f i))
  step (i , e , q) = suc i , (e , q)
select-out (suc n) f (true ∷ v)  zero    = zero , (refl , refl)
select-out (suc n) f (true ∷ v)  (suc j) = step (select-out n (λ i → f (suc i)) v j)
```

第二个子情形重复同样的上移簿记，只是此时头部仍在：`true ∷ v` 的被选族是头部接上尾部的选取结果，因此头部之后的位置在尾部得到回答并映回 `suc i`。两个分支只在这一重定位上不同，这正是它们各自需要一个 `step` 的原因。

```agda
  where
  step : Σ[ i ∈ Fin n ] ((lookup i v ≡ true)
           × (select n (λ i → f (suc i)) v .snd j ≡ f (suc i)))
       → Σ[ i ∈ Fin (suc n) ] ((lookup i (true ∷ v) ≡ true)
           × (select (suc n) f (true ∷ v) .snd (suc j) ≡ f i))
```

反向规格 `select-in` 说每个被标记的条目都被选中：位为 `true` 的原始位置 `i` 拥有一个被选位置 `j`，其条目为 `f i`。同样，这一主张是显式的数据，即一个真实的 `j` 连同一条路径。两个方向都不带截断，这正是后文关于成员性的论证能在选取两侧传递真实见证的原因。

```agda
  step (i , e , q) = suc i , (e , q)

select-in : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (v : Vec Bool n)
            (i : Fin n) → lookup i v ≡ true
          → Σ[ j ∈ Fin (select n f v .fst) ] (select n f v .snd j ≡ f i)
select-in zero    f []          ()      e
```

其证明从另一端映照同一递归。空族中的位置是荒谬的。`false` 情形中头部不可能被标为真，故假设 `e` 与 `false≢true` 矛盾；右移后的位置照旧递归。`true` 情形中头部以零号位置作答，更深的位置照旧递归。

```agda
select-in (suc n) f (false ∷ v) zero    e = Empty.rec (false≢true e)
select-in (suc n) f (false ∷ v) (suc i) e = select-in n (λ i → f (suc i)) v i e
select-in (suc n) f (true ∷ v)  zero    e = zero , refl
select-in (suc n) f (true ∷ v)  (suc i) e = step (select-in n (λ i → f (suc i)) v i e)
  where
```

最后一条子句完成前置的簿记：尾部找到的位置变成现在头部在前的新族中的 `suc j`，条目等式原样保留。两条规格合起来说明选取结果既不比掩码标出的多、也不比它少，尽管没有断言这两种位置对应方式互为逆映射。

```agda
  step : Σ[ j ∈ Fin (select n (λ i → f (suc i)) v .fst) ]
           (select n (λ i → f (suc i)) v .snd j ≡ f (suc i))
       → Σ[ j ∈ Fin (select (suc n) f (true ∷ v) .fst) ]
           (select (suc n) f (true ∷ v) .snd j ≡ f (suc i))
  step (j , q) = suc j , q
```

`marks` 把筛选反过来用：它不读掩码来保留条目，而是取一个关于条目的布尔裁决 `d`，并写下记录该裁决的掩码，每个位置一位。基情形是空向量，递归步在头部询问 `d` 并沿右移后的族继续。

```agda
marks : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) → (Fin n → X) → (X → Bool) → Vec Bool n
marks zero    f d = []
marks (suc n) f d = d (f zero) ∷ marks n (λ i → f (suc i)) d

marks-lookup : {ℓ' : Level} {X : Type ℓ'} (n : ℕ) (f : Fin n → X) (d : X → Bool)
               (i : Fin n) → lookup i (marks n f d) ≡ d (f i)
```

`marks-lookup` 证明记录下的掩码确实在每个位置回答裁决：在 `marks n f d` 的位置 `i` 处查询得到 `d (f i)`。头部情形由 `marks` 的计算规则得 `refl`，更深的位置照旧递归。有了这条引理，后面的 `maskOf` 才能证明它写下的掩码重现给定的子集。

```agda
marks-lookup (suc n) f d zero    = refl
marks-lookup (suc n) f d (suc i) = marks-lookup n (λ i → f (suc i)) d i
```

## 把一个真值判定成一位

排中律把每个命题化为掩码所用的布尔位，而两条规格从该位分别读回真与假。

排中律给出的是一个析取，而掩码需要的是一位，故须把二者衔接起来。裁决作为实参显式传入，而不是在定义内部求解：正是这一点使两条来回引理能靠对它作模式匹配来证明；真值本身也显式给出，使来回规格以预期命题为参数。

这一转换是排中律在点名册构造中的一个具体用途：判定一条成员命题，再把答案记录为一位。

`decideOf` 把裁决变成一位：左支是 `⟨ P ⟩` 的证明，记为 `true`；右支是 `⟨ P ⟩` 的反驳，记为 `false`。命题 `P` 本身与计算无关，被匹配的只是裁决，因此这个定义是一对方程而非证明。

```agda
decideOf : (P : hProp (ℓ-suc ℓ)) → (⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → Bool
decideOf P (inl _) = true
decideOf P (inr _) = false

decide-true : (P : hProp (ℓ-suc ℓ)) (s : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → ⟨ P ⟩ → decideOf P s ≡ true
decide-true P (inl _)  p = refl
```

两条往返把位接回真值。`decide-true` 说 `⟨ P ⟩` 的证明迫使该位为 `true`：在反驳支中这个证明本身会被反驳，那正是矛盾。`decide-sound` 反向读出：位为 `true` 便给出 `⟨ P ⟩` 的证明，或直接取自左支，或因右支会迫使 `false ≡ true` 而得。合起来，它们说明对于传入的那个裁决，该位忠实地回答 `⟨ P ⟩` 是否成立。

```agda
decide-true P (inr np) p = Empty.rec (np p)

decide-sound : (P : hProp (ℓ-suc ℓ)) (s : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → decideOf P s ≡ true → ⟨ P ⟩
decide-sound P (inl p) _ = p
decide-sound P (inr _) e = Empty.rec (false≢true e)
```

## 已清点层的可定义子集

有穷性经由本节沿塔逐级传递。固定序数 `σ` 和层 `Lset σ` 的一份点名册，目标是给出 `𝒟ₒ (Lset σ)` (该层可定义子集的全体) 的点名册。已知点名册的每个条目都是该层的成员，因而在该层的小成员类型中有相应的元素；掩码指明保留哪些元素，`part` 把保留的元素张成有穷集。按基本公理一章的 `finSet∈𝒟ₒ`，这样张成的集合是该层的可定义子集，由「等于这些条目之一」的有穷析取定义。反过来，该层的任何可定义子集 `x` 也能被恢复：按每个点名册条目是否属于 `x` 的可判定成员关系加以标记，该掩码张成的集合恰是 `x`，其中包含关系 `𝒟ₒ∋⊆` 保证 `x` 的每个成员本就被点名册列出。于是 `maskCount size` 个掩码仅仅覆盖全部可定义子集，而这正是 `Tally` 所要求的。

`Lset σ` 的成员作为集合处在该层中，但 `finSet` 需要小成员类型 `⟪ Lset σ ⟫` 中的名字；嵌入 `⟪ Lset σ ⟫↪` 把这种名字读成集合。成员关系呈现为截断原像，不过这个嵌入的原像取值为命题，所以 `∈-asFiber` 可以消去截断，返回一个显式名字及其等同于 `item i` 的路径。`index i` 与 `index-eq i` 正是该原像元素的两个投影。这并非从任意点名册原像中选取索引，因为允许重复的点名册原像未必是命题。

```agda
module PowerStep (σ : S) (oσ : IsOrd σ) (t : Tally (Lset σ)) where
  open Tally t
  open FinOf σ oσ using ( finSet∈𝒟ₒ )

  index : Fin size → ⟪ Lset σ ⟫
  index i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .fst
```

同一纤维的第二个分量是路径 `index-eq i`，它记录嵌入元素经一条路径而非定义等式回到 `item i`。此后在集合 `item i` 与元素 `index i` 之间的每一次转换都要沿这条路径用传输完成。元素就位后，掩码 `v` 被转换为一次选取：`chosen v` 给出一个长度，连同恰好列出被选元素的函数，这由此前的 `select` 构造。

```agda
  index-eq : (i : Fin size) → ⟪ Lset σ ⟫↪ (index i) ≡ item i
  index-eq i = ∈-asFiber {a = item i} {b = Lset σ} (inside i) .snd

  chosen : Vec Bool size → Σ[ k ∈ ℕ ] (Fin k → ⟪ Lset σ ⟫)
  chosen v = select size index v

  part : Vec Bool size → S
```

`part` 就是张成的集合：它把每个被选元素经嵌入读出，并取所得结果的有穷集，落在集合类型 `S` 中。由于 `Lset σ` 成员的有穷族张成该层的可定义子集，`part-def` 直接由 `finSet∈𝒟ₒ` 得到证书 `⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩`，无须额外工作。第一条规格从反方向读成员关系：若 `y` 属于 `part v`，则仅仅存在某个点名册位置，其位为 `true` 且其条目等于 `y`。

```agda
  part v = finSet (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))

  part-def : (v : Vec Bool size) → ⟨ part v ∈ˢ 𝒟ₒ (Lset σ) ⟩
  part-def v = finSet∈𝒟ₒ (chosen v .fst) (chosen v .snd)

  part-out : (v : Vec Bool size) (y : S) → ⟨ y ∈ˢ part v ⟩
           → ∥ Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (item i ≡ y)) ∥₁
```

证明分两步复合。第一步，`finSet-out` 解开有穷张成集中的成员关系：它仅仅给出选取中的一个位置 `j`，使嵌入元素等于 `y`。第二步，`select-out` 把该位置追回到完整点名册中的来源，恢复索引 `i`，满足 `lookup i v ≡ true` 以及 `chosen v .snd j ≡ index i`。两步的数据都在截断之内产生，因此没有从单纯存在性命题中提取选定的见证。

```agda
  part-out v y y∈ = PT.map step
    (finSet-out (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j)) y y∈)
    where
    step : Σ[ j ∈ Fin (chosen v .fst) ] (⟪ Lset σ ⟫↪ (chosen v .snd j) ≡ y)
         → Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (item i ≡ y))
```

最后所需等式的方向是 `item i ≡ y`。先沿 `sym (index-eq i)` 从 `item i` 到嵌入后的名字 `index i`。随后 `select-out` 给出 `chosen v .snd j ≡ index i`，取其对称并施加嵌入，便到达选中的嵌入名字。最后，有限集成员关系给出的路径 `q` 到达 `y`。三者的复合正是证明中显示的三段路径。

```agda
    step (j , q) = out .fst
                 , ( out .snd .fst
                   , (sym (index-eq (out .fst))
                      ∙ cong ⟪ Lset σ ⟫↪ (sym (out .snd .snd)) ∙ q) )
      where
```

相反的规格正向运行。若位置 `i` 处的位为 `true`，则条目 `item i` 确实属于 `part v`。原因在于选取中确实含有该元素：`select-in` 对每个被标记的位置，在被选族中找到一个持有同一元素的槽位，随后 `finSet-in` 证明其嵌入形式的成员关系。

```agda
      out : Σ[ i ∈ Fin size ] ((lookup i v ≡ true) × (chosen v .snd j ≡ index i))
      out = select-out size index v j

  part-mem : (v : Vec Bool size) (i : Fin size) → lookup i v ≡ true
           → ⟨ item i ∈ˢ part v ⟩
  part-mem v i e = subst (λ w → ⟨ w ∈ˢ part v ⟩) path
```

由于张成集中的成员关系是针对嵌入元素陈述的，而目标针对条目 `item i`，两者要靠下文的路径 `path` 连接，并用 `subst` 沿该路径搬移成员证书。辅助的 `ins` 保存 `select-in` 给出的槽位：被选族中的一个位置，其条目等于 `index i`。

```agda
    (finSet-in (chosen v .fst) (λ j → ⟪ Lset σ ⟫↪ (chosen v .snd j))
      (⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst))) ∣ ins .fst , refl ∣₁)
    where
    ins : Σ[ j ∈ Fin (chosen v .fst) ] (chosen v .snd j ≡ index i)
    ins = select-in size index v i e
```

余下的路径 `path` 把槽位的等式与 `index-eq i` 拼接，因此传输后的成员关系正是 `item i` 的成员关系。两个方向就位后，构造可以反向运行。`maskOf` 对任意集合 `x` 给出裁决掩码：对每个点名册条目判定它是否属于 `x`；排中律 `lem` 供给析取，`decideOf` 把它变成一位。目标 `part-mask` 陈述：对该层中的可定义子集 `x`，此掩码张成的集合就是 `x` 本身。

```agda
    path : ⟪ Lset σ ⟫↪ (chosen v .snd (ins .fst)) ≡ item i
    path = cong ⟪ Lset σ ⟫↪ (ins .snd) ∙ index-eq i

  maskOf : S → Vec Bool size
  maskOf x = marks size item (λ y → decideOf (y ∈ˢ x) (lem (y ∈ˢ x)))

  part-mask : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩ → part (maskOf x) ≡ x
```

层次中集合的成员关系是命题，因此外延性 `extensionalV` 把所断言的等式 `part (maskOf x) ≡ x` 归约为逐点的成员关系等价；`⇔toPath` 把两个方向组装成路径。正向表明张成集的每个成员都属于 `x`。

```agda
  part-mask x x∈ = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
    where
    fwd : (y : S) → ⟨ y ∈ˢ part (maskOf x) ⟩ → ⟨ y ∈ˢ x ⟩
    fwd y y∈ = PT.rec (snd (y ∈ˢ x)) step (part-out (maskOf x) y y∈)
      where
```

正向的前提本身就是单纯的存在性：某个被标记的位置，其条目等于 `y`。由于目标 `⟨ y ∈ˢ x ⟩` 是命题，截断可以消去到其中。记录的见证是位置 `i`，其位为 `true` 且条目为 `y`；由于该位正是通过判定这个条目是否属于 `x` 算出的，用 `decide-sound` 把位读回即得 `item i` 属于 `x`，再用等式 `item i ≡ y` 把它传输给 `y`。

```agda
      step : Σ[ i ∈ Fin size ] ((lookup i (maskOf x) ≡ true) × (item i ≡ y))
           → ⟨ y ∈ˢ x ⟩
      step (i , e , q) = subst (λ w → ⟨ w ∈ˢ x ⟩) q
        (decide-sound (item i ∈ˢ x) (lem (item i ∈ˢ x))
          (sym (marks-lookup size item
```

反向从 `y` 属于 `x` 出发，须产生张成集中的成员关系。由于该目标又是命题，其截断的前提可以消去。这里的前提来自点名册的覆盖：`x` 是该层的可定义子集，而 `𝒟ₒ∋⊆` 说 `Lset σ` 的可定义子集的每个成员都是 `Lset σ` 自身的成员，因此点名册的 `onto` 单纯地把 `y` 列为某个条目 `item i`。

```agda
                 (λ z → decideOf (z ∈ˢ x) (lem (z ∈ˢ x))) i) ∙ e))
    bwd : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ part (maskOf x) ⟩
    bwd y y∈x = PT.rec (snd (y ∈ˢ part (maskOf x))) step
      (onto y (𝒟ₒ∋⊆ (Lset σ) x x∈ y y∈x))
      where
```

给定等于 `y` 的条目 `i`，只需证明 `item i` 属于张成集，并沿 `item i ≡ y` 传输。由 `part-mem`，成员关系需要位置 `i` 的位为 `true`。它确实如此：掩码记录了 `item i ∈ˢ x` 的判定，而由于 `y` 属于 `x`，路径 `item i ≡ y` 把该证明传输过来，`decide-true` 便迫使该位为 `true`。

```agda
      step : Σ[ i ∈ Fin size ] (item i ≡ y) → ⟨ y ∈ˢ part (maskOf x) ⟩
      step (i , q) = subst (λ w → ⟨ w ∈ˢ part (maskOf x) ⟩) q
        (part-mem (maskOf x) i
          (marks-lookup size item (λ z → decideOf (z ∈ˢ x) (lem (z ∈ˢ x))) i
           ∙ decide-true (item i ∈ˢ x) (lem (item i ∈ˢ x))
```

`part-mask` 的两个方向就此组装完毕，本节的关键成果随之而来。由于每个掩码都经 `mask-onto` 来自某个索引，掩码 (允许重复、单纯地) 枚举了 `Lset σ` 的全部可定义子集。它们共有 `maskCount size` 个，因此 `powerTally` 记录一个该大小的点名册，其在索引 `j` 处的条目是掩码 `maskAt size j` 张成的集合。其余字段补全记录：每个条目附带其可定义性证书，覆盖条款随后给出。

```agda
               (subst (λ w → ⟨ w ∈ˢ x ⟩) (sym q) y∈x)))

  powerTally : Tally (𝒟ₒ (Lset σ))
  powerTally = record
    { size   = maskCount size
    ; item   = λ j → part (maskAt size j)
```

记录的 `inside` 字段在每个被枚举的掩码处复用证书 `part-def`，因此 `powerTally` 的每个条目确实是该层的可定义子集。剩下检查 `onto`，即截断的覆盖性。给定 `Lset σ` 的任意可定义子集 `x`，必须单纯地给出一个索引，其被枚举的条目等于 `x`。

```agda
    ; inside = λ j → part-def (maskAt size j)
    ; onto   = cover }
    where
    cover : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩
          → ∥ Σ[ j ∈ Fin (maskCount size) ] (part (maskAt size j) ≡ x) ∥₁
```

见证索引是 `mask-onto` 为裁决掩码 `maskOf x` 产生的那个。该索引处被枚举的条目是 `part (maskAt size j)`，沿所得路径改写掩码后它等于 `part (maskOf x)`，随后 `part-mask` 把它与 `x` 等同。整个命题落在截断之中，这正是 `Tally` 的覆盖性所要求的：每个可定义子集都被命中，尽管未必由唯一的掩码命中。

```agda
    cover x x∈ = ∣ mask-onto size (maskOf x) .fst
                 , (cong part (mask-onto size (maskOf x) .snd) ∙ part-mask x x∈) ∣₁
```

## 最小元与良基性

本节花用的是先前造好的点名册，而非再造一份。固定一个类型及其上一个三歧、非自反且传递的关系，即严格良序所要求的一切，只差良基。过程 `scan` 走过一个有穷族，并且不带任何截断地返回：要么是一个满足谓词、且在满足者之中最小的条目，要么是「没有条目满足它」的反驳。它是沿长度的普通递归：每一步由排中律判定谓词在头部是否成立，再由三歧比较头部与迄今为止的最佳者；四种组合即四条子句。全程无截断这一点很要紧，因为调用方要的是一个货真价实的元素，不是仅仅的存在性。在「该族单纯覆盖整个类型」的假设下，`Search.Over.least` 把它升级为「整个类型上任一单纯非空谓词的最小元」：「没有条目满足它」那一支被见证者驳倒，因为该谓词本该命中它在族中的纤维。良基性随后的最小反例论证在其代码处再作说明。

固定 `A` 上满足三歧、非自反与传递的严格关系 `≺`。目标是从有穷覆盖族推出良基性，而不是把良基性作为假设。对谓词 `P`，`Least P m` 同时记录 `m` 满足 `P`，以及每个严格更小的满足者都会导出矛盾。

```agda
module Search {A : Type (ℓ-suc ℓ)} (_≺_ : A → A → Type (ℓ-suc ℓ))
              (tri : (a b : A) → Tri (a ≺ b) (a ≡ b) (b ≺ a))
              (irr : (a : A) → a ≺ a → Empty.⊥)
              (trans : (a b c : A) → a ≺ b → b ≺ c → a ≺ c) where

  Least : (P : A → hProp (ℓ-suc ℓ)) → A → Type (ℓ-suc ℓ)
```

扫描的输出类型 `Found P n f` 是两个显式选项的析取。左支中，某个位置 `i` 持有一个满足 `P` 的条目，且族内没有其他满足 `P` 的条目位于其下。右支中，每个条目都不满足谓词。两个选项携带的都是完整数据而非截断的存在性，这使后续构造能返回真实的元素。

```agda
  Least P m = ⟨ P m ⟩ × ((b : A) → ⟨ P b ⟩ → b ≺ m → Empty.⊥)

  Found : (P : A → hProp (ℓ-suc ℓ)) (n : ℕ) (f : Fin n → A) → Type (ℓ-suc ℓ)
  Found P n f =
    (Σ[ i ∈ Fin n ] (⟨ P (f i) ⟩ × ((j : Fin n) → ⟨ P (f j) ⟩ → f j ≺ f i → Empty.⊥)))
    ⊎ ((i : Fin n) → ⟨ P (f i) ⟩ → Empty.⊥)
```

`scan` 沿族长度递归定义。空族空虚地返回右支。对有头部的族，递归先处理尾部，把位置整体后移一位；排中律对 `P` 在头部的裁决交给 `combine`，它把尾部的结果与头部的裁决合并成整个族的结果。

```agda
  scan : (P : A → hProp (ℓ-suc ℓ)) (n : ℕ) (f : Fin n → A) → Found P n f
  scan P zero    f = inr (λ ())
  scan P (suc n) f = combine (scan P n (λ i → f (suc i))) (lem (P (f zero)))
    where
    combine : Found P n (λ i → f (suc i))
```

`combine` 的第一支处理尾部已经给出最小满足者 `f (suc i)`、而头部也满足谓词的情形。此时两个候选竞争，三歧判定 `f zero` 与 `f (suc i)` 哪个更小；辅助函数 `decide` 分析该比较的三种结果。

```agda
            → (⟨ P (f zero) ⟩ ⊎ (⟨ P (f zero) ⟩ → Empty.⊥)) → Found P (suc n) f
    combine (inl (i , pi , mi)) (inl p₀) = decide (tri (f zero) (f (suc i)))
      where
      decide : Tri (f zero ≺ f (suc i)) (f zero ≡ f (suc i)) (f (suc i) ≺ f zero)
             → Found P (suc n) f
```

若头部严格小于尾部的优胜者，头部便成为新的优胜者。其最小性逐位置核验：在头部自身处，断言 `f zero ≺ f zero` 直接与非自反性矛盾；在尾部各位置，传递性把 `f j ≺ f zero ≺ f (suc i)` 连成链，交给尾部已确立的最小性 `mi`。

```agda
      decide (lt h) = inl (zero , (p₀ , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → Empty.⊥
        minAt zero    pj hj = irr (f zero) hj
        minAt (suc j) pj hj = mi j pj (trans (f (suc j)) (f zero) (f (suc i)) hj h)
```

若头部等于尾部当前的最小候选，该候选仍为最小。假设头部低于候选，沿二者的等式传输后就得到候选低于自身，与非自反性矛盾；尾部位置仍由 `mi` 处理。

```agda
      decide (eq h) = inl (suc i , (pi , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
        minAt zero    pj hj = irr (f (suc i)) (subst (λ w → w ≺ f (suc i)) h hj)
        minAt (suc j) pj hj = mi j pj hj
```

若尾部的优胜者严格小于头部，它得以保留。此时优胜者之下的假设性条目有两条出路：经头部 `f (suc i) ≺ f zero ≺ f (suc i)` 的传递性给出一个自比较，由非自反性驳倒；而尾部自身的各位置交给 `mi`。优胜者的证书在每个分支都由旧证书重建。

```agda
      decide (gt h) = inl (suc i , (pi , minAt))
        where
        minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
        minAt zero    pj hj = irr (f (suc i)) (trans (f (suc i)) (f zero) (f (suc i)) h hj)
        minAt (suc j) pj hj = mi j pj hj
```

第二支在头部不满足谓词时保留尾部的优胜者。这里完全不需要比较：头部既然不满足 `P`，便无从挑战优胜者，因此头部处的假想反例直接由裁决 `n₀` 驳倒，尾部各位置依旧交给 `mi`。

```agda
    combine (inl (i , pi , mi)) (inr n₀) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → Empty.⊥
      minAt zero    pj hj = Empty.rec (n₀ pj)
      minAt (suc j) pj hj = mi j pj hj
```

对称地，当尾部全无满足者而头部确实满足谓词时，头部就是新的优胜者。其最小性立即可得：头部自身由非自反性处理，任何满足谓词的尾部位置都与尾部的反驳 `none` 矛盾。

```agda
    combine (inr none) (inl p₀) = inl (zero , (p₀ , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → Empty.⊥
      minAt zero    pj hj = irr (f zero) hj
      minAt (suc j) pj hj = Empty.rec (none j pj)
```

最后一支是一致情形：尾部与头部都给不出满足者，于是报告整个族中无人满足。反驳逐位置组装：头部交给 `n₀`，每个尾部位置交给 `none`。至此，导言所说的四种组合齐备。

```agda
    combine (inr none) (inr n₀) = inr atAll
      where
      atAll : (i : Fin (suc n)) → ⟨ P (f i) ⟩ → Empty.⊥
      atAll zero    p = n₀ p
      atAll (suc i) p = none i p
```

子模块 `Over` 添加了把有穷族变成点名册所需的那条前提：`cov` 说 `A` 的每个元素都被该族单纯命中，这是允许重复的截断覆盖。在此前提下，`least` 把扫描的答案升级为整个类型上的最小元：其输入只是一个「某元素满足 `P`」的截断见证，其输出则是显式数据，即一个元素连同 `Least P m`。

```agda
  module Over (n : ℕ) (f : Fin n → A)
              (cov : (a : A) → ∥ Σ[ i ∈ Fin n ] (f i ≡ a) ∥₁) where

    least : (P : A → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ A ] ⟨ P a ⟩ ∥₁ → Σ[ m ∈ A ] Least P m
    least P h = decide (scan P n f)
      where
```

在 `least` 内部，辅助函数 `nowhere` 处理扫描的「无满足者」分支：假定没有条目满足 `P`，就必须驳倒给定的截断见证。该消去是合法的，因为目标是空类型这一命题，因此见证的截断可以在不作任何选择的情况下拆开。

```agda
      nowhere : ((i : Fin n) → ⟨ P (f i) ⟩ → Empty.⊥) → Empty.⊥
      nowhere none = PT.rec Empty.isProp⊥ atWitness h
        where
        atWitness : Σ[ a ∈ A ] ⟨ P a ⟩ → Empty.⊥
        atWitness (a , pa) = PT.rec Empty.isProp⊥
```

具体而言，见证给出元素 `a` 及 `⟨ P a ⟩`，覆盖 `cov a` 单纯地指出族中位置 `i` 满足 `f i ≡ a`；由于目标仍是命题，该纤维可以被读出。把 `⟨ P a ⟩` 的证明沿 `f i ≡ a` 反向传输得到 `⟨ P (f i) ⟩`，假定的反驳 `none` 便将其化为矛盾。紧接的代码行执行的正是这次传输。

```agda
          (λ { (i , q) → none i (subst (λ w → ⟨ P w ⟩) (sym q) pa) }) (cov a)
      decide : Found P n f → Σ[ m ∈ A ] Least P m
      decide (inl (i , pi , mi)) = f i , (pi , everywhere)
        where
        everywhere : (b : A) → ⟨ P b ⟩ → b ≺ f i → Empty.⊥
```

前面预告的传输在这里执行，且两个分量同时进行。给定整个类型中位于优胜者之下的假想条目 `b`，附有 `⟨ P b ⟩` 与 `b ≺ f i`，覆盖单纯地给出满足 `f j ≡ b` 的族位置 `j`；把满足性与比较性都沿该路径反向传输，优胜者的族级证书 `mi` 便把二者一并驳倒。于是扫描仅剩的分支，即反驳 `none`，彻底矛盾，因为见证已被证明必然把一个满足者带进族中。

```agda
        everywhere b pb hb = PT.rec Empty.isProp⊥
          (λ { (j , q) → mi j (subst (λ w → ⟨ P w ⟩) (sym q) pb)
                              (subst (λ w → w ≺ f i) (sym q) hb) }) (cov b)
      decide (inr none) = Empty.rec (nowhere none)

    wellFounded : WellFounded _≺_
```

为证明良基性，先判定任意 `a` 是否可及；肯定支直接返回证书。否定支用有穷扫描找出可及性被反驳的最小元素 `m`。若 `m` 的每个前驱都可及，`acc below` 就证明 `m` 可及；把 `found` 中保存的 `m` 的反驳作用于这份证书即得矛盾。最初关于 `a` 的反驳只用于证明「不可及」这一谓词非空。

```agda
    wellFounded a = fromDec (lem (Acc _≺_ a , isPropAcc a))
      where
      fromDec : (Acc _≺_ a ⊎ (Acc _≺_ a → Empty.⊥)) → Acc _≺_ a
      fromDec (inl h) = h
      fromDec (inr nh) = Empty.rec (found .snd .fst (acc below))
```

被取最小的性质是 `NotAcc`，即不可及性。其底层陈述是一个否定，而否定是命题，故 `NotAcc` 是合法的真值 `Ω`，`least` 可以作用于它。输入是 `a` 与假定反驳 `nh` 的截断配对，因此该假设只是说不可及元素之集非空。

```agda
        where
        NotAcc : A → hProp (ℓ-suc ℓ)
        NotAcc b = (Acc _≺_ b → Empty.⊥) , isProp¬ _
        found : Σ[ m ∈ A ] Least NotAcc m
        found = least NotAcc ∣ a , nh ∣₁
```

设 `m` 是刚求得的最小不可及元素。要证它可及，须证每个前驱 `b` 可及，而 `b` 的可及性又是命题，故再次由排中律判定；辅助函数 `pick` 在肯定支中返回证书。

```agda
        below : (b : A) → b ≺ found .fst → Acc _≺_ b
        below b hb = pick (lem (Acc _≺_ b , isPropAcc b))
          where
          pick : (Acc _≺_ b ⊎ (Acc _≺_ b → Empty.⊥)) → Acc _≺_ b
          pick (inl h)  = h
```

在否定支中，`b` 将是严格小于最小不可及元素 `m` 的不可及元素，而 `Least NotAcc m` 的最小性条款恰好驳斥这一点。于是每个前驱皆可及，证书 `acc below` 合法，把它交给假定的可及性反驳便封闭了矛盾。注意：全程并未构造或排除任何无穷下降序列，论证完全就是这个矛盾。

```agda
          pick (inr nb) = Empty.rec (found .snd .snd b nb hb)
```

## 最先的分歧

本节定义有穷层将要携带的序。固定一个集合 `A` 与集合之上的一个关系 `R`，后者读作 `A` 的诸成员上的一个序。`A` 的两个子集，按它们在何处分歧来比较。「`x` 先于 `y`」的见证，是 `A` 的一个成员 `z`，它属于 `y` 而不属于 `x`，且 `x` 与 `y` 在 `z` 之下**一致**，意即 `A` 中被 `R` 排在 `z` 之前的每个成员，属于其中之一当且仅当属于另一个。倒过来读：`z` 就是最先的分歧点，而它属于 `y`。关系 `precedes R A` 是这类见证的截断存在；非自反性立刻成立，且完全不需要任何前提：`x` 对自己的见证会既属于 `x` 又不属于 `x`。后文证明在关于基底序的前提下得到三歧与传递，并用有穷性得到良基性。

两个成分分别陈述。`Agrees R A x y z` 说：对 `A` 中被 `R` 排在 `z` 之前的每个成员 `w`，属于 `x` 与属于 `y` 双向重合。`Witness R A x y z` 随后组装完整见证：`z` 属于 `A`，属于 `y`，不属于 `x`，且其下方一致成立。正是成员条款的方向决定了比较中哪一方胜出。

```agda
Agrees : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Agrees R A x y z = (w : S) → ⟨ w ∈ˢ A ⟩ → ⟨ R w z ⟩
                 → (⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩) × (⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩)

Witness : (R : S → S → hProp (ℓ-suc ℓ)) (A x y z : S) → Type (ℓ-suc ℓ)
Witness R A x y z =
```

`precedes R A x y` 是「这类见证单纯存在」的命题，随 `PT.squash₁` 打包成一个真值。由于见证藏在截断之后，被断言的只有其存在，任何东西都不选定 `z`。非自反性于是只花一行：把截断消去到空类型 (一个命题) 中，暴露出同时有 `z ∈ x` 与 `z ∉ x` 的见证，把第二条施于第一条即是矛盾。

```agda
  ⟨ z ∈ˢ A ⟩ × ⟨ z ∈ˢ y ⟩ × (⟨ z ∈ˢ x ⟩ → Empty.⊥) × Agrees R A x y z

precedes : (R : S → S → hProp (ℓ-suc ℓ)) (A : S) → S → S → hProp (ℓ-suc ℓ)
precedes R A x y = ∥ Σ[ z ∈ S ] Witness R A x y z ∥₁ , PT.squash₁

precedes-irrefl : (R : S → S → hProp (ℓ-suc ℓ)) (A x : S) → ⟨ precedes R A x x ⟩ → Empty.⊥
precedes-irrefl R A x = PT.rec Empty.isProp⊥ (λ { (z , _ , z∈ , z∉ , _) → z∉ z∈ })
```

最先分歧序的传递性与三歧确实需要关于基底序的前提，而二者所需不同，故一并收进一个模块。其参数是 `R` 在 `A` 诸成员上的三歧与传递，以及 `R` 在那些成员上的最小元原则；在塔中，这些都来自下面那一层。

传递性是两个见证之间的比较。若 `x` 在 `p` 处先于 `y`，`y` 在 `q` 处先于 `z`，则 `p` 与 `q` 不可能相等，因为 `p` 属于 `y` 而 `q` 不属于；而二者中较小的那个就见证了 `x` 先于 `z`。两支要核对的是同样的两件事：较小的那一点方向正确，以及它之下的一致性可以复合。

该模块收集最先分歧序将要继承的三条前提。`baseTri` 与 `baseTrans` 说 `R` 限制在 `A` 的成员上时三歧且传递，`baseLeast` 是 `A` 上的最小元原则：从「`A` 成员的某个性质单纯非空」出发，它给出一个满足该性质、且没有更小的 `A` 成员也满足的元素。注意结论的形状：它是显式数据而非截断，因为调用方需要真实的极小元。

```agda
module Difference (R : S → S → hProp (ℓ-suc ℓ)) (A : S)
  (baseTri : (a b : S) → ⟨ a ∈ˢ A ⟩ → ⟨ b ∈ˢ A ⟩ → Tri ⟨ R a b ⟩ (a ≡ b) ⟨ R b a ⟩)
  (baseTrans : (a b c : S) → ⟨ R a b ⟩ → ⟨ R b c ⟩ → ⟨ R a c ⟩)
  (baseLeast : (P : S → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × ⟨ P a ⟩) ∥₁
             → Σ[ m ∈ S ] (⟨ m ∈ˢ A ⟩ × ⟨ P m ⟩
```

传递性的陈述恰好按 `precedes` 的产出形式取两条前提：`x ≺ y` 与 `y ≺ z` 的截断见证，并返回 `x ≺ z` 的截断见证。因此证明先消去第一个截断，再消去第二个，二者的目标都又是截断、因而是命题。

```agda
                 × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ P b ⟩ → ⟨ R b m ⟩ → Empty.⊥)))
  where

  precedes-trans : (x y z : S) → ⟨ precedes R A x y ⟩ → ⟨ precedes R A y z ⟩
                 → ⟨ precedes R A x z ⟩
  precedes-trans x y z hxy hyz =
```

两个见证都暴露后，`both` 接收完整数据：见证 `x` 先于 `y` 的点 `p` 及其成员条款 `agp`，以及见证 `y` 先于 `z` 的点 `q` 及其 `agq`。两个基底点的比较交给基底三歧，辅助函数 `decide` 分析其三种结果。

```agda
    PT.rec PT.squash₁ (λ wp → PT.rec PT.squash₁ (both wp) hyz) hxy
    where
    both : Σ[ p ∈ S ] Witness R A x y p → Σ[ q ∈ S ] Witness R A y z q
         → ⟨ precedes R A x z ⟩
    both (p , p∈A , p∈y , p∉x , agp) (q , q∈A , q∈z , q∉y , agq) =
```

若 `p` 严格小于 `q`，它继续充当 `x` 先于 `z` 的见证。它自身的条款原封不动，因为它们只涉及 `x` 与 `y`；须核实的是 `p` 属于 `z`，以及 `p` 之下 `x` 与 `z` 的一致性。`p` 属于 `z` 由 `agq` 在点 `p` 处给出，它把 `p` 对 `y` 的成员关系沿复合比较传输过去。

```agda
      decide (baseTri p q p∈A q∈A)
      where
      decide : Tri ⟨ R p q ⟩ (p ≡ q) ⟨ R q p ⟩ → ⟨ precedes R A x z ⟩
      decide (lt h) = ∣ p , (p∈A , (agq p p∈A h .fst p∈y , (p∉x , ag))) ∣₁
        where
```

`p` 之下的一致性逐条款复合。要证 `w ∈ x` 蕴含 `w ∈ z`：`agp` 把 `w ∈ x` 提升为 `w ∈ y`，再用 `agq` 把对 `y` 的成员提升到 `z`，其中用基底传递性保证 `w` 也位于 `q` 之下。反向条款对称，把 `z` 降到 `y` 再降到 `x`。相等情形不可能出现：`p` 属于 `y` 而 `q` 不属于，沿路径 `p ≡ q` 传输成员关系即得矛盾。

```agda
        ag : Agrees R A x z p
        ag w w∈A hw =
            (λ wx → agq w w∈A (baseTrans w p q hw h) .fst (agp w w∈A hw .fst wx))
          , (λ wz → agp w w∈A hw .snd (agq w w∈A (baseTrans w p q hw h) .snd wz))
      decide (eq h) = Empty.rec (q∉y (subst (λ v → ⟨ v ∈ˢ y ⟩) h p∈y))
```

若改为 `q` 严格小于 `p`，角色对调：由 `q` 见证 `x` 先于 `z`。它关于 `y` 与 `z` 的条款照旧，但须确立对 `x` 的成员与一致性。关于成员，在点 `q` 处读 `agp`，把 `q` 对 `x` 的成员传输为对 `y` 的成员，与 `q ∉ y` 矛盾；辅助函数 `q∉x` 把这一反驳打包。

```agda
      decide (gt h) = ∣ q , (q∈A , (q∈z , (q∉x , ag))) ∣₁
        where
        q∉x : ⟨ q ∈ˢ x ⟩ → Empty.⊥
        q∉x qx = q∉y (agp q q∈A h .fst qx)
        ag : Agrees R A x z q
```

`q` 之下的一致性以镜像顺序复合：先用 `agp` 借助 `q ≺ p` 的基底传递性把 `w` 置于 `p` 之下，从而把对 `x` 的成员下推到 `y`，`agq` 再把它上提到 `z`；反向条款先把 `z` 降到 `y`，再降到 `x`。两个不对称情形都已处理、相等已被驳倒，传递性就此完成。

```agda
        ag w w∈A hw =
            (λ wx → agq w w∈A hw .fst (agp w w∈A (baseTrans w q p hw h) .fst wx))
          , (λ wz → agp w w∈A (baseTrans w q p hw h) .snd (agq w w∈A hw .snd wz))
```

三歧正是使用排中律与最小元原则的地方。先问这两个子集在 `A` 中是否有分歧之处。若没有，则它们在 `A` 中处处一致；又因二者都不超出 `A`，故它们本就处处一致，外延性把它们认同。若有，则存在一个最先的分歧点；再作一次判定，即该点是否属于第一个子集，就知道比较朝哪个方向走。该点之下的一致性在两支中都自动成立：按该点的选法，它之下无一处分歧。

排中律在 `agree` 内部第二次被使用，用来把「没有分歧」变成「一致」；这一步恰是一次双重否定的消去。

这里的陈述并不把 `A` 的两个子集 `x`、`y` 当作可定义性证书，而是当作普通集合，并附上二者都不超出 `A` 的前提。结论是一个 `Tri`，即本章通用的三分判断：`x` 先于 `y`、作为集合相等，或 `y` 先于 `x`。证明先对 `Some` 使用排中律发问；`Some` 将被构造成一个命题，即一条截断的存在陈述，因此可以把 `PT.squash₁` 作为其命题性证书交给 `lem`。

```agda
  precedes-tri : (x y : S) → ((w : S) → ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ A ⟩)
                           → ((w : S) → ⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ A ⟩)
               → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
  precedes-tri x y x⊆ y⊆ = decide (lem (Some , PT.squash₁))
    where
```

两条截断组织了这个问题。谓词 `Apart w` 仅仅说 `w` 区分了这两个子集，方向不限：它属于其一而不属于另一。截断类型 `Some` 仅仅说 `A` 的某个成员是分歧点。二者都配以 `PT.squash₁`，因而都是命题而非数据；这正是可以用排中律判定它们、随后又能把 `Some` 的反驳消去成矛盾的依据。

```agda
    Apart : S → hProp (ℓ-suc ℓ)
    Apart w = ∥ (⟨ w ∈ˢ x ⟩ × (⟨ w ∈ˢ y ⟩ → Empty.⊥))
              ⊎ ((⟨ w ∈ˢ x ⟩ → Empty.⊥) × ⟨ w ∈ˢ y ⟩) ∥₁ , PT.squash₁
    Some : Type (ℓ-suc ℓ)
    Some = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × ⟨ Apart a ⟩) ∥₁
```

辅助引理 `agree` 把「无分歧」转成「一致」，一次一个方向。前提 `na` 反驳 `Apart w`，结论是 `w` 处成员等价的两条包含子句。证明只有这里需要从否定性陈述造出成员蕴含，而它实际上是化了装的双重否定消去。

```agda
    agree : (w : S) → (⟨ Apart w ⟩ → Empty.⊥)
          → (⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩) × (⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩)
    agree w na = fwd , bwd
      where
      fwd : ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ y ⟩
```

前向子句：设 `w ∈ˢ x`，对 `w ∈ˢ y` 用排中律发问。若成立即完成。若得到反驳 `nh`，那么 `w` 其实是分歧点，左析取支 `wx , nh` 就是见证；把该见证装入截断交给 `na` 便得矛盾，`Empty.rec` 再从矛盾产出所需元素，这里就是缺失的成员证明。目标 `Empty.⊥` 是命题，故把截断的 `Apart w` 消去到它是正当的。

```agda
      fwd wx = pick (lem (w ∈ˢ y))
        where
        pick : (⟨ w ∈ˢ y ⟩ ⊎ (⟨ w ∈ˢ y ⟩ → Empty.⊥)) → ⟨ w ∈ˢ y ⟩
        pick (inl h)  = h
        pick (inr nh) = Empty.rec (na ∣ inl (wx , nh) ∣₁)
```

后向子句是其镜像。设 `w ∈ˢ y`，排中律判定 `w ∈ˢ x`；若有反驳，则经右析取支 `nh , wy` 会使 `w` 成为分歧点，而 `na` 恰好反驳这一点。两条子句合起来说：若在 `w` 处不存在差异点，则属于 `x` 与属于 `y` 在 `w` 处重合。

```agda
      bwd : ⟨ w ∈ˢ y ⟩ → ⟨ w ∈ˢ x ⟩
      bwd wy = pick (lem (w ∈ˢ x))
        where
        pick : (⟨ w ∈ˢ x ⟩ ⊎ (⟨ w ∈ˢ x ⟩ → Empty.⊥)) → ⟨ w ∈ˢ x ⟩
        pick (inl h)  = h
```

现在设 `Some` 被反驳，即 `A` 中没有分歧点。辅助引理 `nApart` 把这一点包装成对 `Apart` 的逐点反驳，`same` 将在每处 `w` 使用它来证明两集合相等。被反驳的见证落在 `A` 中这一前提在下一步了结，随后 `agree` 的成员等价即可在每点使用。

```agda
        pick (inr nh) = Empty.rec (na ∣ inr (nh , wy) ∣₁)
    same : (Some → Empty.⊥) → x ≡ y
    same ns = extensionalV step
      where
      nApart : (w : S) → ⟨ Apart w ⟩ → Empty.⊥
```

只要两个子集都落在 `A` 中，分歧点必属于 `A`。事实上，截断析取 `ha` 被消去到命题 `w ∈ˢ A` 中：左支成立时 `w` 属于 `x`，`x⊆` 把它送进 `A`；右支成立时 `y⊆` 同理。注意消去的方向：进入取值为命题的成员关系，这恰是命题截断所允许的。

```agda
      nApart w ha = ns ∣ w , (inA , ha) ∣₁
        where
        inA : ⟨ w ∈ˢ A ⟩
        inA = PT.rec (snd (w ∈ˢ A))
          (λ { (inl (wx , _)) → x⊆ w wx ; (inr (_ , wy)) → y⊆ w wy }) ha
```

在每处 `w`，`agree w (nApart w)` 的两条子句断言：属于 `x` 当且仅当属于 `y`。组合子 `⇔toPath` 把这两个命题 `w ∈ˢ x` 与 `w ∈ˢ y` 之间的这份当且仅当提升为二者作为类型之间的路径，而这正是累积层级的外延性所消费的形式。把逐点路径交给 `extensionalV` 便得路径 `x ≡ y`，于是三歧的 `eq` 分支得证。

```agda
      step : (w : S) → (w ∈ˢ x) ≡ (w ∈ˢ y)
      step w = ⇔toPath (agree w (nApart w) .fst) (agree w (nApart w) .snd)
    decide : (Some ⊎ (Some → Empty.⊥))
           → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
    decide (inr ns) = eq (same ns)
```

另一支中 `Some` 成立：`A` 的某个成员是分歧点。把最小元原则 `baseLeast` (对 `A` 的成员上的基底序 `R` 可用) 作用于谓词 `Apart`，它返回显式的记录 `found`，而非截断的存在陈述：一个点 `m`，在 `A` 中、分歧，且在 `R` 序之下其下方再无分歧点。正是这种显式性，使得最小分歧点此后能被用作见证。

```agda
    decide (inl hs) = side (lem (m ∈ˢ x))
      where
      found : Σ[ m ∈ S ] (⟨ m ∈ˢ A ⟩ × ⟨ Apart m ⟩
                × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ Apart b ⟩ → ⟨ R b m ⟩ → Empty.⊥))
      found = baseLeast Apart hs
```

`found` 的各分量被一次性拆开并命名：点 `m`、其在 `A` 中的成员关系 `m∈A`、分歧性 `apartM`、以及最小性 `belowM`。逐一命名使下面两个对称分支保持可读，因为每一支都要引用其中若干字段。

```agda
      m : S
      m = found .fst
      m∈A : ⟨ m ∈ˢ A ⟩
      m∈A = found .snd .fst
      apartM : ⟨ Apart m ⟩
```

最小性字段 `belowM` 反驳任何严格低于 `m` 的分歧点；这里把它改排为比较假设在末位的形式，以配合即将到来的用法。手握最小分歧点之后，排中律判定 `m` 是否属于 `x`，`side` 把每个答案化为三歧的一个分支。

```agda
      apartM = found .snd .snd .fst
      belowM : (w : S) → ⟨ w ∈ˢ A ⟩ → ⟨ R w m ⟩ → ⟨ Apart w ⟩ → Empty.⊥
      belowM w w∈A hw ha = found .snd .snd .snd w w∈A ha hw
      side : (⟨ m ∈ˢ x ⟩ ⊎ (⟨ m ∈ˢ x ⟩ → Empty.⊥))
           → Tri ⟨ precedes R A x y ⟩ (x ≡ y) ⟨ precedes R A y x ⟩
```

若 `m` 确实属于 `x`，则 `m` 见证 `y` 先于 `x`：它在第二个集合中而不在第一个中。子引理 `m∉y` 通过对截断的 `apartM` 作情形分析来反驳 `m ∈ˢ y`：左支中见证本身就带有对 `m ∈ˢ y` 的反驳；右支中对 `m ∈ˢ x` 的反驳与 `mx` 相抵触。消去截断是允许的，因为目标 `Empty.⊥` 是命题。

```agda
      side (inl mx) = gt ∣ m , (m∈A , (mx , (m∉y , ag))) ∣₁
        where
        m∉y : ⟨ m ∈ˢ y ⟩ → Empty.⊥
        m∉y my = PT.rec Empty.isProp⊥
          (λ { (inl (_ , nmy)) → nmy my ; (inr (nmx , _)) → nmx mx }) apartM
```

`m` 之下的一致性也免费换边。对 `m` 之下的每个 `w`，`belowM` 反驳 `Apart w`，故 `agree w` 适用，给出双向的成员等价；这里只是把二元组按相反次序写出，把原本从 `x` 到 `y` 取向的一致性变成 `Agrees R A y x m`。与 `m∈A`、`mx`、`m∉y` 合起来，这是一份完整的 `Witness`，见证 `y` 先于 `x`，由 `gt` 装入截断交付。

```agda
        ag : Agrees R A y x m
        ag w w∈A hw = agree w (belowM w w∈A hw) .snd , agree w (belowM w w∈A hw) .fst
      side (inr nmx) = lt ∣ m , (m∈A , (my , (nmx , ag))) ∣₁
        where
        my : ⟨ m ∈ˢ y ⟩
```

镜像的一支改设 `m` 不属于 `x`，产出 `x` 先于 `y` 的 `lt` 见证。从 `apartM` 提取 `m ∈ˢ y` 又是一次截断情形分析：左支会断言 `m ∈ˢ x`，被 `nmx` 反驳，故只有右支存活，而它直接带有该成员关系。这次 `m` 之下的一致性无须换向，因为见证的取向恰与 `agree` 的产出一致。两个对称分支齐备后，`precedes` 的三歧完成，一层上的局部序便是其成员上的线序，只待良基性。

```agda
        my = PT.rec (snd (m ∈ˢ y))
          (λ { (inl (mx , _)) → Empty.rec (nmx mx) ; (inr (_ , h)) → h }) apartM
        ag : Agrees R A x y m
        ag w w∈A hw = agree w (belowM w w∈A hw)
```

## 有穷诸层

沿数码的递归把点名册与最先分歧良序从每个有穷层传到下一层。

以数码为索引的层正是有穷层，每层上的序由递归构造：第零层为空；`n` 的后继层上的序以层 `n` 自身的序为基础，并按最先分歧处比较层 `n` 的可定义子集。`before-irrefl` 在每层都成立且无需归纳，因为该比较的非自反性不需要前提，而第零层没有任何比较。

定义从三分判断的一件小工具开始。`Tri-map` 对 `Tri` 逐支作用：每个备选支各应用一个函数；三条子句就是它的计算规则。它将把「关于两个集合证明的三歧」转换为「关于一层的两个点所需的三歧」，二者只差是否附带成员证明。

```agda
Tri-map : {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ : Level}
          {A₁ : Type ℓ₁} {B₁ : Type ℓ₂} {C₁ : Type ℓ₃}
          {A₂ : Type ℓ₄} {B₂ : Type ℓ₅} {C₂ : Type ℓ₆}
        → (A₁ → A₂) → (B₁ → B₂) → (C₁ → C₂) → Tri A₁ B₁ C₁ → Tri A₂ B₂ C₂
Tri-map f g h (lt a) = lt (f a)
```

以数码为索引的层在此命名：`finiteStage n` 即层 `Lset (# n)`。关系 `before` 随后是对索引的递归。零处它取假真值，任何一对都不会被关系到。后继处它是对前一层使用 `precedes`：比较隶属关系的基底集合就是层 `n` 本身，而寻找最先分歧所沿的基底序是 `before n`，即递归在下一层造出的那个序。

```agda
Tri-map f g h (eq b) = eq (g b)
Tri-map f g h (gt c) = gt (h c)

finiteStage : ℕ → S
finiteStage n = Lset (# n)

before : ℕ → S → S → hProp (ℓ-suc ℓ)
```

`before` 的非自反性在所有数码处成立，且证明不作归纳。零处前提是假命题的证明，由 `Empty.rec*` 消去；后继处恰是 `precedes-irrefl`，即定义该比较时已确立的无前提非自反性。正因如此，非自反性不属于递归必须携带的数据。

```agda
before zero    x y = ⊥
before (suc n) = precedes (before n) (finiteStage n)

before-irrefl : (n : ℕ) (x : S) → ⟨ before n x x ⟩ → Empty.⊥
before-irrefl zero    x h = Empty.rec* h
before-irrefl (suc n) x h = precedes-irrefl (before n) (finiteStage n) x h
```

基例的空性单独记录为 `zero-empty`：没有集合是第零层的成员。从 `Lset (# zero)` 读出成员证书，仅仅给出某一层 `δ`，使 `δ` 属于数码零且 `x` 是 `Lset δ` 的可定义子集；数码零没有成员，`∅-empty` 把任何所谓的成员变成矛盾。由于目标 `Empty.⊥` 是命题，消去该截断是正当的。

```agda
zero-empty : (x : S) → ⟨ x ∈ˢ finiteStage zero ⟩ → Empty.⊥
zero-empty x h = PT.rec Empty.isProp⊥ step (Lset-out (# zero) x h)
  where
  step : Σ[ δ ∈ S ] (⟨ δ ∈ˢ ∅ ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩) → Empty.⊥
  step (δ , δ∈ , _) = ∅-empty δ (∈∈ₛ {a = δ} {b = ∅} .fst δ∈)
```

递归必须携带的数据只有一份对成员的清点、三歧与传递：非自反性在每层都自动成立，而良基性只在用到之处当场推出，不必随身携带。层的一个点是一个集合连同它的隶属证明；由于隶属是命题，两个点只要集合相等就相等。在「关于集合的陈述」与「载体必须是类型的那个束」之间往返时，需要做的全部工作就在于此。

前节的搜索机制作用在类型上，故层的一个成员被包装成 `Point`：一个集合连同它在 `finiteStage n` 中的成员证书。关系 `Below` 在底层集合处读取 `before n`。由于隶属是命题，集合相同的两个点已然相等；这一个事实承担了「关于集合的陈述」与「关于点的陈述」之间往返的全部工作。

```agda
Point : ℕ → Type (ℓ-suc ℓ)
Point n = Σ[ x ∈ S ] ⟨ x ∈ˢ finiteStage n ⟩

Below : (n : ℕ) → Point n → Point n → Type (ℓ-suc ℓ)
Below n a b = ⟨ before n (a .fst) (b .fst) ⟩

record StageOrder (n : ℕ) : Type (ℓ-suc ℓ) where
```

层 `n` 的归纳恰好保留后继步所需的事实：`finiteStage n` 的点名册、`before n` 对该层成员的三歧性，以及 `before n` 对任意集合的传递性。非自反性由最先分歧统一推出；局部序需要良基性时，则从点名册重新得到。

```agda
  field
    tally : Tally (finiteStage n)
    tri   : (x y : S) → ⟨ x ∈ˢ finiteStage n ⟩ → ⟨ y ∈ˢ finiteStage n ⟩
          → Tri ⟨ before n x y ⟩ (x ≡ y) ⟨ before n y x ⟩
    trans : (x y z : S) → ⟨ before n x y ⟩ → ⟨ before n y z ⟩ → ⟨ before n x z ⟩
```

在 `Ordered` 内部，第一项任务是关于点的三歧。`triPoint` 把关于集合的三歧 `tri` 交给 `Tri-map`；中间一支的结论是路径，需要转换，`Σ≡Prop` 恰好提供这一点：由于第二分量是某个命题的证明，底层集合之间的路径可以延拓为点之间的路径。

```agda
module Ordered (n : ℕ) (r : StageOrder n) where
  open StageOrder r public
  open Tally tally

  triPoint : (a b : Point n) → Tri (Below n a b) (a ≡ b) (Below n b a)
  triPoint a b = Tri-map id (Σ≡Prop (λ z → snd (z ∈ˢ finiteStage n))) id
```

点名册由集合提升到点：把每个条目配上它自己的成员证明，得到 `points`。覆盖陈述 `covers` 随后是 `onto` 经这一配对的搬运：给定一个点，`onto` 仅仅提供一个索引，其条目具有相同的集合，`Σ≡Prop` 再把集合的等式升级为点的等式。覆盖仍然是截断的，与点名册本身一样。

```agda
    (tri (a .fst) (b .fst) (a .snd) (b .snd))

  points : Fin size → Point n
  points i = item i , inside i

  covers : (a : Point n) → ∥ Σ[ i ∈ Fin size ] (points i ≡ a) ∥₁
  covers a = PT.map (λ { (i , q) → i , Σ≡Prop (λ z → snd (z ∈ˢ finiteStage n)) q })
```

在层的点上，三歧、非自反与传递同有穷点名册结合，给出两个结论：有穷扫描为每个仅仅非空的谓词找出最小点，而同一个最小反例论证给出点关系的良基性。

```agda
    (onto (a .fst) (a .snd))

  open Search (Below n) triPoint (λ a → before-irrefl n (a .fst))
              (λ a b c → trans (a .fst) (b .fst) (c .fst)) public
  open Over size points covers public

  order : SWO (Point n)
```

这些事实确定了 `finiteStage n` 诸点上的严格良序：关系是 `Before n`，三条序律来自层比较，良基性则来自有穷扫描。因此，构造清楚地区分了局部比较与排除无穷下降的有穷性论证。

```agda
  order = record
    { _<∙_   = Below n
    ; tri∙   = triPoint
    ; irr∙   = λ a → before-irrefl n (a .fst)
    ; trans∙ = λ a b c → trans (a .fst) (b .fst) (c .fst)
```

最后一条引理以下一层所需的形状包装最小元。`leastMem` 取集合上的一个谓词 `P`，它仅仅被该层的某个成员满足，并返回显式的满足 `P` 的成员 `m`，连同 `before n` 序下的最小性：该层中满足 `P` 的成员 `b` 没有严格低于 `m` 的。除前提外，这里没有任何截断。

```agda
    ; wf∙    = wellFounded }

  leastMem : (P : S → hProp (ℓ-suc ℓ)) → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ finiteStage n ⟩ × ⟨ P a ⟩) ∥₁
           → Σ[ m ∈ S ] (⟨ m ∈ˢ finiteStage n ⟩ × ⟨ P m ⟩
               × ((b : S) → ⟨ b ∈ˢ finiteStage n ⟩ → ⟨ P b ⟩
                          → ⟨ before n b m ⟩ → Empty.⊥))
```

证明在点的层面运行搜索并拆包结果。`least` 作用于提升后的谓词与重新包装的截断见证，返回显式的对：一个点 `m` 及其 `Least` 证书。随后把点的三个分量与证书的两个分量重新装配成集合层面的陈述，最小性子句由把证书作用于对 `b , b∈` 而得。

```agda
  leastMem P h = found .fst .fst
               , ( found .fst .snd
                 , ( found .snd .fst
                   , (λ b b∈ pb hb → found .snd .snd (b , b∈) pb hb) ) )
    where
```

剩下的只是粘合：`Q` 在点的底层集合处读取集合层面的谓词，`found` 以从三元组重新包装成「一个点加一个证明」的截断前提调用 `least`。这条 `leastMem` 正是递归在后继层作为 `baseLeast` 喂给 `Difference` 的东西，它把搜索机制与最先分歧序之间的环节闭合。

```agda
    Q : Point n → hProp (ℓ-suc ℓ)
    Q a = P (a .fst)
    found : Σ[ m ∈ Point n ] Least Q m
    found = least Q (PT.map (λ { (a , a∈ , pa) → (a , a∈) , pa }) h)
```

递归在第零层取空点名册，两条序律由空性成立。到后继层，上一层的点名册经可定义幂集提升。最先分歧比较利用两条子集前提给出三歧，并直接从上一层的序推出传递性；只有在成员关系需要于该层与其可定义幂集之间转换时，才使用后继层恒等式。

基例把三个字段装配成一个记录，三者正是刚建立的三件小事。点名册 `empty` 的长度为零：索引类型 `Fin zero` 为空，故条目与成员字段都用荒谬模式给出，即从无可能实参出发的函数。第零层没有可列的东西，这就是该点名册的全部内容。

```agda
stageOrder : (n : ℕ) → StageOrder n
stageOrder zero = record { tally = empty ; tri = triZero ; trans = transZero }
  where
  empty : Tally (finiteStage zero)
  empty = record
```

第零层点名册的其余字段来自同一个事实。任何被列条目的成员证书都不可能出现，因为根本没有索引；而层的覆盖则由 `zero-empty` 给出：假设 `finiteStage zero` 有成员便导出矛盾。因此，`empty` 在两个方向上都确实枚举了空层。

```agda
    { size   = zero
    ; item   = λ ()
    ; inside = λ ()
    ; onto   = λ x x∈ → Empty.rec (zero-empty x x∈) }
  triZero : (x y : S) → ⟨ x ∈ˢ finiteStage zero ⟩ → ⟨ y ∈ˢ finiteStage zero ⟩
```

两条序字段都是空洞的。零处的三歧收到 `x` 与 `y` 的成员证书，但这样的证书不存在，`zero-empty` 从第一个提取矛盾并了结目标。零处的传递收到类型为 `before zero x y` 的前提，按 `before` 的计算规则它是假真值，由 `Empty.rec*` 消去。空前提给出空结论；除「这个序是空的」之外，没有使用空序的任何性质。

```agda
          → Tri ⟨ before zero x y ⟩ (x ≡ y) ⟨ before zero y x ⟩
  triZero x y x∈ y∈ = Empty.rec (zero-empty x x∈)
  transZero : (x y z : S) → ⟨ before zero x y ⟩ → ⟨ before zero y z ⟩
            → ⟨ before zero x z ⟩
  transZero x y z h k = Empty.rec* h
```

后继步需要层 `n` 的三类数学输入：其最小元原理、`before n` 的三歧与传递性，以及其成员的一份点名册。前两类使最先分歧成为该层诸子集上的严格比较，点名册则通过布尔掩码枚举这些子集；三者共同给出层 `suc n` 所需的点名册与序律。

```agda
stageOrder (suc n) = record { tally = raised ; tri = triSuc ; trans = transSuc }
  where
  module Prev = Ordered n (stageOrder n)
  module Diff = Difference (before n) (finiteStage n) Prev.tri Prev.trans Prev.leastMem
  module Power = PowerStep (# n) (numeral-ord n) Prev.tally
```

认同 `step` 是路径 `Lset-suc (# n)`，它断言 `n` 的后继层就是层 `n` 的可定义幂集。新点名册 `raised` 保留幂集点名册的长度与条目，因此枚举的是同样的可定义子集；改变的只是成员证书从何处读取，这正是 `step` 进入之处。

```agda
  step : finiteStage (suc n) ≡ 𝒟ₒ (finiteStage n)
  step = Lset-suc (# n)

  raised : Tally (finiteStage (suc n))
  raised = record
    { size   = Tally.size Power.powerTally
```

`inside` 字段把每份成员证书沿 `step` 的逆向从可定义幂集传输到后继层，因为证书证明的是在幂集中的成员关系，而点名册声称的是在 `Lset (# suc n)` 中的成员关系。对称地，`onto` 取后继层的成员证书，先沿 `step` 向前传输，再调用幂集点名册的覆盖。两个方向的传输都只作用于一句成员陈述，别无其他。

```agda
    ; item   = Tally.item Power.powerTally
    ; inside = λ i → subst (λ w → ⟨ Tally.item Power.powerTally i ∈ˢ w ⟩) (sym step)
                       (Tally.inside Power.powerTally i)
    ; onto   = λ x x∈ → Tally.onto Power.powerTally x
                          (subst (λ w → ⟨ x ∈ˢ w ⟩) step x∈) }
```

辅助引理 `members` 提取 `precedes-tri` 所要求的包含前提。层 `n` 的可定义子集的成员都在层 `n` 中；这就是 `𝒟ₒ∋⊆`，从可定义幂集中的成员关系反向读出。先沿 `step` 把 `x` 的证书传输进幂集，所得是一个函数：对 `x` 的每个成员 `w`，给出 `w` 落在层 `n` 中的证书。

```agda
  members : (x : S) → ⟨ x ∈ˢ finiteStage (suc n) ⟩
          → (w : S) → ⟨ w ∈ˢ x ⟩ → ⟨ w ∈ˢ finiteStage n ⟩
  members x x∈ = 𝒟ₒ∋⊆ (finiteStage n) x (subst (λ v → ⟨ x ∈ˢ v ⟩) step x∈)

  triSuc : (x y : S) → ⟨ x ∈ˢ finiteStage (suc n) ⟩ → ⟨ y ∈ˢ finiteStage (suc n) ⟩
         → Tri ⟨ before (suc n) x y ⟩ (x ≡ y) ⟨ before (suc n) y x ⟩
```

两条后继字段现在都是一行的应用。`triSuc` 是 `Diff.precedes-tri`，两条包含前提由 `members` 提供，因为 `before (suc n)` 按定义就是 `precedes (before n) (finiteStage n)`。`transSuc` 逐字就是 `Diff.precedes-trans`，其前提本就具有正确的形状。递归就此闭合：每层的序事实都是上一层的序事实，被最先分歧理论所消费。

```agda
  triSuc x y x∈ y∈ = Diff.precedes-tri x y (members x x∈) (members y y∈)

  transSuc : (x y z : S) → ⟨ before (suc n) x y ⟩ → ⟨ before (suc n) y z ⟩
           → ⟨ before (suc n) x z ⟩
  transSuc = Diff.precedes-trans
```

## 极限层

`Lset ω` 的每个成员取得其最小有穷层号；先比较层号、再比较局部层序，便得到极限层良序。

`Lset ω` 的成员会出现在某个由数码索引的有穷层。在它出现的诸层中，自然数的最小元搜索给出最小者，称为该元素的**层号**。后文组织不同层号之间的下降时，还会再次使用自然数的良基性。

极限的成员被包装成 `Limit`：一个集合连同它在 `Lset ω` 中的成员证书。引理 `inSome` 把这样的证书转换成一句截断的陈述：该集合出现在某个有穷层。从极限层读出证书，仅仅给出某个属于 `ω` 的 `δ`，使该集合是 `Lset δ` 的可定义子集；外层消去的目标是截断类型，而截断类型是命题，故消去正当。

```agda
Limit : Type (ℓ-suc ℓ)
Limit = Σ[ x ∈ S ] ⟨ x ∈ˢ Lset ω ⟩

inSome : (x : S) → ⟨ x ∈ˢ Lset ω ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩ ∥₁
inSome x h = PT.rec PT.squash₁ atStage (Lset-out ω x h)
  where
```

还需识别 `ω` 以下的索引 `δ`。隶属 `δ ∈ ω` 是一条截断陈述：存在提升后的自然数 `k`，使 `δ` 等于数码 `# (lower k)`。用 `PT.map` 在截断内取得该数码见证后，路径把关于 `𝒟ₒ (Lset δ)` 的可定义子集证书改写到 `Lset (# lower k)` 上；再由 `Lset-suc` 把 `x` 放入 `finiteStage (suc (lower k))`。这证明了元素出现在有穷层，同时没有混淆索引 `ω` 与层 `Lset ω`。

```agda
  atStage : Σ[ δ ∈ S ] (⟨ δ ∈ˢ ω ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩ ∥₁
  atStage (δ , δ∈ω , x∈) = PT.map named δ∈ω
    where
    named : Σ[ k ∈ Lift ℕ ] (# (lower k) ≡ δ) → Σ[ n ∈ ℕ ] ⟨ x ∈ˢ finiteStage n ⟩
```

数码命名之后，`named` 产出实际的出现层。由于 `Lset-suc` 把 `Lset (# (suc k))` 认同为 `Lset (# k)` 的可定义幂集，「该集合是 `Lset (# (lower k))` 的可定义子集」的证书沿 `sym (Lset-suc ...)` 传输为 `finiteStage (suc (lower k))` 中的成员关系。所以索引出现层的数码比出现在 `ω` 内部的数码多一，这正是索引与其后继层之间常见的差一。

```agda
    named (k , q) = suc (lower k)
      , subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-suc (# (lower k))))
          (subst (λ w → ⟨ x ∈ˢ 𝒟ₒ (Lset w) ⟩) (sym q) x∈)

levelData : (a : Limit)
          → Σ[ n ∈ ℕ ] IsLeast natOrder (λ m → a .fst ∈ˢ finiteStage m) n
```

`levelData` 正是截断存在与最小元定理相遇之处。它对谓词 `m ↦ a .fst ∈ˢ finiteStage m` 与截断见证 `inSome` 应用自然数序的 `leastOf` 与排中律，返回一个显式数码连同 `IsLeast` 数据：该数码处的层含有该集合，且更小的数码都没有该性质。因此层号是最小的出现层，而非从截断中任意选出的层。

```agda
levelData a =
  leastOf natOrder lem (λ m → a .fst ∈ˢ finiteStage m) (inSome (a .fst) (a .snd))

level : Limit → ℕ
level a = levelData a .fst

level-in : (a : Limit) → ⟨ a .fst ∈ˢ finiteStage (level a) ⟩
```

两个投影有方便的名字：`level a` 是底层集合出现的最小数码，`level-in a` 是该层处的成员证书。极限序所需的关于成员「楼层」的一切现在都已是数据，下一节将恰好用这两个材料构造那个序。

```agda
level-in a = levelData a .snd .fst
```

极限上的序先按层号比较：层号较低的成员在前，同层的两个成员则按该层自己的序比较。第二支处理层号相等的情形，其方向使得第二个成员可以在第一个成员的层上读出；正因如此，定义中不出现任何跨层的转换。

非自反与传递是对那一支的分情形，层号等式的情形直接使用相应层上的层序事实。三歧先比较层号，仅当层号相同时才由层序判定。

关系 `a ≺ b` 是「占先」的两种方式的不相交和。左支说 `a` 的层号严格更小；右支说两层号相等，并且在层 `level a` 内，两个底层集合处于该层自己的 `before` 序中。左支的 `Lift` 把自然数上的比较从 `Type ℓ-zero` 抬升到 `Type (ℓ-suc ℓ)`，即右支本已所在的宇宙，于是两支共用一个类型。这个关系按字典序读：层号分出高下，唯有打平时才去问层。

```agda
_≺_ : Limit → Limit → Type (ℓ-suc ℓ)
a ≺ b = Lift {ℓ-zero} {ℓ-suc ℓ} (level a < level b)
      ⊎ ((level b ≡ level a) × ⟨ before (level a) (a .fst) (b .fst) ⟩)

limit-irrefl : (a : Limit) → a ≺ a → Empty.⊥
limit-irrefl a (inl h)       = ¬m<m (lower h)
```

非自反性对每一支分别用相应成分的事实处理：严格不等式 `level a < level a` 被 `¬m<m` 拒绝；对 `a` 自身的 `before (level a)` 见证被 `before-irrefl` 拒绝，而后者在每层都成立且无需归纳。传递性则按两个前提各取哪一支来分情形。若两步都在层号上下降，`<-trans` 复合两个不等式；若只有一步在层号上下降，就用另一前提中的层号等式配合 `subst`，把那条严格不等式搬到正确的端点，结果仍在左支。

```agda
limit-irrefl a (inr (_ , h)) = before-irrefl (level a) (a .fst) h

limit-trans : (a b c : Limit) → a ≺ b → b ≺ c → a ≺ c
limit-trans a b c (inl h)       (inl k)       = inl (lift (<-trans (lower h) (lower k)))
limit-trans a b c (inl h)       (inr (q , _)) =
  inl (lift (subst (λ j → level a < j) (sym q) (lower h)))
```

当两个前提都取同层支时，`a ≺ b` 给出 `q : level b ≡ level a`，`b ≺ c` 给出 `p : level c ≡ level b`。复合 `p ∙ q : level c ≡ level a` 正是 `a ≺ c` 所需的等式。层序事实 `hbc` 陈述在 `level b`；沿 `q` 传输后落到 `level a`，便可由 `StageOrder.trans` 与 `hab` 复合。

```agda
limit-trans a b c (inr (q , _)) (inl k)       =
  inl (lift (subst (λ j → j < level c) q (lower k)))
limit-trans a b c (inr (q , hab)) (inr (p , hbc)) = inr (p ∙ q , joined)
  where
  moved : ⟨ before (level a) (b .fst) (c .fst) ⟩
```

`moved` 中的传输沿等式 `q` 移动 `hbc`，只改变 `before` 陈述所处的层，从 `level b` 换到 `level a`。此后两个见证便同处一层：`hab` 说在该层中 `a` 的集合先于 `b` 的，`moved` 说 `b` 的先于 `c` 的，于是在层 `level a` 处用 `StageOrder.trans` 把二者接成 `joined`，即 `a` 在自己层内先于 `c` 的见证。传递性至此完成；接着陈述三歧性，其判定方式是直接比较两层号。

```agda
  moved = subst (λ j → ⟨ before j (b .fst) (c .fst) ⟩) q hbc
  joined : ⟨ before (level a) (a .fst) (c .fst) ⟩
  joined = StageOrder.trans (stageOrder (level a)) (a .fst) (b .fst) (c .fst) hab moved

limit-tri : (a b : Limit) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
limit-tri a b = byLevel (level a ≟ level b)
```

三歧性先判定 `level a ≟ level b`。层号不等时立即得到相应的严格比较支。相等支给出 `p : level a ≡ level b`；沿 `sym p` 传输 `level-in b`，便把 `b` 放入 `finiteStage (level a)`，于是 `StageOrder.tri` 能在同一层比较两个底层集合。

```agda
  where
  byLevel : NatOrder.Trichotomy (level a) (level b) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
  byLevel (NatOrder.lt h) = lt (inl (lift h))
  byLevel (NatOrder.gt h) = gt (inl (lift h))
  byLevel (NatOrder.eq p) = same
```

局部三歧按极限关系所需的方向重新打包。若局部结果是 `a before b`，就在 `a ≺ b` 的同层支中返回 `sym p : level b ≡ level a`；若结果是 `b before a`，就在 `b ≺ a` 的同层支中返回 `p`，并把 before 证明传输到层 `level b`。底层集合相等可提升为 `Limit` 中的相等，因为成员证明分量是命题。

```agda
    (StageOrder.tri (stageOrder (level a)) (a .fst) (b .fst) (level-in a) b∈)
    where
    b∈ : ⟨ b .fst ∈ˢ finiteStage (level a) ⟩
    b∈ = subst (λ j → ⟨ b .fst ∈ˢ finiteStage j ⟩) (sym p) (level-in b)
    same : Tri ⟨ before (level a) (a .fst) (b .fst) ⟩ (a .fst ≡ b .fst)
```

重新包装按该层的判定分三种。若 `a` 的集合先于 `b` 的，结果是 `≺` 的右支，并以 `sym p` 供给等式，方向恰是定义所要求的。若两集合相等，`Σ≡Prop` 把它提升为配对 `a` 与 `b` 之间的路径；这是合法的，因为 `Limit` 的第二个分量是命题，这就是 `eq` 情形。若 `b` 的集合先于 `a` 的，则沿 `p` 把该 `before` 事实传输到它应被陈述的层号处，结果是以相反实参给出的右支。这里的每种情形都没有用到已造好的成分之外的任何东西。

```agda
               ⟨ before (level a) (b .fst) (a .fst) ⟩
         → Tri (a ≺ b) (a ≡ b) (b ≺ a)
    same (lt h) = lt (inr (sym p , h))
    same (eq q) = eq (Σ≡Prop (λ z → snd (z ∈ˢ Lset ω)) q)
    same (gt h) = gt (inr (p , subst (λ j → ⟨ before j (b .fst) (a .fst) ⟩) p h))
```

良基性的证明是两层嵌套的归纳，而把它们分开是有意的。外层是对层号的归纳，采用库中现成的封装，它提供一条覆盖所有更低层的归纳假设。内层沿有穷层已有的可及性作普通的下降，其合法性正来自该层的有穷性。跨层下降的一步使用外层假设，层内的一步使用内层假设；内层函数除自己的可及性实参外不沿任何东西递归，因此二者从不需要同时比较。

固定层号为 `k` 的目标 `b`，以及层 `k` 中与它底层集合相同的点 `u`。内层论证把 `u` 关于局部关系 `Below k` 的可及性转成 `b` 关于极限关系的可及性。展开 `Acc` 后，任意前驱记为 `c`。若 `c` 的层号更低，就使用外层归纳假设；若层号相同，就把它变成 `u` 的局部前驱并使用内层可及性。

```agda
accInside : (k : ℕ)
          → ((m : ℕ) → m < k → (b : Limit) → level b ≡ m → Acc _≺_ b)
          → (u : Point k) → Acc (Below k) u
          → (b : Limit) → level b ≡ k → b .fst ≡ u .fst → Acc _≺_ b
accInside k ih u (acc ru) b q e = acc step
```

完成 `step` 按前提 `c ≺ b` 所取的支分情形。左支中，`c` 的层号严格小于 `b`，因而小于 `k`；该不等式用 `subst` 在等式 `q` 之下搬动，然后在层号 `level c` 处使用 `ih`，这正是跨层的情形。右支中，`c` 与 `b` 同层号，故二者都在层 `k` 之内，下降便交给内层可及性：`ru` 是 `u` 的可及性的 `acc` 构造子所提供的函数，把它作用于与 `c` 对应的点 `pc` 以及 `pc` 位于 `u` 之下的证明。

```agda
  where
  step : (c : Limit) → c ≺ b → Acc _≺_ c
  step c (inl h) = ih (level c) (subst (λ j → level c < j) q (lower h)) c refl
  step c (inr (qb , hc)) = accInside k ih pc (ru pc below) c qc refl
    where
```

右支的簿记需要显式写出。首先 `qc` 复合两条层号等式，即 `sym qb` 与 `q`，证明 `level c ≡ k`；正是这一点使 `c` 能被放到层 `k` 中看。然后 `pc` 把 `c` 的底层集合与它在层 `k` 中的隶属打包在一起，该隶属由 `level-in c` 沿 `qc` 传输得到。`Point k` 就是一个集合连同这样的证书，所以这一个构造把论证从极限带回内层序所在的有穷层。

```agda
    qc : level c ≡ k
    qc = sym qb ∙ q
    pc : Point k
    pc = c .fst , subst (λ j → ⟨ c .fst ∈ˢ finiteStage j ⟩) qc (level-in c)
    below : Below k pc u
```

在层号相同的情形，每个极限前驱 `b` 都与 `u` 位于同一有穷层 `k`，并在该层序中低于 `u`。该分支携带的等式只把两个端点对齐到固定的 `k`；随后 `u` 关于 `Below k` 的可及性给出 `b` 的可及性。因此，内层递归只沿一个有穷层的序下降。

```agda
    below = subst (λ v → ⟨ before k (c .fst) v ⟩) e
              (subst (λ j → ⟨ before j (c .fst) (b .fst) ⟩) qc hc)

accByLevel : (k : ℕ) → (b : Limit) → level b ≡ k → Acc _≺_ b
accByLevel = WFI.induction <-wellfounded outer
  where
```

外层是对自然数层号的良基归纳，其归纳假设处理层号严格小于 `k` 的前驱；内层可及性处理仍处于层号 `k` 的前驱。两种情形合成字典序式的证明，无须假设不同有穷层上的序彼此相容。

```agda
  outer : (k : ℕ) → ((m : ℕ) → m < k → (b : Limit) → level b ≡ m → Acc _≺_ b)
        → (b : Limit) → level b ≡ k → Acc _≺_ b
  outer k ih b q = accInside k ih here
    (Ordered.wellFounded k (stageOrder k) here) b q refl
    where
```

`outer` 的主体把目标化归到内层引理。它先造出 `here`，即与 `b` 对应的层 `k` 的点，其造法与上面的 `pc` 完全相同；然后 `Ordered.wellFounded k (stageOrder k) here` 提供该点在层 `k` 序中的可及性，`accInside` 便由此接手，其余两个实参是层号等式 `q` 以及把 `b` 的底层集合与 `here` 的认同起来的自反等式。最后的陈述 `limit-wf` 说极限的每个成员都可及，做法是在层号 `level a` 处以平凡等式 `refl` 实例化层号归纳。

```agda
    here : Point k
    here = b .fst , subst (λ j → ⟨ b .fst ∈ˢ finiteStage j ⟩) q (level-in b)

limit-wf : WellFounded _≺_
limit-wf a = accByLevel (level a) a refl

limitOrder : SWO Limit
```

因此，`≺` 是 `Limit` 上的严格良序：它满足三歧、非自反与传递，而两层归纳证明其良基性。首次出现层号不同的元素按层号排序；只有层号相同的元素才由一个有穷层序比较。

```agda
limitOrder = record
  { _<∙_   = _≺_
  ; tri∙   = limit-tri
  ; irr∙   = limit-irrefl
  ; trans∙ = limit-trans
```

因此，`limitOrder` 是 `Lset ω` 诸成员上的严格良序：层号是主键，最小层号相同的元素由该有穷层的序比较。于是，它的最小元运算可从极限层上任意仅仅非空的命题值族中作出选取。

```agda
  ; wf∙    = limit-wf }
```

## 小结

有穷点名册沿可定义幂集上升，支撑每个数码层处良基的最先分歧序，并最终给出 `Lset ω` 上的 `limitOrder`。

`Tally` 就是本章拥有的全部有穷性：一个命中每个成员的有穷族，既不要求单射，也不要求可判定的相等。`PowerStep.powerTally` 把它抬到可定义幂集上，办法是枚举点名册上的位向量，并指出已清点层的每个子集都可定义；`stageOrder` 随后沿诸数码跑完这一步，于是每个有穷层都有一份点名册。

`precedes` 在两个子集最先分歧之处比较它们。它的非自反性直接由定义推出，传递性由比较两个见证得到，三歧则由排中律连同基底的最小元得到。良基性并不单由这条比较的定义推出；在这里，它经由 `Search` 从点名册得到。自然数子集上的下降链例子说明了为何有穷层这一假设不可省略。

`limitOrder` 是 `Lset ω` 诸成员上的一个严格良序，以层号为主键，层内则用各有穷层自己的序。它就是选择公理将要取用的接口：有了它，`leastOf` 能从极限层诸成员的任一非空性质中挑出一个成员，且每次挑出同一个。