L 中的幂集

固定宇宙层级 ℓ 与唯一的假设 lem : LEM (ℓ-suc ℓ)。目标模型字段断言：对 L 中每个 a，恰有一个模型元素，其元素正是内部包含于 a 的模型元素。唯一性由宿主类型 isContr 打包；对象理论内容是幂集公理，而唯一性来自外延性。同一个 lem 经四条路径进入证明：命题换级、外围幂集所需的命题宇宙换级、典范层函数，以及完整分离所用的反射。这里没有引入其他经典假设。

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

对可构造集 a，L 内的幂集究竟应当收集什么？模型的量词遍历其载体 S，所以所求幂集的元素是满足内部包含 x ⊆ˢ a 的可构造模型元素 x。外围层级能对底层集 A = a .fst 构造幂集，但其成员关系条件遍历整个V ℓ，不附加可构造性要求。因此，这个外围幂集可以提供索引，却不能直接作为L 内的幂集返回。

证明分三步进行。先由外围幂集取得全部候选者的小表现，再保留其中呈现可构造候选者的索引，并用同一个序数 β 界住它们的诸层；最后在 Lset β 中作分离，恰好收集内部包含于a 的模型元素。宿主层的构造负责给出上界；最终的集合本身则在可构造模型中形成。

构造需要两种宇宙大小控制。命题换级把模型真值层级上的命题换成小索引层级上的等价命题；非直谓性包还为小命题提供一个命题宇宙换级，使外围层级能够构成幂集。两者都由排中律推出，却解决不同的大小问题：命题换级使可构造性能够进入小索引类型，分类器则构造提供这些索引的外围幂集。

证明同时涉及三个层面。宿主类型组织索引与证明；外围结构 𝒮ᵥ 的元素是累积层级中的全部集合；限制结构 𝒮ʟ 的元素则是外围集合与其可构造性证据组成的对。公式语言提供在 𝒮ʟ 内表达包含关系所需的有界全称量词。因此，外围结构可以枚举可能的子集，而对象理论的幂集公理必须在限制结构中成立。

外围层级给出集合 𝒫V A，它包含 A 的每个外围子集，并带有相应的成员关系规格。可构造层级给出诸层 Lset α 及其严格单调性：若 α ∈ β，早期层中的元素可提升到后期层。对每个可构造候选，层函数给出一个典范序数索引，其对应层包含该候选；上界引理再把这一小族序数索引严格界于同一个序数之下。层函数还证明最小性，但本章只使用序数性与层元素这两条事实。

得到序数上界 β 后，LsetS β oβ 是一个模型元素，并且已知它包含所有正在考虑的内部子集。因此，余下的数学操作是按一元包含公式作分离。通用定理 hasSeparationL接受任意公式：它先找到反射层，在该层上用公式的有界相对化取代原公式，再应用有界分离。本章的公式本来就是 Δ₀，但这次调用仍经由上述通用路径。因而，即使在这个有界特例中，公式反射以及为参数构造层的步骤，也确实使用了同一个 lem。

层级中的每个集合都有小表现：索引类型 ⟪P⟫ 与呈现其元素的嵌入 ⟪P⟫↪。属于 P 被定义为该嵌入某个纤维的命题截断。由于此映射是嵌入，每个纤维本来就是命题，故 ∈-asFiber 可以恢复索引及识别它的路径，而无须使用选择公理。换级见证提供类型等价，equivFun 与 invEq 让证明在降级命题与原命题之间往返。最后，命题外延性把两个方向的蕴含变成真值之间的路径。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )

打开 𝒮ʟ 后，下文无修饰的载体 S 与成员关系都指可构造模型。S 的元素由一个可构造集合及其可构造性证据组成；fst 忘去证据，返回对应的外围集合。参数 ℓ 控制 ⟪P⟫ 一类小表现类型，而 V ℓ、载体 S 与两套结构的真值都位于 ℓ-suc ℓ。因此后面的大小问题针对索引类型，不针对模型载体。

open hPropView 𝒮ʟ

两个模型接口给出记号相同而量化域不同的两种子集关系。在 ModelL 中，x ⊆ˢ a 量化 S，所以只检验可构造元素；在 ModelV 中，对应关系量化 V ℓ 中的每个集合。对任意左端而言，后一条件更强。若左端本身可构造，则 L 的传递性把它的每个外围元素变成 S 的元素，从而给出下文所用的精确桥梁：把内部包含提升为外围包含。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf; _⊆ˢ_ )
module ModelV = FOL.ZFModel 𝒮ᵥ

这里的记号 _⊨_ 是载体 S 上公式的内层满足关系，公式在限制结构 𝒮ʟ 中求值。常元表示它所指名的模型元素，而限制结构的成员关系在外围层级中读取这些元素的第一投影。同一模块也提供外层读法，但本章没有应用绝对性定理；此处唯一使用的满足陈述，只是有界包含公式在模型内部的直接含义。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

外围幂集构造以 LEM→ΩResizing lem 给出的命题宇宙换级实例化。这里仅使用由 ΩResizing 导出的分类器：特征函数被表示为一个取值于小真值码类型的函数，再由此形成层级中的集合。对 isL 作命题换级是另一项独立操作，并不进入这次实例化。区分这两种作用，才能看清稍后的小索引是怎样形成的。

module Pow = Power (LEM→ΩResizing lem)

作为公式的条件

对 a : S，公式 subFo a 留有一个自由槽位给候选 x，读作

「对每个 y ∈ x，都有 y ∈ a」。

var zero 的两次出现位于不同语境。有界全称量词之外的那个表示候选 x，量词主体中的那个表示新束缚的元素 y。常元域就是模型载体，所以 con a 可以直接指名 a。在环境 x ∷ [] 中，有界全称的语义直接化归为 x ⊆ˢ a。这是内部包含，其中 y 只遍历可构造模型元素。该公式是 Δ₀，尽管后面的证明把它交给一般的分离接口。

subFo : S → Formula S 
subFo a = ∀̇∈ (var zero) (var zero ∈̇ con a)

界住诸可构造子集

固定 a : S。它的第一投影 A 是忘去可构造性证据后，在外围层级中看到的同一个集合。集合 P = Pow.𝒫V A 满足完整的外围幂集规格：属于 P 只要求在外围意义下包含于 A，不带可构造性前提。因此，若有不可构造的外围子集，P 也会收纳它们。而且，这个构造没有给出P 本身可构造的证明。本证明只使用小表现 ⟪P⟫，随后以可构造性筛选其索引；P 并不是模型中最终返回的幂集。

module Bound (a : S) where

private
  A P : V ℓ
  A = a .fst
  P = Pow.𝒫V A

  rsz : (v : V ℓ) → Σ[ Q ∶ hProp ℓ ] (⟨ isL v ⟩ ≃ ⟨ Q ⟩)
  rsz v = LEM→Resizing lem (isL v)

Ix : Type ℓ
Ix = Σ[ m ∶ ⟪ P ⟫ ] ⟨ rsz (⟪ P ⟫↪ m) .fst ⟩

private
  unres : (i : Ix) → ⟨ isL (⟪ P ⟫↪ (i .fst)) ⟩
  unres i = invEq (rsz (⟪ P ⟫↪ (i .fst)) .snd) (i .snd)

  stg : Ix → V ℓ
  stg i = stage (⟪ P ⟫↪ (i .fst)) (unres i)

  b = boundingOrd Ix stg (λ i → stage-ord (⟪ P ⟫↪ (i .fst)) (unres i))

β : V ℓ
β = b .fst

oβ : IsOrd β
oβ = b .snd .fst

below : (x : S) → ⟨ x ⊆ˢ a ⟩ → ⟨ x .fst ∈ Lset β ⟩
below x x⊆a =
  subst (λ w → ⟨ w ∈ Lset β ⟩) pa
    (Lset-mono {α = β} {β = stg i} (b .snd .snd i) (stage-mem _ (unres i)))
  where

  vsub : ⟨ x .fst ModelV.⊆ˢ A ⟩
  vsub v v∈ = x⊆a (v , isL-trans {x = x .fst} {y = v} v∈ (x .snd)) v∈
  fib = ∈-asFiber {a = x .fst} {b = P}
          (subst ⟨_⟩ (sym (Pow.power-spec A (x .fst))) vsub)
  pa : ⟪ P ⟫↪ (fib .fst) ≡ x .fst

  pa = fib .snd
  i : Ix
  i = fib .fst
    , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd)
        (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))

字段

hasPowerL 的类型就是要证明的精确模型论陈述。它要求由实现者 p : S 组成的类型可缩，而对每个 x : S，p 的元素谓词都是 x ⊆ˢ a。此时外围集合 P 已完成它的作用：它提供了用于构造 Bound.β a 的索引族，却不出现在结论中。

先把 hasSeparationL 应用于模型元素LsetS (Bound.β a) (Bound.oβ a)，就得到一个可缩的 SetOf，它实现的谓词看上去更强：x 属于该层，并且满足 subFo a。余下只须证这个谓词等于内部包含。局部等式 Q≡给出这个识别，最外层的 subst 再把可缩包运输到幂集字段所需的谓词上。

hasPowerL : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
hasPowerL a =
  subst (λ Q → isContr (SetOf Q)) Q≡
    (hasSeparationL (LsetS (Bound.β a) (Bound.oβ a)) (subFo a))
  where

余下的等式比较分离切出的类与幂集字段要求的类。左端说 x 属于作为上界的层，并且 x 满足 subFo a；后一个满足命题化为内部包含 x ⊆ˢ a。正向证明因而舍去层元素这一分量。反向证明则由 x ⊆ˢ a 应用 Bound.below 补出该分量。命题外延性把两个方向的蕴含变成每个 x 处的路径，函数外延性再把这些路径合成为谓词等式 Q≡。最外层的 subst 沿这个等式运输分离所得的可缩实现者类型。Q≡ 本身不使用集合外延性；分离所打包的一意性已经用过集合外延性。

因此，hasPowerL a 以精确的模型论形式证明对象理论的幂集公理。它给出由元素 p : S 组成的可缩类型，并且对每个 x : S，成员关系命题 x ∈ˢ p 恰与内部陈述 x ⊆ˢ a 等价。p 与每个候选 x 都量化于可构造模型的载体。此前使用的宿主层幂集只提供候选者的小索引，并不是此处得到的集合。唯一的假设 LEM (ℓ-suc ℓ) 经命题换级、命题宇宙换级、从命题截断的可构造性中选出典范层，以及完整分离所用的反射，传递到这一构造。

  Q≡ : (λ x → (x ∈ˢ LsetS (Bound.β a) (Bound.oβ a)) ⊓ ((x ∷ []) ⊨ subFo a))
     ≡ (λ x → x ⊆ˢ a)
  Q≡ = funExt (λ x → ⇔toPath
    (λ { (_ , x⊆a) → x⊆a })
    (λ x⊆a → Bound.below a x x⊆a , x⊆a))

小结

这个构造中的三种作用彼此分明：外围幂集提供小表现，宿主理论界住其可构造元素的诸层，内部分离则从该上界中切出所求集合。L.Model 把 hasPowerL 装入 L⊨ZF 的 hasPower字段，随后由这个 record 定义内部运算 𝒫。后续 GCH 论证使用此运算与规格℩-spec (hasPower κ)，在成员关系与内部包含之间往返；它们从不使用辅助的外围 Pow.𝒫V。

逻辑依赖也可以精确列清。唯一的假设 LEM (ℓ-suc ℓ) 分别支持命题宇宙换级、命题换级、典范层构造与完整分离所用的公式反射。本证明不使用任何形式的选择、替换字段或凝聚。