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.

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

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.

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.

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.

  ( 𝒮ʟ; 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.

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.

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.

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.

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.

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.

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.

  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.

  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.

  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.

  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.

  table : CS.S
  table = SatGraph.pairs A

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

  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.

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.

  × ⟨ 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.

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 γ.

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 γ.

  × ((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.

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.

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

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

  ι∈ : (α : 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.

  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 β.

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.

  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.

    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.

    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.

    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.

    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.

    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.

    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 β.

  β : V ℓ
  β = b11 .fst

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

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

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

  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 ∈ β.

    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 β.

    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.

    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 β.

    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 α ∈ β.

  α∈β : ⟨ α ∈ β ⟩
  α∈β = 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.

  ω∈β : ⟨ ω ∈ β ⟩
  ω∈β = 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.

  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.

    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 β.

  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 β.

    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.

      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.

    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.

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

  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.

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.

  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 γ.

  γ : 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.

  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.

  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.

  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.

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.

  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.

  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.

  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.

  γ : 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.

  oγ : IsOrd γ
  oγ = C.oγ

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

  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.

    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 ∈ γ.

  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 γ.

  ω∈γ : ⟨ ω ∈ γ ⟩
  ω∈γ = 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.

  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.

  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.

      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.

  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 + ω.

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.

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.

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.

  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.

    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.

  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 λ.

  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.

  olam : IsOrd lam
  olam = U.oγ

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

  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 λ.

    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 α ∈ λ.

  α∈λ : ⟨ α ∈ 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.

  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 λ.

  ω∈λ : ⟨ ω ∈ 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.

  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 λ.

        , ( 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 λ.

  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 ↦ γ.

  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.

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.

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