L 内部的广义连续统假设

在 L 内部，广义连续统假设比较与每个无穷内部基数 κ 相联系的两个集合：它的幂集与内部后继基数。本书用两个方向的内部编码单射表示二者大小相同。下面的陈述采用模型自身给出的幂集来表述这一比较。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )

内部基数、后继基数和编码单射都相对于这里选定的排中律实例而定义。因此，这一陈述沿用此前基数理论的经典背景，不再加入其他经典假设。

import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd )
open import L.Cardinal {ℓ} lem using ( IsCardinalL; InjL; SuccCardL )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

量词遍历可构造结构的论域。论域中的元素由一个外围集合及其可构造性证明组成。是否属于 ω 通过外围成员关系来解释；其否定给出基数为无穷的条件。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

ZF 模型带有自身的幂集运算。给定模型证明 zf，记号 𝒫 κ 表示该模型的幂集公理为 κ 给出的集合。因此，这一比较中的集合与成员陈述都留在可构造结构内部。

open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )

module ModelL = FOL.ZFModel 𝒮ʟ
GCHStatement : ModelL.isZFModel → Type (ℓ-suc ℓ)

关于 κ 的假设可以依次读出。它的底层集合是序数。它是内部基数，也就是说，对每个 δ ∈ κ，都不存在从 κ 到 δ 的内部编码单射。最后，κ ∉ ω。这些条件合在一起说明 κ 是无穷内部基数。

GCHStatement zf =
  (κ : S)
  → IsOrd (fst κ)
  → IsCardinalL κ
  → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)

结论仅仅断言：存在 κ 的内部后继基数 δ，并且存在从 𝒫 κ 到 δ 以及从 δ 到 𝒫 κ 的内部编码单射。本书用这两个方向的比较表达两集合大小相同。最外层截断不选定某个特定的 δ；其中每个 InjL 又只保留合适的可构造单射码的存在性。

  → ∥ Σ[ δ ∈ S ]
       ( SuccCardL δ κ
       × InjL (𝒫 κ) δ
       × InjL δ (𝒫 κ) ) ∥₁
  where open ModelL.isZFModel zf using ( 𝒫 )