---
title: "Injecting an infinite constructible stage into its index"
module: L.GCH.StageInjection
lang: en
site: "Bedrock"
description: "Injecting an infinite constructible stage into its index"
stage: "Proving GCH"
reading_order: 118
canonical: https://bedrock.institute/en/L.GCH.StageInjection.html
html: L.GCH.StageInjection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/StageInjection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.Renaming, FOL.Absoluteness, V.Hierarchy, V.Collapse, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals, L.Stage, L.Cardinal, L.GCH.Assembly, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.SkolemHull, L.GCH.ConstructibleHull, L.GCH.CardinalSquareLaw, L.GCH.AdequateStages, L.GCH.StageCountingTools, L.GCH.HullCounting]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.StageInjection.md, https://bedrock.institute/ja/L.GCH.StageInjection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Injecting an infinite constructible stage into its index

This chapter proves the stage estimate used in GCH: if `δ` is a non-finite constructible ordinal, then `Lset δ` admits an internal coded injection into `δ`. The conclusion `InjL` is the propositional truncation of the type of constructible graphs satisfying the injection conditions. Thus it asserts that such a graph exists, without retaining a chosen graph; it asserts neither a host-level function nor a bijection, and it does not assume that `δ` is itself an internal cardinal.

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

The proof repeatedly separates existence from choice. Classical reasoning supplies suitable stages and cardinal representatives, while every exported injection remains under propositional truncation. Local witnesses may therefore be used inside propositional arguments without turning them into canonical global data.

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

The argument is uniform in the universe level and uses only the displayed instance `lem : LEM (ℓ-suc ℓ)` of excluded middle. In particular, the later passage to an internal cardinal representative does not add a hidden assumption that the original ordinal `δ` is a cardinal.

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

To turn the inverse collapse into an injection inside `L`, its graph must be expressed in the first-order language of the constructible structure. Only variables, constants, membership, and conjunction are needed. Formula renaming will exchange the two argument positions while preserving satisfaction, and the ambient cumulative hierarchy supplies the sets on which the collapse is computed.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

The collapse will be injective because the hull carries the required extensionality. Later, `self∈sucV` places `δ` in its set-theoretic successor `δ+1`, while the constructible-stage lemmas provide transitivity, monotonicity, and the passage between a stage and its layers. Ordinal successors are kept distinct from successor stages throughout this argument.

```agda
open import V.Collapse {ℓ} using ( isExt )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( #∈ω; suc-ord )
```

Two complementary stage facts will be used. A constructible stage can be packaged as an element of `L`, and if an ordinal `x` belongs to the stage `Lset α`, then rank comparison yields `x ∈ α`. The target `InjL` records the mere existence of an internal coded injection, while `IsCardinalL` will apply only to the cardinal representative introduced later.

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset→∈ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Cardinal {ℓ} lem using ( InjL; IsCardinalL )
```

The desired estimate has the interface `StageCountedCoded`. Its proof first replaces the arbitrary infinite ordinal `δ` by an internal cardinal representative `μ`, counts a suitable Skolem hull into `μ`, and then composes coded injections. To make the inverse collapse participate in this chain, it will be presented as a definable map whose graph is a set of `L`.

```agda
open import L.GCH.Assembly {ℓ} lem using ( StageCountedCoded )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.SkolemHull {ℓ} lem
```

The global comparison will combine three ingredients. Condensation turns a hull into a stage `Lset β`; the shift for non-finite ordinals and the cardinal representative `μ` make the starting set injectable into `μ`; and composition transports these local comparisons back to the desired endpoints. None of these steps changes an internal coded injection into a host-level function.

```agda
  using ( module Frame; module HullStage; module HullElemDown )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module PiIn; module Condense′ )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( ordL; ω⊆; no-fin; module Shift )
open import L.GCH.AdequateStages {ℓ} lem using ( superadequate-above; Superadequate )
open import L.GCH.StageCountingTools {ℓ} lem using ( move )
```

The hull-count theorem is the quantitative input: once its starting set injects into a non-finite internal cardinal, the generated hull does too. We will also use that every ordinal is contained in its own constructible stage, and that equality of the underlying sets determines equality of elements of the constructible carrier because their constructibility proofs are propositions.

```agda
open import L.GCH.HullCounting {ℓ} lem using ( ord⊆Lset; module Count; S≡ )
```

The inverse collapse will be compared as a map between elements of the constructible carrier `S`. Such an element includes both an underlying set and a constructibility proof, but the proof component is propositional. Consequently, equality of underlying sets determines equality in `S`, so the coded graph does not depend on which constructibility evidence presents its values.

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
```

Non-finiteness enters the later counting argument in two concrete ways. It provides the shift injection `δ+1 ↪ δ`, and it implies that every finite ordinal, in particular the empty set, lies below `δ`. The length-two environments used for the inverse-collapse formula are independent of this infinitude argument.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet; ∅ )
open InfinitySet {ℓ} using ( ω; sucV )
open import Cubical.Data.Vec using ( _∷_; [] )
import Cubical.Data.Empty as Empty
```

Propositional truncation appears at two decisive points. It lets the proof use the mere constructibility of the hull when establishing a propositional satisfaction statement, and it is also the outer form of every conclusion `InjL`. Elimination is therefore always into a proposition.

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( squash₁ )
```

Membership written `_∈ˢ_` is membership in the ambient hierarchy structure `𝒮ᵥ`. It is used for statements about the hull, its collapse image, and ordinal indices before those sets are packaged as elements of the constructible structure.

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

The type `S` is the carrier of the constructible structure: an element consists of an ambient set together with a proof that it belongs to `L`. Domains, codomains, and graph parameters of the internal coded maps below all live in this carrier.

```agda
open hPropStructure 𝒮ʟ using ( S )
```

Satisfaction of an object-language formula in `𝒮ʟ` is read through absoluteness as the corresponding proposition about ambient sets. This bridge lets the proof establish the inverse-collapse graph externally and then package the same relation as a definable graph inside `L`.

```agda
open FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using () renaming ( _⊨ᵐ_ to _⊨_ )
```

There is one small mismatch of conventions to resolve. The collapse formula `piFo` is read with its value and preimage in the order `(v,x)`, whereas the definable-map graph is evaluated in the order `(x,v)`. Swapping the two free variables and using invariance of satisfaction under renaming expresses the same relation in the required order; no model or formula meaning is changed.

```agda
module Ren = Sat 𝒮ʟ id using ( Agrees; ⊨-rename )
```

## Counting the hull at a strengthened adequate stage

We first isolate the geometric part of the argument from its later cardinal estimate. Fix an ordinal `lam` closed under successors and a starting set `X` contained in `Lset lam`; assume also that the index contains the empty set and that the Skolem hull generated from `X` is elementary in the required sense. No target cardinal is involved at this point.

```agda
module Site (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆Lλ ∅∈λ)
```

Superadequacy of `lam` supplies the closure and correctness conditions required by condensation. Constructibility of `X` ensures that the successive finite closure stages used to generate the hull, and hence their union, remain in `L`. The hull and its collapse image can therefore both be represented inside the constructible structure.

```agda
  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩) where
```

Condensation now identifies the collapse image with `Lset β` for some ordinal `β`. Independently, the hull construction proves that the hull `M` is constructible. These are exactly the two facts needed to regard the inverse collapse as a map from a constructible stage to a constructible hull.

```agda
  condenses′ = Condense′.condenses′ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
  M-isL = Condense′.M-isL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

Write `π : M → πX` for the collapse and `πX` for its image. The collapse machinery supplies preimages of points in `πX`, injectivity on the extensional hull, and the fact that transitive parts of the hull are fixed. The formula `piFo` represents the graph of `π`; its adequacy lemmas will connect satisfaction of that formula with the actual collapse value.

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( πX; π; fixes; πX-intro; πX-member )
  module P = PiIn (HS.M , M-isL) using ( piFo; up; good-at; piFo-val )
```

The ordinal `β` measures the height of the collapse image. At this general site there is no ordinal `δ` to be counted and no target cardinal, so no comparison between `β` and either of them is available yet.

```agda
  β : V ℓ
  β = condenses′ .fst
```

The accompanying proof that `β` is an ordinal makes `Lset β` a genuine ordinal-indexed stage. It will also be essential later when membership of an ordinal in `Lset β` is converted into an ordinal comparison with `β`.

```agda
  oβ : IsOrd β
  oβ = condenses′ .snd .fst
```

The equality `ext : πX = Lset β` is the hinge between collapse theory and the constructible hierarchy. It converts membership in the collapse image into membership in the stage at `β`; later, once the collapse is shown to fix `δ`, this is exactly how `δ ∈ Lset β` will be obtained.

```agda
  ext : HSC.πX ≡ Lset β
  ext = condenses′ .snd .snd
```

Because `β` is an ordinal, `Lset β` is constructible and can be packaged as an element `Lβ` of the carrier `S`. This packaged stage will be the domain of the inverse-collapse map.

```agda
  Lβ : S
  Lβ = LsetS β oβ
```

The ordinal `β` itself is also constructible and is packaged as `βL`. Although the inverse-collapse map uses `Lβ`, the packaged index will later let the bounded-subset argument compare `β` with a target cardinal by an internal coded injection.

```agda
  βL : S
  βL = ordL β oβ
```

An internal coded map must have a codomain in the carrier `S`, not merely an externally described class of hull members. The element `hullL` supplies that internal presentation of the hull together with its constructibility evidence.

```agda
  hullL : S
  hullL = Condense′.hullL lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

The equality `M≡` connects the two presentations of the hull. Collapse theorems speak about the ambient set `M`, whereas the internal graph speaks about the carrier element `hullL`; transporting along this equality lets the same membership evidence serve on both sides.

```agda
  M≡ : fst hullL ≡ HS.M
  M≡ = Condense′.hullL-spec lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
```

The hull frame proves that membership on `M` is extensional. This is the precise hypothesis needed to deduce that two members of the hull with the same collapse value are equal.

```agda
  Mext : isExt HS.M
  Mext = Frame.Mext lam ordλ succλ X X⊆Lλ ∅∈λ
```

Applying the collapse injectivity theorem to this extensional hull yields `π-inj`. It will prove both uniqueness of each preimage and injectivity of the inverse-collapse map constructed from those preimages.

```agda
  module CI = HullStage.C.InjExt lam ordλ succλ X X⊆Lλ ∅∈λ Mext using ( π-inj )
```

A preimage of a collapse value `v` is an element `x` of the hull whose collapse equals the underlying set of `v`. The record is an untruncated dependent pair: both the preimage and its membership and its identification are carried explicitly.

```agda
  Pre : S → Type (ℓ-suc ℓ)
  Pre v = Σ[ x ∈ V ℓ ] (⟨ x ∈ˢ HS.M ⟩ × (HSC.π x ≡ fst v))
```

Preimages are unique, because the collapse is injective on the hull: two records with the same value identify their preimages through `π-inj`, and the remaining components are propositions. This is why the preimage can be recovered without choosing it.

```agda
  isPropPre : (v : S) → isProp (Pre v)
  isPropPre v (x , mx , e) (x' , mx' , e') =
    Σ≡Prop (λ x → isProp× (snd (x ∈ˢ HS.M)) (setIsSet _ _)) (CI.π-inj x x' mx mx' (e ∙ sym e'))
```

The inverse collapse is required only for points of its image, which condensation identifies with `Lset β`. Accordingly, `Mem v` is the proposition that the underlying set of `v` belongs to this stage; this domain evidence is what produces an inhabited preimage type.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem v = ⟨ fst v ∈ˢ fst Lβ ⟩
```

Membership in `Lset β` gives only the propositionally truncated type of preimages under the collapse. Since `Pre v` has already been proved to be a proposition, truncation elimination recovers its unique inhabitant. Thus `pre` uses uniqueness to obtain the inverse value; it makes no arbitrary choice among competing preimages.

```agda
  pre : (v : S) → Mem v → Pre v
  pre v m = PT.rec (isPropPre v) (λ w → w)
    (HSC.πX-member (fst v) (subst (λ w → ⟨ fst v ∈ˢ w ⟩) (sym ext) m))
```

The preimage is packaged as a constructible set: its constructibility is transported from the hull through the identification of the packaged hull with the hull itself. The function is defined only on members of the stage at `β`, with the hull as its codomain; it is the inverse of the collapse on its image, not a global inverse.

```agda
  fn : (v : S) → Mem v → S
  fn v m = pre v m .fst
         , isL-trans {x = fst hullL} {y = pre v m .fst}
             (subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)) (snd hullL)
```

The renaming swaps the two variable slots: slot zero becomes slot one and conversely.

```agda
  ρ : Fin 2 → Fin 2
  ρ zero = suc zero
  ρ (suc zero) = zero
```

The two environments list the same carrier elements in opposite orders. The proof `ag` checks at each of the two variable indices that looking up a variable after applying `ρ` agrees with looking it up in the swapped environment. This pointwise agreement is the hypothesis needed by satisfaction under renaming.

```agda
  private
    ag : (x v : S) → Ren.Agrees ρ (x ∷ v ∷ []) (v ∷ x ∷ [])
    ag x v zero = refl
    ag x v (suc zero) = refl
```

Satisfaction of the renamed formula at the ordered environment equals satisfaction of the original formula at the swapped environment; this is the transport used to arrange the collapse graph's slots.

```agda
    rn : (x v : S) → ⟨ (x ∷ v ∷ []) ⊨ renameFo ρ P.piFo ⟩ ≡ ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
    rn x v = cong ⟨_⟩ (Ren.⊨-rename ρ P.piFo (x ∷ v ∷ []) (v ∷ x ∷ []) (ag x v))
```

The inverse-collapse graph is the conjunction: the preimage belongs to the hull, and the renamed pairing graph holds of the preimage and the value.

```agda
  invFo : Formula S 2
  invFo = (var zero ∈̇ con hullL) ∧̇ renameFo ρ P.piFo
```

For a hull member `x` whose collapse is `v`, the actual pair `(v,x)` satisfies `piFo`. Constructibility of the hull is itself given through a propositional truncation, so the proof eliminates that truncation into the satisfaction statement, which is a proposition, and works at any constructible stage containing the hull.

```agda
  π-graph : (x : S) (mx : ⟨ fst x ∈ˢ HS.M ⟩) (v : S) → HSC.π (fst x) ≡ fst v
          → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
  π-graph x mx v e = PT.rec (snd ((v ∷ x ∷ []) ⊨ P.piFo)) read M-isL
    where
    read : Σ[ α ∈ V ℓ ] (IsOrd α × ⟨ HS.M ∈ˢ Lset α ⟩) → ⟨ (v ∷ x ∷ []) ⊨ P.piFo ⟩
```

The read statement transports both slots: the collapse value is identified with the underlying set of `v`, and the hull member is identified with the underlying set of `x`.

```agda
    read (α , oα , M∈Lα) =
      subst2 (λ a b → ⟨ (a ∷ b ∷ []) ⊨ P.piFo ⟩)
        (S≡ {x = HSC.π (fst x) , G .fst} {y = v} e) (S≡ {x = P.up (fst x) mx} {y = x} refl)
        (G .snd mx)
      where
```

Given a constructible stage `Lset α` containing the hull, transitivity of the layer places each hull member `x` in that same stage. The lemma `good-at` then supplies a constructibility proof for `π x` together with a proof that the packaged collapse value and the packaged member satisfy `piFo`.

```agda
      G = P.good-at α oα (fst x) mx (layer-trans (Lset-layer α) {x = HS.M} {y = fst x} mx M∈Lα)
```

The proof `defines` is the bridge from the actual inverse value to the internal formula. Its first component places that value in the packaged hull, and its second component uses the collapse equation together with renaming to show that `invFo` relates the value to its image point.

```agda
  defines : (v : S) (m : Mem v) → ⟨ (fn v m ∷ v ∷ []) ⊨ invFo ⟩
  defines v m =
      subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    , transport (sym (rn (fn v m) v)) (π-graph (fn v m) (pre v m .snd .fst) v (pre v m .snd .snd))
```

Only the preimage is left to identify: any preimage satisfying the inverse graph has the same collapse value as the packaged preimage, and the injectivity of the collapse returns the equality of the two preimages.

```agda
  only : (v : S) (m : Mem v) (x' : S) → ⟨ (x' ∷ v ∷ []) ⊨ invFo ⟩ → x' ≡ fn v m
  only v m x' (hx , hp) = S≡ (CI.π-inj (fst x') (pre v m .fst) mx' (pre v m .snd .fst)
    (sym (P.piFo-val x' mx' v (transport (rn x' v) hp)) ∙ sym (pre v m .snd .snd)))
    where
    mx' : ⟨ fst x' ∈ˢ HS.M ⟩
```

For an alternative output `x'` satisfying the graph, the first conjunct says that its underlying set belongs to the packaged hull. Transport along `M≡` turns this into membership in the ambient hull `M`, which is the premise needed to compare `x'` with the recovered preimage by collapse injectivity.

```agda
    mx' = subst (λ w → ⟨ fst x' ∈ˢ w ⟩) M≡ hx
```

These results internalize the restricted inverse as a single-valued definable map. Every `v ∈ Lβ` is sent into the hull and satisfies `invFo`, while `only` shows that any other output satisfying the same graph is equal to this value. Injectivity is a further property and is proved separately next.

```agda
  Dmap : DefinableMap
  Dmap = record
    { dom = Lβ ; cod = hullL ; fn = fn
    ; into = λ v m → subst (λ w → ⟨ pre v m .fst ∈ˢ w ⟩) (sym M≡) (pre v m .snd .fst)
    ; graph = invFo ; defines = defines ; only = only }
```

Each uniquely determined preimage satisfies `π(pre(v)) = v`. Hence, if the two values of the inverse-collapse map are equal, applying `π` to that equality and composing with the two preimage equations gives `v = v'`. Thus the inverse on the collapse image is injective; this step uses the right-inverse equations rather than injectivity of the collapse.

```agda
  inj : (v : S) (m : Mem v) (v' : S) (m' : Mem v') → fst (fn v m) ≡ fst (fn v' m') → fst v ≡ fst v'
  inj v m v' m' q = sym (pre v m .snd .snd) ∙ cong HSC.π q ∙ pre v' m' .snd .snd
```

The restricted inverse is packaged as a coded injection from `Lβ` into the hull, completing the first section's construction. The packaging preserves the truncated form, so only the existence of a coded graph is exposed.

```agda
  Lβ↪M : InjL Lβ hullL
  Lβ↪M = Inj.injL Dmap inj
```

## Collapsing the hull back to the original stage

The counting module `At` fixes a non-finite constructible ordinal `δL`, its ordinality, and its exclusion from `ω`; an internal cardinal representative `μ` with the same non-finiteness; and two coded injections between `δL` and `μ` in both directions. These are exactly the data needed to count a non-finite stage by a cardinal representative.

```agda
module At (δL : S) (oδ : IsOrd (fst δL)) (δ∉ω : ⟨ fst δL ∈ˢ ω ⟩ → Empty.⊥)
          (μ : S) (oμ : IsOrd (fst μ)) (cμ : IsCardinalL μ)
          (μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥)
          (δ↪μ : InjL δL μ) (μ↪δ : InjL μ δL) where
```

It is useful to separate the carrier element `δL` from its underlying ambient ordinal `δ = fst δL`. Set-theoretic successor, stage membership, and the collapse act on `δ`, while internal coded injections retain the packaged endpoint `δL`.

```agda
  δ : V ℓ
  δ = fst δL
```

The stage of the ordinal `δ` is the earliest constructible level containing it; here it provides the starting index for finding a sufficiently high superadequate level.

```agda
  private
    α₀ : V ℓ
    α₀ = stage δ (snd δL)
```

The least-stage construction always returns an ordinal index. Applied to the constructible set `δ`, this gives the ordinality of `α₀`; the argument does not derive it from the separate hypothesis that `δ` is an ordinal.

```agda
    oα₀ : IsOrd α₀
    oα₀ = stage-ord δ (snd δL)
```

The ordinal `δ` belongs to its own stage, which is the membership fact that anchors `δ` inside the constructible hierarchy.

```agda
    δ∈Lα₀ : ⟨ δ ∈ˢ Lset α₀ ⟩
    δ∈Lα₀ = stage-mem δ (snd δL)
```

A superadequate level above the stage index is obtained; it carries all the closure conditions needed for the Skolem hull construction and for the condensation transfer.

```agda
    sa = superadequate-above α₀ oα₀
```

Choose the strengthened adequate stage supplied above and denote its ordinal index by `λ`. All subsequent hull and condensation arguments take place at this one sufficiently high stage.

```agda
  opaque
    lam : V ℓ
    lam = sa .fst
```

The chosen high index `λ` is an ordinal. Its transitivity will first carry `δ` through the comparison `δ ∈ α₀ ∈ λ`, and will then place every member of `δ+1` below `λ`.

```agda
    ordλ : IsOrd lam
    ordλ = sa .snd .fst
```

Successor closure is the second property of the index used immediately below: from `δ ∈ λ` it yields `δ+1 ∈ λ`. This is a statement about the ordinal index `λ`; it should not be confused with taking a successor constructible stage.

```agda
    succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩
    succλ = sa .snd .snd .snd .fst .snd .fst
```

Superadequacy says that above every member `d` of `λ` there merely exists an adequate stage `γ` that still belongs to `λ`. This supply of intermediate adequate stages provides the local reflection and closure used in counting and condensing the hull.

```agda
    sup : Superadequate lam
    sup = sa .snd .snd .snd .snd
```

First, `δ ∈ Lset α₀` and the fact that both `δ` and `α₀` are ordinals imply `δ ∈ α₀`. Since `α₀ ∈ λ`, transitivity of the ordinal `λ` then yields `δ ∈ λ`.

```agda
    δ∈λ : ⟨ δ ∈ˢ lam ⟩
    δ∈λ = ordλ .fst (ord∈Lset→∈ α₀ oα₀ δ oδ δ∈Lα₀) (sa .snd .snd .fst)
```

Take the starting set to be the von Neumann successor `X = δ+1`. It contains `δ` together with every smaller ordinal, and, because `δ` is an ordinal, `X` is transitive; these are exactly the features needed when the collapse is later shown to fix `δ`.

```agda
  X : V ℓ
  X = sucV δ
```

Successor closure of the ordinal index now gives `X = δ+1 ∈ λ`. This is an ordinal comparison. The stronger-looking statement needed by the hull construction, that every member of `X` lies in `Lset λ`, is derived separately in the next step.

```agda
  sucδ∈λ : ⟨ X ∈ˢ lam ⟩
  sucδ∈λ = succλ δ δ∈λ
```

If `z ∈ X`, transitivity of the ordinal `λ` and `X ∈ λ` give `z ∈ λ`. The general inclusion of an ordinal in its own constructible stage then yields `z ∈ Lset λ`. Hence the required premise is precisely `X ⊆ Lset λ`.

```agda
  X⊆Lλ : (z : V ℓ) → ⟨ z ∈ˢ X ⟩ → ⟨ z ∈ˢ Lset lam ⟩
  X⊆Lλ z hz = ord⊆Lset lam ordλ z (ordλ .fst hz sucδ∈λ)
```

Because `δ` is non-finite, every finite ordinal lies below `δ`; in particular `∅ ∈ δ`. Combining this with `δ ∈ λ` and transitivity of the ordinal `λ` gives the separate hull premise `∅ ∈ λ`.

```agda
  ∅∈λ : ⟨ ∅ ∈ˢ lam ⟩
  ∅∈λ = ordλ .fst (ω⊆ δ oδ δ∉ω ∅ (#∈ω zero)) δ∈λ
```

The starting set is constructible, because the coded successor of a constructible set is constructible, transported along the equation identifying the coded successor with the set-theoretic successor.

```agda
  X-isL : ⟨ isL X ⟩
  X-isL = subst (λ w → ⟨ isL w ⟩) (sucʟ-fst δL) (snd (sucʟ δL))
```

The constructibility proof turns the ambient set `X = δ+1` into the carrier element `XS`. This changes only its presentation: the counting problem remains the problem of injecting the successor of `δ` into the cardinal representative `μ`.

```agda
  XS : S
  XS = X , X-isL
```

The start is counted by the chain `δ+1 ↪ δ ↪ μ`. The first coded injection is the shift available for every non-finite ordinal `δ`, and the second is the assumed internal injection from `δ` to its cardinal representative `μ`. Their composition gives `InjL XS μ` without assuming that `δ` itself is a cardinal.

```agda
  base : InjL XS μ
  base = injl-trans XS δL μ
    (move (sucʟ δL) XS δL δL (sucʟ-fst δL) refl (Shift.injL δL oδ δ∉ω))
    δ↪μ
```

The Skolem hull generated from `X` is elementary in the surrounding stage `Lset λ`. This elementarity is what lets the counting theorem and the condensation argument transfer the relevant formulas and witnesses between the hull and the stage.

```agda
  elem = HullElemDown.elem lam ordλ X X⊆Lλ ∅∈λ
```

The Skolem hull is counted by the cardinal representative `μ`, because the starting set already injects into `μ` and the hull chapter shows that closure preserves the counting.

```agda
  hull↪μ = Count.hull↪κ lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL μ oμ cμ μ∉ω base
```

Apply the general condensation construction to this hull. It supplies an ordinal `β` whose stage `Lβ` is the collapse image, presents the hull as a constructible set, and gives the propositionally truncated coded injection `Lβ ↪ M` obtained from the inverse collapse.

```agda
  module St = Site lam ordλ succλ X X⊆Lλ ∅∈λ elem sup X-isL
    using ( β; oβ; ext; Lβ; hullL; Lβ↪M )
```

For the remaining comparison, use three facts about this hull: its underlying set is `M`, every member of the start lies in `M`, and the collapse `π` maps `M` onto `Lβ` while fixing members of any transitive subset of `M`. Applied to the transitive start `δ+1`, these facts will place `δ` in `Lβ`.

```agda
  module HS = HullStage lam ordλ succλ X X⊆Lλ ∅∈λ using ( M )
  module HSH = HullStage.H lam ordλ succλ X X⊆Lλ ∅∈λ using ( X⊆M )
  module HSC = HullStage.C lam ordλ succλ X X⊆Lλ ∅∈λ
    using ( π; fixes; πX-intro )
```

The ordinal `δ` belongs to its own successor, which is the starting set for the hull construction.

```agda
  δ∈X : ⟨ δ ∈ˢ X ⟩
  δ∈X = self∈sucV δ
```

The ordinal `δ` therefore belongs to the hull, because the hull contains every member of the starting set.

```agda
  δ∈M : ⟨ δ ∈ˢ HS.M ⟩
  δ∈M = HSH.X⊆M δ δ∈X
```

The successor `X = δ+1` is transitive and is contained in the hull `M`. The collapse therefore fixes every member of `X`; since `δ ∈ X`, it follows in particular that `π(δ) = δ`.

```agda
  πδ : HSC.π δ ≡ δ
  πδ = HSC.fixes X
    (λ a a∈ₛX → ∈∈ₛ {a = a} {b = HS.M} .fst (HSH.X⊆M a (∈∈ₛ {a = a} {b = X} .snd a∈ₛX)))
    (suc-ord oδ .fst) δ δ∈X
```

The ordinal `δ` lies inside the collapse level `Lβ`, because its collapse (which is itself) belongs to the collapse image, and the collapse image equals `Lset β`.

```agda
  δ∈Lβ : ⟨ δ ∈ˢ Lset St.β ⟩
  δ∈Lβ = subst (λ w → ⟨ w ∈ˢ Lset St.β ⟩) πδ
    (subst (λ w → ⟨ HSC.π δ ∈ˢ w ⟩) St.ext (HSC.πX-intro δ δ∈M))
```

The ordinal-stage bound now applies: when an ordinal `δ` belongs to `Lset β`, it must belong to the ordinal index `β`. Thus `δ ∈ β`. This is the strict comparison needed for monotonicity, and its direction places `Lset δ` inside `Lset β`.

```agda
  δ∈β : ⟨ δ ∈ˢ St.β ⟩
  δ∈β = ord∈Lset→∈ St.β St.oβ δ oδ δ∈Lβ
```

The canonical carrier presentation `Lδ` has underlying set `Lset δ`. It is the source used by `At.result`; the final theorem will later transport this source to any other carrier element whose underlying set is equal to the same stage.

```agda
  Lδ : S
  Lδ = LsetS δ oδ
```

The final comparison follows the chain `Lset δ ↪ Lset β ↪ M ↪ μ ↪ δ`. Its arrows come respectively from stage monotonicity using `δ ∈ β`, the inverse collapse, hull counting, and the assumed injection `μ ↪ δ`. Composing them proves `InjL Lδ δL`, the propositionally truncated existence of an internally coded injection from the stage at `δ` into `δ`.

```agda
  result : InjL Lδ δL
  result = injl-trans Lδ St.Lβ δL
    (inclusion-coded Lδ St.Lβ (λ z hz → Lset-mono {α = St.β} {β = δ} δ∈β hz))
    (injl-trans St.Lβ St.hullL δL St.Lβ↪M
      (injl-trans St.hullL μ δL hull↪μ μ↪δ))
```

For a general non-finite constructible ordinal `δ`, `cardOf` provides a cardinal representative only under propositional truncation. The proof works with a local representative `μ` inside the eliminator and applies `At.result`. This is legitimate because the target `InjL Lδ δ` is itself a propositionally truncated existence and hence a proposition. The resulting theorem is the stage-counting interface used later by both the GCH assembly and the bounded-subset argument; it proves only `Lset δ ↪ δ`, not GCH by itself.

```agda
stage-counted : StageCountedCoded
stage-counted δ Lδ oδ δ∉ω q = PT.rec squash₁ build (cardOf δ oδ)
  where
  build : Σ[ μ ∈ S ]
            ( IsOrd (fst μ) × IsCardinalL μ
```

A local `cardOf` witness records that `μ` is an ordinal and an internal cardinal, that its underlying set is contained in `δ`, and that coded injections exist in both directions. The containment proof is part of the representative package but is not needed by `At.result`; the construction uses the two injections together with ordinality, cardinality, and non-finiteness. Finally, `move` transports the source from the canonical `LsetS (fst δ) oδ` along `q : fst Lδ = Lset (fst δ)` to the presentation required by `StageCountedCoded`.

```agda
            × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst δ ⟩)
            × InjL δ μ × InjL μ δ )
        → InjL Lδ δ
  build (μ , oμ , cμ , μ⊆δ , δ↪μ , μ↪δ) =
    move (LsetS (fst δ) oδ) Lδ δ δ (sym q) refl
```

It remains to justify the non-finiteness required by the hull-count theorem. If `μ ∈ ω`, the coded injection `δ ↪ μ` would inject the non-finite ordinal `δ` into a finite ordinal, contradicting `δ ∉ ω`; hence `μ ∉ ω`. With this last premise, `At.result` supplies exactly the propositionally truncated coded injection from the chosen presentation of `Lset δ` into `δ`.

```agda
      (At.result δ oδ δ∉ω μ oμ cμ μ∉ω δ↪μ μ↪δ)
    where
    μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
    μ∉ω h = no-fin δ μ oδ δ∉ω oμ h δ↪μ
```