---
title: "Injecting the successor cardinal into the power set"
module: L.GCH.SuccessorIntoPowerSet
lang: en
site: "Bedrock"
description: "Injecting the successor cardinal into the power set"
stage: "Proving GCH"
reading_order: 113
canonical: https://bedrock.institute/en/L.GCH.SuccessorIntoPowerSet.html
html: L.GCH.SuccessorIntoPowerSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SuccessorIntoPowerSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.ZFModel, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Axioms.Full, L.Cardinal, L.InjectionComposition, L.Coding.Model, L.Coding.Injection, L.GCH.BelowSuccessorCardinal, L.GCH.Assembly, L.DefinableInjection, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.SuccessorIntoPowerSet.md, https://bedrock.institute/ja/L.GCH.SuccessorIntoPowerSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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 `δ`.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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 `𝒫 κ`.

```agda
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.

```agda
  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.

```agda
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.

```agda
  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.

```agda
  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.

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

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

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    opaque
      φD : Formula SL.S 1
      φ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.

```agda
      φ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.

```agda
      φ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.

```agda
    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.

```agda
    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 `κ`.

```agda
    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₀`.

```agda
    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`.

```agda
      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.

```agda
      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.

```agda
  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.

```agda
      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.

```agda
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.

```agda
  open ModelL.isZFModel zf using ( 𝒫 )
```

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

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

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

```agda
  P : SL.S
  P = 𝒫 κ
```

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

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

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

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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`.

```agda
  private
    env5 : SL.S → SL.S → SL.S → SL.S → SL.S → SL.S ^ 5
    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.

```agda
    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`.

```agda
    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`.

```agda
  private
    opaque
      φR : Formula SL.S 3
      φ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`.

```agda
          ∧̇ (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.

```agda
      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.

```agda
      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`.

```agda
    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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
    (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.

```agda
  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 `δ`.

```agda
  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.

```agda
  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.

```agda
  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 `δ`.

```agda
  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`.

```agda
  ≺-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`.

```agda
        (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.

```agda
  ≺-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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
  ≺-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`.

```agda
  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.

```agda
    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.

```agda
  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`.

```agda
  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.

```agda
  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.

```agda
      (λ { (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.

```agda
    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.

```agda
      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.

```agda
        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.

```agda
  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.

```agda
  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`.

```agda
  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.

```agda
  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`.

```agda
  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.

```agda
    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 `δ`.

```agda
    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.

```agda
      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.

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