L 内部的广义连续统假设

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

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

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

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

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

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω )

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

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

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

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

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

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

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