有限层上的良序

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

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

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

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

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

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

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

{-# 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 相关工具，它们把一层与其内部的有穷集合联系起来。

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；而自然数的实例正是用来给数码排序的那一个。

  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 排除自环，并可用 _≟_ 判定相等。这些恰好是找出见证某性质的最小下标所需的性质，也是扫描中作出逐步判定所需的性质。

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 提供消费良基关系的递归原理。

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 及其极限 ω 用来索引诸有穷层与极限。

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 的证据类型；点名册用这一形式证明每个列出项确实属于集合，并陈述每个成员都被表示。

open InfinitySet using ( #_; ω )

open hPropStructure 𝒮ᵥ

点名册

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

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

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

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

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」的命题截断。因此，只能得到某个索引仅仅存在，而不会暴露一个选定位置。后文只在目标为命题时消去这份截断见证。

    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 显式给出，以便递归能对它作模式匹配。

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 恢复被剥掉的类型。

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 把归纳假设穿过这一移位。相反的复合从未被断言，这里也没有任何关于「拼合是单射」的主张。

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 合起来证明每个位向量都被触及。

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 所期待的形状。

maskCount : ℕ → ℕ
maskCount zero    = 
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 的索引被一分为二，所在的半支给出首位，内层索引给出尾部。这个读法是一个定义而非定理：它只是按规则计算。

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 的路径。基情形中，空向量来自第零号索引。这是整个枚举中唯一必须交付数据而非仅仅存在性的地方，而它之所以能做到，是因为递归沿着向量本身进行。

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 字段所期待的形状。

     ∙ 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。其结果类型把族与长度打包成一个依赖对，于是递归可以增长长度而不必对掩码做任何算术。

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) 所记录的内容。

  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，位与等式都显式给出。

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 恰好完成对见证三元组的这一簿记。

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 成立；否则递归回答尾部的位置，同样的上移照旧适用。

       → Σ[ 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 的原因。

  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 连同一条路径。两个方向都不带截断，这正是后文关于成员性的论证能在选取两侧传递真实见证的原因。

  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 情形中头部以零号位置作答，更深的位置照旧递归。

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，条目等式原样保留。两条规格合起来说明选取结果既不比掩码标出的多、也不比它少，尽管没有断言这两种位置对应方式互为逆映射。

  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 并沿右移后的族继续。

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 才能证明它写下的掩码重现给定的子集。

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 本身与计算无关，被匹配的只是裁决，因此这个定义是一对方程而非证明。

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 ⟩ 是否成立。

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 正是该原像元素的两个投影。这并非从任意点名册原像中选取索引，因为允许重复的点名册原像未必是命题。

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 构造。

  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。

  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。两步的数据都在截断之内产生，因此没有从单纯存在性命题中提取选定的见证。

  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。三者的复合正是证明中显示的三段路径。

    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 证明其嵌入形式的成员关系。

      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。

    (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 本身。

    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。

  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。

      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。

                 (λ 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。

      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 张成的集合。其余字段补全记录：每个条目附带其可定义性证书，覆盖条款随后给出。

               (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。

    ; 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 的覆盖性所要求的：每个可定义子集都被命中，尽管未必由唯一的掩码命中。

    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，以及每个严格更小的满足者都会导出矛盾。

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 的条目位于其下。右支中，每个条目都不满足谓词。两个选项携带的都是完整数据而非截断的存在性，这使后续构造能返回真实的元素。

  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，它把尾部的结果与头部的裁决合并成整个族的结果。

  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 分析该比较的三种结果。

            → (⟨ 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。

      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 处理。

      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。优胜者的证书在每个分支都由旧证书重建。

      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。

    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 矛盾。

    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。至此，导言所说的四种组合齐备。

    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。

  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，就必须驳倒给定的截断见证。该消去是合法的，因为目标是空类型这一命题，因此见证的截断可以在不作任何选择的情况下拆开。

      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 便将其化为矛盾。紧接的代码行执行的正是这次传输。

          (λ { (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，彻底矛盾，因为见证已被证明必然把一个满足者带进族中。

        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 的反驳只用于证明「不可及」这一谓词非空。

    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 的截断配对，因此该假设只是说不可及元素之集非空。

        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 在肯定支中返回证书。

        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 合法，把它交给假定的可及性反驳便封闭了矛盾。注意：全程并未构造或排除任何无穷下降序列，论证完全就是这个矛盾。

          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，且其下方一致成立。正是成员条款的方向决定了比较中哪一方胜出。

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 的见证，把第二条施于第一条即是矛盾。

  ⟨ 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 成员也满足的元素。注意结论的形状：它是显式数据而非截断，因为调用方需要真实的极小元。

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 的截断见证。因此证明先消去第一个截断，再消去第二个，二者的目标都又是截断、因而是命题。

                 × ((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 分析其三种结果。

    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 的成员关系沿复合比较传输过去。

      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 传输成员关系即得矛盾。

        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 把这一反驳打包。

      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。两个不对称情形都已处理、相等已被驳倒，传递性就此完成。

        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。

  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 的反驳消去成矛盾的依据。

    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 处成员等价的两条包含子句。证明只有这里需要从否定性陈述造出成员蕴含，而它实际上是化了装的双重否定消去。

    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 消去到它是正当的。

      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 处重合。

      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 的成员等价即可在每点使用。

        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⊆ 同理。注意消去的方向：进入取值为命题的成员关系，这恰是命题截断所允许的。

      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 分支得证。

      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 序之下其下方再无分歧点。正是这种显式性，使得最小分歧点此后能被用作见证。

    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。逐一命名使下面两个对称分支保持可读，因为每一支都要引用其中若干字段。

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

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

      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.⊥ 是命题。

      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 装入截断交付。

        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 的三歧完成，一层上的局部序便是其成员上的线序，只待良基性。

        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 逐支作用：每个备选支各应用一个函数；三条子句就是它的计算规则。它将把「关于两个集合证明的三歧」转换为「关于一层的两个点所需的三歧」，二者只差是否附带成员证明。

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，即递归在下一层造出的那个序。

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，即定义该比较时已确立的无前提非自反性。正因如此，非自反性不属于递归必须携带的数据。

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.⊥ 是命题，消去该截断是正当的。

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。由于隶属是命题，集合相同的两个点已然相等；这一个事实承担了「关于集合的陈述」与「关于点的陈述」之间往返的全部工作。

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 对任意集合的传递性。非自反性由最先分歧统一推出；局部序需要良基性时，则从点名册重新得到。

  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 恰好提供这一点：由于第二分量是某个命题的证明，底层集合之间的路径可以延拓为点之间的路径。

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 再把集合的等式升级为点的等式。覆盖仍然是截断的，与点名册本身一样。

    (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 })

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

    (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，三条序律来自层比较，良基性则来自有穷扫描。因此，构造清楚地区分了局部比较与排除无穷下降的有穷性论证。

  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 的。除前提外，这里没有任何截断。

    ; 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∈ 而得。

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