---
title: "The first stage meeting a set"
module: L.Choice.FirstIntersectionStage
lang: en
site: "Bedrock"
description: "The first stage meeting a set"
stage: "The canonical well-order and Choice"
reading_order: 72
canonical: https://bedrock.institute/en/L.Choice.FirstIntersectionStage.html
html: L.Choice.FirstIntersectionStage.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/FirstIntersectionStage.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Axioms.Basic]
routes: [canonical-order]
translations: [https://bedrock.institute/zh/L.Choice.FirstIntersectionStage.md, https://bedrock.institute/ja/L.Choice.FirstIntersectionStage.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The first stage meeting a set

This chapter provides two ingredients of the internal choice construction. The
first is a lemma about least stages. When a property of ordinals holds for the
first time, it holds at a least stage; whether that stage is a successor is not
automatic, for the property may hold first at the zero ordinal. The chapter
proves the conditional form that the argument needs: if, besides the least
stage, a carve merely exists, an ordinal below it at whose successor the
property already holds, then the least stage is a successor with a unique
predecessor. The second ingredient is a bounding ordinal: for a constructible
set, one ordinal whose stage contains the set, its members, the members of its
members, and the limit level of the tower.

The material serves a comparison that proceeds by two keys. Two sets that first
appear at different stages are compared by their birth ordinals and by nothing
else; only sets that first appear at the same stage are compared by their names
within that stage. The first ingredient makes each birth ordinal a definite
object rather than a mere existence, and the second guarantees that the
material of a whole family of candidates lives inside one stage, so that the
name comparison has a common arena.

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

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

module L.Choice.FirstIntersectionStage {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The chapter runs under one hypothesis, an excluded-middle instance at the
successor of the model's level, and every statement below is made inside that
setting.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
```

The question of the chapter is one about first appearances. A constructible set
enters the tower of stages at some point; the ambient hierarchy, in which the
tower lives, has irreflexive membership, so no ordinal contains itself, and its
successors are understood: an ordinal sits inside its own successor, and a
member of a successor is a member of the ordinal or the ordinal itself.

```agda
open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )
```

The constructible side answers with its tower `Lset`, indexed by
ordinals, which are sets of the hierarchy, never by universe levels of the
host. Ordinality `IsOrd` is itself a proposition; the tower has a layer
relation, an outward decomposition, and monotonicity; and transitivity moves
members across layers.

```agda
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
```

The argument turns on comparisons and on stages. Comparing an ordinal below a
stage with the stage itself is what decides whether the stage overshoots a
successor, and members of ordinals and successors of ordinals are again
ordinals. Each constructible set carries its earliest ordinal, delivered with
ordinality and membership, and minimality stated refutationally. Two ordinals
have a common bound. And the successor identity says the next stage is exactly
the definable subsets of the previous one, which is the step by which anything
enters the tower at all.

```agda
import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
```

The argument is written in three propositional moves: a split into cases, a
refutation ending in the empty type, and an existence known only to be
existence.

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
```

A predecessor pairs an ordinal with propositional evidence. Such pairs are determined by their first component, and the cumulative hierarchy itself is a set, so equality of predecessors reduces to equality of the underlying ordinals.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )
```

The hierarchy's infinity construction supplies both the von Neumann successor `sucV` and the limit level `ω` used in the bound.

```agda
open hPropStructure 𝒮ᵥ
```

Structure membership `∈ˢ` is the relation in which ordinality, stages and
minimality are all stated.

## The predecessor of a least stage

The question is whether the least stage at which something appears is a
successor, and which stage it succeeds. A least stage taken alone need not be
one, for the property may begin at zero; what the construction produces, under
the additional hypothesis of a carve below, is the unique predecessor.

A successor determines what it succeeds, at least among ordinals. Compare a
candidate predecessor with another: each belongs to the successor of the other,
so each is a member of the other or equal to it, and two ordinals cannot be
members of each other, since transitivity would then make one a member of
itself. So being the predecessor of a given ordinal is a proposition, which is
what lets a merely-existing predecessor be read as a definite one.

That a least stage has a predecessor at all takes two inputs, and it is worth
seeing them separately. The first is the least stage itself: an ordinal `σ` at
which the property holds, with minimality stated refutationally, that no
smaller ordinal has it. The second is the mere existence of a carve at `σ`: some
ordinal `δ` below `σ` at whose successor the property already holds. Given a
carve, minimality rules out the successor staying strictly below, and the
no-overshoot comparison leaves one case: the successor of the carved ordinal is
exactly `σ`. So the least stage is a successor, and the carved ordinal is its
predecessor. Without the carve nothing follows: the property may hold first at
the zero ordinal, below which no ordinal exists at all.

```agda
IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)
```

A candidate predecessor `δ` of an ordinal `σ` is an ordinal whose von Neumann
successor is `σ` itself. Both halves matter: ordinality is what the comparison
needs, and the equation is what pins `δ` to `σ`.

```agda
private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → Empty.⊥
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)
```

No ordinal can be a member of one of its own members: transitivity would carry
the membership around the two-step cycle back to `a` itself, contradicting
irreflexivity. This two-step impossibility forbids two ordinals from
containing each other.

```agda
  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → Empty.rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)
```

The membership branch reads: `δ'` is a member of the successor of `δ`, and `δ`
is a member of `δ'`; the conclusion must be `δ ≡ δ'`. If `δ'` were a member of
`δ` itself, the two-step cycle would close; so `δ'` is `δ` itself, and the
elimination returns exactly that.

```agda
ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')
```

The successor operation is injective on ordinals. From the equation of
successors, `δ` is a member of `sucV δ'`; the elimination offers two readings.
Either `δ` is a member of `δ'`, in which case the membership branch closes the
cycle and gives the equality, or `δ` already is `δ'`. A successor determines
what it succeeds.

```agda
  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')
```

The two memberships feeding the elimination come from the standing fact that an
ordinal sits inside its own successor, transported along the equation and its
reverse.

```agda
isPropPredOf : (σ : S) → isProp (Σ[ δ ∈ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))
```

Any two predecessors of one ordinal are therefore equal. The first components
agree by injectivity, and the remaining data are propositions, so the whole
type of predecessors is a proposition. This is what makes a merely-existing
predecessor usable as a definite one: unwrapping a truncation into a
proposition-valued target is always legitimate.

```agda
module _ (P : S → hProp (ℓ-suc ℓ)) where
```

The least-stage argument is now run once for every property of ordinals at
once: the property is a parameter, and nothing below ever reads into it.

```agda
  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)
```

A carve at `σ` is the datum the argument runs on: an ordinal `δ` strictly below
`σ` whose successor already carries the property. If a carve merely exists, the
least stage cannot be far above `δ`, for the property already holds at
`sucV δ`.

```agda
  private
    below-case : (σ δ : S) → isLeastOrd P σ → IsOrd δ → ⟨ P (sucV δ) ⟩
               → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
    below-case σ δ least ordδ m s∈σ =
      Empty.rec (least (sucV δ) (suc-ord ordδ) m s∈σ)
```

The below branch handles the case in which the successor stays strictly below
the least stage. Minimality is stated refutationally, and the hypotheses of
this branch are exactly its premises, so `least` yields a contradiction first;
`Empty.rec` then eliminates that contradiction to the path the branch owes,
`sucV δ ≡ σ`.

```agda
    same-case : (σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
    same-case σ δ e = e
```

The equal case needs no work at all: the identification of the successor with
the least stage is what the case was handed.

```agda
    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∈ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)
```

`atCarve` turns a carve into a definite predecessor. The witness `δ` is kept,
its ordinality is recovered from belonging to the ordinal `σ`, and the equation
pinning `sucV δ` to `σ` is the content of the case analysis.

```agda
      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ
```

Ordinality of `δ` is inherited from the ordinal `σ`, members of ordinals
being ordinals.

```agda
      suc≡σ : sucV δ ≡ σ
      suc≡σ = Sum.rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)
```

Given `δ ∈ σ`, `suc∈or≡` leaves exactly two possibilities for its successor: it remains strictly below `σ`, or it equals `σ`. Minimality refutes the first, so the second gives the required equation.

```agda
  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∈ S ] IsPredOf σ δ
  predOf σ ordσ least = PT.rec (isPropPredOf σ) (atCarve σ ordσ least)
```

`predOf` consumes a carve known only to exist and returns the predecessor. The
truncated input is eliminated into the proposition that the predecessor type
is, so no choice among hypothetical carves is ever made; whichever carve the
truncation hands over, the answer is the same definite predecessor.

```agda
  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁
```

`carveAt` produces a carve from a member `z` of the least stage, together with
the observation that whenever `z` appears at a successor stage, the property
already holds there. That observation is exactly the shape of the descent into
the tower: appearing at a stage is appearing inside a definable powerset of an
earlier stage, and every definable powerset is a successor stage by the
successor identity.

```agda
  carveAt σ z z∈Lσ k = PT.map
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)
```

The tower decomposes the membership of `z` truncatedly: some stage `δ` below
`σ` with `z` in the definable powerset of `Lset δ`. The decomposition is mapped
inside the truncation only: the successor identity, read backwards, transports
`z` from `𝒟ₒ (Lset δ)` into `Lset (sucV δ)`, the observation `k` fires at that
successor, and the resulting carve is injected back into the truncation.

## One stage for everything below a set

This section turns stage transitivity and an ordinal bound into one level that
contains a set's members, their members, and the limit level `ω`.

The other thing the construction needs is a bound, and no comparison is involved
in getting one. A stage is transitive, so the stage of a set already holds the
set's members, and their members after them; the earliest stage is a stage like
any other, so it serves.

One more ordinal remains to be fixed: the tower's limit level. The comparison
ahead is written in the object language, and the codes of all parameter-free formulas
`Formula ⊥* n`, of every arity, belong to `Lset ω`; such a code may have free variables, so
these are formulas, not sentences. A full name of a member of a successor stage
says more than its code: it names the arity and a vector of parameters from
earlier stages. The bound covers the codes, because `ω ∈ β` and monotonicity
lift `Lset ω` into `Lset β`; the parameters lie below the bound
for the reason the next fact records: members of the set and members of those
land in the same level.

```agda
stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)
```

Stages are transitive, and the earliest stage of `a` is a stage. So a member
`x` of `a` lies in the tower's level at `a`'s own stage: transitivity moves the
membership from the set into the level that holds the set.

```agda
stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)
```

Transitivity applied twice reaches two levels down: a member of a member of
`a` lies in the same level, because it lies in `x` and `x` lies in the level.

```agda
stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∈ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)
```

The two ordinals that must be dominated are the limit level `ω` and the set's
own earliest stage; `bound2` returns a single ordinal above both, with its
ordinality certified.

```agda
bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)
```

Monotonicity of the tower lifts the two-level fact from the earliest stage into
the stage of the bounding ordinal. One level now holds `a`, its members, their
members, and the formula codes the comparison reads.

## Recap

The chapter's reusable outputs are the unique predecessor of a least stage,
when that stage is a successor, and a bounding ordinal large enough for the
choice construction. The least-stage lemma is conditional, and the condition is
its content. For a property of ordinals with least stage `σ`, the property may
well hold first at the zero ordinal, and then there is nothing below to carve.
When a carve at `σ` merely exists, an ordinal below `σ` at whose successor the
property already holds, `carveAt` produces it, `predOf` turns it
into the unique predecessor by closing the truncation on
`isPropPredOf`, and `ord-suc-inj` is why a successor determines
what it succeeds. `stageBound` supplies the bounding ordinal: above a
set's own stage, hence above its members and theirs, and above the tower's
limit level, where the formula codes live.