首次与集合相交的层

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

本章为内部选择构造提供两样原料。第一是关于最小层的引理。当一条序数性质首次成立时，它在一个最小层处成立；该层是否为后继并非自动成立，因为性质可能在零序数处首次成立。本章证明论证所需的条件形式：若除最小层之外，一次雕出仅仅存在，即存在低于它的序数 δ 使性质在后继 sucV δ 处已经成立，则最小层是后继，且有唯一的前一层。第二样原料是一个上界序数：对可构造集合而言，存在一个序数，其层同时容纳该集合、它的成员、成员的成员，以及塔的极限层。

这些材料服务于一把双钥匙的比较。首次出现在不同层的两个集合，仅凭各自的诞生序数比较，别无其他；只有首次出现在同一层的集合，才在该层之内按名字比较。第一样原料使每个诞生序数成为确定的对象，而非单纯的存在；第二样原料保证一整族候选者所需的材料都住进同一个层，从而名字的比较有共同的场地。

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

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

module L.Choice.FirstIntersectionStage {ℓ : 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; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )

可构造一侧以塔 Lset 作答，塔由序数索引，序数是层级的集合，而非宿主的宇宙层级。序数性 IsOrd 本身是命题；塔有层关系、向外的分解与单调性；传递性则在层之间搬运成员。

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; 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 ( ∥_∥₁ )

论证以三个命题动作写成：分裂成情形、以空类型告终的反驳，以及仅知其为存在的存在。

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

层级的无穷构造同时给出冯·诺伊曼后继 sucV，以及上界所要包含的极限层 ω。

open hPropStructure 𝒮ᵥ

结构隶属 ∈ˢ 是序数性、层与极小性共同陈述其中的关系。

最小层的前一层

问题是：某物现身的那个最小层是否为后继，若是，它后继的是哪一层。单独的最小层未必是后继，因为性质可能从零开始；构造在「其下有雕出」这一附加假设之下产出唯一的前一层。

后继决定它所后继的东西，至少在序数之内如此。把一个候选前一层与另一个相比：各自属于对方的后继，故各自或是对方的成员、或与对方相等；而两个序数不能互为成员，否则传递性会使其一属于自身。于是「是给定序数的前一层」是命题，正是这一点使一个仅仅存在的前一层可以被读作一个确定的前一层。

最小层凭什么有前一层？这需要两样输入，值得分开看。第一是最小层自身：性质在其中成立的序数 σ，其极小性以反驳形式陈述，即没有更小的序数拥有该性质。第二是 σ 处雕出的仅仅存在：σ 以下的某个序数 δ，其后续 sucV δ 处性质已经成立。有了雕出，极小性排除「后继仍严格在下」，而不越头的比较只剩一种情形：被雕出序数的后继恰是 σ。于是最小层是后继，而被雕出的序数就是它的前一层。没有雕出则推不出任何东西：性质可能恰在零序数处首次成立，而零以下根本没有序数。

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

序数 σ 的候选前一层 δ 是一个序数，其冯·诺伊曼后继就是 σ 本身。两半都不可或缺：序数性是比较所需的，等式则是把 δ 钉在 σ 上的。

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)

没有序数能属于它自己的某个成员：传递性会把这条隶属沿两步循环搬回 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δ)
    (λ δ≡δ' → δ≡δ')

后继运算在序数上是单射的。由后继的等式，δ 属于 sucV δ'；消去给出两种读法。要么 δ 属于 δ'，此时隶属分支闭合循环并给出等式；要么 δ 本来就是 δ'。后继决定它所后继者。

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

于是同一序数的任意两个前一层相等。第一分量由单射性一致，其余数据都是命题，故前一层组成的整个类型是命题。正是这一点使「仅仅存在的前一层」可当作确定的前一层使用：把截断展开到命题值的目标永远合法。

module _ (P : S → hProp (ℓ-suc ℓ)) where

最小层论证对每条序数性质同时只写一次：性质是参数，以下任何地方都不读入其内部。

  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)

σ 处的一次雕出是论证所运行的数据：一个严格低于 σ 的序数 δ，其后继已携带该性质。若雕出仅仅存在，最小层就不可能远在 δ 之上，因为性质在 sucV δ 处已经成立。

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

below 分支处理「后继仍严格低于最小层」的情形。极小性以反驳形式陈述，而本分支的假设恰是它的前提，故 least 先给出矛盾；Empty.rec 再把该矛盾消去成分支所欠的路径 sucV δ ≡ σ。

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

相等情形无须任何工作：交给该情形的恰是「后继与最小层等同」这件事本身。

    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∈ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)

atCarve 把一次雕出变成确定的前一层。见证 δ 被保留，其序数性由属于序数 σ 而恢复，而把 sucV δ 钉到 σ 上的等式正是那场情形分析的内容。

      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ

δ 的序数性承继自序数 σ，因为序数的成员是序数。

      suc≡σ : sucV δ ≡ σ
      suc≡σ = Sum.rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)

由 δ ∈ σ 出发，suc∈or≡ 为其后继留下两种可能：仍严格低于 σ，或等于 σ。极小性排除前者，后者便给出所需等式。

  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∈ S ] IsPredOf σ δ
  predOf σ ordσ least = PT.rec (isPropPredOf σ) (atCarve σ ordσ least)

predOf 消费一个仅知其存在的雕出，返回前一层。截断的输入被消去到「前一层类型是命题」这一事实之中，因此从不在假想的雕出之间作选择；无论截断交出哪次雕出，答案都是同一个确定的前一层。

  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁

carveAt 从最小层的一个成员 z 造出雕出，配合的是这样一条观察：但凡 z 在某个后继层现身，性质便已在彼处成立。这正是进入塔之下降的形状：出现在某层，就是出现在某个更早层的可定义幂集之内，而由后继恒等式，每个可定义幂集都是一个后继层。

  carveAt σ z z∈Lσ k = PT.map
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)

塔以截断的方式分解 z 的隶属：给出某个低于 σ 的层 δ，使 z 落在 Lset δ 的可定义幂集之内。映射只在截断内部进行：后继恒等式反向读取，把 z 从 𝒟ₒ (Lset δ) 搬到 Lset (sucV δ)，观察 k 在该后继处触发，所得的雕出被重新注入截断。

一层装下一个集合以下的一切

本节用层的传递性与序数上界，得到一个同时包含集合的成员、成员的成员以及极限层 ω 的层。

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

还需确定一个包含塔的极限层的序数。前方的比较以对象语言书写，而各元数的无常元公式 Formula ⊥* n 的码都属于 Lset ω；这样的码可以带有自由变量，因此它们是公式，而非句子。后继层中一个成员的完整名字所说的多于它的码：它还要指名元数，以及取自更早层的参数向量。这里造出的界覆盖码，因为 ω ∈ β 加上单调性把 Lset ω 抬进 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)

层传递，而 a 的最早层也是一个层。故 a 的成员 x 落在塔在 a 自身层处的层里：传递性把隶属从集合搬进容纳该集合的那一层。

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)

传递性应用两次即可下探两层：a 的成员的成员落在同一层里，因为它属于 x，而 x 属于那一层。

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

必须被支配的两个序数是极限层 ω 与该集合自身的最早层；bound2 返回一个同时高于两者的序数，并附带其序数性证书。

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)

塔的单调性把「下探两层」的事实从最早层提升到界序数的层。现在这一层同时容纳 a、它的成员、成员的成员，以及比较所要读取的公式码。

小结

本章可复用的结果，是最小层为后继时的唯一前一层，以及足以承载选择构造的上界序数。最小层引理是带条件的，而条件正是它的内容。对以 σ 为最小层的某条序数性质而言，性质完全可能恰在零序数处首次成立，此时其下无可雕出之物。当 σ 处的雕出仅仅存在，即有低于 σ 的序数使其后继已具该性质时，carveAt 产出雕出，predOf 按 isPropPredOf 闭合截断，把它化为唯一的前一层；而 ord-suc-inj 正是「后继决定它所后继者」的理由。stageBound 给出上界序数：它在一个集合自身的层之上，从而在其成员及其成员之上，也在塔的极限层之上，而公式码恰在那里。