---
title: "Adequate stages for the GCH argument"
module: L.GCH.AdequateStages
lang: en
site: "Bedrock"
description: "Adequate stages for the GCH argument"
stage: "Proving GCH"
reading_order: 102
canonical: https://bedrock.institute/en/L.GCH.AdequateStages.html
html: L.GCH.AdequateStages.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/AdequateStages.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Hierarchy, L.Axioms.Basic, L.Coding.CodeSet, L.Definability, L.Coding.EnvironmentTower, L.Coding.SatisfactionGraphSet]
routes: [gch-descriptions]
translations: [https://bedrock.institute/zh/L.GCH.AdequateStages.md, https://bedrock.institute/ja/L.GCH.AdequateStages.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Adequate stages for the GCH argument

The internal descriptions used by condensation require four witness sets to be present together. This chapter defines when an ordinal index is adequate, constructs such an index `γ` above any given ordinal, and then constructs an index `λ` whose members are locally covered by smaller adequate indices. The corresponding constructible stages are `Lset γ` and `Lset λ`. Here adequate is a term of this book for a four-part closure condition tailored to the GCH argument, not the classical notion of an admissible ordinal.

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

All constructions in this chapter are relative to one explicit instance of excluded middle. It enters through the construction of birth stages and of the coded witnesses; it does not supply a choice function. In particular, the existence obtained later from membership in a union remains propositionally truncated.

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

Fix a universe level `ℓ` and excluded middle for propositions at level `ℓ-suc ℓ`. The adequate indices and their corresponding stages constructed below depend on this single classical hypothesis.

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

The construction takes place in the ambient cumulative hierarchy `V ℓ`. Its objects `c`, `γ`, and later `λ` are ordinal indices, whereas `Lset c`, `Lset γ`, and `Lset λ` are the constructible stages indexed by them. Unions are formed among the ordinal indices in the ambient hierarchy; the truth formula will be used only at the end to show that a whole constructible stage is an element of its successor stage.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( ⊤̇ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( union-family-in; union-family-out )
open import L.Constructible {ℓ} using
```

To place a constructible witness in a later stage, first take its birth-stage index, then bound that ordinal index, and finally use monotonicity of `Lset`. Separate ordinal facts ensure that members of an ordinal, their successors, and the common bounds used along the way are still ordinals. Thus the bounding argument acts on indices, while its conclusion places witness sets inside a stage.

```agda
  ( 𝒮ʟ; isL; IsOrd; isPropIsOrd; Lset; Lset-mono; Lset→isL; 𝒟ₒ-intro )
open import L.Ordinal {ℓ} using ( boundingOrd; bound2; setUnion-ord; mem-ord; suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
open import L.Hierarchy {ℓ} lem using ( hierL )
```

For a fixed ordinal index `c`, the later hierarchy description needs four constructible sets associated with `Lset c`: the internal hierarchy table, the set of all formula codes, the graph of uniform satisfaction, and the environment tower. Adequacy places all four together in one later constructible stage, where a single bounded description can range over them.

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )
```

Membership assertions and the witness conditions built from them are propositions. This matters when an element of a union yields only propositionally truncated information about which member of the family contains it: such information may be eliminated into a proposition, without choosing and retaining a particular index.

```agda
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; sett )
```

Every set in the cumulative hierarchy has a small presentation: a small index type maps onto its elements. This presentation permits the next bounding construction to range over all members of an ordinal. In the other direction, membership in a family union exposes a family index only under propositional truncation, a distinction used essentially in the countable-chain arguments below.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; module InfinitySet )
open InfinitySet {ℓ} using ( sucV; ω )
```

We read ambient membership `x ∈ y` through its proposition of witnesses `⟨ x ∈ y ⟩`. This is membership in `V ℓ`; it should not be confused with membership in the constructible carrier introduced next.

```agda
open hPropStructure 𝒮ᵥ
```

An element of the constructible carrier `CS.S` packages an ambient set together with evidence that it is constructible. Consequently, the four witnesses below are first produced as elements of `CS.S`, and their first projections are the actual ambient sets whose membership in a later `Lset` is required.

```agda
module CS = hPropStructure 𝒮ʟ using (S)
```

## The four witnesses held by an adequate stage

The witness module fixes an ordinal `c` with the proof that it is an ordinal.

```agda
module At (c : V ℓ) (oc : IsOrd c) where
```

The constructible stage `Lset c` is packaged as the carrier `A`. The hierarchy table, formula-code set, satisfaction graph and environment tower are then constructed from this carrier as four separate witnesses.

```agda
  A : CS.S
  A = LsetS c oc
```

The ordinal index `c` is itself constructible: `ord∈Lset-suc` places it in `Lset (sucV c)`, and membership in an ordinal-indexed constructible stage yields the required evidence `cL`.

```agda
  cL : ⟨ isL c ⟩
  cL = Lset→isL (sucV c) (suc-ord oc) c (ord∈Lset-suc c oc)
```

The first witness is the internal hierarchy table at `c`. It records within `L` the constructible stages whose ordinal indices lie below `c`.

```agda
  hier : CS.S
  hier = hierL c cL oc
```

The second witness is the set of all formula codes over the stage carrier. These are the codes later used by the hierarchy description.

```agda
  codes : CS.S
  codes = AllCodes A
```

The ordered-pair graph of the uniform satisfaction table is the third witness: it records the value assigned to each key.

```agda
  table : CS.S
  table = SatGraph.pairs A
```

The environment tower is the fourth witness: it collects the environments of every finite length.

```agda
  tower : CS.S
  tower = Tower.tower A
```

For an ordinal stage index `c`, the witness predicate requires the four underlying sets just constructed to belong to one common container `K`. It quantifies over the proof `oc : IsOrd c`, so the predicate does not retain a preferred proof of ordinality. Later `K` will be `Lset γ`, where `γ` is a larger ordinal index.

```agda
Witnesses : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Witnesses K c = (oc : IsOrd c)
  → ⟨ fst (At.hier c oc) ∈ K ⟩
  × ⟨ fst (At.codes c oc) ∈ K ⟩
  × ⟨ fst (At.table c oc) ∈ K ⟩
```

The fourth membership completes the witness predicate: the environment tower belongs to the same container.

```agda
  × ⟨ fst (At.tower c oc) ∈ K ⟩
```

The witness predicate is a proposition. For each possible proof that `c` is an ordinal, its conclusion is a product of four membership propositions; a dependent function whose values are propositions is again a proposition. This propositionhood later permits elimination from a propositionally truncated chain index directly into `Witnesses`, without selecting that index as data.

```agda
isPropWitnesses : (K c : V ℓ) → isProp (Witnesses K c)
isPropWitnesses K c = isPropΠ λ oc →
  isProp× (snd (fst (At.hier c oc) ∈ K))
    (isProp× (snd (fst (At.codes c oc) ∈ K))
      (isProp× (snd (fst (At.table c oc) ∈ K)) (snd (fst (At.tower c oc) ∈ K))))
```

An adequate index `γ` is an ordinal with three further properties: every `x ∈ γ` has `sucV x ∈ γ`, the ordinal `ω` belongs to `γ`, and every ordinal `c ∈ γ` has its four witness sets inside the single constructible stage `Lset γ`. The closure conditions concern the ordinal index `γ`; the witness condition concerns the distinct set `Lset γ`.

```agda
Adequate : V ℓ → Type (ℓ-suc ℓ)
Adequate γ =
    IsOrd γ
  × ((x : V ℓ) → ⟨ x ∈ γ ⟩ → ⟨ sucV x ∈ γ ⟩)
  × ⟨ ω ∈ γ ⟩
```

The last clause is where the two levels of the construction meet. Its argument `c ∈ γ` is a membership fact about ordinal indices, while its conclusion places the four sets associated with `c` inside the constructible stage `Lset γ`.

```agda
  × ((c : V ℓ) → ⟨ c ∈ γ ⟩ → Witnesses (Lset γ) c)
```

The four fields are named for the arguments ahead: ordinalness, successor closure, membership of the infinite ordinal, and the witness clause.

```agda
module Adequate (γ : V ℓ) (ad : Adequate γ) where
  ord = ad .fst
  succ = ad .snd .fst
  ω∈ = ad .snd .snd .fst
  wit = ad .snd .snd .snd
```

## Constructing an adequate stage above any ordinal

To take bounds over all members of a set `α`, use its small presentation `⟪ α ⟫`. The map `ι α` sends each presentation index to the ambient set it names. At this point `α` need not be described by the notation itself as an ordinal; ordinality enters when the construction proves that each named member is an ordinal.

```agda
private
  ι : (α : V ℓ) → ⟪ α ⟫ → V ℓ
  ι α = ⟪ α ⟫↪
```

Every presented index names a member of the ordinal, through the bridge between the small and ambient membership relations.

```agda
  ι∈ : (α : V ℓ) (m : ⟪ α ⟫) → ⟨ ι α m ∈ α ⟩
  ι∈ α m = ∈∈ₛ {a = ι α m} {b = α} .snd (∈ₛ⟪ α ⟫↪ m)
```

The transitivity of an ordinal is packaged once: two chained memberships inside the ordinal collapse into a single membership in it.

```agda
  tr : (β : V ℓ) → IsOrd β → (x y : V ℓ) → ⟨ x ∈ β ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ β ⟩
  tr β oβ x y x∈ y∈ = oβ .fst {x = x} {y = y} y∈ x∈
```

Starting from an ordinal index `α`, one bounding step will construct a larger ordinal index `β`. The step pays all obligations generated by members of `α`: their successors and the birth-stage indices of their four witness sets. It does not yet claim that `β` is adequate, because it has not paid the corresponding obligations for new members of `β`.

```agda
module Bound1 (α : V ℓ) (oα : IsOrd α) where
```

Every packaged constructible set `s : CS.S` has a birth-stage index `stage (fst s) (snd s)`. The auxiliary expression records this operation in the context of a presented member of `α`; the resulting index depends on the witness set `s`, while the surrounding arguments keep track of the member for which that witness was built.

```agda
  private
    W : ⟪ α ⟫ → (c : V ℓ) → IsOrd c → CS.S → V ℓ
    W m c oc s = stage (fst s) (snd s)
```

Every presented member of `α` is an ordinal, since members of ordinals are ordinals.

```agda
    oc : (m : ⟪ α ⟫) → IsOrd (ι α m)
    oc m = mem-ord {A = α} oα (ι α m) (ι∈ α m)
```

Applying `st` to each of the four witness constructions produces four ordinal-indexed families of birth stages. These are the families that the next common bounds must dominate.

```agda
    st : (f : (c : V ℓ) (o : IsOrd c) → CS.S) → ⟪ α ⟫ → V ℓ
    st f m = stage (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))
```

The birth-stage index `st f m` is an ordinal. This follows from the general theorem `stage-ord` for the birth-stage construction, applied to the underlying set of the witness together with its constructibility evidence.

```agda
    st-ord : (f : (c : V ℓ) (o : IsOrd c) → CS.S) (m : ⟪ α ⟫) → IsOrd (st f m)
    st-ord f m = stage-ord (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))
```

Five strict common bounds are taken. The first four bound the birth-stage indices of the hierarchy table, code set, satisfaction graph, and environment tower for every presented member of `α`. The fifth bounds the ordinal successors `sucV (ι α m)` themselves. These are bounds among ordinal indices; the fifth family is not a family of birth stages.

```agda
    b1 = boundingOrd ⟪ α ⟫ (st At.hier) (st-ord At.hier)
    b2 = boundingOrd ⟪ α ⟫ (st At.codes) (st-ord At.codes)
    b3 = boundingOrd ⟪ α ⟫ (st At.table) (st-ord At.table)
    b4 = boundingOrd ⟪ α ⟫ (st At.tower) (st-ord At.tower)
    b5 = boundingOrd ⟪ α ⟫ (λ m → sucV (ι α m)) (λ m → suc-ord (oc m))
```

A sixth strict bound contains both the starting index `α` and `ω`. Binary bounds then combine the six obligations: `b7` joins the first two witness bounds, `b8` joins the other two, `b9` joins the successor bound with the bound for `α` and `ω`, and `b10` joins the four witness bounds. No least bound is asserted; these operations merely provide strict common bounds with the required membership proofs.

```agda
    b6 = bound2 α ω oα ω-ord
    b7 = bound2 (b1 .fst) (b2 .fst) (b1 .snd .fst) (b2 .snd .fst)
    b8 = bound2 (b3 .fst) (b4 .fst) (b3 .snd .fst) (b4 .snd .fst)
    b9 = bound2 (b5 .fst) (b6 .fst) (b5 .snd .fst) (b6 .snd .fst)
    b10 = bound2 (b7 .fst) (b8 .fst) (b7 .snd .fst) (b8 .snd .fst)
```

One final binary bound joins the branch carrying successor, `α` and `ω` with the branch carrying the four birth-stage bounds. Its first component will therefore dominate all six kinds of obligation at once.

```agda
    b11 = bound2 (b9 .fst) (b10 .fst) (b9 .snd .fst) (b10 .snd .fst)
```

The first component of the final bound is the new ordinal index `β`. It is an index in `V ℓ`; the constructible stage used for witnesses will be `Lset β`.

```agda
  β : V ℓ
  β = b11 .fst
```

The final bound is an ordinal, since it was built from ordinals by the binary bound.

```agda
  oβ : IsOrd β
  oβ = b11 .snd .fst
```

The two partial bounds feeding the last combination lie below the final bound.

```agda
  private
    b9∈ : ⟨ b9 .fst ∈ β ⟩
    b9∈ = b11 .snd .snd .fst
    b10∈ : ⟨ b10 .fst ∈ β ⟩
    b10∈ = b11 .snd .snd .snd
```

Because `β` is transitive, strict membership can be propagated down the bound tree. From `b9 ∈ β` one obtains both the successor bound `b5 ∈ β` and the joint bound `b6 ∈ β` for `α` and `ω`; from `b10 ∈ β` one first obtains `b7 ∈ β`.

```agda
    b5∈ : ⟨ b5 .fst ∈ β ⟩
    b5∈ = tr β oβ (b9 .fst) (b5 .fst) b9∈ (b9 .snd .snd .fst)
    b6∈ : ⟨ b6 .fst ∈ β ⟩
    b6∈ = tr β oβ (b9 .fst) (b6 .fst) b9∈ (b9 .snd .snd .snd)
    b7∈ : ⟨ b7 .fst ∈ β ⟩
```

The other branch gives `b8 ∈ β`. Descending once more through `b7`, the first witness bound `b1` also belongs to `β`. Repeating the same transitivity argument will place every remaining witness bound in `β`.

```agda
    b7∈ = tr β oβ (b10 .fst) (b7 .fst) b10∈ (b10 .snd .snd .fst)
    b8∈ : ⟨ b8 .fst ∈ β ⟩
    b8∈ = tr β oβ (b10 .fst) (b8 .fst) b10∈ (b10 .snd .snd .snd)
    b1∈ : ⟨ b1 .fst ∈ β ⟩
    b1∈ = tr β oβ (b7 .fst) (b1 .fst) b7∈ (b7 .snd .snd .fst)
```

The second and third witness bounds, `b2` and `b3`, are obtained from the two branches `b7` and `b8`. The fourth bound `b4` has the same position under `b8`, so the following line closes the symmetric argument.

```agda
    b2∈ : ⟨ b2 .fst ∈ β ⟩
    b2∈ = tr β oβ (b7 .fst) (b2 .fst) b7∈ (b7 .snd .snd .snd)
    b3∈ : ⟨ b3 .fst ∈ β ⟩
    b3∈ = tr β oβ (b8 .fst) (b3 .fst) b8∈ (b8 .snd .snd .fst)
    b4∈ : ⟨ b4 .fst ∈ β ⟩
```

The last descent through the witness branch gives `b4 ∈ β`. At this point each of the four birth-stage bounds has been related to the common ordinal index `β`.

```agda
    b4∈ = tr β oβ (b8 .fst) (b4 .fst) b8∈ (b8 .snd .snd .snd)
```

The branch through `b6` also preserves the starting ordinal index: from `α ∈ b6` and `b6 ∈ β`, transitivity gives `α ∈ β`.

```agda
  α∈β : ⟨ α ∈ β ⟩
  α∈β = tr β oβ (b6 .fst) α b6∈ (b6 .snd .snd .fst)
```

The same branch preserves `ω`: its membership in `b6`, followed by `b6 ∈ β`, yields the membership `ω ∈ β` needed later.

```agda
  ω∈β : ⟨ ω ∈ β ⟩
  ω∈β = tr β oβ (b6 .fst) ω b6∈ (b6 .snd .snd .snd)
```

If `x ∈ α`, the presentation fibre supplies an index `m` with `ι α m ≡ x`. The fifth common bound contains `sucV (ι α m)`, and its membership in `β` follows through `b5 ∈ β`; substitution along the fibre equality then yields `sucV x ∈ β`. Thus this step proves successor closure only for members of `α`, as required of one bounding step.

```agda
  suc∈β : (x : V ℓ) → ⟨ x ∈ α ⟩ → ⟨ sucV x ∈ β ⟩
  suc∈β x x∈ = subst (λ u → ⟨ sucV u ∈ β ⟩) (fib .snd)
    (tr β oβ (b5 .fst) (sucV (ι α (fib .fst))) b5∈ (b5 .snd .snd (fib .fst)))
    where
    fib : Σ[ m ∈ ⟪ α ⟫ ] (ι α m ≡ x)
```

The fibre is recovered from the ambient membership proof by `∈-asFiber`. Here the conclusion is an actual dependent pair, rather than merely a propositionally truncated existence: the small presentation uses an embedding, so the fibre identifying the presentation index of `x` is proposition-valued.

```agda
    fib = ∈-asFiber {a = x} {b = α} x∈
```

The common ordinal bound `β` has already been arranged to dominate the birth-stage bounds for all four witnesses. We now use that arrangement to place the witnesses themselves in the constructible level `Lset β`.

```agda
  private
```

Fix one of the four witness constructions `f` and an index `m` presenting a member of `α`. Its value is born in `Lset (st f m)`; the recorded bound `b.fst` strictly contains this birth index, and the final bound `β` strictly contains `b.fst`. The landing lemma packages the resulting membership in `Lset β`.

```agda
    land : (f : (c : V ℓ) (o : IsOrd c) → CS.S)
           (b : Σ[ σ ∈ V ℓ ] (IsOrd σ × ((m : ⟪ α ⟫) → ⟨ st f m ∈ σ ⟩)))
         → ⟨ b .fst ∈ β ⟩
         → (m : ⟪ α ⟫) → ⟨ fst (f (ι α m) (oc m)) ∈ Lset β ⟩
    land f b b∈ m =
```

The inner use of `Lset-mono` moves the witness from `Lset (st f m)` to `Lset (b.fst)`. The outer use then moves it from `Lset (b.fst)` to `Lset β`; both moves follow from strict membership between the corresponding ordinal indices.

```agda
      Lset-mono {α = β} {β = b .fst} b∈
        (Lset-mono {α = b .fst} {β = st f m} (b .snd .snd m)
          (stage-mem (fst (f (ι α m) (oc m))) (snd (f (ι α m) (oc m)))))
```

For the member presented by `m`, the proof first lands the hierarchy table and the formula-code set in `Lset β`. The caller may supply any proof `o : IsOrd (ι α m)`; since ordinality is a proposition, it can be identified with the proof `oc m` used to construct the witnesses.

```agda
    witAt : (m : ⟪ α ⟫) → Witnesses (Lset β) (ι α m)
    witAt m o =
        subst (λ u → ⟨ fst (At.hier (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
          (land At.hier b1 b1∈ m)
      , ( subst (λ u → ⟨ fst (At.codes (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
```

The same argument completes the code-set membership and places the satisfaction graph and the environment tower in `Lset β`. Thus all four components of `Witnesses (Lset β) (ι α m)` are obtained with no dependence on a particular proof of ordinality.

```agda
            (land At.codes b2 b2∈ m)
        , ( subst (λ u → ⟨ fst (At.table (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
              (land At.table b3 b3∈ m)
          , subst (λ u → ⟨ fst (At.tower (ι α m) u) ∈ Lset β ⟩) (isPropIsOrd (ι α m) (oc m) o)
              (land At.tower b4 b4∈ m) ))
```

A membership proof `c ∈ α` has an actual presentation fibre: it yields an index `m` together with an equality `ι α m ≡ c`. Transporting `witAt m` along that equality gives the four witnesses for the abstractly named member `c`; this step does not eliminate a propositional truncation or make a choice.

```agda
  wit : (c : V ℓ) → ⟨ c ∈ α ⟩ → Witnesses (Lset β) c
  wit c c∈ = subst (Witnesses (Lset β)) (fib .snd) (witAt (fib .fst))
    where
    fib : Σ[ m ∈ ⟪ α ⟫ ] (ι α m ≡ c)
    fib = ∈-asFiber {a = c} {b = α} c∈
```

The union construction begins with an arbitrary natural-number-indexed family `ch` of ordinals. No monotonicity assumption is needed for the union itself; the two later applications will separately prove that each entry belongs to its successor.

```agda
module Union (ch : ℕ → V ℓ) (och : (n : ℕ) → IsOrd (ch n)) where
```

The cumulative-hierarchy union expects a small index type at the ambient universe level. Replacing `ℕ` by `Lift ℕ` changes only its universe placement: `F (lift n)` is still the ordinal `ch n`.

```agda
  private
    F : Lift {ℓ-zero} {ℓ} ℕ → V ℓ
    F n = ch (lower n)
```

The set-theoretic union of the family is denoted by the ordinal index `γ`. At this point `γ` is a set in the ambient cumulative hierarchy; the associated constructible level is `Lset γ`.

```agda
  γ : V ℓ
  γ = ⋃ (sett (Lift {ℓ-zero} {ℓ} ℕ) F)
```

The set-theoretic union of any family of ordinals is again an ordinal. Applying that fact to `F` proves `IsOrd γ`; no ordering or cofinality property of the natural-number index is used here.

```agda
  oγ : IsOrd γ
  oγ = setUnion-ord (Lift {ℓ-zero} {ℓ} ℕ) F (λ n → och (lower n))
```

The inward reading admits every member of every chain entry into the union.

```agda
  into : (n : ℕ) (x : V ℓ) → ⟨ x ∈ ch n ⟩ → ⟨ x ∈ γ ⟩
  into n x = union-family-in (Lift {ℓ-zero} {ℓ} ℕ) F (lift n) x
```

The outward reading recovers, under truncation, a chain entry containing any given member of the union. The truncated index is consumed only into propositions.

```agda
  outof : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ∥ Σ[ n ∈ ℕ ] ⟨ x ∈ ch n ⟩ ∥₁
  outof x h = PT.map (λ { (n , hn) → lower n , hn })
    (union-family-out (Lift {ℓ-zero} {ℓ} ℕ) F x h)
```

One bounding step settles only the obligations generated by the preceding ordinal. To settle every obligation generated along the construction, start above `p` and `ω`, repeat `Bound1` through a natural-number sequence, and take the union of the resulting ordinal indices.

```agda
module Above (p : V ℓ) (op : IsOrd p) where
```

The initial bound is an ordinal that strictly contains both the starting ordinal `p` and the ordinal `ω`. This immediately supplies the two memberships that must survive into the final union.

```agda
  private
    base = bound2 p ω op ω-ord
```

The zeroth ordinal is the initial common bound. Each later ordinal applies `Bound1` to its predecessor, so obligations arising from members of `ch n` are fulfilled in `ch (suc n)`; a single step is not claimed to be adequate for all of its own members.

```agda
  ch : ℕ → Σ[ β ∈ V ℓ ] IsOrd β
  ch zero = base .fst , base .snd .fst
  ch (suc n) = Bound1.β (ch n .fst) (ch n .snd) , Bound1.oβ (ch n .fst) (ch n .snd)
```

We now apply the preceding union construction to these ordinal indices. Its inward map will insert known memberships into the union, while its outward map will locate an arbitrary member only under propositional truncation.

```agda
  module C = Union (λ n → ch n .fst) (λ n → ch n .snd) using (into; outof; oγ; γ)
```

Let `γ` be this union of ordinal indices. The one-step delay is now absorbed by the union: any member found at one entry has its successor and four witness sets handled by a later entry. The witnesses ultimately have to lie in `Lset γ`, not in the index `γ` itself.

```agda
  γ : V ℓ
  γ = C.γ
```

Because every `ch n` is an ordinal, their set-theoretic union `γ` is an ordinal as well. This establishes only `IsOrd γ`; the closure and witness fields of `Adequate γ` are proved separately below.

```agda
  oγ : IsOrd γ
  oγ = C.oγ
```

Each chain entry is strictly below its successor entry, by the membership clause of the one-step bound.

```agda
  private
    up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
    up n = Bound1.α∈β (ch n .fst) (ch n .snd)
```

To put the ordinal index `ch n` itself into the union `γ`, use its strict membership in `ch (suc n)` and then include every member of `ch (suc n)` in the union. This fact later provides the index comparison needed for monotonicity of `Lset`.

```agda
    ch∈γ : (n : ℕ) → ⟨ ch n .fst ∈ γ ⟩
    ch∈γ n = C.into (suc n) (ch n .fst) (up n)
```

The base bound already contains `p`. Since the base is the zeroth entry of the family, the inward union map preserves this membership and yields `p ∈ γ`.

```agda
  p∈γ : ⟨ p ∈ γ ⟩
  p∈γ = C.into zero p (base .snd .snd .fst)
```

The same inward map carries `ω ∈ ch 0` to `ω ∈ γ`. This supplies the specific membership field required by `Adequate γ`.

```agda
  ω∈γ : ⟨ ω ∈ γ ⟩
  ω∈γ = C.into zero ω (base .snd .snd .snd)
```

Given `x ∈ γ`, the outward map produces the propositionally truncated existence of an index `n` with `x ∈ ch n`. In each branch, the next application of `Bound1` puts `sucV x` in `ch (suc n)`, hence in `γ`. The branches may be recombined because the target membership `sucV x ∈ γ` is a proposition; no particular `n` escapes the truncation.

```agda
  succ : (x : V ℓ) → ⟨ x ∈ γ ⟩ → ⟨ sucV x ∈ γ ⟩
  succ x x∈ = PT.rec (snd (sucV x ∈ γ))
    (λ { (n , x∈n) → C.into (suc n) (sucV x) (Bound1.suc∈β (ch n .fst) (ch n .snd) x x∈n) })
    (C.outof x x∈)
```

For `c ∈ γ`, the outward map likewise gives the propositionally truncated existence of `n` with `c ∈ ch n`. In each branch, the one-step bound supplies the four witnesses in `Lset (ch (suc n))`, and `ch (suc n) ∈ γ` lets `Lset-mono` move them into `Lset γ`. The result can be eliminated from the truncation because `Witnesses (Lset γ) c` is a proposition.

```agda
  wit : (c : V ℓ) → ⟨ c ∈ γ ⟩ → Witnesses (Lset γ) c
  wit c c∈ = PT.rec (isPropWitnesses (Lset γ) c)
    (λ { (n , c∈n) → λ oc →
      let w = Bound1.wit (ch n .fst) (ch n .snd) c c∈n oc
          mono = Lset-mono {α = γ} {β = ch (suc n) .fst} (ch∈γ (suc n))
```

The single map `mono` is monotonicity of the constructible hierarchy from the index `ch (suc n)` to the index `γ`. Applying it separately to the hierarchy table, code set, satisfaction graph and environment tower completes the four-component witness tuple.

```agda
      in mono (w .fst) , ( mono (w .snd .fst) , ( mono (w .snd .snd .fst) , mono (w .snd .snd .snd) )) })
    (C.outof c c∈)
```

The ordinal index `γ` now satisfies all four clauses of `Adequate`: ordinality, successor closure, membership of `ω`, and containment of the four witnesses for every `c ∈ γ` in the distinct constructible stage `Lset γ`. This four-part conclusion is the full content of adequacy used later.

```agda
  adequate : Adequate γ
  adequate = oγ , ( succ , ( ω∈γ , wit ))
```

The theorem returns an explicit ordinal index `γ`, together with `p ∈ γ` and `Adequate γ`. The outer dependent pair is not truncated, so later arguments may name this `γ`; the construction proves neither that it is least nor that it is obtained by a standard ordinal operation such as `p + ω`.

```agda
adequate-above : (p : V ℓ) → IsOrd p
               → Σ[ γ ∈ V ℓ ] (IsOrd γ × ⟨ p ∈ γ ⟩ × Adequate γ)
adequate-above p op = Above.γ p op , ( Above.oγ p op , ( Above.p∈γ p op , Above.adequate p op ))
```

## Strengthening the conditions throughout a stage

`Superadequate λ` means that for every `d ∈ λ` there merely exists an adequate ordinal index `γ` with both `γ ∈ λ` and `d ∈ γ`. Thus `γ` lies strictly below the ordinal `λ` and covers `d`, but the propositional truncation retains neither a chosen `γ` nor a least one.

```agda
Superadequate : V ℓ → Type (ℓ-suc ℓ)
Superadequate lam = (d : V ℓ) → ⟨ d ∈ lam ⟩
  → ∥ Σ[ γ ∈ V ℓ ] (⟨ γ ∈ lam ⟩ × ⟨ d ∈ γ ⟩ × Adequate γ) ∥₁
```

To build such a strengthened adequate stage above an ordinal `α`, we iterate `adequate-above` once more. This time every entry in the natural-number sequence is already an adequate ordinal index, so the entries themselves can later serve as local adequate witnesses.

```agda
module Super (α : V ℓ) (oα : IsOrd α) where
```

The zeroth entry is the explicit ordinal index returned by `adequate-above α oα`. It is adequate and strictly contains the starting ordinal `α`; these facts are stored with the entry for later use.

```agda
  ch : ℕ → Σ[ γ ∈ V ℓ ] (IsOrd γ × Adequate γ)
  ch zero =
    adequate-above α oα .fst
    , ( adequate-above α oα .snd .fst , adequate-above α oα .snd .snd .snd )
  ch (suc n) =
```

From an adequate ordinal index `ch n`, another application of `adequate-above` produces the next adequate index `ch (suc n)` with `ch n ∈ ch (suc n)`. The theorem supplies some such next index explicitly, without asserting minimality.

```agda
    adequate-above (ch n .fst) (ch n .snd .fst) .fst
    , ( adequate-above (ch n .fst) (ch n .snd .fst) .snd .fst
      , adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .snd )
```

Apply the union construction to this sequence of adequate ordinal indices. As before, membership in the union can be localized to an entry only under propositional truncation.

```agda
  module U = Union (λ n → ch n .fst) (λ n → ch n .snd .fst) using (into; outof; oγ; γ)
```

Denote the union of these ordinal indices by `lam` in the code and by `λ` in the exposition. The proof concerns the ordinal index `λ`: it will satisfy both `Adequate λ` and `Superadequate λ`. The corresponding constructible stage, used only in the witness clauses, is `Lset λ`.

```agda
  lam : V ℓ
  lam = U.γ
```

The set-theoretic union `λ` is an ordinal because all entries `ch n` are ordinals. No stronger limit, regularity or cardinal property follows from this argument.

```agda
  olam : IsOrd lam
  olam = U.oγ
```

Each chain entry is strictly below its successor, by the strict membership produced by `adequate-above`.

```agda
  private
    up : (n : ℕ) → ⟨ ch n .fst ∈ ch (suc n) .fst ⟩
    up n = adequate-above (ch n .fst) (ch n .snd .fst) .snd .snd .fst
```

Since `ch n ∈ ch (suc n)`, the inward map for the union shows `ch n ∈ λ`. Thus every adequate index in the sequence is itself available as a member of the final ordinal index `λ`.

```agda
    ch∈λ : (n : ℕ) → ⟨ ch n .fst ∈ lam ⟩
    ch∈λ n = U.into (suc n) (ch n .fst) (up n)
```

The zeroth adequate index strictly contains `α`, and it is one of the sets forming the union. Consequently `α ∈ λ`.

```agda
  α∈λ : ⟨ α ∈ lam ⟩
  α∈λ = U.into zero α (adequate-above α oα .snd .snd .fst)
```

Given `x ∈ λ`, the outward map supplies only the propositionally truncated existence of an `n` with `x ∈ ch n`. In each branch, adequacy of that entry gives `sucV x ∈ ch n`, and the inward map yields `sucV x ∈ λ`. Since the target is a membership proposition, the result may be eliminated from the truncation without retaining `n`.

```agda
  succ : (x : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ sucV x ∈ lam ⟩
  succ x x∈ = PT.rec (snd (sucV x ∈ lam))
    (λ { (n , x∈n) → U.into n (sucV x) (Adequate.succ (ch n .fst) (ch n .snd .snd) x x∈n) })
    (U.outof x x∈)
```

The zeroth entry is adequate and therefore contains `ω`. The inward union map carries this fact to the membership `ω ∈ λ` required by `Adequate λ`.

```agda
  ω∈λ : ⟨ ω ∈ lam ⟩
  ω∈λ = U.into zero ω (Adequate.ω∈ (ch zero .fst) (ch zero .snd .snd))
```

For `c ∈ λ`, the outward map gives the propositionally truncated existence of an `n` with `c ∈ ch n`. In each branch, adequacy of `ch n` supplies the four witnesses in `Lset (ch n)`, and `ch n ∈ λ` lets monotonicity move them into `Lset λ`. Elimination from the truncation is valid because `Witnesses (Lset λ) c` is a proposition.

```agda
  wit : (c : V ℓ) → ⟨ c ∈ lam ⟩ → Witnesses (Lset lam) c
  wit c c∈ = PT.rec (isPropWitnesses (Lset lam) c)
    (λ { (n , c∈n) → λ oc →
      let w = Adequate.wit (ch n .fst) (ch n .snd .snd) c c∈n oc
      in  Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .fst)
```

Each component is transported by monotonicity of the constructible levels along `ch n ∈ λ`: the hierarchy table, code set, satisfaction graph and environment tower all pass from `Lset (ch n)` to `Lset λ`.

```agda
        , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .fst)
          , ( Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .fst)
            , Lset-mono {α = lam} {β = ch n .fst} (ch∈λ n) (w .snd .snd .snd) )) })
    (U.outof c c∈)
```

Ordinality of the union, successor closure, `ω ∈ λ`, and the transported witnesses together prove `Adequate λ`. The first three facts concern the ordinal index `λ`; the fourth places sets in the constructible stage `Lset λ`. These are closure facts used by the later hierarchy description, rather than a model-theoretic assertion about `Lset λ`.

```agda
  adequate : Adequate lam
  adequate = olam , ( succ , ( ω∈λ , wit ))
```

For `d ∈ λ`, the outward map gives only the propositionally truncated existence of an `n` with `d ∈ ch n`. Mapping within that truncation uses `γ = ch n`: this index belongs to `λ`, contains `d`, and is adequate. The result remains truncated, so it defines no choice function `d ↦ γ`.

```agda
  super : Superadequate lam
  super d d∈ = PT.map
    (λ { (n , d∈n) → ch n .fst , ( ch∈λ n , ( d∈n , ch n .snd .snd )) })
    (U.outof d d∈)
```

The exported theorem returns an explicit ordinal index `λ` above `α`, together with proofs of `Adequate λ` and `Superadequate λ`. Although `λ` itself is available as data, the local adequate indices promised for its members remain under propositional truncation; no least local index or global family of choices is produced.

```agda
superadequate-above : (α : V ℓ) → IsOrd α
                    → Σ[ lam ∈ V ℓ ] (IsOrd lam × ⟨ α ∈ lam ⟩ × Adequate lam × Superadequate lam)
superadequate-above α oα =
  Super.lam α oα , ( Super.olam α oα , ( Super.α∈λ α oα , ( Super.adequate α oα , Super.super α oα )))
```

## A stage belongs to its successor stage

For every ambient set `β`, the whole set `Lset β` is an element of `Lset (sucV β)`; no ordinality hypothesis on `β` is needed. The equation `Lset (sucV β) = 𝒟ₒ (Lset β)` reduces the claim to definability over `Lset β`, and the constant-true formula defines the whole carrier as a subset of itself. The conclusion is membership of the set `Lset β` in the next constructible stage, a different statement from pointwise inclusion of one stage in another.

```agda
Lset∈suc : (β : V ℓ) → ⟨ Lset β ∈ Lset (sucV β) ⟩
Lset∈suc β = subst (λ w → ⟨ Lset β ∈ w ⟩) (sym (Lset-suc β))
  (𝒟ₒ-intro (Lset β) (Lset β) ∣ ⊤̇ , DefOf.defSet⊤≡A (Lset β) ∣₁)
```