One order for every stage

前几章备齐了三样东西，还缺一样。阶段那一章为每一格定位了它首次拥有成员的那个阶段，并证明那是一个后继；有穷那一章把 ω 以下的每个阶段连同极限阶段本身都良序化了；命名那一章把后继阶段的每个成员写成名字，并把诸名字良序化，前提是下面那个阶段已有良序。所缺的正是这个前提。下面那个阶段未被排序之前，名字排不了这个阶段的序，故要造的不是一个序，而是一族：每个阶段一个序，而每一个都是下一个的配料。

这一族沿序数的成员归纳造出，而全章的关键是一个决定：先比较什么。阶段的一个成员是在一个确定的时刻进入塔的：存在包含它的最早阶段，那个阶段是后继，而它所后继的那个序数，就是该集合被雕出时所依据的那一个。那个序数就是主键。 雕出时刻不同的两个集合，仅凭那两个时刻比较，别无其他；只有雕出时刻相同的两个集合，才由那个时刻的机器来比较，而那机器就是上一章的名字，或者，在极限阶段以下，是有穷那一章按最先分歧处的比较。

以阶段为主键，换来的正是本部余下部分所需的那条性质。大阶段上的序，限制到较小的阶段上，必须就是那里的序，否则在一个阶段作出的选取会在下一个阶段被推翻。而此处这不是关于该构造的一条定理，而是定义的一种读法：两个集合的比较从不提到它是在哪个阶段处被读的。它提到的是那两个集合各自的诞生阶段，而那是不动的。

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

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

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

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; isPropIsOrd; isL; Lset; Lset-out; Lset-mono; Lset→isL; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
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.Stage {ℓ} lem using ( IsPredOf; isPropPredOf )
open import L.Choice.Finite {ℓ} lem using ( Tri-map )
open import L.Choice.Name {ℓ} lem using ( module Naming )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; isPropLeastOf )

open import Cubical.Foundations.Prelude using ( J; PathP; 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 )
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
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

一个集合被雕出的阶段

阶段那一章为每个可构造集给出了它的最早阶段，而选取阶段那一章为一格证明了与它相交的最早阶段是后继。同一论证逐字适用于单个集合，理由也相同：集合进入塔的唯一途径是从下面那个阶段中被雕出，故它若到最早阶段为止已在那里，那个阶段就有前一阶段，而该集合是其上的可定义子集之一。

论证中唯一的分情形是乔装的比较，它写成写明结论的具名辅助件：候选者的后继或严格落在最早阶段之下，这被极小性反驳；或就是那个阶段。

private
  decideSuc : (x : S) (p : ⟨ isL x ⟩) (δ : S) → IsOrd δ
            → ⟨ x ∈ˢ Lset (sucV δ) ⟩
            → ⟨ sucV δ ∈ˢ stage x p ⟩ ⊎ (sucV δ ≡ stage x p)
            → sucV δ ≡ stage x p
  decideSuc x p δ ordδ m (inl s∈) =
    Empty.rec (stage-earliest x p (sucV δ) (suc-ord ordδ) m s∈)
  decideSuc x p δ ordδ m (inr e) = e

  atCarve : (x : S) (p : ⟨ isL x ⟩)
          → Σ[ δ ∈ S ] (⟨ δ ∈ˢ stage x p ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
  atCarve x p (δ , (δ∈ , x∈)) = δ , (ordδ , suc≡)
    where
    ordδ : IsOrd δ
    ordδ = mem-ord {A = stage x p} (stage-ord x p) δ δ∈
    atSuc : ⟨ x ∈ˢ Lset (sucV δ) ⟩
    atSuc = subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-suc δ)) x∈
    suc≡ : sucV δ ≡ stage x p
    suc≡ = decideSuc x p δ ordδ atSuc
      (suc∈or≡ δ (stage x p) ordδ (stage-ord x p) δ∈)

theCarve : (x : S) (p : ⟨ isL x ⟩) → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
theCarve x p = PT.rec (isPropPredOf (stage x p)) (atCarve x p)
  (Lset-out (stage x p) x (stage-mem x p))

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

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

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

如此取出的那个序数，就是该集合的诞生阶段：x 据以被雕出的那个阶段，比包含它的最早阶段低一级。它按 stage 与 defStage 当初那样封印，理由相同：它展开是一次穿过那座塔的良基下降，而此后每个提到它的类型都会把那次下降拖进转换检查。

有两条读式开封，别无其他：诞生阶段是序数；它的后继是最早阶段。本章所用的一切都由这两条推出，不再开封任何东西。该集合是它诞生阶段之上一级那个阶段的成员，而命名那一章正是在那里找它。诞生阶段不依赖于所供给的是哪一份可构造性证明，因为可构造性是命题，而正是这一行使本章末尾的末端扩张得以成立。以及，一个阶段的成员诞生于严格更低处：它的最早阶段或低于该阶段、或与之相等，而它的诞生阶段低于它的最早阶段，故序数三歧了结这三种情形，同样写在一个写明结论的具名辅助件里。

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)

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

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 γ∈)
  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∈

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

沿一个单射搬运良序

本章有三处，是某个类型上的良序已知，而想要的是另一个单射进它的类型上的良序。序就是对像的比较。三歧取源头的三歧，由单射性把它中间那一情形变回相等；非自反与传递直接读出；良基性则向下传递，因为一串像的下降就是一次下降。

整个搬运四行，写一遍，取的是它三处用法共有的形状。它不是一套「诱导序」的理论，尤其此处没有任何东西是对「以第一个键为索引的一族序」泛型的：那样一件东西得携带那一族并在那种一般性下证出它的诸定律，而这比本章所要的任何定理都大。

有两样缩写随这次搬运同行。Mem A 是一个集合的诸成员，取「集合连同它的隶属」之对的形式，而以下一切都陈述在这个形状上；relOf 则把一个束的比较当作函数读出来，于是一个序可以作为值传递，而不必被打开。

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

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

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

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ᶜ )

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

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

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

  pullOrder : SWO B
  pullOrder = record
    { _<∙_   = _<ᵇ_
    ; tri∙   = pullTri
    ; irr∙   = λ u h → irrᶜ (f u) h
    ; trans∙ = λ u v z → transᶜ (f u) (f v) (f z)
    ; wf∙    = λ u → pullAcc u (wfᶜ (f u)) }

第一处用法是一个集合的典范表示。集合的成员有两种形状：一种是「集合连同它属于该集合的证明」之对，这是下面的构造所产出的形状；另一种是层级用来表示该集合的那个小索引类型，这是命名那一章所取用的形状。索引映射是嵌入，故把一个序从第一种形状搬到第二种，就是那次搬运的一次施用，此处做一遍，不再重做。

第二处用法是包含。当一个集合的每个成员都是另一个集合的成员时，第二个集合上的序限制到第一个上，而那个单射在底下的集合上是恒等的。

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

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
  inj u v q = isEmbedding→Inj isEmb⟪ A ⟫↪ u v (cong fst q)

步进

步进是本章的第一件交付物：由 Lset δ 诸成员上的一个良序，得出 Lset (sucV δ) 诸成员上的一个良序 (下文记作 New δ)，也就是 Lset δ 的诸可定义子集上的良序。

它只有一支，而当初写成了两支。极限阶段以下诸成员本已有序，即有穷那一章为 Lset ω 造的良序，而那也正是一个名字的第一个键据以比较的序；故初稿在那里取那个序，只在极限阶段之上才动用名字。实测下来，第二支是多余的：处处取名字，同样三秒检查完毕。那个守卫真正贡献的并不是一次情形区分，而是一道归一化屏障：排中律尚是模块参数时，据它作出的判定是卡住的，而正是「卡住」阻止了这个序展开成命名那一章的序。opaque 封印就是那道屏障，一个词说完，这也是下面那条定义只有一行的原因。

初稿给出的理由，即本书不该为同一个集合携带两个互不相干的良序，是一条相干性主张，而本章从未证明它。留住代码所需的正当理由，要强过一个无人交付的论证，故那一支已删，那条主张随之。基础情形也无须任何东西：第一个阶段是空的，其诸成员因无可比较而良序。

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

另一支按最小名字比较。Lset (sucV δ) 的每个成员都被某个名字指称，且是截断的，因为可定义幂集本来就是这样交出公式的；而只要下面那个阶段带有良序，诸名字就带有良序，那恰是本步进的假设；于是指称一个集合的最小名字是一个确定的名字，每个集合被送到它那里。那个映射是单射，因为名字决定它所指称的东西，而步进的序就是名字的序沿它拉回。

此处没有任何关于名字的东西被拆开。命名数据留在绑定它们的那条模块序列所在的章内，而本章看到的是一个带序的类型。这不是讲究：上一章量过「命名数据从另一个模块够取」会发生什么，答案是每一次码的比较都会把极限序逼开。

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

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

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

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

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

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

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

    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)

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

有三个定义离开本模块，而它们是「要说清这个序是什么，调用方最少须被给予的东西」。denotesAt 是那场搜寻所针对的那一族，即一个集合的诸名字；IsLeastName 是「是某个集合的一个最小名字」，而它就是良序那一章的 IsLeast 架在那一族上，不是它的另一种写法；leastNameOf 为新阶段的每个成员当场拿出一个，而它就是那场搜寻本身，原样交回。

IsLeastName 是一个定义、而不是一次重写，这是量出来的。若写成「一条指称等式加一条极小性子句」之对，那场搜寻就得在一个算出来的名字处被转换成它，而在算出来的名字处比较名字，会把码之序展开到它据以定义的那场层号搜寻：仅那一行 16 秒，而当那条性质就是那一族自家的 IsLeast 时，分文不花。命名数据仍然留在里面；跨过边界的是一个调用方早已持有的名字。

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

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

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

    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₂)

两支由排中律接起来，写在一个写明结论、而非留待推断的具名辅助件里。这是本章唯一一处自己花掉那条假设之处；其余各处它到场时都已被花掉，花在序数的三歧里、最早阶段里，以及寻找最小名字的搜索里。

  opaque
    stepAt : SWO (New δ)
    stepAt = byName

那道封印是一道归一化屏障、不是一个秘密，故有两条读式被放行，一个方向一条：那一步关联两个成员，当且仅当名字之序关联「调用方已证为最小的任意两个名字」。它们就是上面那条等式，搬运过来。

它们证在此处，即绑定阶段与其序的那条模块序列之内，而这个位置同样是量出来的。若陈述在顶层、再拿上面那条引理去填，任一条读式要花 39 秒，而这正是第 20 条定律在新地方的形状：一条把类型写下来、又用同一条陈述去填的陈述，会逼出一次这条路线付不起的转换。在里面，在封印所在之处，两条都分文不花。

  opaque
    unfolding stepAt

    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₂))

    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-at 则在任选的一对证明处把那条比较读回来，而这就是那次量化所花的全部记账。

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)

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))
    (snd (x ∈ˢ Lset (sucV δ)) kx hx) (snd (y ∈ˢ Lset (sucV δ)) ky hy) h

归纳的这一步，收下 γ 以下每个序数处的序，产出 γ 处的一个。Lset γ 的每个成员都可构造，因为 γ 是序数，故它有诞生阶段；而那个诞生阶段是 γ 的成员。把诞生阶段与那条隶属打成包，得到的恰是归纳假设可以施用其上的那个数据，而 stepIn 就是那里的步进序。

于是比较是两个键的：先诞生阶段，若诞生阶段相符，则用共同诞生阶段处的步进序。诞生阶段的等式所携带的方向，使第二个集合可以在第一个的诞生阶段处读出，这让定义中不出现搬运；而它携带的是序数之间的等式、不是打包之对之间的等式，正是这一点使下文的末端扩张成为一条路径、而非一段论证。打包的形式在诸搬运需要它的地方现取，因为那条隶属是命题。

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

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

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

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

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

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

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

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

非自反是两个键各自的：没有序数属于自身，也没有哪个步进序把一个集合排在它自己之下。传递是四种情形，其中两种混合情形把一条诞生阶段的等式带过一条隶属，最后一种在把第二条比较挪到同一个诞生阶段之后，把两条比较复合起来。

三歧沿诸键下行，每一个唯有在前一个宣布相等时才被抵达：先序数，后步进序。两次分情形都是写明结论的具名辅助件。这是前两章付过学费、本章继承下来的纪律：分支结论落在隶属命题上的分情形，若交给 with 或交给推断，就会对着整个析取、而不是对着它自己那一支求解。

  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)
        (under-at (bornAt a .fst) (stepIn (bornAt a)) (a .fst) (a .fst)
          (newIn a) (newIn a) u)

    ≺-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)
    ≺-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
      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
        , 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)
              (moved .fst) (moved .snd .fst) moved))

    ≺-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 ⟩
              ⊎ ((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)) =
        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)) ⟩
        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))
                      (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
          , subst (λ z → UnderAt z b a)
              (packBirth (bornAt a) (bornAt b) (sym same)) (hb , ha , h)))

良基性是两层嵌套的归纳，其分开的方式与有穷那一章把它自己那两层分开的方式完全相同。外层是对诞生阶段的成员归纳，它交下一个覆盖所有更早诞生阶段的假设；内层则是沿步进序在那个诞生阶段处本已具备的可及性作普通下降。降一个诞生阶段的一步诉诸外层假设，诞生阶段之内的一步诉诸内层假设，而由于内层函数除自己的可及性实参外不沿任何东西递归，二者从不需要放在一起比较。

成员总是以成员的身份到场，外加一条说明它的诞生阶段坐在哪里的等式。这与三歧那一条是同一条规矩，此番从另一侧再度出现：陈述在一个成员的诸分量上的可及性，将不得不与陈述在那个成员上的可及性对上。

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

    accByBirth : (δ : S) (i : ⟨ δ ∈ˢ γ ⟩)
               → (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
    accByBirth = ∈-induction {P = Motive} outer
      where
      Motive : S → Type (ℓ-suc ℓ)
      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
        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

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

  famOrder : SWO (Mem (Lset γ))
  famOrder = record
    { _<∙_   = _≺_
    ; tri∙   = ≺-tri
    ; irr∙   = ≺-irr
    ; trans∙ = ≺-trans
    ; wf∙    = ≺-wf }

这一族就是那一步沿成员归纳跑出来的东西，而它被封印。不封印的话，一个阶段处的序会展开成一场遍历整座层级的递归，而每个提到某个这样的序的类型都会把那次展开带进转换检查；orderAt-step 开封一次，且只为那条递归方程，而下文的末端扩张是它唯一的消费方。stageOrder 是同一个序，取在命名那一章所用的那种表示上，而它正是后续论证将要递给 leastName 的东西。

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

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

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

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

末端扩张

两个阶段，其一是另一个的成员，还有一个同为两者成员的集合：那两个序必须在它上面相符。它们确实相符，而理由就是整套设计。一次比较提到的是那两个诞生阶段以及那两处的步进序，从不提到它是在哪个阶段处被读的。于是要查的有两件，而两件都是关于命题的事实。一个集合的诞生阶段，不依赖于它是被当作哪个阶段的成员来读的，因为可构造性是命题。而诞生阶段处的步进序也不依赖：它由下面那一族造出，施用于一份「该诞生阶段是序数」的证明，而任何两份这样的证明都相等。

其中第二件是本章唯一的一次路径归纳，而它的全部内容就是上一句话，沿两个诞生阶段的等式搬运过去。

private
  stepPath : (δ : S) (o : IsOrd δ) (δ' : S) (e : δ ≡ δ') (o' : IsOrd δ')
           → PathP (λ k → SWO (New (e k)))
               (stepAt δ (carry (Lset δ) (orderAt δ o)))
               (stepAt δ' (carry (Lset δ') (orderAt δ' o')))
  stepPath δ o δ' e o' = J Motive base e o'
    where
    Motive : (z : S) → δ ≡ z → Type (ℓ-suc (ℓ-suc ℓ))
    Motive z ez = (oz : IsOrd z) → PathP (λ k → SWO (New (ez k)))
      (stepAt δ (carry (Lset δ) (orderAt δ o)))
      (stepAt z (carry (Lset z) (orderAt z oz)))
    base : Motive δ refl
    base oz =
      cong (λ q → stepAt δ (carry (Lset δ) (orderAt δ q))) (isPropIsOrd δ o oz)

有了它，相符就是一行。比较是两个分量的和，而每个分量都逐点地是一条沿诞生阶段等式的路径，故那两次比较不只是等价，而是相等；末端扩张的每一种读法，包括蕴含的任一方向，皆由搬运随之而来。较大阶段处的序限制到较小者上，就是那里的序。

这正是路线审计所预测的，而测量也证实了：一条十来行的路径归纳引理、一行相符，外加两行在两端解封那条递归方程。本章余下之处未为它花过一分。这个理由值得再说一遍，因为它正是主键当初如此选取的理由：那次比较的定义本就与阶段无关，故末端扩张除了「它确实提到的那两个命题的证明无关性」之外，无事可证。

module _ (γ β : S) (oγ : IsOrd γ) (oβ : IsOrd β) (i : ⟨ γ ∈ˢ β ⟩) where
  private
    module Fγ = Family γ (λ δ _ → orderAt δ) oγ
    module Fβ = Family β (λ δ _ → orderAt δ) oβ
    open Fγ using () renaming ( _≺_ to _≺ᵍ_ ; bornAt to bornγ )
    open Fβ using () renaming ( _≺_ to _≺ᵇ_ ; bornAt to bornβ )

    up : Mem (Lset γ) → Mem (Lset β)
    up a = a .fst , Lset-mono {α = β} {β = γ} i {x = a .fst} (a .snd)

    sameBirth : (a : Mem (Lset γ)) → bornγ a .fst ≡ bornβ (up a) .fst
    sameBirth a = birth-proof (a .fst) _ _

    sameStep : (a : Mem (Lset γ))
             → PathP (λ k → SWO (New (sameBirth a k)))
                 (Fγ.stepIn (bornγ a)) (Fβ.stepIn (bornβ (up a)))
    sameStep a = stepPath (bornγ a .fst) _ (bornβ (up a) .fst) (sameBirth a) _

    agree : (a b : Mem (Lset γ)) → (a ≺ᵍ b) ≡ (up a ≺ᵇ up b)
    agree a b k = ⟨ sameBirth a k ∈ˢ sameBirth b k ⟩
                ⊎ ( (sameBirth b k ≡ sameBirth a k)
                  × Under (sameBirth a k) (sameStep a k) (a .fst) (b .fst) )

    unfoldγ : (a b : Mem (Lset γ)) → relOf (orderAt γ oγ) a b ≡ (a ≺ᵍ b)
    unfoldγ a b = cong (λ z → relOf (z oγ) a b) (orderAt-step γ)

    unfoldβ : (a b : Mem (Lset β)) → relOf (orderAt β oβ) a b ≡ (a ≺ᵇ b)
    unfoldβ a b = cong (λ z → relOf (z oβ) a b) (orderAt-step β)

  endExtension : (a b : Mem (Lset γ))
               → relOf (orderAt γ oγ) a b ≡ relOf (orderAt β oβ) (up a) (up b)
  endExtension a b = unfoldγ a b ∙ agree a b ∙ sym (unfoldβ (up a) (up b))

小结

birth 是一个可构造集据以被雕出的那个序数，比包含它的最早阶段低一级；它之所以存在，是因为集合进入塔的唯一途径就是被雕出 (theCarve)。birth-in 把它安置在该集合所属的任何阶段之下且严格更低，而 birth-proof 说它不依赖于所供给的那份可构造性证明。

stepAt 就是步进：由 Lset δ 上的一个良序造出 Lset (sucV δ) 上的一个，在每一个阶段处都是上一章的名字序沿最小名字拉回，而最小名字之所以是函数，是因为只要下面那个阶段已被良序化，诸名字就已被良序化。它当初写着「极限阶段以下另有一支」，而那一支被实测为多余并删去；正文说了为什么。pullOrder 沿一个单射搬运良序，是本章写下的唯一一次搬运；步进用它，carry 也用它，后者把一个阶段的诸成员呈现为命名那一章所取的索引类型。

有三个定义为外面的调用方说清那个拉回的序是什么：denotesAt 是一个集合的诸名字，IsLeastName 是良序那一章的 IsLeast 架在那一族上，而 leastNameOf 就是那场搜寻。随后 stepAt-fill 与 stepAt-read 两个方向地把那一步对着名字之序读出来，读在「调用方已证为最小的任意两个名字」处。这五行背后有两次实测：那条性质必须是那一族自家的 IsLeast、绝不可另写一遍 (16 秒对分文不花，因为在算出来的名字处的一次比较会把码之序打开)，而两条读式都必须证在封印所在的那条模块序列之内、绝不可在顶层重述 (各 39 秒对分文不花，这是第 20 条定律在新地方)。

orderAt 就是那一族：在每个序数处，该阶段诸成员上的一个严格良序，四条定律齐备，由下面诸序沿成员归纳造出。它的比较以诞生阶段为主键，以共同诞生阶段处的步进序为次键；endExtension 就是这一点换来的东西，而它是一条路径、不是一个蕴含：两个成员的比较从不提到它是在哪个阶段处被读的，故大阶段处的序限制到小阶段上，分毫不差地就是那里的序。

现在到手的，恰是上一章所缺的那个前提，且一举在每个阶段处到手。后续论证取选取阶段那一章单挑出来的那一个阶段，把 stageOrder 递给写在其上的诸名字，再挑出最小的名字。