The stage where a set first has a member

The last debt asks for a set that meets each cell of a disjoint family in exactly one point. The textbook pays it by well-ordering the universe and taking the least member of every cell, and that road is expensive here: a well-order of all of L is a relation on a proper class, and nothing built so far speaks of one.

There is a cheaper road, and it starts by asking where a cell's members are. A cell is a set of L, so each of its members appears somewhere in the tower; so there is an earliest stage at which any of them has appeared at all. That stage cannot be a limit and cannot be zero: a set enters the tower only by being carved out of the stage below it, so the earliest stage that meets the cell is the successor of a stage that does not. The cell therefore carries a canonical ordinal of its own, the stage one below its first appearance, and at that ordinal every member of the cell that appears first is a definable subset of one and the same set.

That is what replaces the well-order. Choosing a member of the cell becomes a comparison between names written over a single stage, never a comparison between arbitrary elements of L; the ordinal doing the bookkeeping is the stage, so sets that appear at different times are never compared at all. This chapter builds that ordinal and proves the two facts the rest of the part turns on: that it exists and is unique, and that one ordinal suffices to hold a set, its members and their members, together with the tower's limit level.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; isL-trans; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans; 𝒟ₒ )
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; LeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )

import Cubical.Data.Sum as Sum
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

The least stage meeting a set

"Some member of u has appeared by stage σ" is a property of ordinals and nothing more, so the least-ordinal operator applies to it with no work: that operator was written generic in its property precisely so that instances like this one cost a line.

The operator wants a truncated witness that some ordinal qualifies, and an inhabited cell supplies it. A member of the cell is constructible, because L is a transitive class and the cell is one of its sets; and constructibility is by definition the existence of a stage containing it. So the witness is the member's own stage, read straight off the class.

meets : S → S → Ω
meets u σ = ⋁ S (λ z → (z ∈ˢ u) ⊓ (z ∈ˢ Lset σ))

Inhabited : S → Type (ℓ-suc ℓ)
Inhabited u = ∥ Σ[ z ∈ S ] ⟨ z ∈ˢ u ⟩ ∥₁

meetsSome : (u : S) → ⟨ isL u ⟩ → Inhabited u
          → ∥ Σ[ σ ∈ S ] (IsOrd σ × ⟨ meets u σ ⟩) ∥₁
meetsSome u pu = PT.rec squash₁ atMember
  where
  atMember : Σ[ z ∈ S ] ⟨ z ∈ˢ u ⟩
           → ∥ Σ[ σ ∈ S ] (IsOrd σ × ⟨ meets u σ ⟩) ∥₁
  atMember (z , z∈u) = PT.map
    (λ { (α , (ordα , z∈Lα)) → α , (ordα , ∣ z , (z∈u , z∈Lα) ∣₁) })
    (isL-trans {x = u} {y = z} z∈u pu)

The least such ordinal is μ u, and it is sealed exactly as the stage function was, for exactly the same reason: it unfolds to a well-founded descent whose steps mention the tower, and every later type mentioning it would drag that unfolding into conversion. The three projections open the seal once each, and they are the whole interface.

theEarliestMeet : (u : S) → ⟨ isL u ⟩ → Inhabited u → LeastOrd (meets u)
theEarliestMeet u pu h = leastOrd (meets u) (meetsSome u pu h)

opaque
  μ : (u : S) → ⟨ isL u ⟩ → Inhabited u → S
  μ u pu h = theEarliestMeet u pu h .fst

opaque
  unfolding μ
  μ-ord : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u) → IsOrd (μ u pu h)
  μ-ord u pu h = theEarliestMeet u pu h .snd .fst

  μ-meets : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u) → ⟨ meets u (μ u pu h) ⟩
  μ-meets u pu h = theEarliestMeet u pu h .snd .snd .fst

  μ-earliest : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
             → isLeastOrd (meets u) (μ u pu h)
  μ-earliest u pu h = theEarliestMeet u pu h .snd .snd .snd

A first appearance is a successor

Take a member of the cell that has appeared by the least stage. Membership in a stage is membership in the definable subsets of some earlier stage, and the successor identity says those definable subsets are the next stage; so that member has already appeared one stage above the earlier one, and the cell is already met there. Minimality forbids that stage from being strictly below the least one, and a member's successor cannot overshoot: it belongs to the least stage or it is it. The first case is the one minimality just refuted, so the second holds, and the least stage is a successor.

The refuted case is a named helper with its conclusion written down. That is the discipline the stages chapter set for every split coming out of trichotomy, and the split here is one: suc∈or≡ is a comparison in disguise.

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

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

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

meet-suc : (u σ : S) → IsOrd σ → ⟨ meets u σ ⟩ → isLeastOrd (meets u) σ
         → ∥ Σ[ δ ∈ S ] IsPredOf σ δ ∥₁
meet-suc u σ ordσ m least = PT.rec squash₁ atMember m
  where
  atCarve : (z : S) → ⟨ z ∈ˢ u ⟩
          → Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ z ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → Σ[ δ ∈ S ] IsPredOf σ δ
  atCarve z z∈u (δ , (δ∈σ , z∈𝒟ₒδ)) = δ , (ordδ , suc≡σ)
    where
    ordδ : IsOrd δ
    ordδ = mem-ord {A = σ} ordσ δ δ∈σ
    metAtSuc : ⟨ meets u (sucV δ) ⟩
    metAtSuc = ∣ z , (z∈u
      , subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟ₒδ) ∣₁
    suc≡σ : sucV δ ≡ σ
    suc≡σ = Sum.rec (below-case u σ δ least ordδ metAtSuc) (same-case u σ δ)
      (suc∈or≡ δ σ ordδ ordσ δ∈σ)

  atMember : Σ[ z ∈ S ] (⟨ z ∈ˢ u ⟩ × ⟨ z ∈ˢ Lset σ ⟩)
           → ∥ Σ[ δ ∈ S ] IsPredOf σ δ ∥₁
  atMember (z , (z∈u , z∈Lσ)) = PT.map (atCarve z z∈u) (Lset-out σ z z∈Lσ)

The stage a first appearance is defined over

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, and the predecessor of the least stage may be extracted from the merely-existing one the previous section produced.

That extraction is what makes defStage a function: the definition stage of a cell, the stage over which the cell's first members are written. It is sealed with its two properties beside it, as μ was.

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)

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

ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')
  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')

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'))

thePred : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
        → Σ[ δ ∈ S ] IsPredOf (μ u pu h) δ
thePred u pu h = PT.rec (isPropPredOf (μ u pu h)) (λ d → d)
  (meet-suc u (μ u pu h) (μ-ord u pu h) (μ-meets u pu h) (μ-earliest u pu h))

opaque
  defStage : (u : S) → ⟨ isL u ⟩ → Inhabited u → S
  defStage u pu h = thePred u pu h .fst

opaque
  unfolding defStage
  defStage-ord : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
               → IsOrd (defStage u pu h)
  defStage-ord u pu h = thePred u pu h .snd .fst

  defStage-suc : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
               → sucV (defStage u pu h) ≡ μ u pu h
  defStage-suc u pu h = thePred u pu h .snd .snd

Two readings of that equation, and they are the two the construction ahead uses. The stage where the cell is first met is the definable powerset of the definition stage, so a first member of the cell is a definable subset there and has a name. And the definition stage misses the cell outright, since it belongs to the least stage that does not.

Lset-μ : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
       → Lset (μ u pu h) ≡ 𝒟ₒ (Lset (defStage u pu h))
Lset-μ u pu h =
  cong Lset (sym (defStage-suc u pu h)) ∙ Lset-suc (defStage u pu h)

defStage-misses : (u : S) (pu : ⟨ isL u ⟩) (h : Inhabited u)
                → ⟨ meets u (defStage u pu h) ⟩ → Empty.⊥
defStage-misses u pu h m = μ-earliest u pu h (defStage u pu h)
  (defStage-ord u pu h) m
  (subst (λ w → ⟨ defStage u pu h ∈ˢ w ⟩) (defStage-suc u pu h)
    (self∈sucV (defStage u pu h)))

One stage for everything below a set

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 has to be cleared, the tower's limit level. The construction ahead compares names; a name is built from numerals and pairs and from nothing else, so it has appeared by Lset ω, and the stage doing the bookkeeping must therefore lie above ω as well as above the set's own stage. The bounding ordinal of two ordinals settles that in one line, and monotonicity carries both levels up into its stage.

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)

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)

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

bound-limit : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ Lset ω ⟩
            → ⟨ x ∈ˢ Lset (stageBound a p .fst) ⟩
bound-limit a p x x∈ = Lset-mono (stageBound a p .snd .snd .fst) x∈

bound-self : (a : S) (p : ⟨ isL a ⟩) → ⟨ a ∈ˢ Lset (stageBound a p .fst) ⟩
bound-self a p = Lset-mono (stageBound a p .snd .snd .snd) (stage-mem a p)

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

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)

Recap

μ is the earliest stage at which a set of L has a member, and

meet-suc says that stage is a successor, because a set enters the tower only by being carved out of the stage below. defStage is the stage it succeeds, a function because a successor determines what it succeeds among ordinals (ord-suc-inj), and Lset-μ identifies the stage of first appearance with the definable powerset over it. So every set that first appears there carries a name written over one fixed stage, which is what the choosing device will compare. stageBound supplies the ordinal the bookkeeping runs in: above a set's own stage, hence above its members and theirs, and above the tower's limit level, where the names themselves live.

Nothing here states a relation on L, and nothing here is a recursion. The comparison and the recursion both arrive in the next chapters, and both are confined to the material this one has located.