The power set in L

The power set of a set of L, taken inside L, is the set of its constructible subsets, and that is what the model's field asks for: the inclusion it quantifies over ranges across the model's own carrier, so a subset that is not constructible is not a candidate. The task is to collect the ones that are.

The argument is bounding and then carving, the same two moves the axioms before it used. Every subset of a set is a member of the hierarchy's power set, which is indexed by a small type; the constructible ones among them form a small family too, so their stages have a common bound, and every constructible subset appears below it. Carving that stage by the formula "every member of this is a member of a" gives exactly the constructible subsets, because the bound makes the membership half of the condition automatic.

Two things make the proof short. Separation in L now accepts any formula, so the condition may be written as it reads. And the smallness that the hierarchy's power set needs, and that resizing an unbounded constructibility statement needs, are the two halves of the impredicativity package the book already redeems from the excluded middle: no new principle enters, and no new level of it either, which is worth checking rather than assuming, since the two halves live one universe apart.

Condensation is not part of this. It is the sharper statement that a subset of a stage appears at a stage bounded in terms of that stage rather than in terms of the subsets themselves, and it is what a cardinal arithmetic would want. The axiom does not.

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

open import Base.Prelude
open import Base.Truth
open import Base.Classical using ( LEM; lem→resizing; lem→impredicativity )
open import Base.Impredicativity using ( module Impredicativity )

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ∀̇∈ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( module Power )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )

open import Cubical.Foundations.Equiv using ( _≃_; invEq; equivFun )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

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

module Pow = Power (Impredicativity.hPropSmallness (lem→impredicativity lem))

The condition, as a formula

"Everything in this is in a", with a named as a constant, which it may be because it is an element of the model. Its meaning is the model's own inclusion, on the nose: the object language's bounded universal is the truth algebra's meet over the carrier guarded by membership, and that is how inclusion was defined.

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

subFo-is-⊆ : (a x : S) → ((x ∷ []) ⊨ subFo a) ≡ (x ⊆ˢ a)
subFo-is-⊆ a x = refl

Bounding the constructible subsets

The hierarchy's power set is indexed by a small type, and the constructible members of it are cut out by a constructibility statement, which lives one universe too high to keep the index small. Resizing brings it back down, and resizing is what the excluded middle was already bought for. With the index small the stages form a small family and the bounding lemma applies.

Then the surjectivity: every constructible subset really does appear below the bound. Its underlying set is a subset in the hierarchy's sense, because a member of a constructible set is constructible and so is covered by the model's own inclusion; the hierarchy's power set therefore contains it, its index gives a point of the small family, and its own earliest stage lies below the bound.

module Bound (a : S) where
  private
    A P : V ℓ
    A = fst a
    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 ⟩ → ⟨ fst x ∈ Lset β ⟩
  below x x⊆a =
    subst (λ w → ⟨ w ∈ Lset β ⟩) pa
      (Lset-mono {α = β} {β = stg i} (b .snd .snd i) (stage-mem _ (unres i)))
    where
    vsub : ⟨ ModelV._⊆ˢ_ (fst x) A ⟩
    vsub v v∈ = x⊆a (v , isL-trans {x = fst x} {y = v} v∈ (x .snd)) v∈
    fib = ∈-asFiber {a = fst x} {b = P}
            (subst ⟨_⟩ (sym (Pow.power-spec A (fst x))) vsub)
    pa : ⟪ P ⟫↪ (fib .fst) ≡ fst x
    pa = fib .snd
    i : Ix
    i = fib .fst
      , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd)
          (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))

The field

Separate the bounding stage by the condition. What comes out is indexed by the conjunction "in the stage, and included in a", and the second conjunct implies the first, so the two predicates agree pointwise and the answer transports across.

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

Recap

hasPowerL is the model's power-set field, proved by bounding the constructible subsets and carving one stage. The frontier is down to choice.

What the proof used, and what it did not, is the point worth carrying away. It used the classical interface twice, once to resize an unbounded constructibility statement and once for the hierarchy's own power set, and it used separation for an arbitrary formula, which the previous part paid for. It did not use condensation, and did not need to: the axiom asks for the constructible subsets to form a set, not for them to appear early.