One order for every stage

The previous chapters have three things ready and one thing missing. The stage chapter located, for each cell, the one stage at which it first has a member, and showed that stage to be a successor; the finite chapter well-ordered every stage below ω and the limit stage itself; the naming chapter wrote each member of a successor stage as a name and well-ordered the names, given a well-order of the stage below. That proviso is the missing thing. Names cannot order a stage until the stage below is ordered, so what has to be built is not one order but a family: an order at every stage, each of them an ingredient of the next.

The family is built by membership induction on the ordinal, and the whole chapter turns on one decision about what it compares first. A member of a stage entered the tower at a definite moment: there is an earliest stage containing it, that stage is a successor, and the ordinal it succeeds is the one the set was carved over. That ordinal is the primary key. Two sets carved at different moments are compared by those moments and by nothing else; only two sets carved at the same moment are compared by the machinery of that moment, which is the previous chapter's names, or, below the limit stage, the finite chapter's comparison at the earliest disagreement.

Taking the stage as the primary key buys the property the rest of the part needs. The order at a large stage has to restrict, on a smaller one, to the order there, or a choice made at one stage would be unmade at the next. Here that is not a theorem about the construction but a reading of the definition: the comparison of two sets never mentions the stage it is being read at. It mentions the two sets' own births, and those do not move.

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

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

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

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; isPropIsOrd; isL; Lset; Lset-out; Lset-mono; Lset→isL; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
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.Stage {ℓ} lem using ( IsPredOf; isPropPredOf )
open import L.Choice.Finite {ℓ} lem using ( Tri-map )
open import L.Choice.Name {ℓ} lem using ( module Naming )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( Tri; lt; eq; gt; SWO; IsLeast; isPropLeastOf )

open import Cubical.Foundations.Prelude using ( J; PathP; 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 )
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
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV )

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

The stage a set is carved at

The stage chapter gave every constructible set its earliest stage, and the choice-stage chapter showed, for a cell, that the earliest stage meeting it is a successor. The argument applies verbatim to a single set, and for the same reason: a set enters the tower only by being carved out of the stage below, so if it is there at all by its earliest stage, that stage has a predecessor and the set is one of the definable subsets over it.

The one split in the argument is a comparison in disguise, and it is written as a named helper with its conclusion spelled out: either the candidate's successor lies strictly below the earliest stage, which minimality refutes, or it is that stage.

private
  decideSuc : (x : S) (p : ⟨ isL x ⟩) (δ : S) → IsOrd δ
            → ⟨ x ∈ˢ Lset (sucV δ) ⟩
            → ⟨ sucV δ ∈ˢ stage x p ⟩ ⊎ (sucV δ ≡ stage x p)
            → sucV δ ≡ stage x p
  decideSuc x p δ ordδ m (inl s∈) =
    Empty.rec (stage-earliest x p (sucV δ) (suc-ord ordδ) m s∈)
  decideSuc x p δ ordδ m (inr e) = e

  atCarve : (x : S) (p : ⟨ isL x ⟩)
          → Σ[ δ ∈ S ] (⟨ δ ∈ˢ stage x p ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset δ) ⟩)
          → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
  atCarve x p (δ , (δ∈ , x∈)) = δ , (ordδ , suc≡)
    where
    ordδ : IsOrd δ
    ordδ = mem-ord {A = stage x p} (stage-ord x p) δ δ∈
    atSuc : ⟨ x ∈ˢ Lset (sucV δ) ⟩
    atSuc = subst (λ w → ⟨ x ∈ˢ w ⟩) (sym (Lset-suc δ)) x∈
    suc≡ : sucV δ ≡ stage x p
    suc≡ = decideSuc x p δ ordδ atSuc
      (suc∈or≡ δ (stage x p) ordδ (stage-ord x p) δ∈)

theCarve : (x : S) (p : ⟨ isL x ⟩) → Σ[ δ ∈ S ] IsPredOf (stage x p) δ
theCarve x p = PT.rec (isPropPredOf (stage x p)) (atCarve x p)
  (Lset-out (stage x p) x (stage-mem x p))

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

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

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

The ordinal so extracted is the set's birth: the stage x is carved over, one below the earliest stage containing it. It is sealed exactly as

stage and defStage were, and for the same reason: it unfolds to a well-founded descent through the tower, and every later type mentioning it would drag that descent into conversion.

Two readings open the seal and nothing else does: the birth is an ordinal, and its successor is the earliest stage. Everything the chapter uses is derived from those two without opening anything. The set is a member of the stage just above its birth, which is where the naming chapter looks for it. The birth does not depend on which proof of constructibility is supplied, because constructibility is a proposition, and that one line is what makes the end extension work at the end of the chapter. And a member of a stage is born strictly below that stage: its earliest stage is below the stage or equal to it, and its birth is below its earliest stage, so ordinal trichotomy settles the three cases, again in a named helper with its conclusion written down.

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)

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

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)

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

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

Three times in this chapter a well-order is known on one type and wanted on another that injects into it. The order is the comparison of the images. Trichotomy is the source's trichotomy, with injectivity turning its middle case back into an equality; irreflexivity and transitivity are read off; and well-foundedness descends, because a descent of images is a descent.

The whole transfer is four lines, written once, in the shape its three uses share. It is not a theory of induced orders, and in particular nothing here is generic in a family of orders indexed by a first key: such a thing would have to carry that family and prove its laws in that generality, which is a larger theorem than any this chapter wants.

Two abbreviations travel with the transfer. Mem A is a set's members as pairs of a set with its membership, the shape everything below is stated at; and

relOf reads a bundle's comparison out as a function, which is how an order is passed around as a value rather than opened.

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

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

  relOf : A → A → Type (ℓ-suc ℓ)
  relOf a b = a <ʷ 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ᶜ )

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

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

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

  pullOrder : SWO B
  pullOrder = record
    { _<∙_   = _<ᵇ_
    ; tri∙   = pullTri
    ; irr∙   = λ u h → irrᶜ (f u) h
    ; trans∙ = λ u v z → transᶜ (f u) (f v) (f z)
    ; wf∙    = λ u → pullAcc u (wfᶜ (f u)) }

The first use is the canonical presentation of a set. A set's members come in two shapes: as pairs of a set with a proof that it belongs, which is the shape the construction below produces, and as the small index type the hierarchy presents the set by, which is the shape the naming chapter takes. The index map is an embedding, so moving an order from the first shape to the second is one application of the transfer, done here and not again.

The second use is an inclusion. When every member of one set is a member of another, an order on the second restricts to the first, and the injection is the identity on the underlying sets.

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

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
  inj u v q = isEmbedding→Inj isEmb⟪ A ⟫↪ u v (cong fst q)

The step

The step is the chapter's first deliverable: from a well-order of the members of

Lset δ, a well-order of the members of Lset (sucV δ), written

New δ below, which is to say of the definable subsets of

Lset δ.

It has one branch, and it was written with two. Below the limit stage the members are already ordered, by the finite chapter's well-order of

Lset ω, which is also the order a name's first key is compared by; so a first draft took that order there and the names only above. Measured, the second branch is surplus: taking the names everywhere checks in the same three seconds. What the guard was actually contributing was not a case distinction but a normalization barrier, since a decision by the excluded middle is stuck while the excluded middle is a module parameter, and being stuck is what stops this order from unfolding into the naming chapter's. The opaque seal is that barrier, said in one word, and it is why the definition below is one line.

The reason the first draft gave, that the book should not carry two unrelated well-orders of one set, was a coherence claim, and this chapter never proved it. Kept code needs a better warrant than an argument nobody discharged, so the branch is gone and the claim with it. The base case needs nothing either: the first stage is empty, so its members are well-ordered for want of any.

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

The other branch compares by least name. Every member of

Lset (sucV δ) is denoted by some name, truncated, which is how the definable powerset gives up a formula; the names carry a well-order as soon as the stage below carries one, which is exactly the hypothesis of this step; so the least name denoting a set is a definite name, and each set is sent to it. That map is injective because a name determines what it denotes, and the step order is the name order pulled back along it.

Nothing about names is unpacked here. The naming data stay inside the chapter whose telescope binds them, and this chapter sees a type carrying an order. That is not fastidiousness: the previous chapter measured what happens when naming data are reached from another module, and the answer was that every comparison of codes forces the limit order open.

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

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

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

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

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

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

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

    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)

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

Three definitions leave the module, and they are the least a caller can be given and still say what this order is. denotesAt is the family the search is run at, a set's names; IsLeastName is being a least name of a set, and it is the well-order chapter's IsLeast at that family, not a re-spelling of it; leastNameOf exhibits one for every member of the new stage, and it is the search itself, returned.

That IsLeastName is a definition and not a re-spelling is a measurement. Written out as a pair of a denotation equation and a minimality clause, the search would have to be converted into it at a computed name, and a comparison of names at a computed name unfolds the code order down to the level search it is defined by: 16 s for that one line, against nothing when the property is the family's own IsLeast. The naming data still stay inside; what crosses the boundary is a name the caller already holds.

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

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

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

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

The two branches are joined by the excluded middle, in a named helper whose conclusion is written out rather than inferred. This is the only place the chapter spends the assumption itself; everywhere else it arrives already spent, inside the trichotomy of ordinals, inside the earliest stage, and inside the search for a least name.

  opaque
    stepAt : SWO (New δ)
    stepAt = byName

The seal is a normalization barrier and not a secret, so two readings are let through it, one each way: the step relates two members exactly when the name order relates any two names the caller has shown least. They are the equation above, transported.

They are proved here, inside the telescope that binds the stage and its order, and that placement is a measurement too. Stated at top level and filled with the very lemma above, either reading costs 39 s, which is law 20's shape met at a new place: a statement whose type is written down and whose filling is the same statement forces a conversion this route cannot afford. Inside, where the seal is, both are free.

  opaque
    unfolding stepAt

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

    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

One piece of vocabulary comes first. The step order at a birth has to be applied to two sets that are members of the stage just above that birth, and the membership proofs are in the way: they are what makes the two sets members, they are propositions, and they arrive differently at each occurrence. So the comparison is stated between two sets, with the two memberships quantified inside it, and the ordinal is an explicit argument of the statement.

That shape is what lets an equality of births move a whole comparison from one birth to another in a single transport, which is the recurring move of the proofs below; and under-at reads the comparison back out at any chosen pair of proofs, which is the only bookkeeping the quantification costs.

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)

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))
    (snd (x ∈ˢ Lset (sucV δ)) kx hx) (snd (y ∈ˢ Lset (sucV δ)) ky hy) h

The induction's step takes the orders at every ordinal below γ and produces one at γ. Each member of Lset γ is constructible, because γ is an ordinal, so it has a birth; and that birth is a member of γ. Packaging the birth with that membership gives exactly the datum the induction hypothesis can be applied at, and stepIn is the step order there.

The comparison is then the two-key one: births first, and, when the births agree, the step order at the common birth. The equality of births is carried in the direction that lets the second set be read at the first's birth, which keeps the definition free of a transport; and it is carried as an equality of ordinals rather than of the packaged pairs, which is what makes the end extension below a path instead of an argument. The packaged form is recovered where the transports want it, since the membership is a proposition.

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

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

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

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

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

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

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

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

Irreflexivity is the two keys' own: no ordinal belongs to itself, and no step order puts a set below itself. Transitivity is four cases, of which the two mixed ones carry an equality of births across a membership, and the last composes two comparisons at one birth after moving the second one there.

Trichotomy descends the keys, each reached only when the previous one has pronounced equality: the ordinals first, the step order second. Both splits are named helpers with their conclusion written down. That is the discipline the previous two chapters paid for and this one inherits: a split whose branches conclude in a membership proposition, left to a with or to inference, is solved against the whole disjunction rather than against its own branch.

  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)
        (under-at (bornAt a .fst) (stepIn (bornAt a)) (a .fst) (a .fst)
          (newIn a) (newIn a) u)

    ≺-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)
    ≺-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 γ
      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
        , 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)
              (moved .fst) (moved .snd .fst) moved))

    ≺-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 ⟩
              ⊎ ((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)) =
        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)) ⟩
        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))
                      (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
          , subst (λ z → UnderAt z b a)
              (packBirth (bornAt a) (bornAt b) (sym same)) (hb , ha , h)))

Well-foundedness is two nested inductions, kept apart exactly as the finite chapter kept its own two apart. The outer one is membership induction on the birth, and it hands down a hypothesis covering every earlier birth; the inner one is an ordinary descent along the accessibility the step order already has at that birth. A step down in birth appeals to the outer hypothesis, a step within a birth to the inner one, and since the inner function recurses on nothing but its own accessibility argument the two never have to be compared.

The member always arrives as a member, with an equation saying where its birth sits. That is the same law as the trichotomy's, met again from the other side: an accessibility stated at a member's components would have to be matched against one stated at the member.

  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
              → (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)
        (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
        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
        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)

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

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

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

The family is that step run by membership induction, and it is sealed. Unsealed, an order at a stage unfolds into a recursion over the whole hierarchy, and every type mentioning one would carry that unfolding into conversion;

orderAt-step opens the seal once, on the recursion equation alone, and the end extension below is its only consumer. stageOrder is the same order at the presentation the naming chapter takes, and it is what the argument ahead will hand to leastName.

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

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

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

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

End extension

Two stages, one a member of the other, and a set that is a member of both: the two orders have to agree on it. They do, and the reason is the whole design. A comparison mentions the two births and the step orders at those births, and never the stage it is read at. So two things have to be checked, and both are facts about propositions. The birth of a set does not depend on which stage it was read as a member of, since constructibility is a proposition. And the step order at a birth does not either: it is built from the family below, applied to a proof that the birth is an ordinal, and any two such proofs are equal.

The second of those is the chapter's one path induction, and its whole content is that last sentence, transported over the equality of the two births.

private
  stepPath : (δ : S) (o : IsOrd δ) (δ' : S) (e : δ ≡ δ') (o' : IsOrd δ')
           → PathP (λ k → SWO (New (e k)))
               (stepAt δ (carry (Lset δ) (orderAt δ o)))
               (stepAt δ' (carry (Lset δ') (orderAt δ' o')))
  stepPath δ o δ' e o' = J Motive base e o'
    where
    Motive : (z : S) → δ ≡ z → Type (ℓ-suc (ℓ-suc ℓ))
    Motive z ez = (oz : IsOrd z) → PathP (λ k → SWO (New (ez k)))
      (stepAt δ (carry (Lset δ) (orderAt δ o)))
      (stepAt z (carry (Lset z) (orderAt z oz)))
    base : Motive δ refl
    base oz =
      cong (λ q → stepAt δ (carry (Lset δ) (orderAt δ q))) (isPropIsOrd δ o oz)

With that, the agreement is one line. The comparison is a sum of two components, each of which is a path pointwise in the equality of births, so the two comparisons are not merely equivalent but equal, and every reading of end extension, either direction of the implication included, follows by transport. The order at the larger stage, restricted to the smaller, is the order there.

This is what the route audit predicted, and the measurement bears it out: one path-induction lemma of a dozen lines, one line for the agreement, and two lines to unseal the recursion equation at either end. Nothing else in the chapter was spent on it. The reason is worth stating once more, because it is the reason the primary key was chosen the way it was: the definition of the comparison is already stage-free, so end extension has nothing left to prove beyond the proof-irrelevance of the two propositions it does mention.

module _ (γ β : S) (oγ : IsOrd γ) (oβ : IsOrd β) (i : ⟨ γ ∈ˢ β ⟩) where
  private
    module Fγ = Family γ (λ δ _ → orderAt δ) oγ
    module Fβ = Family β (λ δ _ → orderAt δ) oβ
    open Fγ using () renaming ( _≺_ to _≺ᵍ_ ; bornAt to bornγ )
    open Fβ using () renaming ( _≺_ to _≺ᵇ_ ; bornAt to bornβ )

    up : Mem (Lset γ) → Mem (Lset β)
    up a = a .fst , Lset-mono {α = β} {β = γ} i {x = a .fst} (a .snd)

    sameBirth : (a : Mem (Lset γ)) → bornγ a .fst ≡ bornβ (up a) .fst
    sameBirth a = birth-proof (a .fst) _ _

    sameStep : (a : Mem (Lset γ))
             → PathP (λ k → SWO (New (sameBirth a k)))
                 (Fγ.stepIn (bornγ a)) (Fβ.stepIn (bornβ (up a)))
    sameStep a = stepPath (bornγ a .fst) _ (bornβ (up a) .fst) (sameBirth a) _

    agree : (a b : Mem (Lset γ)) → (a ≺ᵍ b) ≡ (up a ≺ᵇ up b)
    agree a b k = ⟨ sameBirth a k ∈ˢ sameBirth b k ⟩
                ⊎ ( (sameBirth b k ≡ sameBirth a k)
                  × Under (sameBirth a k) (sameStep a k) (a .fst) (b .fst) )

    unfoldγ : (a b : Mem (Lset γ)) → relOf (orderAt γ oγ) a b ≡ (a ≺ᵍ b)
    unfoldγ a b = cong (λ z → relOf (z oγ) a b) (orderAt-step γ)

    unfoldβ : (a b : Mem (Lset β)) → relOf (orderAt β oβ) a b ≡ (a ≺ᵇ b)
    unfoldβ a b = cong (λ z → relOf (z oβ) a b) (orderAt-step β)

  endExtension : (a b : Mem (Lset γ))
               → relOf (orderAt γ oγ) a b ≡ relOf (orderAt β oβ) (up a) (up b)
  endExtension a b = unfoldγ a b ∙ agree a b ∙ sym (unfoldβ (up a) (up b))

Recap

birth is the ordinal a constructible set is carved over, one below the earliest stage containing it, and it exists because a set enters the tower only by being carved out (theCarve). birth-in places it strictly below any stage the set belongs to, and birth-proof says it does not depend on the constructibility proof supplied.

stepAt is the step: a well-order of Lset (sucV δ) out of one of

Lset δ, at every stage by the previous chapter's name order pulled back along least name, which is a function because the names are well-ordered as soon as the stage below is. It was written with a second branch below the limit stage and that branch was measured surplus and deleted; the body says why.

pullOrder moves a well-order along an injection and is the only transfer written; the step uses it, and so does carry, which presents a stage's members as the index type the naming chapter takes.

Three definitions say what that pulled-back order is, for a caller outside:

denotesAt is a set's names, IsLeastName is the well-order chapter's IsLeast at that family, and leastNameOf is the search.

stepAt-fill and stepAt-read then read the step both ways against the name order, at any two names the caller has shown least. Two measurements sit behind those five lines: the property must be the family's own

IsLeast and never a re-spelling of it (16 s against nothing, because a comparison at a computed name opens the code order), and both readings must be proved inside the telescope the seal lives in and never restated at top level (39 s each against nothing, which is law 20 at a new place).

orderAt is the family: at every ordinal, a strict well-order of that stage's members, all four laws included, built by membership induction from the orders below. Its comparison has the birth as the primary key and the step order at a common birth as the secondary; endExtension is what that buys, and it is a path, not an implication: the comparison of two members never mentions the stage it is read at, so the order at a large stage, restricted to a small one, is the order there on the nose.

What is now available is exactly the missing hypothesis of the previous chapter, at every stage at once. The argument ahead takes the one stage the choice-stage chapter singled out, hands stageOrder to the names written over it, and picks the least name.