有限层上的良序

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

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

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

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

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

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

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

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

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

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

module SemV = FOL.Semantics 𝒮ᵥ

open import Cubical.Data.Bool using ( false≢true )

布尔值在这里作为掩码出现：要枚举带点名册的集合的子集，就把每个条目保留或丢弃，用 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

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

open import Cubical.Induction.WellFounded
  using ( Acc; acc; WellFounded; isPropAcc; module WFI )

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

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 hPropView 𝒮ᵥ

点名册

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     (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     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     (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     = 
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     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 , 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     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     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     f []          ()      e

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

select-in (suc n) f (false ∷ v) zero    e = ⊥₀-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     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 证明记录下的掩码确实在每个位置重现 d 给出的布尔值：在 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 把判定变成一位：yes 携带 ⟨ P ⟩ 的证明，记为 true；no 携带反驳，记为 false。命题 P 本身与计算无关，被匹配的只是判定，因此这个定义是一对方程而非证明。

decideOf : (P : hProp (ℓ-suc ℓ)) → Dec ⟨ P ⟩ → Bool
decideOf P (yes _) = true
decideOf P (no _) = false

decide-true : (P : hProp (ℓ-suc ℓ)) (s : Dec ⟨ P ⟩) → ⟨ P ⟩ → decideOf P s ≡ true
decide-true P (yes _) p = refl

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

decide-true P (no np) p = ⊥₀-rec (np p)

decide-sound : (P : hProp (ℓ-suc ℓ)) (s : Dec ⟨ P ⟩) → decideOf P s ≡ true → ⟨ P ⟩
decide-sound P (yes p) _ = p
decide-sound P (no _) e = ⊥₀-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 : 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 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)) ∥₁

part-out v y y∈ = 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))

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

    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

  (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 : ⟪ 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) (SemV.decideMembership lem y x))

part-mask : (x : S) → ⟨ x ∈ˢ 𝒟ₒ (Lset σ) ⟩ → part (maskOf x) ≡ 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∈ = rec₁ ((y ∈ˢ x) .snd) step (part-out (maskOf x) y y∈)
    where

    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) (SemV.decideMembership lem (item i) x)
        (sym (marks-lookup size item

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

    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) (SemV.decideMembership lem z x)) i
         ∙ decide-true (item i ∈ˢ x)
           (SemV.decideMembership lem (item i) x)

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

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

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

  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 → ⊥₀)
              (trans : (a b c : A) → a ≺ b → b ≺ c → a ≺ c) where

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

Least P m = ⟨ P m ⟩ × ((b : A) → ⟨ P b ⟩ → b ≺ m → ⊥₀)

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 → ⊥₀)))
  ⊎ ((i : Fin n) → ⟨ P (f i) ⟩ → ⊥₀)

scan : (P : A → hProp (ℓ-suc ℓ))
     → ((a : A) → Dec ⟨ P a ⟩)
     → (n : ℕ) (f : Fin n → A) → Found P n f
scan P decP     f = inr (λ ())
scan P decP (suc n) f = combine (scan P decP n (λ i → f (suc i))) (decP (f zero))
  where
  combine : Found P n (λ i → f (suc i))

          → Dec ⟨ P (f zero) ⟩ → Found P (suc n) f
  combine (inl (i , pi , mi)) (yes 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

    decide (lt h) = inl (zero , (p₀ , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f zero → ⊥₀
      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)

    decide (eq h) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → ⊥₀
      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

    decide (gt h) = inl (suc i , (pi , minAt))
      where
      minAt : (j : Fin (suc n)) → ⟨ P (f j) ⟩ → f j ≺ f (suc i) → ⊥₀
      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

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

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

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

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

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

  nowhere : ((i : Fin n) → ⟨ P (f i) ⟩ → ⊥₀) → ⊥₀
  nowhere none = rec₁ isProp⊥ atWitness h
    where
    atWitness : Σ[ a ∶ A ] ⟨ P a ⟩ → ⊥₀
    atWitness (a , pa) = rec₁ isProp⊥

      (λ { (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 → ⊥₀

    everywhere b pb hb = rec₁ 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) = ⊥₀-rec (nowhere none)

wellFounded : WellFounded _≺_

wellFounded a = fromDec (lem (Acc _≺_ a , isPropAcc a))
  where
  fromDec : Dec (Acc _≺_ a) → Acc _≺_ a
  fromDec (yes h) = h
  fromDec (no nh) = ⊥₀-rec (found .snd .fst (acc below))

    where
    NotAcc : A → hProp (ℓ-suc ℓ)
    NotAcc b = (Acc _≺_ b → ⊥₀) , isProp→ isProp⊥
    found : Σ[ m ∶ A ] Least NotAcc m
    found = least NotAcc (λ b → lem (NotAcc b)) ∣ a , nh ∣₁

    below : (b : A) → b ≺ found .fst → Acc _≺_ b
    below b hb = pick (lem (Acc _≺_ b , isPropAcc b))
      where
      pick : Dec (Acc _≺_ b) → Acc _≺_ b
      pick (yes h) = h

      pick (no nb) = ⊥₀-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 是「这类见证单纯存在」的命题，随 squash₁ 打包成一个真值。由于见证藏在截断之后，被断言的只有其存在，任何东西都不选定 z。非自反性于是只花一行：把截断消去到空类型 (一个命题) 中，暴露出同时有 z ∈ x 与 z ∉ x 的见证，把第二条施于第一条即是矛盾。

  ⟨ z ∈ˢ A ⟩ × ⟨ z ∈ˢ y ⟩ × (⟨ z ∈ˢ x ⟩ → ⊥₀) × 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 ∥₁ , squash₁

precedes-irrefl : (R : S → S → hProp (ℓ-suc ℓ)) (A x : S) → ⟨ precedes R A x x ⟩ → ⊥₀
precedes-irrefl R A x = rec₁ 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 ⟩
                 × ((b : S) → ⟨ b ∈ˢ A ⟩ → ⟨ P b ⟩ → ⟨ R b m ⟩ → ⊥₀)))
  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 =

  rec₁ squash₁ (λ wp → rec₁ 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) =