后继基数以下的序数单射到其基数

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

module L.GCH.BelowSuccessorCardinal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

后继基数是严格超过其基数的第一个基数。假设 δ 是 L 内 κ 的后继基数，本章证明每个序数 α ∈ δ 都有到 κ 的内部单射。证明把良基归纳与序数三分法结合起来。排中律有两项明确作用：给出序数三分法；并在 κ ∈ α 的情形，把「α 不是基数」转化为「仅仅存在一个更小的目标」。

固定一个宇宙层级，并假设在层级所用的命题层上成立排中律。这个经典假设是显式的，其层级也有精确规定。证明先通过序数三分法使用它，随后又用它判定呈现 Ex 的公式；其余材料都是关于 V、L、序数和内部单射的结构性事实。

论证在两个结构之间往返。外围层级提供良基的成员关系及其不可反性；可构造宇宙提供序数与基数谓词。序数三分法比较当前序数与 κ，包含关系的编码和单射的传递性则构造并复合所得的内部单射。

特殊分支只产生一个截断的见证。因此，证明用和类型与空类型分析判定，用命题截断表达仅仅存在，并用良基归纳沿成员关系下降。这些逻辑形式与结论 InjL 相配，因为 InjL 本身也是命题截断。

import Cubical.Induction.WellFounded as WF

open hPropView 𝒮ᵥ using ( _∈ˢ_ )

以 SV.S 表示外围层级的论域。成员关系归纳在这个类型上进行：它的元素是 V 中的集合，此时还没有附带该集合属于 L 的证书。

module SV = hPropView 𝒮ᵥ using ( S )

以 SL.S 表示可构造宇宙的论域。它的元素是由外围集合及其可构造性证书组成的依值对；SuccCardL、IsCardinalL 与 InjL 都以这个论域的元素为对象。

module SL = hPropView 𝒮ʟ using ( S )
module Sem = FOL.Semantics 𝒮ʟ
module At = Sem.At SL.S id

假设 δ 是 κ 的后继基数，并设序数 α 属于 δ。目标 InjL α κ 仅仅断言存在一个从 α 到 κ 的内部单射；这正是「κ 的后继基数以下每个序数的基数都不超过 κ」的形式化表述。

below-succ-injects :
    (κ δ : SL.S) → SuccCardL δ κ
  → (α : SL.S) → IsOrd (α .fst) → ⟨ α .fst ∈ˢ δ .fst ⟩
  → InjL α κ

良基归纳作用于 α 的底层集合。谓词 P a 恰好补回把外围集合 a 视为当前序数所需的数据：可构造性证书、序数性以及属于 δ 的证明。在这些假设下，它要求从 (a , la) 到 κ 的内部单射。

below-succ-injects κ δ (ordδ , _ , κ∈δ , least) α =
  WF.WFI.induction regularityV {P = P} step (α .fst) (α .snd)
  where
  P : SV.S → Type (ℓ-suc ℓ)
  P a = (la : ⟨ isL a ⟩) → IsOrd a → ⟨ a ∈ˢ δ .fst ⟩ → InjL (a , la) κ

由于 κ ∈ δ 且 δ 是序数，κ 本身也是序数。因此归纳步骤可以对 a 与 κ 的底层集合应用序数三分法。归纳假设在 a 的每个元素处都可用，这恰好是三分法第三个分支所需的条件。

  ordκ : IsOrd (κ .fst)
  ordκ = mem-ord {A = δ .fst} ordδ (κ .fst) κ∈δ

  step : (a : SV.S) → (∀ a' → ⟨ a' ∈ˢ a ⟩ → P a') → P a
  step a ih la orda a∈δ = go (ord-tri a orda (κ .fst) ordκ)
    where

把外围集合 a 与证书 la 配成依值对，便得到 L 中对应的元素 α'。这样，良基归纳仍在较简单的论域 SV.S 上进行，而基数陈述则位于其应属的论域 SL.S 中。

    α' : SL.S
    α' = a , la

考虑 κ ∈ a 的分支。如果 α' 是 L-基数，那么 SuccCardL δ κ 的最小性条款会使 δ 包含于 α'。又因 a ∈ δ，便得到 a ∈ a，与成员关系的不可反性矛盾。因此在这个分支中，α' 不可能是基数。

类型 Ex 以肯定形式表达这里所需的非基数性：仅仅存在某个 γ ∈ α'，使 α' 内部单射到 γ。

    not-card : ⟨ κ .fst ∈ˢ a ⟩ → IsCardinalL α' → ⊥₀
    not-card κ∈a c = ∈-irrefl a (least α' orda c κ∈a α' a∈δ)

    Ex : Type (ℓ-suc ℓ)
    Ex = ∥ Σ[ γ ∶ SL.S ] (⟨ γ .fst ∈ˢ a ⟩ × InjL α' γ) ∥₁

    exFo : Formula SL.S 
    exFo = ∃̇ ((var zero ∈̇ var (suc zero))
             ∧̇ injLAt (suc zero) zero)

    exFill : Ex → ⟨ (α' ∷ []) At.⊨ exFo ⟩
    exFill = map₁ (λ { (γ , γ∈a , inj) → γ , γ∈a
      , InjLAt.fill (suc zero) zero (γ ∷ α' ∷ []) inj })

    exRead : ⟨ (α' ∷ []) At.⊨ exFo ⟩ → Ex
    exRead = map₁ (λ { (γ , γ∈a , sat) → γ , γ∈a
      , InjLAt.read (suc zero) zero (γ ∷ α' ∷ []) sat })

    exDecision : Dec Ex
    exDecision = mapDec exRead (λ ns e → ns (exFill e))
      (FOL.Semantics.decideSatisfaction 𝒮ʟ id lem (α' ∷ []) exFo)

公式 exFo 约束可能的 γ，把 γ ∈ α' 与公式 injLAt α' γ 合取起来，因而恰好呈现 Ex。映射 exFill 与 exRead 在命题截断下证明两个方向。随后经 decideSatisfaction 对这条公式应用排中律。若满足成立，所需的仅仅见证已经得到；若满足被反驳，那么任取元素与单射都会导出矛盾，这恰好是说 α' 为基数的条件。

    some-γ : ⟨ κ .fst ∈ˢ a ⟩ → Ex
    some-γ κ∈a = decide exDecision
      where
      decide : Dec Ex → Ex

反驳分支与 not-card 矛盾，所以两种结果都给出 Ex。在这一步，排中律给出分支分析；它没有消去截断，也没有选出某个特定的 γ。

      decide (yes e) = e
      decide (no ¬e) =
        ⊥₀-rec (not-card κ∈a (λ γ γ∈a inj → ¬e ∣ γ , γ∈a , inj ∣₁))

Ex 的未截断内容给出 γ ∈ a 以及从 α' 到 γ 的内部单射。序数的元素仍是序数，并且 δ 具有传递性，所以 γ 再次满足归纳谓词。归纳假设给出从 γ 到 κ 的单射，再由内部单射的传递性把两者复合。

    from-γ : Σ[ γ ∶ SL.S ] (⟨ γ .fst ∈ˢ a ⟩ × InjL α' γ) → InjL α' κ
    from-γ (γ , γ∈a , α↪γ) =
      injl-trans α' γ κ α↪γ

在 γ 处调用归纳假设，需要依次提供 P 的三个条件：γ 的第二分量给出可构造性；由 γ ∈ a 及 a 的序数性得到 γ 的序数性；再由 γ ∈ a ∈ δ 及序数 δ 的传递性得到 γ ∈ δ。

        (ih (γ .fst) γ∈a (γ .snd)
            (mem-ord {A = a} orda (γ .fst) γ∈a)
            (ordδ .fst γ∈a a∈δ))

三分法的第一个分支是 a ∈ κ。序数具有传递性，所以 a 的每个元素也都是 κ 的元素；把这个包含关系编码起来，就得到从 α' 到 κ 的内部单射。

    go : Tri a (κ .fst) → InjL α' κ
    go (inl a∈κ)       =
      inclusion-coded α' κ (λ z z∈a → ordκ .fst z∈a a∈κ)

在相等分支中，沿 a ≡ κ .fst 搬运同一个包含关系即可得到所需单射。在余下的 κ ∈ a 分支中，把上面得到的截断见证消去到 InjL α' κ；由于 InjL 本身是命题，这个消去是合法的。

    go (inr (inl e))   =
      inclusion-coded α' κ (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) e z∈a)
    go (inr (inr κ∈a)) = rec₁ squash₁ from-γ (some-γ κ∈a)

序数三分法的三个分支至此全部闭合。因此，后继基数 δ 以下的每个序数都在内部单射到其基数 κ。成员关系的良基性使证明能够下降到 γ。排中律用在两处：ord-tri 用它取得三分法；高于 κ 的分支用它取得截断的小目标。