Injecting the successor cardinal into the power set

Cantor's theorem inside L rules out an internally coded injection from 𝒫 κ into κ. Starting from a successor cardinal δ of κ and a separately supplied comparison InjL (𝒫 κ) δ, this chapter constructs the reverse comparison InjL δ (𝒫 κ). Here InjL a b is the propositional truncation of the existence of a graph in L coding an injection from a to b. The proof transfers the ordinal order on δ back to 𝒫 κ, collapses that order to an ordinal μ, and uses Cantor's obstruction to show that μ cannot lie below δ.

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

Classical reasoning enters through the explicit parameter lem. Ordinal trichotomy supplies the visible case splits, while the separation and coded-injection results used in the argument are also instantiated with the same assumption. Thus the chapter records its classical dependence in one place.

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

The excluded-middle assumption is indexed at ℓ-suc ℓ, the level at which the relevant propositions about sets and coded graphs live. Every classical comparison used below is consequently traceable to this one parameter.

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

The diagonal subset and the later pullback order must be sets of L, so both are described by first-order formulas interpreted in the constructible model. The available syntax expresses membership, conjunction, negation, and the bounded or unbounded existential witnesses needed to describe those relations.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_; ∃̇∈ )
import FOL.ZFModel
import FOL.Absoluteness

The pullback order will be proved well-founded by sending every descending step to a membership step in the ambient cumulative hierarchy and applying regularity there. Facts about constructible ordinals then turn membership below an ordinal into the ordinal structure needed for comparison.

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; IsOrd; isL; isL-trans; isTransV; isPropIsTransV )
open import L.Ordinal {ℓ} using ( mem-ord )

An internal size comparison has two levels. InjCode F a b retains a particular constructible graph and its injection laws, whereas InjL a b retains only the propositionally truncated existence of such a code. Successor-cardinal minimality, coded inclusions, and composition will let the proof combine these comparisons without exposing a global graph.

open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; SuccCardL )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate; inclusion-coded; injl-trans; module Relation )
open import L.Coding.Model {ℓ} using ( svAt-out; domAt-in )

Two earlier results control the final comparison. Every ordinal strictly below the successor cardinal δ injects into its base κ, and a coded well-order can be collapsed to a constructible ordinal together with coded maps to and from its collapse image. The third ingredient, InjL (𝒫 κ) δ, is an assumption of this chapter's conditional theorem; it is not a consequence of the successor-cardinal record alone.

open import L.Coding.Injection {ℓ} lem using ( injAt-out )
open import L.GCH.BelowSuccessorCardinal {ℓ} lem using ( below-succ-injects )
open import L.GCH.Assembly {ℓ} lem using ( SuccIntoPower )
open import L.DefinableInjection {ℓ} lem using ( module Inj )
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )

Several equalities below identify dependent pairs whose second components are proofs. Since those proof components are propositions, equality of the underlying sets suffices; transport then moves membership and graph facts along the resulting identifications.

open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

Accessibility records express the well-founded recursion used for the pulled-back order. Propositional truncation expresses mere existence throughout the chapter, and its eliminations will always have a proposition, such as the empty type or another InjL statement, as their target.

import Cubical.Induction.WellFounded as WF
open WF using ( Acc; acc; WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

Membership of underlying sets is read in the ambient hierarchy when regularity and transitivity are applied. This ambient relation must be distinguished from membership between elements packaged with their constructibility proofs.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

Write SV.S for an ambient set. It is used when a claim, such as pointwise containment between underlying ordinals, ranges over the cumulative hierarchy itself.

module SV = hPropStructure 𝒮ᵥ using ( S )

Write SL.S for a set together with its certificate of constructibility. The internal power set, successor-cardinal predicate, and coded-injection relation all take their arguments in this carrier.

module SL = hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )

The ZF structure on L determines its internal power set. Its specification identifies membership in 𝒫 κ with the internal subset relation, where the quantification ranges over constructible model elements.

module ModelL = FOL.ZFModel 𝒮ʟ using ( isZFModel; module isZFModel; ℩-spec )

Object-language formulas will be evaluated in environments of constructible sets. Absoluteness supplies the semantic reading that connects those satisfaction statements to the host-level predicates used in the proof.

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

An element of SL.S consists of an underlying set and a proof of constructibility. Because constructibility is a proposition, equality of the underlying sets lifts to equality in SL.S; no additional choice of equality between certificates is required.

S≡ : {x y : SL.S} → fst x ≡ fst y → x ≡ y
S≡ = Σ≡Prop (λ v → snd (isL v))

Internal subsets belong to the model's power set

The first construction converts pointwise internal containment into membership in the model's power set. It applies to arbitrary constructible sets κ and y: if every constructible element of y belongs to κ, then y is an internal subset of κ and hence a member of 𝒫 κ.

into-power :
    (zf : ModelL.isZFModel) (κ y : SL.S)
  → ((z : SL.S) → ⟨ fst z ∈ˢ fst y ⟩ → ⟨ fst z ∈ˢ fst κ ⟩)
  → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩
into-power zf κ y sub =

The power-set specification states that membership of y in 𝒫 κ is equivalent to the pointwise internal subset condition. Rewriting by this equivalence leaves exactly the supplied containment proof.

  subst ⟨_⟩ (sym (ModelL.℩-spec (hasPower κ) y)) sub
  where open ModelL.isZFModel zf using ( hasPower )

Cantor's diagonal argument inside L

We now fix an arbitrary constructible set κ and prove the internal Cantor obstruction for its model power set. No cardinality or infinitude hypothesis on κ is needed for this part.

module Cantor (zf : ModelL.isZFModel) (κ : SL.S) where

Throughout the diagonal argument, 𝒫 κ means the power set supplied by the fixed ZF model on L. Thus its elements are precisely the subsets recognized inside that model.

  open ModelL.isZFModel zf using ( 𝒫 )

The diagonal argument is carried out for one explicitly given graph F together with its coding. All later statements concern this fixed graph.

  module Diag (F : SL.S) (code : InjCode F (𝒫 κ) κ) where

The environment of the graph pairs the graph with the power set over which it is total.

    γF : SL.S ^ 
    γF = F ∷ 𝒫 κ ∷ []

The range clause of the coding says that every value recorded by the graph belongs to κ.

    ranF : (x y : SL.S) → Holds F x y → ⟨ fst y ∈ fst κ ⟩
    ranF = code .snd .snd .snd

The totality clause says that every member of 𝒫 κ has some value under F. The value witness remains under propositional truncation, so this statement supplies existence without choosing a value globally.

    valF : (x : SL.S) → ⟨ fst x ∈ fst (𝒫 κ) ⟩
         → ∥ Σ[ y ∈ SL.S ] Holds F x y ∥₁
    valF = domAt-in zero (suc zero) γF (code .snd .fst)

The injectivity clause recovers the input from the value: two members with the same recorded value have equal underlying sets.

    injF : (y x x' : SL.S) → Holds F x y → Holds F x' y → fst x ≡ fst x'
    injF = injAt-out zero γF (code .snd .snd .fst)

The diagonal predicate says, merely, that some member A of the power set has its recorded value equal to ξ, while ξ does not belong to A. Existence is truncated; no such set is chosen.

    Diagonal : SL.S → Type (ℓ-suc ℓ)
    Diagonal ξ = ∥ Σ[ A ∈ SL.S ] ( ⟨ fst A ∈ fst (𝒫 κ) ⟩ × Holds F A ξ
                                 × (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) ) ∥₁

Satisfaction of the application atom is literally the host-level graph holding, by the adequacy of the application coding.

    private
      a1 : (ξ A : SL.S)
         → ⟨ (A ∷ ξ ∷ []) ⊨ appC F zero (suc zero) ⟩ ≡ Holds F A ξ
      a1 ξ A = cong ⟨_⟩ (appC-adequate F zero (suc zero) (A ∷ ξ ∷ []))

The formula defining the diagonal condition searches within 𝒫 κ for a set A such that F records the pair (A, ξ) and ξ does not belong to A. The bounded quantifier records exactly that the witness is an internal subset of κ; separation over κ then forms the set of all ξ∈κ satisfying this condition.

    opaque
      φD : Formula SL.S 
      φD = ∃̇∈ (con (𝒫 κ))
             (appC F zero (suc zero) ∧̇ ¬̇ (var (suc zero) ∈̇ var zero))

Adequacy of the application coding identifies the formula atom for applying F to A with the semantic statement Holds F A ξ. This equality is what allows the diagonal formula and the coded graph to be used interchangeably in the two directions below.

      φD-out : (ξ : SL.S) → ⟨ (ξ ∷ []) ⊨ φD ⟩ → Diagonal ξ
      φD-out ξ = PT.map (λ { (A , (mA , (h , n))) →
        A , mA , transport (a1 ξ A) h , (λ k → lower (n k)) })

Conversely, a chosen A ∈ 𝒫 κ, a graph fact Holds F A ξ, and a proof that ξ ∉ A satisfy the diagonal formula. These data are packaged under the formula's truncated bounded existential.

      φD-in : (ξ A : SL.S) → ⟨ fst A ∈ fst (𝒫 κ) ⟩ → Holds F A ξ
            → (⟨ fst ξ ∈ fst A ⟩ → Empty.⊥) → ⟨ (ξ ∷ []) ⊨ φD ⟩
      φD-in ξ A mA h n =
        ∣ A , (mA , (transport (sym (a1 ξ A)) h , (λ k → lift (n k)))) ∣₁

The diagonal set is separated out of κ by the bounded formula.

    D₀ : SL.S
    D₀ = fst (fst (hasSeparationL κ φD))

Its membership specification is the separation's own reading: membership in the diagonal set is membership in κ conjoined with satisfaction of the diagonal formula.

    D₀-spec : (ξ : SL.S) → (ξ SL.∈ˢ D₀) ≡ ((ξ SL.∈ˢ κ) ⊓ ((ξ ∷ []) ⊨ φD))
    D₀-spec = snd (fst (hasSeparationL κ φD))

The diagonal set is a member of the internal power set: the pointwise reading proves that every model element of it belongs to κ.

    D₀∈𝒫κ : ⟨ fst D₀ ∈ fst (𝒫 κ) ⟩
    D₀∈𝒫κ = into-power zf κ D₀ (λ z h → fst (subst ⟨_⟩ (D₀-spec z) h))

To derive the contradiction, suppose the graph assigns the diagonal set D₀ some value ξ. The range clause will show ξ ∈ κ, while the definition of D₀ will force both ξ ∈ D₀ and ξ ∉ D₀.

    absurd : Σ[ ξ ∈ SL.S ] Holds F D₀ ξ → Empty.⊥
    absurd (ξ , h₀) = out inside
      where

Assume ξ ∈ D₀. The diagonal formula then supplies, under truncation, a set A ∈ 𝒫 κ such that F sends A to ξ and ξ ∉ A. Since F also sends D₀ to ξ, injectivity identifies the underlying sets of A and D₀; transporting the assumed membership into A contradicts ξ ∉ A.

      out : ⟨ fst ξ ∈ fst D₀ ⟩ → Empty.⊥
      out hm = PT.rec Empty.isProp⊥
        (λ { (A , _ , hA , n) →
          n (subst (λ w → ⟨ fst ξ ∈ w ⟩) (injF ξ D₀ A h₀ hA) hm) })
        (φD-out ξ (snd (subst ⟨_⟩ (D₀-spec ξ) hm)))

The converse direction uses that refutation as data. The range clause gives ξ ∈ κ, and choosing A = D₀ witnesses the diagonal formula because F sends D₀ to ξ and the preceding function proves ξ ∉ D₀. Separation therefore yields ξ ∈ D₀, to which the refutation is applied.

      inside : ⟨ fst ξ ∈ fst D₀ ⟩
      inside = subst ⟨_⟩ (sym (D₀-spec ξ))
        (ranF D₀ ξ h₀ , φD-in ξ D₀ D₀∈𝒫κ h₀ out)

The two halves refute any internal coded injection from the power set into κ: the injection is eliminated into a graph, and the graph's value at the diagonal set is eliminated into the contradiction. The target is the empty type, so both eliminations are legitimate.

  no-inj : InjL (𝒫 κ) κ → Empty.⊥
  no-inj = PT.rec Empty.isProp⊥ step
    where
    step : Σ[ F ∈ SL.S ] InjCode F (𝒫 κ) κ → Empty.⊥
    step (F , code) = PT.rec Empty.isProp⊥ D.absurd (D.valF D.D₀ D.D₀∈𝒫κ)

For the chosen graph F, the diagonal construction supplies both the internal subset D₀ and the proof that no value can be assigned to it. Totality assigns such a value nevertheless, completing the contradiction for this graph.

      where module D = Diag F code

Ordering the power set and comparing its order type

For the reverse comparison, fix a successor cardinal δ of κ and one particular graph G coding the assumed injection 𝒫 κ ↪ δ. This graph is available only inside a local branch obtained from the propositional truncation; the final result will again be an InjL statement.

module Build (zf : ModelL.isZFModel) (κ δ : SL.S) (sc : SuccCardL δ κ)
             (G : SL.S)
             (code : InjCode G (ModelL.isZFModel.𝒫 zf κ) δ) where

The source 𝒫 κ is again the internal power set determined by the fixed ZF model. The construction never replaces it by the ambient power set of the underlying set.

  open ModelL.isZFModel zf using ( 𝒫 )

The ordinality of the successor is the first component of its record.

  ordδ : IsOrd (fst δ)
  ordδ = sc .fst

The power set is named as the source of the comparison.

  P : SL.S
  P = 𝒫 κ

The environment of the graph pairs the graph with the power set.

  γG : SL.S ^ 
  γG = G ∷ P ∷ []

The range clause of the coding says every value lands in the successor.

  ranG : (x y : SL.S) → Holds G x y → ⟨ fst y ∈ fst δ ⟩
  ranG = code .snd .snd .snd

Single-valuedness concerns one fixed input: if G records both G(x)=y and G(x)=y', then the underlying sets of y and y' are equal. This uniqueness will make the type of possible values of x a proposition.

  svG : (x y y' : SL.S) → Holds G x y → Holds G x y' → fst y ≡ fst y'
  svG = svAt-out zero γG (code .fst)

Totality gives a propositionally truncated value witness for every x ∈ P. It does not yet choose a value. Shortly, single-valuedness will show that the fibre of possible values is a proposition, which permits elimination of this truncation and yields a locally readable value.

  valG : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → ∥ Σ[ y ∈ SL.S ] Holds G x y ∥₁
  valG = domAt-in zero (suc zero) γG (code .snd .fst)

The injectivity clause for the coded injection G recovers a source member from its value: if two source members have the same recorded value, then their underlying sets are equal.

  injG : (y x x' : SL.S) → Holds G x y → Holds G x' y → fst x ≡ fst x'
  injG = injAt-out zero γG (code .snd .snd .fst)

For a fixed input x, any two graph values of G must coincide by single-valuedness. Since constructibility proofs are propositions, equality of the underlying values lifts to equality of the complete witnesses. Thus the fibre of possible values is itself a proposition.

  isPropVal : (x : SL.S) → isProp (Σ[ y ∈ SL.S ] Holds G x y)
  isPropVal x (y , h) (y' , h') =
    Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst G)) (S≡ (svG x y y' h h'))

The domain clause initially supplies a value of G only under propositional truncation. The preceding uniqueness result makes the target fibre proposition-valued, so the truncation may be eliminated and the unique value used in the rest of the construction. This step uses uniqueness, not a general choice principle.

  val : (x : SL.S) → ⟨ fst x ∈ fst P ⟩ → Σ[ y ∈ SL.S ] Holds G x y
  val x m = PT.rec (isPropVal x) (λ z → z) (valG x m)

Define a to precede b when they both belong to P and there merely exist graph values x and y with G(a)=x, G(b)=y and x∈y. Propositional truncation records that suitable images exist without retaining a choice of witnesses.

  Read : SL.S → SL.S → Type (ℓ-suc ℓ)
  Read a b = ∥ Σ[ x ∈ SL.S ] Σ[ y ∈ SL.S ]
               ( ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩
               × Holds G a x × Holds G b y × ⟨ fst x ∈ fst y ⟩ ) ∥₁

To express this relation in the object language, the environment places A, B and their candidate images x, y where the two applications of G can read them. This lets one formula speak simultaneously about G(A)=x, G(B)=y and x∈y.

  private
    env5 : SL.S → SL.S → SL.S → SL.S → SL.S → SL.S ^ 
    env5 p A B x y = y ∷ x ∷ B ∷ A ∷ p ∷ []

The first adequacy equality identifies the encoded application with the graph statement Holds G A x. It is the bridge between the object-language formula and the assertion that x is the value assigned to A by the coded graph.

    b1 : (p A B x y : SL.S)
       → ⟨ env5 p A B x y ⊨ appC G (suc (suc (suc zero))) (suc zero) ⟩
       ≡ Holds G A x
    b1 p A B x y = cong ⟨_⟩
      (appC-adequate G (suc (suc (suc zero))) (suc zero) (env5 p A B x y))

The second adequacy equality performs the same translation for B and y. Together the two equalities allow the pullback relation to be proved either through formula satisfaction or through ordinary statements about the graph of G.

    b2 : (p A B x y : SL.S)
       → ⟨ env5 p A B x y ⊨ appC G (suc (suc zero)) zero ⟩ ≡ Holds G B y
    b2 p A B x y = cong ⟨_⟩
      (appC-adequate G (suc (suc zero)) zero (env5 p A B x y))

The defining formula first restricts both endpoints to the internal power set, then quantifies over two model elements that serve as their images. Together with the two application atoms and the membership comparison between the images, this gives a first-order description of a relation on P; the relation construction represents that description by a set in L.

  private
    opaque
      φR : Formula SL.S 
      φR = (var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ∃̇ (∃̇
        (appC G (suc (suc (suc zero))) (suc zero)

Inside the two existential binders, the remaining clauses say that the witnesses are respectively the G-images of the endpoints and that the first image belongs to the second. This is precisely the membership order on δ pulled back along G.

          ∧̇ (appC G (suc (suc zero)) zero ∧̇ (var (suc zero) ∈̇ var zero)))))

Reading the formula outward first retains the two image witnesses under propositional truncation. The two adequacy equalities then turn the encoded applications into graph facts, yielding exactly the semantic data in Read: endpoint membership, the two values and their membership comparison.

      read : (a b p : SL.S) → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩ → Read a b
      read a b p (ma , mb , h) = PT.rec squash₁
        (λ { (x , hx) → PT.map (λ { (y , ha , hb , hxy) → x , y , ma , mb
          , transport (b1 p a b x y) ha , transport (b2 p a b x y) hb , hxy }) hx }) h

The inward reading transports each host-side fact back through the reversed adequacy equations, filling the existential and application slots to reconstruct the formula satisfaction.

      fill : (a b p : SL.S) → Read a b → ⟨ (b ∷ a ∷ p ∷ []) ⊨ φR ⟩
      fill a b p = PT.rec (snd ((b ∷ a ∷ p ∷ []) ⊨ φR))
        (λ { (x , y , ma , mb , ha , hb , hxy) → ma , mb , ∣ x , ∣ y
          , transport (sym (b1 p a b x y)) ha
          , transport (sym (b2 p a b x y)) hb , hxy ∣₁ ∣₁ })

The bounded-relation construction now turns this definable predicate into an actual relation set in L. The two readings proved above ensure that membership in the coded relation has exactly the intended truncated content Read.

    module Pullback = Relation P P φR (λ a b → Read a b , squash₁) read fill

For the converse reading, the two adequacy equalities turn the graph facts Holds G A x and Holds G B y back into application atoms. Packaging x and y as the two existential witnesses then reconstructs satisfaction of the defining formula.

  R : SL.S
  R = Pullback.rel

An entry of R can be read back as the truncated data defining the pullback: the two endpoints lie in the power set, they have G-images, and the first image belongs to the second.

  R-out : (a b : SL.S) → Holds R a b → Read a b
  R-out = Pullback.pair-out

The inward reading constructs the relation entry from the two endpoint memberships, the two G-image facts and the membership between the images.

  R-in : (a b x y : SL.S) → ⟨ fst a ∈ fst P ⟩ → ⟨ fst b ∈ fst P ⟩
       → Holds G a x → Holds G b y → ⟨ fst x ∈ fst y ⟩ → Holds R a b
  R-in a b x y ma mb ha hb hxy = Pullback.into a b ma mb ∣ x , y , ma , mb , ha , hb , hxy ∣₁

Every entry of the coded relation has endpoints in P. The proof reads its truncated witnesses and discards the image data, retaining only the two endpoint-membership facts; this elimination is allowed because their product is a proposition.

  Rsub : (a b : SL.S) → Holds R a b
       → ⟨ fst a ∈ fst P ⟩ × ⟨ fst b ∈ fst P ⟩
  Rsub a b h = PT.rec
    (isProp× (snd (fst a ∈ fst P)) (snd (fst b ∈ fst P)))
    (λ { (_ , _ , ma , mb , _) → ma , mb })

Applying the outward reading supplies the witnesses needed by the extraction. Eliminating their truncation is legitimate because the conclusion, the pair of endpoint-membership propositions, is itself a proposition.

    (R-out a b h)

The order-type construction replaces members of P by a small presented domain Dom. Its relation a ≺ b records exactly the coded fact that the represented members are related by R; the following proof can therefore study the pullback order on indices and later collapse it.

  module OT = Code P R Rsub
    using ( Dom; Dom≡; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out
          ; module Conjuncts )

For an index b in this domain, let v b be the unique value that G assigns to the represented member of P. The next steps show that these representatives are ordinals below δ.

  v : OT.Dom → SL.S
  v b = fst (val (OT.up b) (OT.up-mem b))

The second component of the chosen value records the corresponding graph fact Holds G (up b) (v b). It will connect comparisons among the representatives with entries of the pulled-back relation.

  v-holds : (b : OT.Dom) → Holds G (OT.up b) (v b)
  v-holds b = snd (val (OT.up b) (OT.up-mem b))

Every value of G belongs to the successor cardinal δ, by the range clause of the injection code. This places all representatives inside one ordinal, where membership comparisons and ordinal trichotomy are available.

  v∈δ : (b : OT.Dom) → ⟨ fst (v b) ∈ fst δ ⟩
  v∈δ b = ranG (OT.up b) (v b) (v-holds b)

Each G-value is an ordinal, inherited from the ordinality of δ.

  ord-v : (b : OT.Dom) → IsOrd (fst (v b))
  ord-v b = mem-ord {A = fst δ} ordδ (fst (v b)) (v∈δ b)

The forward comparison turns a predecessor step in the pulled-back relation into membership between the two representative ordinals. Reading the relation entry gives two possible image witnesses; single-valuedness of G identifies them with the fixed values v a and v b.

  ≺-fwd : (a b : OT.Dom) → a OT.≺ b → ⟨ fst (v a) ∈ fst (v b) ⟩
  ≺-fwd a b k = PT.rec (snd (fst (v a) ∈ fst (v b)))
    (λ { (x , y , _ , _ , ha , hb , hxy) →
      subst2 (λ s t → ⟨ s ∈ t ⟩)
        (svG (OT.up a) x (v a) ha (v-holds a))

The two single-valuedness equalities replace the image witnesses read from R by the fixed representatives v a and v b. Transporting x∈y along both equalities yields the required comparison v a ∈ v b.

        (svG (OT.up b) y (v b) hb (v-holds b)) hxy })
    (R-out (OT.up a) (OT.up b) (OT.≺-out a b k))

The backward comparison constructs the pulled-back relation from the membership of the two representative ordinals, by reintroducing the two graph facts and the membership between their images.

  ≺-bwd : (a b : OT.Dom) → ⟨ fst (v a) ∈ fst (v b) ⟩ → a OT.≺ b
  ≺-bwd a b h = OT.≺-in a b
    (R-in (OT.up a) (OT.up b) (v a) (v b)
      (OT.up-mem a) (OT.up-mem b) (v-holds a) (v-holds b) h)

To prove well-foundedness, fix a hierarchy element u and consider every domain index whose representative value is u. The predicate Pacc u asks that each such index be accessible in the pullback order, setting up induction on ambient membership.

  private
    Pacc : V ℓ → Type (ℓ-suc ℓ)
    Pacc u = (b : OT.Dom) → fst (v b) ≡ u → Acc OT._≺_ b

The induction step constructs accessibility for a predecessor whose representative ordinal lies strictly below u: the forward comparison carries the membership to the representative, and the induction hypothesis supplies accessibility there.

    accStep : (u : V ℓ) → (∀ u' → ⟨ u' ∈ˢ u ⟩ → Pacc u') → Pacc u
    accStep u IH b e = acc (λ a k →
      IH (fst (v a)) (subst (λ w → ⟨ fst (v a) ∈ˢ w ⟩) e (≺-fwd a b k))
         a refl)

Accessibility at every hierarchy element is proved by the regularity induction of the ambient hierarchy, which is the well-foundedness of its membership.

    accAt : (u : V ℓ) → Pacc u
    accAt = WF.WFI.induction regularityV {P = Pacc} accStep

Well-foundedness of the pulled-back order is assembled from the accessibility at each representative ordinal.

  wf : WellFounded OT._≺_
  wf b = accAt (fst (v b)) b refl

Transitivity of the pulled-back order composes the two forward comparisons through the transitivity of the ordinal δ applied to the two representative memberships.

  ≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
  ≺-trans {a} {b} {c} k k' = ≺-bwd a c
    (ordδ .snd (fst (v c)) (v∈δ c) (≺-fwd a b k) (≺-fwd b c k'))

Trichotomy of the pulled-back order is transported from ordinal trichotomy for the representative values in δ: for any a and b, either v a ∈ v b, the two values are equal, or v b ∈ v a.

  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (ord-tri (fst (v a)) (ord-v a) (fst (v b)) (ord-v b))
    where
    go : Tri (fst (v a)) (fst (v b))
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))

The strict-below case produces the pulled-back comparison directly. The equal case identifies the two domain members through the injectivity of G applied to the equal representative values. The strictly-above case reverses the comparison.

    go (inl h)       = inl (≺-bwd a b h)
    go (inr (inl e)) = inr (inl (OT.Dom≡
      (injG (v a) (OT.up a) (OT.up b) (v-holds a)
        (subst (λ w → ⟨ pr (OT.↪ b) w ∈ fst G ⟩) (sym e) (v-holds b)))))
    go (inr (inr h)) = inr (inr (≺-bwd b a h))

Well-foundedness and transitivity now support the collapse map col and its image otL. Trichotomy adds injectivity of the collapse: distinct domain indices cannot have the same collapse value. These facts provide both the collapse table and the data needed to reverse it later.

  module C = OT.Conjuncts wf ≺-trans
    using ( module Inj; col; col-ord; col-out; colTable; colTable-in
          ; colTable-pair; otL; otL-in; otL-out )
  module I = C.Inj tri using ( code; col-inj; module Inverse )

The collapse table is a coded injection from the internal power set P into its collapse image otL. Wrapping that particular table and its injection proof in propositional truncation gives the internal statement InjL P otL.

  power-into-ot : InjL P C.otL
  power-into-ot = ∣ C.colTable , I.code ∣₁

To prove that the collapse image is an ordinal, one must show both that the image is transitive and that each of its members is transitive. For the second condition, membership in otL gives, under propositional truncation, an index b whose collapse value presents the given member.

  ot-ord : IsOrd (fst C.otL)
  ot-ord = tr , mem
    where
    mem : (x : V ℓ) → ⟨ x ∈ˢ fst C.otL ⟩ → isTransV x
    mem x h = PT.rec (isPropIsTransV x)

Every collapse value col b is already known to be an ordinal, hence transitive. Transporting this transitivity along the equation col b = x proves that the arbitrary member x of the image is transitive.

      (λ { (b , e) → subst isTransV e (C.col-ord b .fst) })
      (C.otL-out x h)

It remains to show that the image itself is transitive. Given y∈x and x∈otL, the outward description of otL presents x, under propositional truncation, as a collapse value col b; the target membership y∈otL is a proposition, so this witness may be used locally.

    tr : isTransV (fst C.otL)
    tr {x} {y} y∈x x∈ot =
      PT.rec (snd (y ∈ˢ fst C.otL)) outer (C.otL-out x x∈ot)
      where
      outer : Σ[ b ∈ OT.Dom ] (C.col b ≡ x) → ⟨ y ∈ˢ fst C.otL ⟩

After replacing x by col b, the collapse equation for membership in col b yields, again under propositional truncation, a predecessor r≺b whose collapse value is y. This is the smaller collapse value needed to place y back in the image.

      outer (b , e) = PT.rec (snd (y ∈ˢ fst C.otL)) inner
        (C.col-out b y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym e) y∈x))
        where
        inner : Σ[ r ∈ OT.Dom ] ((r OT.≺ b) × (C.col r ≡ y))
              → ⟨ y ∈ˢ fst C.otL ⟩

The predecessor's collapse is transported to y along its equation, completing the transitivity proof by placing y inside the image.

        inner (r , _ , e2) =
          subst (λ w → ⟨ w ∈ˢ fst C.otL ⟩) e2 (C.otL-in r)

For a hierarchy element w, the fibre Fib w consists of an index b together with an equality col b = w. Thus an inhabitant of this fibre is precisely a preimage of w under the collapse.

  Fib : V ℓ → Type (ℓ-suc ℓ)
  Fib w = Σ[ b ∈ OT.Dom ] (C.col b ≡ w)

Injectivity of col makes each fibre a proposition. If b and b' both collapse to w, their equations identify col b with col b', so injectivity identifies the indices. The ambient hierarchy V ℓ is a set, hence each equality type col b = w is a proposition and its proofs add no further distinction.

  isPropFib : (w : V ℓ) → isProp (Fib w)
  isPropFib w (b , e) (b' , e') =
    Σ≡Prop (λ _ → setIsSet _ _) (I.col-inj b b' (e ∙ sym e'))

Membership w∈otL supplies a preimage index only under propositional truncation. Since Fib w has just been shown to be a proposition, the truncation can be eliminated to recover the unique index whose collapse value is w.

  fib : (w : V ℓ) → ⟨ w ∈ˢ fst C.otL ⟩ → Fib w
  fib w h = PT.rec (isPropFib w) (λ z → z) (C.otL-out w h)

The unique preimage just obtained lets the collapse table be read in reverse on all of otL. The represented source member lies in P, so the inverse construction produces a graph in L and, in particular, the internal coded injection Back.injL : InjL otL P used below.

  module Back where
    open I.Inverse C.otL P (λ w mw → fib (fst w) mw)
      (λ w mw → OT.up-mem (fib (fst w) mw .fst)) public
      using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )

Let μ denote the collapse ordinal otL. Ordinal trichotomy compares μ with the successor cardinal δ. The helper from-sub isolates the common construction for the equality and δ∈μ branches: whenever every member of δ is also a member of μ, it will produce the desired InjL δ P.

  result : InjL δ P
  result = go (ord-tri (fst C.otL) ot-ord (fst δ) ordδ)
    where
    from-sub : ((z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst C.otL ⟩)
             → InjL δ P

The inclusion coding packages the subset fact into a coded injection from δ into the collapse image, and the reverse-collapse injection composes it into the power set.

    from-sub sub =
      injl-trans δ C.otL P (inclusion-coded δ C.otL sub) Back.injL

Trichotomy first considers μ∈δ. In this branch, below-succ-injects applies the successor-cardinal facts to obtain InjL μ κ. Composing it with InjL P μ gives InjL P κ, contradicting the internal Cantor theorem. This rules out exactly the case in which the collapse ordinal is strictly below δ.

    go : Tri (fst C.otL) (fst δ) → InjL δ P
    go (inl ot∈δ)       = Empty.rec (Cantor.no-inj zf κ
      (injl-trans P C.otL κ power-into-ot
        (below-succ-injects κ δ sc C.otL ot-ord ot∈δ)))
    go (inr (inl e))    =

Both remaining cases give the containment needed by from-sub. If μ=δ, transport sends every membership in δ to membership in μ. If δ∈μ, transitivity of the ordinal μ gives the same containment δ⊆μ. Coding this inclusion and composing it with the reverse-collapse injection yields InjL δ P in either case.

      from-sub (λ z h → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) h)
    go (inr (inr δ∈ot)) =
      from-sub (λ z h → ot-ord .fst h δ∈ot)

The successor cardinal reaches the power set

The theorem receives a successor-cardinal witness sc and a propositionally truncated injection InjL (𝒫 κ) δ. It may inspect a particular graph G only within a local branch, because the target InjL δ (𝒫 κ) is itself a proposition. The additional hypothesis κ∉ω occurs in the statement of SuccIntoPower but is not used by this proof. In the GCH assembly, succCardExists supplies only a truncated choice of δ together with sc; power-into-succ separately constructs pis : InjL (𝒫 κ) δ, which is then passed to succ-into-power. The result records two truncated coded-injection existences. It does not select either graph or produce a bijection, a set equality, or a cardinal equation.

succ-into-power : (zf : ModelL.isZFModel) → SuccIntoPower zf
succ-into-power zf κ δ κ∉ω sc =
  PT.rec squash₁ (λ { (G , code) → Build.result zf κ δ sc G code })