The stage where a set first has a member

最后一笔债索取的，是一个与不交族的每一格恰交于一点的集合。教科书的偿付方式是把宇宙良序化，再取每一格中最小的成员，而这条路在此处代价高昂：L 整体的良序是一个真类上的关系，而迄今造出的东西没有一样谈得到它。

有一条更廉价的路，它从「一格的诸成员在哪里」问起。一格是 L 的一个集合，故它的每个成员都现身于塔中某处；于是存在一个最早的阶段，其中已经现身了它的某个成员。那个阶段既不能是极限，也不能是零：集合进入塔的唯一途径是从它下面那个阶段中被雕出，故与该格相交的最早阶段，是某个与它不相交的阶段的后继。于是这一格自带一个典范的序数，即它首次现身之前的那个阶段；而在那个序数处，该格中最先现身的每个成员，都是同一个集合的可定义子集。

这就是取代良序的东西。为一格选取成员，从此成为写在单一阶段之上的诸名字之间的比较，而绝非 L 的任意元素之间的比较；记账的序数就是阶段，故现身时刻不同的集合根本不会被拿来比较。本章造出那个序数，并证明本部余下部分所系的两件事：它存在且唯一；以及单一序数足以装下一个集合、它的成员与它们的成员，连同塔的极限层。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; isL-trans; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; LeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )

import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

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

与一个集合相交的最小阶段

「到阶段 σ 为止，u 的某个成员已经现身」是一条关于序数的性质，仅此而已，故最小序数算子对它零成本地适用：当初把那个算子写成对性质泛型的，正是为了让这样的实例只花一行。

算子要一份截断的见证，说某个序数合用，而一个非空的格恰好供得出。该格的成员可构造，因为 L 是传递类而该格是它的一个集合；而可构造按定义就是「存在一个包含它的阶段」。于是见证就是那个成员自己的阶段，从类上直接读出。

meets : S → S → Ω
meets u σ = ⋁ S (λ z → (z ∈ˢ u) ⊓ (z ∈ˢ Lset σ))

Inhabited : S → Type (ℓ-suc ℓ)
Inhabited u = ∥ Σ[ z ∈ S ] ⟨ z ∈ˢ u ⟩ ∥₁

meetsSome : (u : S) → ⟨ isL u ⟩ → Inhabited u
          → ∥ Σ[ σ ∈ S ] (IsOrd σ × ⟨ meets u σ ⟩) ∥₁
meetsSome u pu = PT.rec squash₁ atMember
  where
  atMember : Σ[ z ∈ S ] ⟨ z ∈ˢ u ⟩
           → ∥ Σ[ σ ∈ S ] (IsOrd σ × ⟨ meets u σ ⟩) ∥₁
  atMember (z , z∈u) = PT.map
    (λ { (α , (ordα , z∈Lα)) → α , (ordα , ∣ z , (z∈u , z∈Lα) ∣₁) })
    (isL-trans {x = u} {y = z} z∈u pu)

最小的这样的序数是 μ u，它按阶段函数当初那样封印，理由完全相同：它展开是一次良基下降，其步进提到那座塔，而此后每个提到它的类型都会把那次展开拖进转换检查。三个投影各开封一次，而它们就是全部接口。

theEarliestMeet : (u : S) → ⟨ isL u ⟩ → Inhabited u → LeastOrd (meets u)
theEarliestMeet u pu h = leastOrd (meets u) (meetsSome u pu h)

opaque
  μ : (u : S) → ⟨ isL u ⟩ → Inhabited u → S
  μ u pu h = theEarliestMeet u pu h .fst

opaque
  unfolding μ
  μ-ord : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u) → IsOrd (μ u pu h)
  μ-ord u pu h = theEarliestMeet u pu h .snd .fst

  μ-meets : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u) → ⟨ meets u (μ u pu h) ⟩
  μ-meets u pu h = theEarliestMeet u pu h .snd .snd .fst

  μ-earliest : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
             → isLeastOrd (meets u) (μ u pu h)
  μ-earliest u pu h = theEarliestMeet u pu h .snd .snd .snd

首次现身处是后继

取该格中一个到最小阶段为止已现身的成员。属于一个阶段，就是属于某个更早阶段的可定义子集，而后继恒等式说那些可定义子集就是下一个阶段；故那个成员在那个更早阶段之上一级就已现身，该格在那里就已被相交。极小性禁止那个阶段严格低于最小阶段，而成员的后继又不会越过头：它或属于最小阶段，或就是最小阶段。前一种情形正是极小性刚刚反驳的，故后一种成立，于是最小阶段是后继。

被反驳的那一支写成写明结论的具名辅助件。这是阶段那一章为每个出自三歧的分情形定下的纪律，而此处的分情形正是其一：suc∈or≡ 是乔装的比较。

IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)

private
  below-case : (u σ δ : S) → isLeastOrd (meets u) σ → IsOrd δ
             → ⟨ meets u (sucV δ) ⟩ → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
  below-case u σ δ least ordδ m s∈σ =
    Empty.rec (least (sucV δ) (suc-ord ordδ) m s∈σ)

  same-case : (u σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
  same-case u σ δ e = e

meet-suc : (u σ : S) → IsOrd σ → ⟨ meets u σ ⟩ → isLeastOrd (meets u) σ
         → ∥ Σ[ δ ∈ S ] IsPredOf σ δ ∥₁
meet-suc u σ ordσ m least = PT.rec squash₁ atMember m
  where
  atCarve : (z : S) → ⟨ z ∈ˢ u ⟩
          → Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ z ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → Σ[ δ ∈ S ] IsPredOf σ δ
  atCarve z z∈u (δ , (δ∈σ , z∈𝒟ₒδ)) = δ , (ordδ , suc≡σ)
    where
    ordδ : IsOrd δ
    ordδ = mem-ord {A = σ} ordσ δ δ∈σ
    metAtSuc : ⟨ meets u (sucV δ) ⟩
    metAtSuc = ∣ z , (z∈u
      , subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟ₒδ) ∣₁
    suc≡σ : sucV δ ≡ σ
    suc≡σ = Sum.rec (below-case u σ δ least ordδ metAtSuc) (same-case u σ δ)
      (suc∈or≡ δ σ ordδ ordσ δ∈σ)

  atMember : Σ[ z ∈ S ] (⟨ z ∈ˢ u ⟩ × ⟨ z ∈ˢ Lset σ ⟩)
           → ∥ Σ[ δ ∈ S ] IsPredOf σ δ ∥₁
  atMember (z , (z∈u , z∈Lσ)) = PT.map (atCarve z z∈u) (Lset-out σ z z∈Lσ)

首次现身所依据的那个阶段

后继决定它所后继的东西，至少在序数之内如此。把一个候选前一阶段与另一个相比：各自属于对方的后继，故各自或是对方的成员、或与对方相等；而两个序数不能互为成员，否则传递性会使其一属于自身。于是「是给定序数的前一阶段」是命题，而最小阶段的前一阶段可以从上一节造出的那个仅仅存在者中取出。

正是这次取出使 defStage 成为函数：一格的定义阶段，即该格最先现身的诸成员所依据写出的那个阶段。它连同两条性质一并封印，与 μ 当初一样。

private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → Empty.⊥
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)

  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → Empty.rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)

ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')
  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')

isPropPredOf : (σ : S) → isProp (Σ[ δ ∈ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))

thePred : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
        → Σ[ δ ∈ S ] IsPredOf (μ u pu h) δ
thePred u pu h = PT.rec (isPropPredOf (μ u pu h)) (λ d → d)
  (meet-suc u (μ u pu h) (μ-ord u pu h) (μ-meets u pu h) (μ-earliest u pu h))

opaque
  defStage : (u : S) → ⟨ isL u ⟩ → Inhabited u → S
  defStage u pu h = thePred u pu h .fst

opaque
  unfolding defStage
  defStage-ord : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
               → IsOrd (defStage u pu h)
  defStage-ord u pu h = thePred u pu h .snd .fst

  defStage-suc : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
               → sucV (defStage u pu h) ≡ μ u pu h
  defStage-suc u pu h = thePred u pu h .snd .snd

那条等式的两种读法，也正是后续构造所用的两种。该格首次被相交的那个阶段，是定义阶段的可定义幂集，故该格的一个最先成员就是那里的一个可定义子集，从而有名字。而定义阶段则干脆与该格不相交，因为它属于那个相交的最小阶段。

Lset-μ : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
       → Lset (μ u pu h) ≡ 𝒟ₒ (Lset (defStage u pu h))
Lset-μ u pu h =
  cong Lset (sym (defStage-suc u pu h)) ∙ Lset-suc (defStage u pu h)

defStage-misses : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
                → ⟨ meets u (defStage u pu h) ⟩ → Empty.⊥
defStage-misses u pu h m = μ-earliest u pu h (defStage u pu h)
  (defStage-ord u pu h) m
  (subst (λ w → ⟨ defStage u pu h ∈ˢ w ⟩) (defStage-suc u pu h)
    (self∈sucV (defStage u pu h)))

一个阶段装下一个集合以下的一切

构造还需要另一样东西：一个上界，而取得它不牵涉任何比较。阶段传递，故一个集合的阶段已经装着该集合的诸成员，以及其后它们的诸成员；最早的阶段与别的阶段无异，故它就够用。

还有一个序数要清出来，即塔的极限层。后续构造比较的是名字，而一个名字由数码与对造成、别无他物，故它到 Lset ω 为止已经现身；于是记账的那个阶段必须既在该集合自身的阶段之上，也在 ω 之上。两个序数的界层序数一行解决，而单调性把两层一并抬进它的阶段。

stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)

stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)

stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∈ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)

bound-limit : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ Lset ω ⟩
            → ⟨ x ∈ˢ Lset (stageBound a p .fst) ⟩
bound-limit a p x x∈ = Lset-mono (stageBound a p .snd .snd .fst) x∈

bound-self : (a : S) (p : ⟨ isL a ⟩) → ⟨ a ∈ˢ Lset (stageBound a p .fst) ⟩
bound-self a p = Lset-mono (stageBound a p .snd .snd .snd) (stage-mem a p)

bound-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below a p x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below a p x x∈a)

bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)

小结

μ 是 L 的一个集合拥有成员的最早阶段，而 meet-suc 说那个阶段是后继，因为集合进入塔的唯一途径是从它下面那个阶段中被雕出。defStage 是它所后继的那个阶段，之所以是函数，是因为在序数之内后继决定它所后继的东西 (ord-suc-inj)；而 Lset-μ 把首次现身的那个阶段与其上的可定义幂集认同。于是每个首次现身于该处的集合，都带着一个写在单一固定阶段之上的名字，而那正是选取装置将要比较的东西。stageBound 供应记账所在的序数：在一个集合自身的阶段之上，从而在它的成员及其成员之上，也在塔的极限层之上，而诸名字自身正住在那里。

此处没有一条陈述涉及 L 上的关系，也没有一处是递归。比较与递归都在后面几章到场，而两者都被限制在本章所定位的材料之内。