---
title: "Assembling GCH from four internal bounds"
module: L.GCH.Assembly
lang: en
site: "Bedrock"
description: "Assembling GCH from four internal bounds"
stage: "Proving GCH"
reading_order: 97
canonical: https://bedrock.institute/en/L.GCH.Assembly.html
html: L.GCH.Assembly.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/Assembly.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, V.Hierarchy, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Axioms.Basic, L.Cardinal, L.CardinalAbove, L.GCH, L.InjectionComposition]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.GCH.Assembly.md, https://bedrock.institute/ja/L.GCH.Assembly.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
This chapter completes the stated form of GCH inside `L`. For each infinite internal ordinal cardinal `κ`, it proves, under an outer propositional truncation, that there is a successor cardinal `δ` together with the two coded injections `𝒫κ ↪ δ` and `δ ↪ 𝒫κ`. The proof may work with witnesses inside a truncated branch, but it exports neither a chosen `δ` nor either injection graph.

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

The only classical principle used in the assembly is excluded middle. It will turn a merely inhabited family of candidates into its unique least member, once the candidates have been placed in a small well-order.

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

We fix this hypothesis at the single universe level required by the proof. Thus every construction below, including the least-candidate argument, depends on the same explicit instance `LEM (ℓ-suc ℓ)`.

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

Two set-theoretic viewpoints meet here. The ambient cumulative hierarchy supplies membership and small presentations, while the constructible subuniverse supplies the predicate `isL` and the stages `Lset α`; the ZF model structure later interprets the internal power set.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Presentation {ℓ} using ( member; fiber )
open import L.Constructible {ℓ}
```

The minimization argument uses three facts about ordinals: membership in an ordinal is transitive, any two ordinals satisfy trichotomy, and the membership order on the small presentation of an ordinal is a well-order. These facts let a least candidate found in a bounded search control every competing cardinal.

```agda
  using ( 𝒮ʟ; IsOrd; Lset; Lset-mono; isL; isL-trans )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord )
open import L.Ordinal.Linear {ℓ} lem using ( Tri; ord-tri )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
```

Internal size comparisons are expressed by `InjL`, the propositional truncation of a constructible graph coding an injection. From these comparisons, `IsCardinalL` defines internal cardinals and `SuccCardL` specifies the least internal ordinal cardinal strictly above a given one; `CardAboveL` supplies only some larger cardinal, still under truncation.

```agda
  using ( SWO; IsLeast; leastOf; module SWO )
open import L.Axioms.Basic {ℓ} using ( isL-Lset )
open import L.Cardinal {ℓ} lem
  using ( InjL; SuccCardL; IsCardinalL; module LeastCardInjL )
open import L.CardinalAbove {ℓ} lem using ( CardAboveL )
```

The final GCH statement asks for a successor cardinal together with coded injections in both directions between it and the model's power set. To construct the forward comparison, inclusions will first be coded as injections and then composed with the injection that counts a constructible stage.

```agda
open import L.GCH {ℓ} lem using ( GCHStatement )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

The bounded search is made small by using the presentation of the ordinal `sucV (fst θ)`. Its indices represent the members of `sucV (fst θ)`, hence ordinals no larger than `θ`; `ω` is used separately to express that the cardinal under study is not finite. When two constructible pairs have equal underlying sets, propositionhood of constructibility lifts that equality to the pairs themselves.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
```

Trichotomy will be analyzed through three coproduct branches. Impossible branches end in the empty type, while propositional truncation records existence without exposing a chosen witness; its eliminations below therefore always target propositions such as membership or another truncated existence statement.

```agda
open import Cubical.Data.Sum using ( inl; inr )
open import Cubical.Foundations.HLevels using ( isPropΠ; isProp× )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
```

Membership written `_∈ˢ_` is ambient membership in the cumulative hierarchy. This is the relation needed for pointwise containments, including the claim that every ambient member of a constructible subset of `κ` also belongs to `κ`.

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
```

We write `SV` for the ambient proposition-valued set-theoretic structure. Its carrier includes every set over which the pointwise subset hypotheses range.

```agda
module SV = hPropStructure 𝒮ᵥ
```

We write `SL` for the corresponding structure restricted to constructible sets. Its elements pair an underlying ambient set with a proof that the set lies in `L`.

```agda
module SL = hPropStructure 𝒮ʟ
```

The ZF model structure on `SL` supplies the specified internal power set `𝒫κ`. Hence every later reference to a power set concerns the power set of the constructible model, rather than the ambient power set in the whole cumulative hierarchy.

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
```

## Four internal estimates

The first interface says what it means for a stage to be counted: for every pair of a constructible ordinal `δ` and a set `Lδ` whose underlying set is the stage `Lset δ`, if `δ` is not finite, then the stage injects into the ordinal. The type excludes finite ordinals and produces only the truncated existence of a coded injection.

```agda
StageCountedCoded : Type (ℓ-suc ℓ)
StageCountedCoded =
    (δ Lδ : SL.S) → IsOrd (fst δ) → (⟨ fst δ ∈ˢ ω ⟩ → Empty.⊥)
  → fst Lδ ≡ Lset (fst δ) → InjL Lδ δ
```

The second interface states the bounded-subset theorem. For an ordinal internal cardinal `κ` that is not finite, and any constructible set `y` whose ambient members all belong to `κ`, there is, merely, an ordinal `β` such that `y` lies in the stage `Lset β` and `β` injects into `κ`. The subset hypothesis quantifies over ambient sets, which covers members that carry no constructibility proof of their own.

```agda
InternalBoundedSubset : Type (ℓ-suc ℓ)
InternalBoundedSubset =
    (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (y : SL.S) → ((z : SV.S) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩)
  → ∥ Σ[ β ∈ SL.S ]
```

The produced record contains the ordinality of `β`, the landing of `y` in the stage, and the coded injection of `β` into `κ`.

```agda
       (IsOrd (fst β) × ⟨ fst y ∈ˢ Lset (fst β) ⟩ × InjL β κ) ∥₁
```

The third interface is a conditional reverse comparison: given that the internal power set of `κ` injects into a successor cardinal `δ` of `κ`, it returns the reverse injection of `δ` into the power set. The hypothesis is genuinely conditional; the interface cannot be invoked from the successor-cardinal record alone.

```agda
SuccIntoPower : ModelL.isZFModel → Type (ℓ-suc ℓ)
SuccIntoPower zf =
    (κ δ : SL.S) → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥) → SuccCardL δ κ
  → InjL (𝒫 κ) δ → InjL δ (𝒫 κ)
  where open ModelL.isZFModel zf using ( 𝒫 )
```

The fourth interface states the mere existence of a successor cardinal: for every infinite internal ordinal cardinal, some successor cardinal exists. The conclusion is truncated, so a caller cannot select a global representative from it.

```agda
SuccCardExists : Type (ℓ-suc ℓ)
SuccCardExists =
    (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ
  → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → ∥ Σ[ δ ∈ SL.S ] SuccCardL δ κ ∥₁
```

## Larger internal cardinals exist

The reduction module fixes an ordinal internal cardinal `θ` strictly above `κ` and proves that, within the small search space determined by the successor of `θ`, a least cardinal above `κ` exists. This is the heart of the chapter: first fix an explicit upper bound, then minimize inside it.

```agda
module Reduce (κ : SL.S) (oκ : IsOrd (fst κ))
              (θ : SL.S) (oθ : IsOrd (fst θ))
              (cθ : IsCardinalL θ) (κ∈θ : ⟨ fst κ ∈ˢ fst θ ⟩) where
```

The earlier cardinal machinery supplies a map `up` from indices in the small presentation of the ordinal `sucV (fst θ)` to constructible sets. It also supplies an index `self` that presents `θ` itself and an equation `self-eq` identifying the underlying set of `up self` with `θ`. Thus the known cardinal `θ` occurs among the candidates of the bounded search.

```agda
  open LeastCardInjL θ oθ using ( up; self; self-eq )
```

The search space is the small presentation of the ordinal successor `sucV (fst θ)`. It is a presentation of an ordinal, not a constructible stage `Lset (fst θ)`.

```agda
  A : Type ℓ
  A = ⟪ sucV (fst θ) ⟫
```

Membership on the ordinal `sucV (fst θ)` induces a strict well-order on this presentation. That well-order makes it possible to search the small candidate family for a least member.

```agda
  opaque
    w : SWO A
    w = ordSWO (sucV (fst θ)) (suc-ord oθ)
```

For presentation indices `m` and `n`, the induced relation `m < n` holds exactly when the ordinal represented by `m` belongs to the ordinal represented by `n`. Consequently, being earlier in the search order has the intended mathematical meaning of being a smaller ordinal.

```agda
  opaque
    unfolding w
    w-lt : (m n : A) → SWO._<∙_ w m n
         ≡ ⟨ ⟪ sucV (fst θ) ⟫↪ m ∈ˢ ⟪ sucV (fst θ) ⟫↪ n ⟩
    w-lt m n = refl
```

Internal cardinality is a proposition. Indeed, `IsCardinalL x` says, for every constructible member `δ` of `x`, that any coded injection from `x` into `δ` leads to the empty type; dependent function types with proposition-valued conclusions remain propositions. This allows cardinality to form one component of the proposition-valued candidate predicate below.

```agda
  isPropIsCardinalL : (x : SL.S) → isProp (IsCardinalL x)
  isPropIsCardinalL x =
    isPropΠ (λ _ → isPropΠ (λ _ → isPropΠ (λ _ → Empty.isProp⊥)))
```

The candidate predicate asks two things of an index: the constructible set it presents is an internal cardinal, and `κ` belongs to it. Ordinality need not be stored in the predicate, because every presented set is a member of the ordinal `sucV (fst θ)` and is therefore itself an ordinal.

```agda
  Good : A → hProp (ℓ-suc ℓ)
  Good b = (IsCardinalL (up b) × ⟨ fst κ ∈ˢ fst (up b) ⟩)
         , isProp× (isPropIsCardinalL (up b)) (snd (fst κ ∈ˢ fst (up b)))
```

The index presenting `θ` itself presents a constructible set whose underlying set is `θ`, by the propositionhood of constructibility.

```agda
  upSelf : up self ≡ θ
  upSelf = Σ≡Prop (λ x → snd (isL x)) self-eq
```

The candidate class is nonempty: the index presenting `θ` is a candidate, carrying the cardinality and the membership transported along that identification.

```agda
  nonempty : ∥ Σ[ b ∈ A ] ⟨ Good b ⟩ ∥₁
  nonempty = ∣ self
            , subst (λ z → IsCardinalL z × ⟨ fst κ ∈ˢ fst z ⟩)
                (sym upSelf) (cθ , κ∈θ) ∣₁
```

The well order of the search space then produces an actual least candidate, with its leastness proof. The least-witness type is a proposition, so the truncation of nonemptiness can be eliminated here; the search itself uses excluded middle.

```agda
  least : Σ[ b ∈ A ] IsLeast w Good b
  least = leastOf w lem Good nonempty
```

Name the constructible set presented by the least candidate `δ`. The following argument verifies that its local leastness in the bounded search gives all four clauses of `SuccCardL δ κ`, including leastness against every competing internal ordinal cardinal above `κ`.

```agda
  δ : SL.S
  δ = up (fst least)
```

By the presentation's membership record, the underlying set of `δ` belongs to the ordinal `sucV (fst θ)`. Thus the construction proves only `fst δ ∈ sucV (fst θ)`, which places `δ` at or below `θ`; it does not assert `fst δ ∈ fst θ`.

```agda
  δ∈sθ : ⟨ fst δ ∈ˢ sucV (fst θ) ⟩
  δ∈sθ = member (sucV (fst θ)) (fst least)
```

The underlying set of `δ` is an ordinal, because it is a member of the ordinal successor of an ordinal.

```agda
  oδ : IsOrd (fst δ)
  oδ = mem-ord {A = sucV (fst θ)} (suc-ord oθ) (fst δ) δ∈sθ
```

The least candidate is an internal cardinal, read off the candidate record.

```agda
  cδ : IsCardinalL δ
  cδ = fst (fst (snd least))
```

The given cardinal lies below the least candidate, also read off the candidate record.

```agda
  κ∈δ : ⟨ fst κ ∈ˢ fst δ ⟩
  κ∈δ = snd (fst (snd least))
```

Leastness says that no earlier index of the search space is a candidate.

```agda
  δ-min : (b : A) → ⟨ Good b ⟩ → (SWO._<∙_ w b (fst least) → Empty.⊥)
  δ-min = snd (snd least)
```

Global leastness is stated as a containment: for every ordinal internal cardinal `c` above `κ`, every member of `δ` belongs to `c`. This is exactly the last clause of the successor-cardinal record, and the proof compares the ordinals `δ` and `c`.

```agda
  leastness : (c : SL.S) → IsOrd (fst c) → IsCardinalL c
            → ⟨ fst κ ∈ˢ fst c ⟩
            → (x : SL.S) → ⟨ fst x ∈ˢ fst δ ⟩ → ⟨ fst x ∈ˢ fst c ⟩
  leastness c oc cc κ∈c = go (ord-tri (fst δ) oδ (fst c) oc)
    where
```

The three trichotomy cases are handled directly: if `δ` lies below `c`, the transitivity of `c` gives the containment; if they are equal, the equation transports the containment; if `c` lies below `δ`, a contradiction is derived from the leastness.

```agda
    go : Tri (fst δ) (fst c)
       → (x : SL.S) → ⟨ fst x ∈ˢ fst δ ⟩ → ⟨ fst x ∈ˢ fst c ⟩
    go (inl δ∈c)       x x∈δ = oc .fst x∈δ δ∈c
    go (inr (inl e))   x x∈δ = subst (λ v → ⟨ fst x ∈ˢ v ⟩) e x∈δ
    go (inr (inr c∈δ)) x x∈δ = Empty.rec (δ-min b bGood b<δ)
```

In the remaining case, `c ∈ δ`. Since `fst δ ∈ sucV (fst θ)` and the ordinal `sucV (fst θ)` is transitive, it follows that `fst c ∈ sucV (fst θ)`. Only this contradictory branch needs to pull the competing cardinal back into the bounded search space; no prior bound on an arbitrary competitor was assumed.

```agda
      where
      c∈sθ : ⟨ fst c ∈ˢ sucV (fst θ) ⟩
      c∈sθ = suc-ord oθ .fst c∈δ δ∈sθ
      b : A
      b = fiber (sucV (fst θ)) c∈sθ .fst
```

The recovered index presents exactly `c`, and the constructible set it presents is therefore `c` itself; the candidate predicate for this index is obtained by transporting the cardinality and the membership of `c` along that identification.

```agda
      be : ⟪ sucV (fst θ) ⟫↪ b ≡ fst c
      be = fiber (sucV (fst θ)) c∈sθ .snd
      upb : up b ≡ c
      upb = Σ≡Prop (λ v → snd (isL v)) be
      bGood : ⟨ Good b ⟩
```

The membership of `c` below `δ` is then converted into the strict order of the search space, contradicting the leastness of the selected index.

```agda
      bGood = subst (λ z → IsCardinalL z × ⟨ fst κ ∈ˢ fst z ⟩)
                (sym upb) (cc , κ∈c)
      b<δ : SWO._<∙_ w b (fst least)
      b<δ = transport (λ i → sym (w-lt b (fst least)) i)
              (subst (λ v → ⟨ v ∈ˢ fst δ ⟩) (sym be) c∈δ)
```

`CardAboveL` supplies only the propositionally truncated existence of some ordinal internal cardinal `θ` with `κ ∈ θ`; it supplies no leastness and does not select `θ`. The proof maps each local witness through `Reduce`, where minimization occurs inside the presentation of `sucV (fst θ)`. The resulting successor cardinal therefore remains under propositional truncation.

```agda
succCardExists : SuccCardExists
succCardExists κ oκ cκ κ∉ω = PT.map build (CardAboveL κ oκ cκ κ∉ω)
  where
  build : Σ[ θ ∈ SL.S ]
            (IsOrd (fst θ) × IsCardinalL θ × ⟨ fst κ ∈ˢ fst θ ⟩)
```

Within one local branch, `build` packages the chosen `δ` with the four clauses of `SuccCardL δ κ`: `δ` is an ordinal, it is an internal cardinal, `κ ∈ δ`, and `δ` is contained in every ordinal internal cardinal lying above `κ`.

```agda
        → Σ[ δ ∈ SL.S ] SuccCardL δ κ
  build (θ , oθ , cθ , κ∈θ) = R.δ , R.oδ , R.cδ , R.κ∈δ , R.leastness
    where module R = Reduce κ oκ θ oθ cθ κ∈θ
```

## Discharging the structural estimates

A stage whose index is an ordinal is constructible, by the axiom relating stages and constructibility.

```agda
stage-is-L : (δ : SL.S) → IsOrd (fst δ) → ⟨ isL (Lset (fst δ)) ⟩
stage-is-L δ ordδ = isL-Lset (fst δ) ordδ
```

The bridging predicate for the power set states its content: for two constructible sets `κ` and `y`, with `κ` an ordinal and `y` a member of the model's power set of `κ`, every ambient member `z` of `y` is constructible, belongs to `κ`, and is an ordinal.

```agda
zStrongest : ModelL.isZFModel → Type (ℓ-suc ℓ)
zStrongest zf =
    (κ y : SL.S) → IsOrd (fst κ) → ⟨ fst y ∈ˢ fst (𝒫 κ) ⟩
  → (z : SV.S) → ⟨ z ∈ˢ fst y ⟩
  → (⟨ isL z ⟩ × ⟨ z ∈ˢ fst κ ⟩ × IsOrd z)
```

The bridge depends on the chosen ZF model because its premise refers to that model's specified power set. Thus `𝒫κ` here remains the internal power set of `L` throughout the argument.

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

The subtle point is a change of domains. Power-set membership yields a subset statement quantified over constructible sets, whereas `z` initially ranges over the ambient hierarchy. Transitivity of `L` first makes `z` available as a constructible set; only then can the internal subset statement be applied, after which ordinality follows from `z ∈ κ` and the ordinality of `κ`.

```agda
z-strongest : (zf : ModelL.isZFModel) → zStrongest zf
z-strongest zf κ y ordκ y∈𝒫κ z z∈y = isLz , z∈κ , mem-ord {A = fst κ} ordκ z z∈κ
  where
  open ModelL.isZFModel zf using ( 𝒫; hasPower )
```

The constructibility of `z` follows by transitivity: `z` belongs to the constructible set `y`, which is itself constructible.

```agda
  isLz : ⟨ isL z ⟩
  isLz = isL-trans z∈y (snd y)
```

The defining specification of the model's power set identifies `y ∈ 𝒫κ` with the internal subset relation `y ⊆ κ`. This relation quantifies over elements of `SL`, so the constructibility established in the preceding step is essential.

```agda
  y⊆κ : ⟨ y ModelL.⊆ˢ κ ⟩
  y⊆κ = subst ⟨_⟩ (ModelL.℩-spec (hasPower κ) y) y∈𝒫κ
```

The internal subset relation is then applied to the pair of `z` and its constructibility, yielding membership of `z` in `κ`.

```agda
  z∈κ : ⟨ z ∈ˢ fst κ ⟩
  z∈κ = y⊆κ (z , isLz) z∈y
```

## Every subset lands before the successor

The landing lemma is stated for the model, the bounded-subset interface, and a fixed successor cardinal `δ` of `κ`: every member of the model's power set of `κ` lies in the stage `Lset δ`.

```agda
stage-landing :
    (zf : ModelL.isZFModel) → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : SL.S) → SuccCardL δ κ
  → (y : SL.S) → ⟨ fst y ∈ˢ fst (ModelL.isZFModel.𝒫 zf κ) ⟩
```

For each fixed `y`, the bounded-subset theorem returns a suitable stage index `β` only under propositional truncation. The desired conclusion `y ∈ Lset δ` is itself a proposition, so the proof may reason with a local `β` without choosing such indices uniformly. The ambient pointwise subset hypothesis required by that theorem is exactly the bridge just established.

```agda
  → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
stage-landing zf ibs κ ordκ cardκ κ∉ω δ (ordδ , cardδ , κ∈δ , _) y y∈𝒫κ =
  PT.rec (snd (fst y ∈ˢ Lset (fst δ))) place (ibs κ ordκ cardκ κ∉ω y y⊆κ)
  where
  y⊆κ : (z : SV.S) → ⟨ z ∈ˢ fst y ⟩ → ⟨ z ∈ˢ fst κ ⟩
```

From `y ∈ 𝒫κ` and `z ∈ y`, the strongest-member lemma yields `z ∈ κ`. Its proof first uses the transitivity of `L` to recognize the ambient member `z` as constructible, so that the internal subset relation expressed by power-set membership can be applied to it.

```agda
  y⊆κ z z∈y = z-strongest zf κ y ordκ y∈𝒫κ z z∈y .snd .fst
```

No injection from `δ` into `κ` can exist, because `δ` is an internal cardinal and `κ` is a member of `δ`. This refutation is the tool used to eliminate the impossible trichotomy branches below.

```agda
  no-δ↪κ : InjL δ κ → Empty.⊥
  no-δ↪κ = cardδ κ κ∈δ
```

For the fixed subset `y`, the bounded-subset estimate supplies, under propositional truncation, an ordinal `β` such that `y ∈ Lset β` and there is an internal coded injection `β ↪ κ`. Once such a witness is exposed locally, `place` compares `β` with `δ` by ordinal trichotomy and proves that `y` already belongs to `Lset δ`.

```agda
  place : Σ[ β ∈ SL.S ]
            (IsOrd (fst β) × ⟨ fst y ∈ˢ Lset (fst β) ⟩ × InjL β κ)
        → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
  place (β , ordβ , y∈Lβ , β↪κ) = go (ord-tri (fst β) ordβ (fst δ) ordδ)
    where
```

If `β` lies below `δ`, monotonicity of the tower directly places the member at the lower stage inside the higher stage. If `β` equals `δ`, the injection `β ↪ κ` would become an injection `δ ↪ κ`, contradicting the cardinality of `δ`.

```agda
    go : Tri (fst β) (fst δ) → ⟨ fst y ∈ˢ Lset (fst δ) ⟩
    go (inl β∈δ)       = Lset-mono β∈δ y∈Lβ
    go (inr (inl e))   = Empty.rec (no-δ↪κ (subst (λ b → InjL b κ) β≡δ β↪κ))
      where
      β≡δ : β ≡ δ
```

In the equality branch, equality of the underlying sets lifts to equality of the corresponding elements of `L` because constructibility is proposition-valued. In the remaining branch, where `δ ∈ β`, the inclusion `δ ↪ β` followed by the given coded injection `β ↪ κ` would produce the forbidden coded injection `δ ↪ κ`.

```agda
      β≡δ = Σ≡Prop (λ x → snd (isL x)) e
    go (inr (inr δ∈β)) = Empty.rec (no-δ↪κ
      (injl-trans δ β κ (inclusion-coded δ β δ⊆β) β↪κ))
      where
      δ⊆β : (z : SV.S) → ⟨ z ∈ˢ fst δ ⟩ → ⟨ z ∈ˢ fst β ⟩
```

The inclusion is the transitivity of the ordinal `β` applied to the two memberships.

```agda
      δ⊆β z z∈δ = ordβ .fst z∈δ δ∈β
```

## Coding the power set below the successor

The power-set comparison now follows from the chain `𝒫κ ↪ Lset δ ↪ δ`. The first arrow comes from the fact that every member of the internal power set lies in `Lset δ`, and the second counts that constructible stage by `δ`. No stage index is chosen uniformly for the members of `𝒫κ`.

```agda
power-into-succ :
    (zf : ModelL.isZFModel) → StageCountedCoded → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (fst κ) → IsCardinalL κ → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  → (δ : SL.S) → SuccCardL δ κ
  → InjL (ModelL.isZFModel.𝒫 zf κ) δ
```

Pointwise containment is first converted by `inclusion-coded` into the coded injection `𝒫κ ↪ Lset δ`. The stage-counting hypothesis supplies `Lset δ ↪ δ`, and `injl-trans` composes the two. Since both comparisons are expressed by `InjL`, their witnessing graphs remain propositionally truncated.

```agda
power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc@(ordδ , _ , κ∈δ , _) =
  injl-trans (𝒫 κ) Lδ δ (inclusion-coded (𝒫 κ) Lδ into)
    (scc δ Lδ ordδ δ∉ω refl)
  where
  open ModelL.isZFModel zf using ( 𝒫 )
```

The stage at `δ` is presented as an element of `L` by pairing the stage set with its constructibility certificate, obtained from the ordinality of `δ`.

```agda
  Lδ : SL.S
  Lδ = Lset (fst δ) , stage-is-L δ ordδ
```

The successor cardinal `δ` lies outside `ω`: if it were inside, the membership `κ ∈ δ` would force `κ ∈ ω` by transitivity of `ω`, contradicting the hypothesis.

```agda
  δ∉ω : ⟨ fst δ ∈ˢ ω ⟩ → Empty.⊥
  δ∉ω δ∈ω = κ∉ω (ω-ord .fst {x = fst δ} {y = fst κ} κ∈δ δ∈ω)
```

Every member of the power set is landed inside `Lset δ` by the landing lemma, with its constructibility supplied through the transitivity of `L` from the power-set membership.

```agda
  into : (z : SV.S) → ⟨ z ∈ˢ fst (𝒫 κ) ⟩ → ⟨ z ∈ˢ fst Lδ ⟩
  into z z∈ =
    stage-landing zf ibs κ ordκ cardκ κ∉ω δ sc (z , isL-trans z∈ (snd (𝒫 κ))) z∈
```

## The generalized continuum hypothesis

The final theorem keeps the two directions logically separate. Stage counting and the bounded-subset theorem establish `𝒫κ ↪ δ`. Only after that injection has been obtained does the independent conditional theorem `SuccIntoPower` apply, using it together with the successor-cardinal facts to establish `δ ↪ 𝒫κ`.

```agda
gch-from-internal-bill :
    (zf : ModelL.isZFModel)
  → StageCountedCoded → InternalBoundedSubset → SuccIntoPower zf
  → GCHStatement zf
gch-from-internal-bill zf scc ibs sip κ ordκ cardκ κ∉ω =
```

The theorem `succCardExists` gives only the propositionally truncated existence of a successor cardinal `δ`. The map therefore works inside each local witness: `step` keeps the successor-cardinal proof, constructs the truncated coded injection `𝒫κ ↪ δ` by the landing argument, and passes that result to the independent conditional interface to obtain the truncated coded injection `δ ↪ 𝒫κ`.

```agda
  PT.map step (succCardExists κ ordκ cardκ κ∉ω)
  where
  open ModelL.isZFModel zf using ( 𝒫 )
  step : Σ[ δ ∈ SL.S ] SuccCardL δ κ
       → Σ[ δ ∈ SL.S ] (SuccCardL δ κ × InjL (𝒫 κ) δ × InjL δ (𝒫 κ))
```

The landing argument supplies `pis : InjL (𝒫 κ) δ`, and the independent conditional interface uses `pis` to supply `InjL δ (𝒫 κ)`. Each `InjL` is the propositional truncation of the existence of a constructible injection code, so the result records exactly two opposite coded-injection existences; it does not select either graph or construct a bijection, a set equality, or a cardinal-arithmetic equality.

```agda
  step (δ , sc) = δ , sc , pis , sip κ δ κ∉ω sc pis
    where
    pis : InjL (𝒫 κ) δ
    pis = power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc
```