Well-orders on all stages

For each ordinal γ, this chapter constructs in the ambient type theory a strict well-order on the members of Lset γ. The construction has two nested parts. A set is first assigned the ordinal over which it is first definable; sets born at different ordinals are ordered by those ordinals, while sets born together are ordered by their least names over the common earlier stage. Membership induction then supplies these stage orders simultaneously. The result is a host-level order at each stage, not yet an internal relation of set theory and not a single well-order of all of L.

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

The classical assumption is used at the point where a merely inhabited family of names is turned into its determined least member. For every index, stepAt is uniformly obtained from this least-name construction.

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

All constructions are carried out at a fixed universe level under the single hypothesis LEM (ℓ-suc ℓ). This same assumption is passed to the construction of the name order and to the least-name search; assembling the stage orders introduces no additional classical premise.

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

The objects ordered here are members of the cumulative hierarchy as seen by the ambient type theory. Their membership proofs travel with them, but those proofs are propositions, so they do not create extra copies of an element. This distinction will matter when the same order is later described and represented inside L.

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl; ∈-induction; ∈-induction-compute )
open import V.Model {ℓ} using ( self∈sucV )
open import L.Constructible {ℓ}
  using ( IsOrd; isL; Lset; Lset→isL )

To locate a set's birth, begin with the earliest ordinal stage containing it. That stage is a successor, so it has a predecessor; this predecessor is the stage over which the set first appears as a definable subset. Ordinal trichotomy will later show that this birth lies strictly below every ordinal stage containing the set.

open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( IsPredOf; predOf; carveAt )

Once a stage is well-ordered, its formulas and parameter lists form well-ordered names for the next stage. A successor-stage member may have many such names, so the construction selects the least one and compares members through these selected representatives. The relevant uniqueness belongs to the least representative, not to names in general.

open import L.Choice.FiniteStageOrders {ℓ} lem using ( Tri-map )
open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; isPropLeastOf )

Several changes of representation occur in this construction: from a presented index to the set it denotes, from a set to a member paired with its membership proof, and from a member to its least name. Each change is injective, so equality and strict comparison can be transported without identifying distinct elements.

open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )

Name completeness gives only propositional truncation of existence: it says that a denoting name merely exists, without exposing a chosen one. The later least-element argument may eliminate this truncation because the total type of least names is itself a proposition.

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties

A hierarchy set has both a small presentation type and an ambient membership type. The presentation map embeds the former into the latter. This bridge lets the construction use small parameters when forming names while retaining an order stated directly on the members of Lset γ.

  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV )

From this point on, S denotes the ambient carrier of sets. Statements such as x ∈ˢ Lset γ are therefore external types expressing membership in a constructible stage; they are not yet formulas evaluated in the object theory.

open hPropStructure 𝒮ᵥ

The stage a set is carved at

Apply the general carving argument to the property that x belongs to a stage. Since stage x p is the earliest stage with this property, the result supplies an ordinal δ whose successor is exactly stage x p. Thus δ is the predecessor of the earliest containing stage, rather than another least stage chosen independently.

theCarve : (x : S) (p : ⟨ isL x ⟩) → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
theCarve x p = predOf (λ σ → x ∈ˢ Lset σ) (stage x p) (stage-ord x p)
  (stage-earliest x p)
  (carveAt (λ σ → x ∈ˢ Lset σ) (stage x p) x (stage-mem x p) (λ δ hz → hz))

The ordinal birth x p is this predecessor. Mathematically, it records the stage over which x first appears as a definable subset. It should not be read as the von Neumann rank of x; the only identification made here is between its successor and the earliest constructible stage containing x.

opaque
  birth : (x : S) → ⟨ isL x ⟩ → S
  birth x p = theCarve x p .fst

The predecessor data in theCarve x p contain both a proof that the chosen predecessor is an ordinal and the equation identifying its successor with stage x p. The theorem birth-ord reads the former component, so birth x p may later be compared with other ordinals and used as an index for membership induction.

opaque
  unfolding birth
  birth-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (birth x p)
  birth-ord x p = theCarve x p .snd .fst

The second projection gives the defining equation sucV (birth x p) ≡ stage x p. This equation connects the two useful viewpoints: stage tells where x first belongs, while birth tells the earlier stage over which x was formed.

  birth-suc : (x : S) (p : ⟨ isL x ⟩) → sucV (birth x p) ≡ stage x p
  birth-suc x p = theCarve x p .snd .snd

Because x belongs to its earliest stage and that stage is sucV (birth x p), it belongs to the successor stage over its birth. This is precisely the membership needed to treat x as a definable subset of Lset (birth x p) and hence to assign it a name there.

birth-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (sucV (birth x p)) ⟩
birth-mem x p =
  subst (λ w → ⟨ x ∈ˢ Lset w ⟩) (sym (birth-suc x p)) (stage-mem x p)

The birth ordinal itself lies in its successor ordinal, and the predecessor equation transports this membership to stage x p. Consequently the earliest stage containing x also contains the ordinal over which x was formed.

birth-stage : (x : S) (p : ⟨ isL x ⟩) → ⟨ birth x p ∈ˢ stage x p ⟩
birth-stage x p =
  subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (birth-suc x p) (self∈sucV (birth x p))

Although birth receives a proof p that x is constructible, its value contains no mathematical choice of such a proof. Constructibility is a proposition, so any two proofs p and q are equal; applying birth x to that equality shows that both inputs yield the same ordinal.

birth-proof : (x : S) (p q : ⟨ isL x ⟩) → birth x p ≡ birth x q
birth-proof x p q = cong (birth x) (snd (isL x) p q)

Suppose x ∈ Lset γ, with γ an ordinal. Trichotomy compares γ with the earliest stage stage x p. The case γ ∈ stage x p is impossible: it would exhibit an earlier ordinal stage that already contains x, contradicting the defining minimality of stage x p.

private
  decideIn : (γ x : S) → IsOrd γ → (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
           → ⟨ γ ∈ˢ stage x p ⟩ ⊎ ((γ ≡ stage x p) ⊎ ⟨ stage x p ∈ˢ γ ⟩)
           → ⟨ birth x p ∈ˢ γ ⟩
  decideIn γ x ordγ p h (inl γ∈) = Empty.rec (stage-earliest x p γ ordγ h γ∈)

If γ equals the earliest stage, birth-stage gives the desired membership directly after transport. If the earliest stage belongs to γ, transitivity of the ordinal γ combines birth x p ∈ stage x p with stage x p ∈ γ. These are the two possible noncontradictory cases.

  decideIn γ x ordγ p h (inr (inl e)) =
    subst (λ w → ⟨ birth x p ∈ˢ w ⟩) (sym e) (birth-stage x p)
  decideIn γ x ordγ p h (inr (inr s∈)) = ordγ .fst (birth-stage x p) s∈

It follows that whenever x is a member of an ordinal stage Lset γ, its birth ordinal is a member of γ. The conclusion is strict. Later, when constructing the order at γ, this fact places every member's birth among the smaller ordinals for which the induction hypothesis has already supplied an order.

birth-in : (γ : S) → IsOrd γ → (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset γ ⟩
         → ⟨ birth x p ∈ˢ γ ⟩
birth-in γ ordγ x p h =
  decideIn γ x ordγ p h (ord-tri γ ordγ (stage x p) (stage-ord x p))

Moving a well-order along an injection

For an ambient set A, the type Mem A consists of a set together with evidence that it belongs to A. Carrying the evidence makes later order relations well-typed. Since membership is proposition-valued, two inhabitants with the same underlying set cannot differ merely because their membership evidence was obtained in different ways.

Mem : S → Type (ℓ-suc ℓ)
Mem A = Σ[ x ∈ S ] ⟨ x ∈ˢ A ⟩

Fix a strict well-order w on a type A. The next construction uses only the relation and laws contained in this structure, so it applies equally to name orders, stage-member orders, and their changes of representation.

module _ {ℓc : Level} {A : Type ℓc} (w : SWO A) where
  open SWO w using () renaming ( _<∙_ to _<ʷ_ )

Writing relOf w a b for the strict comparison contained in w lets later statements discuss the relation without exposing how the well-order was assembled. In particular, this notation does not turn the relation into an object of the internal set theory; it remains a type-valued relation in the host theory.

  relOf : A → A → Type (ℓ-suc ℓ)
  relOf a b = a <ʷ b

Let f : B → C be injective and suppose C is strictly well-ordered. Comparing u and v in B by comparing f u and f v should then inherit a strict well-order. Injectivity is essential only for reflecting the equality case back from C to B.

module _ {ℓb ℓc : Level} (B : Type ℓb) (C : Type ℓc) (w : SWO C)
         (f : B → C) (finj : (u v : B) → f u ≡ f v → u ≡ v) where
  open SWO w using () renaming
    ( _<∙_ to _<ᶜ_ ; tri∙ to triᶜ ; irr∙ to irrᶜ
    ; trans∙ to transᶜ ; wf∙ to wfᶜ )

The pulled-back relation declares u smaller than v exactly when the image f u is smaller than f v. Thus it orders B as the ordered subcollection represented by its image in C; no surjectivity or order isomorphism is claimed.

  private
    _<ᵇ_ : B → B → Type (ℓ-suc ℓ)
    u <ᵇ v = f u <ᶜ f v

Trichotomy in C gives three cases for the two images. The two strict cases are already comparisons in the pulled-back relation, while equality of the images gives equality of the original points by injectivity. Hence the relation on B is trichotomous.

    pullTri : (u v : B) → Tri (u <ᵇ v) (u ≡ v) (v <ᵇ u)
    pullTri u v = Tri-map id (finj u v) id (triᶜ (f u) (f v))

Well-foundedness also pulls back. If f u is accessible in C, its accessibility tree contains a subtree for every f v below it. A predecessor v of u supplies exactly such a comparison, and recursively pulling back the corresponding subtree makes v accessible in B. Thus accessibility, rather than merely the absence of a displayed descending sequence, is transported along f.

    pullAcc : (u : B) → Acc _<ᶜ_ (f u) → Acc _<ᵇ_ u
    pullAcc u (acc r) = acc (λ v h → pullAcc v (r (f v) h))

Irreflexivity transfers immediately: a point below itself in the pulled-back relation would make its image below itself in C. Together with the trichotomy just proved, this supplies the first order laws on the source.

  pullOrder : SWO B
  pullOrder = record
    { _<∙_   = _<ᵇ_
    ; tri∙   = pullTri
    ; irr∙   = λ u h → irrᶜ (f u) h

Transitivity follows by composing comparisons of the three images in C, and the accessibility argument supplies well-foundedness. These laws complete pullOrder, the strict well-order on B obtained by viewing its elements through the injection f.

    ; trans∙ = λ u v z → transᶜ (f u) (f v) (f z)
    ; wf∙    = λ u → pullAcc u (wfᶜ (f u)) }

Every index in the small presentation ⟪ A ⟫ denotes an actual member of A. Pairing its image with this membership evidence gives a map from presentation indices into Mem A, the form on which stage orders are constructed.

memOf : (A : S) (m : ⟪ A ⟫) → ⟨ ⟪ A ⟫↪ m ∈ˢ A ⟩
memOf A m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)

The function carry uses this map to pull an order on ambient member pairs back to the small presentation type. This is the direction required by the naming construction, whose parameter vectors range over ⟪ A ⟫, while the family constructed later naturally orders Mem A.

carry : (A : S) → SWO (Mem A) → SWO ⟪ A ⟫
carry A w = pullOrder ⟪ A ⟫ (Mem A) w (λ m → ⟪ A ⟫↪ m , memOf A m) inj
  where
  inj : (u v : ⟪ A ⟫)
      → _≡_ {A = Mem A} (⟪ A ⟫↪ u , memOf A u) (⟪ A ⟫↪ v , memOf A v) → u ≡ v

The presentation map is an embedding, so equality of the resulting member pairs forces equality of their underlying presented elements and hence of the original indices. This verifies the injectivity needed by pullOrder; it does not assert that every arbitrary presentation of a member has been chosen.

  inj u v q = isEmbedding→Inj isEmb⟪ A ⟫↪ u v (cong fst q)

The step

For a stage index δ, New δ is the type of all members of Lset (sucV δ), each paired with its membership evidence. The name is convenient for the one-step construction, but it does not mean that every such member is born exactly at δ; older members may also persist into this successor stage.

New : S → Type (ℓ-suc ℓ)
New δ = Mem (Lset (sucV δ))

Fix an index δ and a strict well-order on the small members of Lset δ. The naming construction can now compare names over this stage, because its parameter component is compared using precisely that supplied order. This gives the uniform local construction used at every index.

module _ (δ : S) (w : SWO ⟪ Lset δ ⟫) where
  private
    module NM = Naming (Lset δ) w

A name denotes a set x when its semantic value is equal to x. Equality of hierarchy sets is a proposition, so denotation forms an hProp-valued family. This proposition-valued form is what the general least-element construction requires.

  denotesAt : S → NM.Name → hProp (ℓ-suc ℓ)
  denotesAt x n = (NM.denote n ≡ x) , setIsSet (NM.denote n) x

For a : New δ, only the underlying set a.fst is named. Its membership evidence establishes that the set lies in the successor stage, but it is not part of the denotation equation and therefore cannot affect which name is least.

  private
    denotes : New δ → NM.Name → hProp (ℓ-suc ℓ)
    denotes a = denotesAt (a .fst)

Membership in Lset (sucV δ) is rewritten by the successor-stage equation as membership in the definable powerset over Lset δ. Name completeness then gives the propositional truncation of a pair consisting of a name and evidence that it denotes a.fst. At this point there is still no chosen name.

    hasName : (a : New δ) → ∥ Σ[ n ∈ NM.Name ] ⟨ denotes a n ⟩ ∥₁
    hasName a = NM.names-complete (a .fst)
      (subst (λ v → ⟨ a .fst ∈ˢ v ⟩) (Lset-suc δ) (a .snd))

The name order is a strict well-order, so a merely inhabited family of denoting names has a least member. The least-element construction uses the classical hypothesis for its descent. Eliminating the propositional truncation is legitimate because the total type of a name together with proof that it is least is a proposition: any two such names are equal by trichotomy.

    leastOfNew : (a : New δ)
               → Σ[ n ∈ NM.Name ] IsLeast NM.nameOrder (denotes a) n
    leastOfNew a = NM.leastName (denotes a) (hasName a)

Define theName a to be the name component of this least witness. The construction is canonical in the precise sense supplied by the well-order: although completeness exposed no arbitrary representative, the least representative is uniquely determined.

    theName : New δ → NM.Name
    theName a = leastOfNew a .fst

Leastness includes membership in the family being minimized. Hence the selected name really denotes a.fst; minimality alone would not suffice, since a name outside the denoting family could lie anywhere in the ambient name order.

    theName-denote : (a : New δ) → NM.denote (theName a) ≡ a .fst
    theName-denote a = leastOfNew a .snd .fst

If two successor-stage members have the same selected least name, applying denotation shows that their underlying sets are equal. Their membership components are propositions, so this equality lifts to equality of the member pairs. Thus selecting the least name defines an injection, even though denotation on all names need not be injective.

    nameInj : (u v : New δ) → theName u ≡ theName v → u ≡ v
    nameInj u v q = Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV δ)))
      (sym (theName-denote u) ∙ cong NM.denote q ∙ theName-denote v)

Pull the strict well-order of names back along this injection. Two members of Lset (sucV δ) are then compared by their selected least names. This is the sole construction used by the later stepAt: every δ follows this same least-name route.

  byName : SWO (New δ)
  byName = pullOrder (New δ) NM.Name NM.nameOrder theName nameInj

IsLeastName t x says two things: t denotes x, and no other name that denotes x lies strictly below t in the name order. The restriction to names that denote x matters; names denoting other sets play no role in this leastness assertion.

  IsLeastName : NM.Name → S → Type (ℓ-suc ℓ)
  IsLeastName t x = IsLeast NM.nameOrder (denotesAt x) t

For each member a : New δ, the construction supplies a name together with IsLeastName evidence for its underlying set. Subsequent proofs can therefore reason with a least name without unfolding how the search found it or replacing propositional truncation by an arbitrary choice.

  leastNameOf : (a : New δ) → Σ[ t ∈ NM.Name ] IsLeastName t (fst a)
  leastNameOf a = leastOfNew a

Suppose t is any name satisfying IsLeastName t (fst c). Both (theName c, leastOfNew c .snd) and (t,h) are least witnesses for the same denotation predicate. The total type of such least witnesses is a proposition: trichotomy rules out either name being strictly below the other and forces the names to be equal. Projecting that equality yields theName c ≡ t. Thus the least name is unique, while the set may still have many nonleast names.

  private
    pin : (c : New δ) (t : NM.Name) → IsLeastName t (fst c) → theName c ≡ t
    pin c t h = cong fst
      (isPropLeastOf NM.nameOrder (denotes c) (leastOfNew c) (t , h))

The comparison fact pins each candidate's least name: if t₁ is a least name for a and t₂ is a least name for b, then the order relation computed by the pullback agrees with the order of the two least names themselves. This follows because each pinned name equals the computed minimum, so the pullback order transports through those equalities.

    byName-least : (a b : New δ) (t₁ t₂ : NM.Name)
                 → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                 → relOf byName a b ≡ NM._≺ₙ_ t₁ t₂
    byName-least a b t₁ t₂ h₁ h₂ = cong₂ NM._≺ₙ_ (pin a t₁ h₁) (pin b t₂ h₂)

For every ordinal δ, the step order is the single order byName: members of Lset (sucV δ) are compared through their uniquely determined least names over Lset δ. There is no separate finite-stage or limit-stage branch in this construction.

  opaque
    stepAt : SWO (New δ)
    stepAt = byName

The two bridge lemmas let us reason about stepAt through any representatives already proved least. For least names t₁ and t₂ of two members, comparison in stepAt and comparison of t₁ with t₂ determine one another. Hence later arguments need the specification of the selected names, not the particular search that produced them.

  opaque
    unfolding stepAt

The filling reading says: if two names are least for their respective members, then the order of the names determines the order of the members. The proof transports the name comparison through the agreement between each pinned name and the computed minimum.

    stepAt-fill : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → NM._≺ₙ_ t₁ t₂ → relOf stepAt a b
    stepAt-fill a b t₁ t₂ h₁ h₂ =
      transport (sym (byName-least a b t₁ t₂ h₁ h₂))

The reading lemma says the converse: if the step order holds between two members, the least names of those members are ordered the same way.

    stepAt-read : (a b : New δ) (t₁ t₂ : NM.Name)
                → IsLeastName t₁ (fst a) → IsLeastName t₂ (fst b)
                → relOf stepAt a b → NM._≺ₙ_ t₁ t₂
    stepAt-read a b t₁ t₂ h₁ h₂ =
      transport (byName-least a b t₁ t₂ h₁ h₂)

The family

The relation Under δ v x y records a comparison of the underlying sets x and y without fixing particular membership proofs in advance. It consists of two certificates placing them in Lset (sucV δ), together with the comparison of the resulting members by v. This is an ordinary Sigma type, not a propositional truncation; only the membership certificates themselves are propositionally unique.

Under : (δ : S) → SWO (New δ) → S → S → Type (ℓ-suc ℓ)
Under δ v x y = Σ[ hx ∈ ⟨ x ∈ˢ Lset (sucV δ) ⟩ ]
                Σ[ hy ∈ ⟨ y ∈ˢ Lset (sucV δ) ⟩ ]
                relOf v (x , hx) (y , hy)

Given any chosen membership certificates hx and hy, under-at reads an Under comparison at those presentations. The certificates stored by Under need not be the same terms as hx and hy; their equality follows from the propositionality of membership.

under-at : (δ : S) (v : SWO (New δ)) (x y : S)
           (hx : ⟨ x ∈ˢ Lset (sucV δ) ⟩) (hy : ⟨ y ∈ˢ Lset (sucV δ) ⟩)
         → Under δ v x y → relOf v (x , hx) (y , hy)
under-at δ v x y hx hy (kx , ky , h) =
  subst2 (λ p q → relOf v (x , p) (y , q))

This certificate alignment is what makes Under useful in the recursive family. Equal birth ordinals often place the same set in the same successor stage by different proofs; under-at lets the local comparison survive those changes of evidence without requiring the comparison type itself to be a proposition.

    (snd (x ∈ˢ Lset (sucV δ)) kx hx) (snd (y ∈ˢ Lset (sucV δ)) ky hy) h

Fix an ordinal γ. To construct its stage order, assume recursively that every ordinal δ ∈ γ already carries a strict well-order on Mem (Lset δ). The module Family turns precisely these smaller-stage orders into an order on the members of Lset γ.

module Family (γ : S)
              (IH : (δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
              (ordγ : IsOrd γ) where
  private
    Member : Type (ℓ-suc ℓ)

The carrier at this stage is Member = Mem (Lset γ): an element of the hierarchy together with evidence that it belongs to the stage Lset γ.

    Member = Mem (Lset γ)

Because γ is an ordinal, membership in Lset γ implies constructibility. Thus every a : Member has the constructibility proof required to form its birth ordinal.

    memberL : (a : Member) → ⟨ isL (a .fst) ⟩
    memberL a = Lset→isL γ ordγ (a .fst) (a .snd)

Each layer member belongs to the successor of its own birth ordinal, by the membership reading of the birth construction.

    newIn : (a : Member) → ⟨ a .fst ∈ˢ Lset (sucV (birth (a .fst) (memberL a))) ⟩
    newIn a = birth-mem (a .fst) (memberL a)

The birth of a member is packaged as a member of the ordinal index γ: the birth ordinal together with the proof that it lies below γ, which follows from the member being in the layer at γ.

  bornAt : Member → Mem γ
  bornAt a = birth (a .fst) (memberL a)
           , birth-in γ ordγ (a .fst) (memberL a) (a .snd)

For d : Mem γ, the induction hypothesis supplies an order on the certified members of Lset (d .fst). The operation carry moves it to the small presentation used by names, and stepAt then well-orders the certified members of Lset (sucV (d .fst)) by their least names. This is the local order used for sets born over d .fst.

  stepIn : (d : Mem γ) → SWO (New (d .fst))
  stepIn d = stepAt (d .fst) (carry (Lset (d .fst))
    (IH (d .fst) (d .snd) (mem-ord {A = γ} ordγ (d .fst) (d .snd))))

For a packaged ordinal d : Mem γ, UnderAt d a b applies the certificate-independent relation Under to the local step order at d. In the equal-birth branch below, d will be the common birth of a and b.

  UnderAt : (d : Mem γ) → Member → Member → Type (ℓ-suc ℓ)
  UnderAt d a b = Under (d .fst) (stepIn d) (a .fst) (b .fst)

The main relation is lexicographic. If the birth ordinal of a belongs to the birth ordinal of b, then a ≺ b. When the two birth ordinals are equal, their underlying sets are compared by the local step order at a's birth. The equality is oriented from b's birth to a's so that the second set can be placed directly in that same local order.

  _≺_ : Member → Member → Type (ℓ-suc ℓ)
  a ≺ b = ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩
        ⊎ ((bornAt b .fst ≡ bornAt a .fst) × UnderAt (bornAt a) a b)

The packaging helper says that two members of the ordinal index with the same underlying ordinal are equal, using the propositionality of membership in the ordinal.

  private
    packBirth : (d z : Mem γ) → d .fst ≡ z .fst → d ≡ z
    packBirth d z = Σ≡Prop (λ v → snd (v ∈ˢ γ))

Irreflexivity follows from the two meanings of the lexicographic relation. An early-birth witness for a ≺ a would make the ordinal birth(a) a member of itself. An equal-birth witness instead gives a local comparison of a with itself; its stored membership certificates may differ from newIn a, but under-at reads the comparison at the latter certificates so that local irreflexivity applies.

  private
    ≺-irr : (a : Member) → a ≺ a → Empty.⊥
    ≺-irr a (inl h) = ∈-irrefl (bornAt a .fst) h
    ≺-irr a (inr (_ , u)) =
      SWO.irr∙ (stepIn (bornAt a)) (a .fst , newIn a)

Only the membership certificates are replaced in this passage. Their propositionhood identifies the two presentations of a, while the local comparison proof is transported unchanged to the presentation at which the strict well-order forbids self-comparison.

        (under-at (bornAt a .fst) (stepIn (bornAt a)) (a .fst) (a .fst)
          (newIn a) (newIn a) u)

Transitivity has four cases. In the early-early case, transitivity of the birth ordinals composes the two strict memberships. In the early-equal case, the equality transports the birth membership past the common birth ordinal.

    ≺-trans : (a b c : Member) → a ≺ b → b ≺ c → a ≺ c
    ≺-trans a b c (inl h) (inl k) =
      inl (birth-ord (c .fst) (memberL c) .fst h k)
    ≺-trans a b c (inl h) (inr (e , _)) =
      inl (subst (λ v → ⟨ bornAt a .fst ∈ˢ v ⟩) (sym e) h)

The remaining mixed case transports the strict inequality between birth ordinals across their equality. When both comparisons use the equal-birth branch, the two equalities identify a single birth ordinal, and transitivity reduces to composing the two comparisons in its local step order.

    ≺-trans a b c (inr (e , _)) (inl k) =
      inl (subst (λ v → ⟨ v ∈ˢ bornAt c .fst ⟩) e k)
    ≺-trans a b c (inr (e , u)) (inr (eb , v)) = inr (eb ∙ e , joined)
      where
      d : Mem γ

In the equal-equal case, take d = bornAt a as the common packaged birth. The first comparison already lives in the local order stepIn d. Equality of the packaged births transports the second comparison from the local order indexed by bornAt b to that same stepIn d; this alignment is necessary because the local order depends on its packaged index.

      d = bornAt a
      moved : UnderAt d b c
      moved = subst (λ z → UnderAt z b c) (packBirth (bornAt b) d e) v
      joined : UnderAt d a c
      joined = u .fst , (moved .snd .fst

Both premises can now be read inside one strict well-order. The certificates carried by the two UnderAt witnesses are aligned at the middle set b, and transitivity of stepIn d composes the local comparisons from a to b and from b to c.

        , SWO.trans∙ (stepIn d) (a .fst , u .fst) (b .fst , moved .fst)
            (c .fst , moved .snd .fst)
            (under-at (d .fst) (stepIn d) (a .fst) (b .fst)
              (u .fst) (moved .fst) u)
            (under-at (d .fst) (stepIn d) (b .fst) (c .fst)

The composite local comparison, together with the endpoint certificates already obtained at the common birth, is an UnderAt d a c witness. Thus the equal-birth branch is transitive for the same mathematical reason as the name order beneath it: all three sets are compared in one fixed local order.

              (moved .fst) (moved .snd .fst) moved))

For trichotomy, first compare the two birth ordinals. Their ordinality proofs make ordinal trichotomy applicable, producing exactly the alternatives「the first birth is earlier」，「the births are equal」，and“the second birth is earlier”. Only the middle alternative requires a comparison in a local step order.

    ≺-tri : (a b : Member) → Tri (a ≺ b) (a ≡ b) (b ≺ a)
    ≺-tri a b = byBirth (ord-tri (bornAt a .fst) (birth-ord (a .fst) (memberL a))
                                 (bornAt b .fst) (birth-ord (b .fst) (memberL b)))
      where
      byBirth : ⟨ bornAt a .fst ∈ˢ bornAt b .fst ⟩

When the births differ, their strict ordinal comparison already decides the main order. No name of either set is inspected in these two cases; the least-name order is reserved for sets with a common birth ordinal.

              ⊎ ((bornAt a .fst ≡ bornAt b .fst) ⊎ ⟨ bornAt b .fst ∈ˢ bornAt a .fst ⟩)
              → Tri (a ≺ b) (a ≡ b) (b ≺ a)
      byBirth (inl h)       = lt (inl h)
      byBirth (inr (inr h)) = gt (inl h)
      byBirth (inr (inl e)) =

In the equal-birth case, the local step order at the common birth ordinal decides the comparison. The two members' certificates are realigned to the common birth ordinal.

The alignment of the first certificate is the member's own successor membership.

        bySteps (SWO.tri∙ (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
        where
        same : bornAt b .fst ≡ bornAt a .fst
        same = sym e
        ha : ⟨ a .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩

The first set already belongs to the successor of its birth. Equality of births transports the corresponding certificate for the second set to that same successor layer, so the local trichotomy can compare both members in one carrier.

        ha = newIn a
        hb : ⟨ b .fst ∈ˢ Lset (sucV (bornAt a .fst)) ⟩
        hb = subst (λ v → ⟨ b .fst ∈ˢ Lset (sucV v) ⟩) (sym e) (newIn b)
        bySteps : Tri (relOf (stepIn (bornAt a)) (a .fst , ha) (b .fst , hb))
                      ((a .fst , ha) ≡ (b .fst , hb))

Local trichotomy supplies comparison in either direction or equality of the two certified successor-stage members. In the equality case, equality of the underlying sets follows immediately; since membership in Lset γ is a proposition, that equality lifts to equality of the original members a and b of the stage.

                      (relOf (stepIn (bornAt a)) (b .fst , hb) (a .fst , ha))
                → Tri (a ≺ b) (a ≡ b) (b ≺ a)
        bySteps (lt h) = lt (inr (same , (ha , hb , h)))
        bySteps (eq q) = eq (Σ≡Prop (λ v → snd (v ∈ˢ Lset γ)) (cong fst q))
        bySteps (gt h) = gt (inr (sym same

If the local trichotomy places b below a, the common-birth equality is reoriented and the packaged birth index is transported accordingly. This produces the right-hand alternative b ≺ a of the main trichotomy.

          , subst (λ z → UnderAt z b a)
              (packBirth (bornAt a) (bornAt b) (sym same)) (hb , ha , h)))

Well-foundedness requires two coordinated descents. Fix a packaged birth ordinal d. The outer hypothesis supplies accessibility for members whose births are strictly below d, while an accessibility tree for stepIn d supplies the inner descent among members born at d. The role of accInside is to lift this inner tree to accessibility for the full lexicographic relation while retaining access to the outer hypothesis.

  private
    accInside : (d : Mem γ)
              → ((z : Mem γ) → ⟨ z .fst ∈ˢ d .fst ⟩
                 → (b : Member) → bornAt b ≡ z → Acc _≺_ b)
              → (u : New (d .fst)) → Acc (relOf (stepIn d)) u

Assume that a local element u is accessible in stepIn d, and that a stage member b has birth d and the same underlying set as u. To prove b accessible for the main relation, consider an arbitrary predecessor c ≺ b. The definition of the main relation tells us which of the two descent resources applies to c.

              → (b : Member) → bornAt b ≡ d → b .fst ≡ u .fst → Acc _≺_ b
    accInside d ih u (acc r) b q qu = acc step
      where
      step : (c : Member) → c ≺ b → Acc _≺_ c
      step c (inl h) = ih (bornAt c)

If c was compared with b by an earlier birth, its birth is strictly below d, so the outer induction hypothesis makes c accessible. If their births agree, c is a predecessor of u in the fixed local order, and the accessibility tree of u supplies the smaller inner subtree. These are precisely the two clauses of the lexicographic relation.

        (subst (λ v → ⟨ bornAt c .fst ∈ˢ v ⟩) (cong fst q) h) c refl
      step c (inr (eb , v)) =
        accInside d ih (c .fst , hc) (r (c .fst , hc) below) c qc refl
        where
        qc : bornAt c ≡ d

In the equal-birth clause, equality of the underlying birth ordinals is first lifted to equality of their packaged members of γ. This permits the UnderAt comparison to be transported to the fixed index d; its first component then certifies that c belongs to the successor stage on which stepIn d is defined.

        qc = packBirth (bornAt c) d (sym eb ∙ cong fst q)
        moved : UnderAt d c b
        moved = subst (λ z → UnderAt z c b) qc v
        hc : ⟨ c .fst ∈ˢ Lset (sucV (d .fst)) ⟩
        hc = moved .fst

Reading the transported UnderAt witness with the aligned certificates gives a comparison from the local representative of c to that of b. The assumed equality between the underlying sets of b and u changes the right endpoint to u. The resulting local predecessor proof selects the subtree below u, and recursion lifts that subtree back to accessibility for c in the main order.

        below : relOf (stepIn d) (c .fst , hc) u
        below = subst (λ z → relOf (stepIn d) (c .fst , hc) z)
          (Σ≡Prop (λ x → snd (x ∈ˢ Lset (sucV (d .fst)))) qu)
          (under-at (d .fst) (stepIn d) (c .fst) (b .fst)
            hc (moved .snd .fst) moved)

The outer descent is membership induction on the birth ordinal. Its motive says that every stage member whose packaged birth is (δ , i) is accessible for the main relation. Consequently, at the induction step for δ, the hypothesis covers exactly the members whose births are packaged over ordinals strictly belonging to δ.

    accByBirth : (δ : S) (i : ⟨ δ ∈ˢ γ ⟩)
               → (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
    accByBirth = ∈-induction {P = Motive} outer
      where
      Motive : S → Type (ℓ-suc ℓ)

At a fixed birth δ, the local strict well-order already makes the corresponding representative of b accessible. The outer step feeds this local accessibility and the hypotheses for all smaller births into accInside. This is where the inner descent is started inside the outer membership induction.

      Motive δ = (i : ⟨ δ ∈ˢ γ ⟩) (b : Member) → bornAt b ≡ (δ , i) → Acc _≺_ b
      outer : (δ : S) → ((z : S) → ⟨ z ∈ˢ δ ⟩ → Motive z) → Motive δ
      outer δ ih i b q = accInside (δ , i) inner (b .fst , hb)
        (SWO.wf∙ (stepIn (δ , i)) (b .fst , hb)) b q refl
        where

The equality q identifies the packaged birth of b with (δ , i), so birth-mem can be transported to a certificate hb placing b in Lset (sucV δ). For a smaller packaged birth z, its first component lies in δ; the outer induction hypothesis at that ordinal, together with z's membership in γ, supplies accessibility for every member born at z.

        hb : ⟨ b .fst ∈ˢ Lset (sucV δ) ⟩
        hb = subst (λ z → ⟨ b .fst ∈ˢ Lset (sucV (z .fst)) ⟩) q (newIn b)
        inner : (z : Mem γ) → ⟨ z .fst ∈ˢ δ ⟩
              → (c : Member) → bornAt c ≡ z → Acc _≺_ c
        inner z h c qz = ih (z .fst) h (z .snd) c qz

Every member is therefore accessible for the main relation. The conclusion uses both layers: the outer membership induction handles a predecessor with an earlier birth, and at each fixed birth the accessibility tree of the local step order handles a predecessor with the same birth. Neither layer alone proves well-foundedness of the lexicographic order.

    ≺-wf : WellFounded _≺_
    ≺-wf a = accByBirth (bornAt a .fst) (bornAt a .snd) a refl

The lexicographic relation and the proofs just established now form a strict well-order on Mem (Lset γ): birth ordinals give the primary comparison, and the least-name step order resolves equal births.

  famOrder : SWO (Mem (Lset γ))
  famOrder = record
    { _<∙_   = _≺_
    ; tri∙   = ≺-tri
    ; irr∙   = ≺-irr

Transitivity and the two-level well-foundedness argument complete the order laws, so famOrder is available from the assumed orders at all smaller ordinal stages.

    ; trans∙ = ≺-trans
    ; wf∙    = ≺-wf }

The function famStep packages this recursive step: at γ, it takes the orders already constructed at every member ordinal δ ∈ γ and returns the strict well-order of Mem (Lset γ) proved above. The same construction applies uniformly to every ordinal; it has no separate zero, successor, or limit clause.

famStep : (γ : S) → ((δ : S) → ⟨ δ ∈ˢ γ ⟩ → IsOrd δ → SWO (Mem (Lset δ)))
        → IsOrd γ → SWO (Mem (Lset γ))
famStep = Family.famOrder

Membership induction applies famStep simultaneously at all ordinal indices. The result orderAt γ is a host-level strict well-order on the certified members of the single stage Lset γ; it is neither an object-language relation nor one relation on all of L.

opaque
  orderAt : (γ : S) → IsOrd γ → SWO (Mem (Lset γ))
  orderAt = ∈-induction famStep

The equation orderAt-step exposes one recursive layer: the order at γ is famStep γ applied to the previously constructed orders orderAt δ for δ ∈ γ. It permits later arguments to use the birth-first description without unfolding the entire membership recursion.

opaque
  unfolding orderAt
  orderAt-step : (γ : S) → orderAt γ ≡ famStep γ (λ δ _ → orderAt δ)
  orderAt-step = ∈-induction-compute famStep

Finally, stageOrder γ presents the same stagewise order on the small index type ⟪ Lset γ ⟫. The canonical embedding sends each index to its represented member with a membership certificate, and carry pulls orderAt γ back along this injection. This changes only the representation of the carrier, not the comparison being constructed.

stageOrder : (γ : S) → IsOrd γ → SWO ⟪ Lset γ ⟫
stageOrder γ oγ = carry (Lset γ) (orderAt γ oγ)

Recap

For every ordinal γ, orderAt γ is a host-level strict well-order on the certified members of Lset γ. It first compares the predecessors of the members' earliest containing stages, and only for equal births compares their uniquely determined least names over the common earlier stage. The local stepAt construction has this one least-name form at every index, while the global well-foundedness proof combines descent of birth ordinals with descent in the local name order. The relation has not yet been turned into an object-language formula or a set belonging to L; later chapters perform those internalization steps.