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

对每个序数 `γ`，本章在宿主类型论中构造 `Lset γ` 的成员上的严格良序。构造分为相互嵌套的两层。先为每个集合指定它最初成为可定义子集时所依据的序数；诞生序数不同的集合按诞生序数排序，同生的集合则按共同前层之上的最小名字排序。随后借隶属归纳同时得到各层的序。所得结果是每一层处的宿主层良序，还不是集合论内部的关系，也不是整个 `L` 上的单一良序。

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

经典假设用于把仅仅非空的名字族变成其确定的最小成员。对每个指数，`stepAt` 都统一地由这个最小名字构造得到。

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

全部构造都在固定的宇宙层级与单一假设 `LEM (ℓ-suc ℓ)` 下进行。同一假设既传给名字序的构造，也传给最小名字的搜索；把各层的序装配成族时不再加入其他经典前提。

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

此处被排序的对象，是宿主类型论所见的累积层级成员。隶属证明随成员一同携带，但这些证明是命题，因而不会制造同一元素的额外副本。后文在 `L` 内描述并表示同一良序时，这一区分至关重要。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isL; Lset; Lset→isL )
```

为确定集合的诞生序数，先取包含它的最早序数层。该层是后继层，因而有一个前驱；这个前驱就是该集合首次作为可定义子集出现时所依据的层。随后，序数三歧性将说明这个诞生序数严格低于每个包含该集合的序数层。

```agda
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( IsPredOf; predOf; carveAt )
```

一旦某层已有良序，其公式与参数列便组成下一层的良序名字。一个后继层成员可能有许多这样的名字，因此构造选取其中最小者，并借这些选定代表比较成员。这里的唯一性属于最小代表，而不属于一般的名字。

```agda
open import L.Choice.FiniteStageOrders {ℓ} lem using ( Tri-map )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; isPropLeastOf )
```

本构造会数次改变表示：从呈现索引到它所表示的集合，从集合到集合与其隶属证明组成的成员，以及从成员到其最小名字。每次改变都是单射的，因此可以搬运相等与严格比较，而不会认同不同的元素。

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
```

名字完备性只给出存在性的命题截断：它断言指称该集合的名字仅仅存在，并不展示某个选定名字。后面的极小元论证能够消去这一截断，因为最小名字的总类型本身是命题。

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

层级中的集合既有小呈现类型，也有宿主隶属类型。呈现映射把前者嵌入后者。这座桥使构造能在形成名字时使用小参数，同时保留直接陈述在 `Lset γ` 成员上的序。

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

从此处起，`S` 表示集合的宿主载体。因此，`x ∈ˢ Lset γ` 一类陈述是表达可构造层隶属关系的外部类型，还不是在对象理论中求值的公式。

```agda
open hPropStructure 𝒮ᵥ
```

## 一个集合被雕出的层

把一般切取论证用于「`x` 属于某层」这一性质。由于 `stage x p` 是满足该性质的最早层，结果给出序数 `δ`，其后继恰等于 `stage x p`。因此，`δ` 是最早包含层的前驱，并不是另行选出的另一个最早层。

```agda
theCarve : (x : S) (p : ⟨ isL x ⟩) → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
theCarve x p = predOf (λ σ → x ∈ˢ Lset σ) (stage x p) (stage-ord x p)
  (stage-earliest x p)
  (carveAt (λ σ → x ∈ˢ Lset σ) (stage x p) x (stage-mem x p) (λ δ hz → hz))
```

序数 `birth x p` 就是这个前驱。从数学上说，它记录 `x` 首次作为可定义子集出现时所依据的层。不应把它理解为 `x` 的冯·诺伊曼秩；此处给出的等同仅是：它的后继就是最早包含 `x` 的可构造层。

```agda
opaque
  birth : (x : S) → ⟨ isL x ⟩ → S
  birth x p = theCarve x p .fst
```

`theCarve x p` 给出的前驱数据同时包含两项：所取前驱是序数，以及它的后继等于 `stage x p`。定理 `birth-ord` 读出前一项，使 `birth x p` 随后可以与其他序数比较，也可以作为隶属归纳的指标。

```agda
opaque
  unfolding birth
  birth-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (birth x p)
  birth-ord x p = theCarve x p .snd .fst
```

第二个投影给出定义性等式 `sucV (birth x p) ≡ stage x p`。这条等式连接两种有用观点：`stage` 指出 `x` 首次属于哪一层，而 `birth` 指出 `x` 据哪一前层形成。

```agda
  birth-suc : (x : S) (p : ⟨ isL x ⟩) → sucV (birth x p) ≡ stage x p
  birth-suc x p = theCarve x p .snd .snd
```

因为 `x` 属于其最早层，而该层就是 `sucV (birth x p)`，所以 `x` 属于其诞生序数的后继层。正是这条隶属关系，使我们能把 `x` 看作 `Lset (birth x p)` 的可定义子集，并在那里为它指定名字。

```agda
birth-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (sucV (birth x p)) ⟩
birth-mem x p =
  subst (λ w → ⟨ x ∈ˢ Lset w ⟩) (sym (birth-suc x p)) (stage-mem x p)
```

诞生序数自身属于它的后继序数，前驱等式把这条隶属搬运到 `stage x p`。因此，最早包含 `x` 的层也包含 `x` 形成时所依据的序数。

```agda
birth-stage : (x : S) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ˢ stage x p ⟩
birth-stage x p =
  subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (birth-suc x p) (self∈sucV (birth x p))
```

虽然 `birth` 接收 `x` 可构造的一份证明 `p`，其值并不包含对这类证明的数学选择。可构造性是命题，所以任意两份证明 `p` 与 `q` 都相等；把函数 `birth x` 作用于该等式，即得两种输入产生同一序数。

```agda
birth-proof : (x : S) (p q : ⟨ isL x ⟩) → birth x p ≡ birth x q
birth-proof x p q = cong (birth x) (snd (isL x) p q)
```

设 `x ∈ Lset γ`，且 `γ` 是序数。用三歧性比较 `γ` 与最早层 `stage x p`。情形 `γ ∈ stage x p` 不可能成立：它会给出一个更早且已包含 `x` 的序数层，违背 `stage x p` 的定义性最早性。

```agda
private
  decideIn : (γ x : S) → IsOrd γ → (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
           → ⟨ γ ∈ˢ stage x p ⟩ ⊎ ((γ ≡ stage x p) ⊎ ⟨ stage x p ∈ˢ γ ⟩)
           → ⟨ birth x p ∈ˢ γ ⟩
  decideIn γ x ordγ p h (inl γ∈) = Empty.rec (stage-earliest x p γ ordγ h γ∈)
```

若 `γ` 等于最早层，搬运 `birth-stage` 即直接得到所需隶属。若最早层属于 `γ`，则序数 `γ` 的传递性把 `birth x p ∈ stage x p` 与 `stage x p ∈ γ` 合成。它们是两个不导致矛盾的可能情形。

```agda
  decideIn γ x ordγ p h (inr (inl e)) =
    subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (sym e) (birth-stage x p)
  decideIn γ x ordγ p h (inr (inr s∈)) = ordγ .fst (birth-stage x p) s∈
```

由此，只要 `x` 是序数层 `Lset γ` 的成员，它的诞生序数就属于 `γ`。这个结论是严格的。随后构造 `γ` 处的序时，该事实把每个成员的诞生序数置于更小的序数之中，而归纳假设已经为这些序数提供了层序。

```agda
birth-in : (γ : S) → IsOrd γ → (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
         → ⟨ birth x p ∈ˢ γ ⟩
birth-in γ ordγ x p h =
  decideIn γ x ordγ p h (ord-tri γ ordγ (stage x p) (stage-ord x p))
```

## 沿一个单射搬运良序

对宿主集合 `A`，类型 `Mem A` 的元素由一个集合及其属于 `A` 的证据组成。携带这份证据，使后面的序关系具有正确类型。由于隶属关系取值于命题，两个成员只要底层集合相同，就不会仅因隶属证据的取得方式不同而有所区别。

```agda
Mem : S → Type (ℓ-suc ℓ)
Mem A = Σ[ x ∈ S ] ⟨ x ∈ˢ A ⟩
```

固定类型 `A` 上的严格良序 `w`。接下来的构造只使用该结构所含的关系与定律，因此同样适用于名字序、层成员序及其不同表示之间的转换。

```agda
module _ {ℓc : Level} {A : Type ℓc} (w : SWO A) where
  open SWO w using () renaming ( _<∙_ to _<ʷ_ )
```

用 `relOf w a b` 表示 `w` 中所含的严格比较，使后文能讨论该关系而无须展开良序的构造。特别地，这一记法不会把该关系变成对象集合论中的对象；它仍是宿主类型论中的类型值关系。

```agda
  relOf : A → A → Type (ℓ-suc ℓ)
  relOf a b = a <ʷ b
```

设 `f : B → C` 为单射，且 `C` 已带严格良序。若通过比较 `f u` 与 `f v` 来比较 `B` 中的 `u` 与 `v`，所得关系应继承一个严格良序。单射性不可缺少之处，正是把 `C` 中的相等情形反映回 `B`。

```agda
module _ {ℓb ℓc : Level} (B : Type ℓb) (C : Type ℓc) (w : SWO C)
         (f : B → C) (finj : (u v : B) → f u ≡ f v → u ≡ v) where
  open SWO w using () renaming
    ( _<∙_ to _<ᶜ_ ; tri∙ to triᶜ ; irr∙ to irrᶜ
    ; trans∙ to transᶜ ; wf∙ to wfᶜ )
```

拉回关系规定：`u` 小于 `v`，当且仅当像 `f u` 小于 `f v`。因此，它把 `B` 排成由其在 `C` 中的像所表示的有序子集；这里既不要求满射，也不声称存在序同构。

```agda
  private
    _<ᵇ_ : B → B → Type (ℓ-suc ℓ)
    u <ᵇ v = f u <ᶜ f v
```

`C` 中的三歧性为两个像给出三种情形。两个严格情形已经是拉回关系中的比较，而像相等时由单射性得到原点相等。因此，`B` 上的关系满足三歧性。

```agda
    pullTri : (u v : B) → Tri (u <ᵇ v) (u ≡ v) (v <ᵇ u)
    pullTri u v = Tri-map id (finj u v) id (triᶜ (f u) (f v))
```

良基性也能拉回。若 `f u` 在 `C` 中可及，它的可及树就为每个低于它的 `f v` 含有一棵子树。`u` 的前驱 `v` 恰好给出这样的比较，递归地拉回相应子树便证明 `v` 在 `B` 中可及。因此沿 `f` 搬运的是可及性本身，而不只是「没有展示出下降序列」这一较弱陈述。

```agda
    pullAcc : (u : B) → Acc _<ᶜ_ (f u) → Acc _<ᵇ_ u
    pullAcc u (acc r) = acc (λ v h → pullAcc v (r (f v) h))
```

非自反性直接转移：若某点在拉回关系中小于自身，它的像就会在 `C` 中小于自身。结合刚证明的三歧性，这给出了源类型上的前两条序定律。

```agda
  pullOrder : SWO B
  pullOrder = record
    { _<∙_   = _<ᵇ_
    ; tri∙   = pullTri
    ; irr∙   = λ u h → irrᶜ (f u) h
```

传递性来自在 `C` 中合成三个像之间的比较，而可及性论证给出良基性。这些定律补全 `pullOrder`，即通过单射 `f` 观察 `B` 的元素而得到的严格良序。

```agda
    ; trans∙ = λ u v z → transᶜ (f u) (f v) (f z)
    ; wf∙    = λ u → pullAcc u (wfᶜ (f u)) }
```

小呈现 `⟪ A ⟫` 中的每个索引都表示 `A` 的一个实际成员。把其像与这份隶属证据配对，便得到从呈现索引到 `Mem A` 的映射，而层序正是在后一形式上构造的。

```agda
memOf : (A : S) (m : ⟪ A ⟫) → ⟨ ⟪ A ⟫↪ m ∈ˢ A ⟩
memOf A m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)
```

函数 `carry` 沿这条映射，把宿主成员对上的序拉回到小呈现类型。这正是命名构造所需的方向：它的参数向量取自 `⟪ A ⟫`，而后文构造的层序自然作用于 `Mem A`。

```agda
carry : (A : S) → SWO (Mem A) → SWO ⟪ A ⟫
carry A w = pullOrder ⟪ A ⟫ (Mem A) w (λ m → ⟪ A ⟫↪ m , memOf A m) inj
  where
  inj : (u v : ⟪ A ⟫)
      → _≡_ {A = Mem A} (⟪ A ⟫↪ u , memOf A u) (⟪ A ⟫↪ v , memOf A v) → u ≡ v
```

呈现映射是嵌入，因此所得成员对相等会迫使其底层呈现元素相等，进而迫使原索引相等。这验证了 `pullOrder` 所需的单射性；它并未声称为每个成员选取了任意一种呈现。

```agda
  inj u v q = isEmbedding→Inj isEmb⟪ A ⟫↪ u v (cong fst q)
```

## 步进

对层指数 `δ`，`New δ` 是 `Lset (sucV δ)` 的全部成员所成的类型，每个成员都与其隶属证据配对。这个名字便于表述单步构造，但并不意味着每个这样的成员都恰好诞生于 `δ`；较早的成员也可能继续属于这个后继层。

```agda
New : S → Type (ℓ-suc ℓ)
New δ = Mem (Lset (sucV δ))
```

固定指数 `δ`，并固定 `Lset δ` 的小成员上的严格良序。此时命名构造可以比较这一层之上的名字，因为名字的参数部分恰按所给的序比较。这就给出用于每个指数处的统一局部构造。

```agda
module _ (δ : S) (w : SWO ⟪ Lset δ ⟫) where
  private
    module NM = Naming (Lset δ) w
```

若一个名字的语义值等于集合 `x`，就说该名字指称 `x`。层级集合的相等是命题，因此指称构成一个取值于 `hProp` 的族。这一命题值形式正是一般极小元构造所要求的。

```agda
  denotesAt : S → NM.Name → hProp (ℓ-suc ℓ)
  denotesAt x n = (NM.denote n ≡ x) , setIsSet (NM.denote n) x
```

对 `a : New δ`，被命名的只有底层集合 `a.fst`。它的隶属证据证明该集合位于后继层，却不是指称等式的一部分，因而不会影响哪个名字最小。

```agda
  private
    denotes : New δ → NM.Name → hProp (ℓ-suc ℓ)
    denotes a = denotesAt (a .fst)
```

借后继层等式，把 `Lset (sucV δ)` 中的隶属改写为 `Lset δ` 上可定义幂集中的隶属。随后名字完备性给出一个二元组的命题截断，其中包含名字及其指称 `a.fst` 的证据。此时仍没有选定任何名字。

```agda
    hasName : (a : New δ) → ∥ Σ[ n ∈ NM.Name ] ⟨ denotes a n ⟩ ∥₁
    hasName a = NM.names-complete (a .fst)
      (subst (λ v → ⟨ a .fst ∈ˢ v ⟩) (Lset-suc δ) (a .snd))
```

名字序是严格良序，因此仅仅非空的指称名字族有极小元。极小元构造在其下降过程中使用经典假设。消去命题截断是正当的，因为由名字及其最小性证明组成的总类型是命题：任意两个这样的名字都由三歧性得到相等。

```agda
    leastOfNew : (a : New δ)
               → Σ[ n ∈ NM.Name ] IsLeast NM.nameOrder (denotes a) n
    leastOfNew a = NM.leastName (denotes a) (hasName a)
```

定义 `theName a` 为这个最小见证中的名字分量。该构造在良序所赋予的精确意义下是典范的：完备性虽然没有展示任意代表，但最小代表却被唯一确定。

```agda
    theName : New δ → NM.Name
    theName a = leastOfNew a .fst
```

最小性包含「属于正在取极小元的族」这一条件。因此，所选名字确实指称 `a.fst`；只有极小性约束还不够，因为不属于指称名字族的名字可以位于外围名字序中的任意位置。

```agda
    theName-denote : (a : New δ) → NM.denote (theName a) ≡ a .fst
    theName-denote a = leastOfNew a .snd .fst
```

若两个后继层成员具有同一个选定的最小名字，对名字取指称便说明它们的底层集合相等。其隶属分量都是命题，所以该等式提升为成员对的相等。因此，选取最小名字定义了一个单射，尽管所有名字上的指称映射不必是单射。

```agda
    nameInj : (u v : New δ) → theName u ≡ theName v → u ≡ v
    nameInj u v q = Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV δ)))
      (sym (theName-denote u) ∙ cong NM.denote q ∙ theName-denote v)
```

沿这条单射拉回名字上的严格良序。于是，`Lset (sucV δ)` 的两个成员按各自选定的最小名字比较。后面的 `stepAt` 只使用这一种构造：每个 `δ` 都遵循同一条最小名字路线。

```agda
  byName : SWO (New δ)
  byName = pullOrder (New δ) NM.Name NM.nameOrder theName nameInj
```

`IsLeastName t x` 包含两项内容：`t` 指称 `x`，并且在名字序中，没有另一个指称 `x` 的名字严格位于 `t` 之下。把范围限制在指称 `x` 的名字上很重要；指称其他集合的名字与这条最小性断言无关。

```agda
  IsLeastName : NM.Name → S → Type (ℓ-suc ℓ)
  IsLeastName t x = IsLeast NM.nameOrder (denotesAt x) t
```

对每个成员 `a : New δ`，该构造给出一个名字，以及它对底层集合满足 `IsLeastName` 的证据。因此，后续证明可以直接使用最小名字推理，而无须展开搜索如何找到它，也无须把命题截断替换成任意选择。

```agda
  leastNameOf : (a : New δ) → Σ[ t ∈ NM.Name ] IsLeastName t (fst a)
  leastNameOf a = leastOfNew a
```

设 `t` 是满足 `IsLeastName t (fst c)` 的任意名字。`(theName c, leastOfNew c .snd)` 与 `(t,h)` 都是同一指称谓词的最小见证。这类最小见证的总类型是命题：三歧性排除任一名字严格小于另一个的两种情形，并迫使两个名字相等。投影该等式便得到 `theName c ≡ t`。因此唯一的是最小名字，而该集合仍可能有许多非最小名字。

```agda
  private
    pin : (c : New δ) (t : NM.Name) → IsLeastName t (fst c) → theName c ≡ t
    pin c t h = cong fst
      (isPropLeastOf NM.nameOrder (denotes c) (leastOfNew c) (t , h))
```

比较事实把每个候选的最小名字钉住：若 `t₁` 是 `a` 的最小名字、`t₂` 是 `b` 的最小名字，则拉回序所算出的关系与两条最小名字自身的序一致。原因在于每个被钉住的名字等于算出的最小值，拉回序沿这些等式搬运。

```agda
    byName-least : (a b : New δ) (t₁ t₂ : NM.Name)
                 → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                 → relOf byName a b ≡ NM._≺ₙ_ t₁ t₂
    byName-least a b t₁ t₂ h₁ h₂ = cong₂ NM._≺ₙ_ (pin a t₁ h₁) (pin b t₂ h₂)
```

对每个序数 `δ`，步进序都是同一个 `byName`：`Lset (sucV δ)` 的成员通过它们在 `Lset δ` 上唯一确定的最小名字来比较。这个构造不另设有穷层支或极限层支。

```agda
  opaque
    stepAt : SWO (New δ)
    stepAt = byName
```

接下来的两条桥接引理使我们能借任意已证为最小的代表来推理 `stepAt`。若 `t₁` 与 `t₂` 分别是两个成员的最小名字，则 `stepAt` 中的成员比较与 `t₁`、`t₂` 的名字比较可以相互推出。因此，后文只需使用所选名字的规格，而不依赖产生它们的具体搜索过程。

```agda
  opaque
    unfolding stepAt
```

填充读法说：若两个名字分别是各自成员的最小名字，则名字的序决定成员的序。证明把名字比较沿每个被钉住的名字与算出最小值之间的相合运输。

```agda
    stepAt-fill : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → NM._≺ₙ_ t₁ t₂ → relOf stepAt a b
    stepAt-fill a b t₁ t₂ h₁ h₂ =
      transport (sym (byName-least a b t₁ t₂ h₁ h₂))
```

读取引理说其反向：若步进序在两个成员间成立，则这些成员的最小名字也以同样方式排序。

```agda
    stepAt-read : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → relOf stepAt a b → NM._≺ₙ_ t₁ t₂
    stepAt-read a b t₁ t₂ h₁ h₂ =
      transport (byName-least a b t₁ t₂ h₁ h₂)
```

## 族

关系 `Under δ v x y` 记录底层集合 `x` 与 `y` 的比较，而不预先固定具体的隶属证明。它由两份把二者放入 `Lset (sucV δ)` 的证书，以及 `v` 对所得两个成员的比较组成。这是普通的 Sigma 类型，并非命题截断；只有其中的隶属证书因命题性而唯一。

```agda
Under : (δ : S) → SWO (New δ) → S → S → Type (ℓ-suc ℓ)
Under δ v x y = Σ[ hx ∈ ⟨ x ∈ˢ Lset (sucV δ) ⟩ ]
                Σ[ hy ∈ ⟨ y ∈ˢ Lset (sucV δ) ⟩ ]
                relOf v (x , hx) (y , hy)
```

给定任意选定的隶属证书 `hx` 与 `hy`，`under-at` 在这两个呈现上读出一条 `Under` 比较。`Under` 所携带的证书不必与 `hx`、`hy` 是同一证明项；它们的相等来自隶属的命题性。

```agda
under-at : (δ : S) (v : SWO (New δ)) (x y : S)
           (hx : ⟨ x ∈ˢ Lset (sucV δ) ⟩) (hy : ⟨ y ∈ˢ Lset (sucV δ) ⟩)
         → Under δ v x y → relOf v (x , hx) (y , hy)
under-at δ v x y hx hy (kx , ky , h) =
  subst2 (λ p q → relOf v (x , p) (y , q))
```

这种证书对齐正是 `Under` 能用于递归序族的原因。诞生序数相等时，同一集合往往由不同证明被放入同一个后继层；`under-at` 使局部比较在更换这些证据后仍可使用，而无须假定比较类型本身是命题。

```agda
    (snd (x ∈ˢ Lset (sucV δ)) kx hx) (snd (y ∈ˢ Lset (sucV δ)) ky hy) h
```

固定一个序数 `γ`。为了构造这一层的序，递归地假定每个 `δ ∈ γ` 都已在 `Mem (Lset δ)` 上带有严格良序。模块 `Family` 恰用这些较小层的序构造 `Lset γ` 诸成员上的序。

```agda
module Family (γ : S)
              (IH : (δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
              (ordγ : IsOrd γ) where
  private
    Member : Type (ℓ-suc ℓ)
```

这一层的载体是 `Member = Mem (Lset γ)`：一个层级中的集合，连同它属于 `Lset γ` 的证据。

```agda
    Member = Mem (Lset γ)
```

由于 `γ` 是序数，属于 `Lset γ` 蕴含可构造性。因此每个 `a : Member` 都有定义其诞生序数所需的可构造性证明。

```agda
    memberL : (a : Member) → ⟨ isL (a .fst) ⟩
    memberL a = Lset→isL γ ordγ (a .fst) (a .snd)
```

每个层成员属于其自身诞生序数的后继，由诞生构造的隶属读式而来。

```agda
    newIn : (a : Member) → ⟨ a .fst ∈ˢ Lset (sucV (birth (a .fst) (memberL a))) ⟩
    newIn a = birth-mem (a .fst) (memberL a)
```

成员的诞生被打包为序数索引 `γ` 的成员：诞生序数连同「它低于 `γ`」的证明，后者由成员属于 `γ` 处的层而来。

```agda
  bornAt : Member → Mem γ
  bornAt a = birth (a .fst) (memberL a)
           , birth-in γ ordγ (a .fst) (memberL a) (a .snd)
```

对 `d : Mem γ`，归纳假设给出 `Lset (d .fst)` 的带证书成员上的序。`carry` 把它搬到名字所用的小表示类型上，随后 `stepAt` 按最小名字良序化 `Lset (sucV (d .fst))` 的带证书成员。这就是比较诞生于 `d .fst` 之上的集合时所用的局部序。

```agda
  stepIn : (d : Mem γ) → SWO (New (d .fst))
  stepIn d = stepAt (d .fst) (carry (Lset (d .fst))
    (IH (d .fst) (d .snd) (mem-ord {A = γ} ordγ (d .fst) (d .snd))))
```

对打包的序数 `d : Mem γ`，`UnderAt d a b` 把不依赖具体证书的关系 `Under` 用于 `d` 处的局部步进序。在下文的同生支中，`d` 将是 `a` 与 `b` 的共同诞生序数。

```agda
  UnderAt : (d : Mem γ) → Member → Member → Type (ℓ-suc ℓ)
  UnderAt d a b = Under (d .fst) (stepIn d) (a .fst) (b .fst)
```

主关系是字典序。若 `a` 的诞生序数属于 `b` 的诞生序数，则 `a ≺ b`。两条诞生序数相等时，则在 `a` 的诞生序数处用局部步进序比较它们的底层集合。等式从 `b` 的诞生序数指向 `a` 的诞生序数，从而可把第二个集合直接放入同一个局部序。

```agda
  _≺_ : Member → Member → Type (ℓ-suc ℓ)
  a ≺ b = ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩
        ⊎ ((bornAt b .fst ≡ bornAt a .fst) × UnderAt (bornAt a) a b)
```

打包辅助说：底层序数相同的序数索引的两个成员相等，依据是序数中隶属的命题性。

```agda
  private
    packBirth : (d z : Mem γ) → d .fst ≡ z .fst → d ≡ z
    packBirth d z = Σ≡Prop (λ v → snd (v ∈ˢ γ))
```

主序的非自反性分别来自字典序两支的含义。若 `a ≺ a` 由早生见证给出，就会使序数 `birth(a)` 属于自身。若它由同生见证给出，则得到 `a` 与自身的局部比较；其中保存的隶属证书可能不同于 `newIn a`，但 `under-at` 会在后一组证书处读出同一比较，于是可以应用局部序的非自反性。

```agda
  private
    ≺-irr : (a : Member) → a ≺ a → Empty.⊥
    ≺-irr a (inl h) = ∈-irrefl (bornAt a .fst) h
    ≺-irr a (inr (_ , u)) =
      SWO.irr∙ (stepIn (bornAt a)) (a .fst , newIn a)
```

这里更换的只有隶属证书。证书的命题性认同 `a` 的两种呈现，而局部比较证明则原样搬运到严格良序禁止自比较的那种呈现上。

```agda
        (under-at (bornAt a .fst) (stepIn (bornAt a)) (a .fst) (a .fst)
          (newIn a) (newIn a) u)
```

传递性有四种情形。早早情形由诞生序数的传递性复合两条严格隶属；早等情形由等式把诞生隶属搬运过共同诞生序数。

```agda
    ≺-trans : (a b c : Member) → a ≺ b → b ≺ c → a ≺ c
    ≺-trans a b c (inl h) (inl k) =
      inl (birth-ord (c .fst) (memberL c) .fst h k)
    ≺-trans a b c (inl h) (inr (e , _)) =
      inl (subst (λ v → ⟨ bornAt a .fst ∈ˢ v ⟩) (sym e) h)
```

余下的混合情形沿诞生序数的等式搬运它们之间的严格不等关系。当两条比较都走同生支时，两条等式把诞生序数认作同一个，传递性便归结为在该处的局部步进序中复合两条比较。

```agda
    ≺-trans a b c (inr (e , _)) (inl k) =
      inl (subst (λ v → ⟨ v ∈ˢ bornAt c .fst ⟩) e k)
    ≺-trans a b c (inr (e , u)) (inr (eb , v)) = inr (eb ∙ e , joined)
      where
      d : Mem γ
```

在同生与同生的情形，取 `d = bornAt a` 为共同的打包诞生。第一条比较已经位于局部序 `stepIn d` 中。打包诞生的相等把第二条比较从以 `bornAt b` 为指标的局部序搬到同一个 `stepIn d`；这一步不可省略，因为局部序依赖其打包指标。

```agda
      d = bornAt a
      moved : UnderAt d b c
      moved = subst (λ z → UnderAt z b c) (packBirth (bornAt b) d e) v
      joined : UnderAt d a c
      joined = u .fst , (moved .snd .fst
```

此时两条前提都能在同一严格良序中读取。两份 `UnderAt` 见证所携带的证书在中间集合 `b` 处对齐，`stepIn d` 的传递性便把从 `a` 到 `b` 与从 `b` 到 `c` 的局部比较复合起来。

```agda
        , SWO.trans∙ (stepIn d) (a .fst , u .fst) (b .fst , moved .fst)
            (c .fst , moved .snd .fst)
            (under-at (d .fst) (stepIn d) (a .fst) (b .fst)
              (u .fst) (moved .fst) u)
            (under-at (d .fst) (stepIn d) (b .fst) (c .fst)
```

复合后的局部比较连同共同诞生处已有的两个端点证书，组成一份 `UnderAt d a c` 见证。因此同生支具有传递性，理由与其下的名字序相同：三个集合都在同一个固定局部序中比较。

```agda
              (moved .fst) (moved .snd .fst) moved))
```

为证明三歧性，先比较两条诞生序数。它们的序数性证明使序数三歧性可用，从而恰好得到「第一条诞生更早」「两条诞生相等」「第二条诞生更早」三种情形。只有中间情形需要诉诸局部步进序。

```agda
    ≺-tri : (a b : Member) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
    ≺-tri a b = byBirth (ord-tri (bornAt a .fst) (birth-ord (a .fst) (memberL a))
                                 (bornAt b .fst) (birth-ord (b .fst) (memberL b)))
      where
      byBirth : ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩
```

诞生序数不同时，它们之间的严格序数比较已经决定主序。这两种情形都不查看任一集合的名字；最小名字序只用于诞生序数相同的集合。

```agda
              ⊎ ((bornAt a .fst ≡ bornAt b .fst) ⊎ ⟨ bornAt b .fst ∈ˢ bornAt a .fst ⟩)
              → Tri (a ≺ b) (a ≡ b) (b ≺ a)
      byBirth (inl h)       = lt (inl h)
      byBirth (inr (inr h)) = gt (inl h)
      byBirth (inr (inl e)) =
```

等诞生情形中，共同诞生序数处的局部步进序决定比较。两个成员的证书被重新对齐到共同诞生序数。

第一条证书的对齐即该成员自身的后继隶属。

```agda
        bySteps (SWO.tri∙ (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
        where
        same : bornAt b .fst ≡ bornAt a .fst
        same = sym e
        ha : ⟨ a .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩
```

第一个集合本来就属于其诞生序数的后继层。诞生序数的相等把第二个集合的相应证书搬到同一个后继层，于是局部三歧可以在同一载体中比较两个成员。

```agda
        ha = newIn a
        hb : ⟨ b .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩
        hb = subst (λ v → ⟨ b .fst ∈ˢ Lset (sucV v) ⟩) (sym e) (newIn b)
        bySteps : Tri (relOf (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
                      ((a .fst , ha) ≡ (b .fst , hb))
```

局部三歧性给出两个带证书后继层成员的一个比较方向，或给出二者相等。相等情形立即推出底层集合相等；又因属于 `Lset γ` 是命题，这条等式提升为原层成员 `a` 与 `b` 的相等。

```agda
                      (relOf (stepIn (bornAt a)) (b .fst , hb) (a .fst , ha))
                → Tri (a ≺ b) (a ≡ b) (b ≺ a)
        bySteps (lt h) = lt (inr (same , (ha , hb , h)))
        bySteps (eq q) = eq (Σ≡Prop (λ v → snd (v ∈ˢ Lset γ)) (cong fst q))
        bySteps (gt h) = gt (inr (sym same
```

若局部三歧把 `b` 排在 `a` 之前，就反向使用共同诞生序数的等式，并相应搬运打包的诞生索引。这样便得到主三歧的右侧选项 `b ≺ a`。

```agda
          , subst (λ z → UnderAt z b a)
              (packBirth (bornAt a) (bornAt b) (sym same)) (hb , ha , h)))
```

良基性需要两种相互配合的下降。固定一条打包诞生序数 `d`。外层假设为诞生严格低于 `d` 的成员提供可及性，而 `stepIn d` 的可及树处理同在 `d` 处诞生的成员之间的内层下降。`accInside` 的作用，是在保留外层假设可用的同时，把这棵内层树提升为主字典序下的可及性。

```agda
  private
    accInside : (d : Mem γ)
              → ((z : Mem γ) → ⟨ z .fst ∈ˢ d .fst ⟩
                 → (b : Member) → bornAt b ≡ z → Acc _≺_ b)
              → (u : New (d .fst)) → Acc (relOf (stepIn d)) u
```

设局部元素 `u` 在 `stepIn d` 中可及，并且层成员 `b` 的诞生为 `d`，其底层集合与 `u` 相同。要证明 `b` 对主关系可及，就考察任意前驱 `c ≺ b`。主关系的定义会指出应当对 `c` 使用两种下降资源中的哪一种。

```agda
              → (b : Member) → bornAt b ≡ d → b .fst ≡ u .fst → Acc _≺_ b
    accInside d ih u (acc r) b q qu = acc step
      where
      step : (c : Member) → c ≺ b → Acc _≺_ c
      step c (inl h) = ih (bornAt c)
```

若 `c` 因诞生更早而排在 `b` 之前，则它的诞生严格低于 `d`，外层归纳假设由此证明 `c` 可及。若二者同生，则 `c` 是固定局部序中 `u` 的前驱，`u` 的可及树便给出相应的较小内层子树。这恰好对应字典序关系的两项子句。

```agda
        (subst (λ v → ⟨ bornAt c .fst ∈ˢ v ⟩) (cong fst q) h) c refl
      step c (inr (eb , v)) =
        accInside d ih (c .fst , hc) (r (c .fst , hc) below) c qc refl
        where
        qc : bornAt c ≡ d
```

在同生子句中，先把底层诞生序数的相等提升为它们作为 `γ` 成员的打包相等。于是可以把 `UnderAt` 比较搬到固定指标 `d`；其第一分量随即证明 `c` 属于 `stepIn d` 所定义在的后继层。

```agda
        qc = packBirth (bornAt c) d (sym eb ∙ cong fst q)
        moved : UnderAt d c b
        moved = subst (λ z → UnderAt z c b) qc v
        hc : ⟨ c .fst ∈ˢ Lset (sucV (d .fst)) ⟩
        hc = moved .fst
```

用对齐后的证书读取经搬运的 `UnderAt` 见证，便得到从 `c` 的局部代表到 `b` 的局部代表的比较。由 `b` 与 `u` 底层集合相等，可把右端点改为 `u`。所得局部前驱证明从 `u` 下方选出相应子树，递归再把这棵子树提升为 `c` 对主序的可及性。

```agda
        below : relOf (stepIn d) (c .fst , hc) u
        below = subst (λ z → relOf (stepIn d) (c .fst , hc) z)
          (Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV (d .fst)))) qu)
          (under-at (d .fst) (stepIn d) (c .fst) (b .fst)
            hc (moved .snd .fst) moved)
```

外层下降是对诞生序数作隶属归纳。其动机断言：每个打包诞生为 `(δ , i)` 的层成员都对主关系可及。因此在 `δ` 处的归纳步中，归纳假设恰好覆盖那些诞生序数严格属于 `δ` 的成员。

```agda
    accByBirth : (δ : S) (i : ⟨ δ ∈ˢ γ ⟩)
               → (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
    accByBirth = ∈-induction {P = Motive} outer
      where
      Motive : S → Type (ℓ-suc ℓ)
```

固定诞生序数 `δ` 后，局部严格良序已经保证 `b` 的相应代表可及。外层归纳步把这份局部可及性与所有更早诞生处的归纳假设一同交给 `accInside`。内层下降正是在外层隶属归纳的这一位置启动。

```agda
      Motive δ = (i : ⟨ δ ∈ˢ γ ⟩) (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
      outer : (δ : S) → ((z : S) → ⟨ z ∈ˢ δ ⟩ → Motive z) → Motive δ
      outer δ ih i b q = accInside (δ , i) inner (b .fst , hb)
        (SWO.wf∙ (stepIn (δ , i)) (b .fst , hb)) b q refl
        where
```

等式 `q` 把 `b` 的打包诞生认同为 `(δ , i)`，因而可以搬运 `birth-mem`，得到把 `b` 放入 `Lset (sucV δ)` 的证书 `hb`。对更小的打包诞生 `z`，其第一分量属于 `δ`；在该序数处的外层归纳假设，连同 `z` 属于 `γ` 的证明，为每个诞生于 `z` 的成员给出可及性。

```agda
        hb : ⟨ b .fst ∈ˢ Lset (sucV δ) ⟩
        hb = subst (λ z → ⟨ b .fst ∈ˢ Lset (sucV (z .fst)) ⟩) q (newIn b)
        inner : (z : Mem γ) → ⟨ z .fst ∈ˢ δ ⟩
              → (c : Member) → bornAt c ≡ z → Acc _≺_ c
        inner z h c qz = ih (z .fst) h (z .snd) c qz
```

因此每个成员都对主关系可及。这个结论同时使用两层论证：外层隶属归纳处理诞生更早的前驱，而在每个固定诞生序数处，局部步进序的可及树处理同生前驱。缺少其中任何一层，都不足以证明该字典序良基。

```agda
    ≺-wf : WellFounded _≺_
    ≺-wf a = accByBirth (bornAt a .fst) (bornAt a .snd) a refl
```

刚才建立的字典序关系及其证明现在组成 `Mem (Lset γ)` 上的严格良序：诞生序数给出第一层比较，最小名字的步进序处理诞生序数相等的情形。

```agda
  famOrder : SWO (Mem (Lset γ))
  famOrder = record
    { _<∙_   = _≺_
    ; tri∙   = ≺-tri
    ; irr∙   = ≺-irr
```

传递性与双层良基性论证补齐序定律，因此从所有较小序数层处的已知序即可得到 `famOrder`。

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

函数 `famStep` 封装这次递归步：在 `γ` 处，它接收每个成员序数 `δ ∈ γ` 上已经构造的序，返回上文证明的 `Mem (Lset γ)` 上的严格良序。同一个构造统一适用于每个序数，并无另设的零、后继或极限分支。

```agda
famStep : (γ : S) → ((δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
        → IsOrd γ → SWO (Mem (Lset γ))
famStep = Family.famOrder
```

隶属归纳在所有序数索引处同时施用 `famStep`。所得 `orderAt γ` 是宿主层中单个层 `Lset γ` 的带证书成员上的严格良序；它既不是对象语言中的关系，也不是整个 `L` 上的一条关系。

```agda
opaque
  orderAt : (γ : S) → IsOrd γ → SWO (Mem (Lset γ))
  orderAt = ∈-induction famStep
```

等式 `orderAt-step` 展开一层递归：`γ` 处的序就是把 `famStep γ` 施用于每个 `δ ∈ γ` 处先前构造的 `orderAt δ`。后文由此可以使用诞生优先的描述，而无须展开整个隶属递归。

```agda
opaque
  unfolding orderAt
  orderAt-step : (γ : S) → orderAt γ ≡ famStep γ (λ δ _ → orderAt δ)
  orderAt-step = ∈-induction-compute famStep
```

最后，`stageOrder γ` 把同一条逐层序呈现在小索引类型 `⟪ Lset γ ⟫` 上。典范嵌入把每个索引送到它所表示的成员及其隶属证书，`carry` 再沿这条单射拉回 `orderAt γ`。这里改变的只是载体的表示，并未另造一种比较。

```agda
stageOrder : (γ : S) → IsOrd γ → SWO ⟪ Lset γ ⟫
stageOrder γ oγ = carry (Lset γ) (orderAt γ oγ)
```

## 小结

对每个序数 `γ`，`orderAt γ` 是宿主层中 `Lset γ` 的带证书成员上的严格良序。它先比较各成员最早包含层的前驱；只有诞生序数相等时，才比较它们在共同前层之上唯一确定的最小名字。局部构造 `stepAt` 在每个指标处都只有这一种最小名字形式，而全局良基性证明把诞生序数的下降与局部名字序中的下降结合起来。此处尚未把该关系写成对象语言公式，也未把它构造成 `L` 中的集合；这些内部化步骤留给后续章节。