--- title: "Well-orders on all stages" module: L.Choice.StageOrders lang: en site: "Bedrock" description: "Well-orders on all stages" stage: "The canonical well-order and Choice" reading_order: 76 canonical: https://bedrock.institute/en/L.Choice.StageOrders.html html: L.Choice.StageOrders.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/StageOrders.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Stage, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.FiniteStageOrders, L.Choice.CanonicalNames, L.WellOrder.Base] routes: [canonical-order, hulls-and-counting] translations: [https://bedrock.institute/zh/L.Choice.StageOrders.md, https://bedrock.institute/ja/L.Choice.StageOrders.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 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`. ```agda {-# 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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 γ`. ```agda 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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`. ```agda 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. ```agda 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`. ```agda ; 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda 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. ```agda (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 γ`. ```agda 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 γ`. ```agda 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. ```agda 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. ```agda 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 `γ`. ```agda 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`. ```agda 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`. ```agda 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. ```agda _≺_ : 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. ```agda 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. ```agda 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. ```agda (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. ```agda ≺-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. ```agda ≺-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. ```agda 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`. ```agda , 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. ```agda (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. ```agda ≺-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. ```agda ⊎ ((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. ```agda 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. ```agda 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. ```agda (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. ```agda , 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. ```agda 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`. ```agda → (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. ```agda (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. ```agda 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. ```agda 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 `δ`. ```agda 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. ```agda 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`. ```agda 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. ```agda ≺-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. ```agda 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. ```agda ; 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. ```agda 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`. ```agda 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. ```agda 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. ```agda 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.