The order on the limit stage, as an element of L

Every chapter of this part has reduced its obligation to a smaller one, and the last chapter named what was left: the frame that internalizes the naming comparison holds a relation slot for the codes, and what that slot wants is the order on the members of the limit stage, limitOrder, as a set of the model. Nothing built it. This chapter does.

The order is level-primary. A member of the limit stage first appears at some finite stage, the least such numeral is its level, and two members of different levels are compared by their levels alone. Two members of one level are compared by that level's own order, which is comparison at the earliest disagreement: the two sets differ somewhere, and the least point of difference under the previous stage's order decides, with the set holding it placed later.

So there are two keys, and each has to be said in the object language. The first is short and the machinery for it exists: a numeral is the level of a set when the tower there holds the set and no smaller numeral's tower does. The second is a recursion along the numerals whose values are relations, and a recursion whose values are sets cannot be named by a term, so what gets described is an approximation, exactly as the tower and the order table were described. The two keys are then joined by a disjunction, and the model's own separation carves the set out of a bound the pairs cannot escape.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; var; con; _∈̇_; _∧̇_; _∨̇_; ¬̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #mono; #-inj′ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd )
open import L.Ordinal {ℓ} using ( numeral-ord; #∈ω; ∈#-elim; #∈#-elim; ω-ord )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Coding.Model {ℓ}
  using ( numL; appAt; appAt-adequate; prAtL; prAtL-adequate; prʟ; prʟ-fst )
open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt )
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Choice.Finite {ℓ} lem
  using ( Limit; level; level-in; levelData; limitOrder
        ; before; precedes; Agrees; Witness )
open import L.Choice.Internal {ℓ} lem using ( module Adequacy )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )

import FOL.Absoluteness
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Nat.Order using ( _<_; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; ω )

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

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

open SWO limitOrder using () renaming ( _<∙_ to _≺ˡ_ )

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

-- perf: the tower at a numeral is sealed where it is built, as in the birth
-- description of the previous chapter (measured there at 178 s against 2 s)
opaque
  towerS : ℕ → S
  towerS k = LsetS (# k) (numeral-ord k)

  towerS-fst : (k : ℕ) → fst (towerS k) ≡ Lset (# k)
  towerS-fst k = refl

  numS : ℕ → S
  numS k = # k , numL k

  numS-fst : (k : ℕ) → fst (numS k) ≡ # k
  numS-fst k = refl

towerGraph : ∀ {n} (j : ℕ) (δ : S ^ n) (i : Fin n) → fst (lookup i δ) ≡ # j
           → ⟨ (towerS j ∷ δ) ⊨ LsetGraphAt zero (suc i) ⟩
towerGraph j δ i q = Lset-defines zero (suc i) (towerS j ∷ δ)
  (subst IsOrd (sym q) (numeral-ord j))
  (towerS-fst j ∙ cong Lset (sym q))

The level, said inside

Three conjuncts, and no constant other than ω itself. The slot b holds a member of ω, so it holds a numeral; there is a tower at b and the slot x belongs to it; and for every member of b, that is, every smaller numeral, the tower there does not hold x. The tower is reached by the sequence chapter's graph, which is the only way to reach it, since the hierarchy is described and not named by a term.

The third conjunct is the first universal quantifier used anywhere in this part. It costs nothing, and the reason is worth recording: the indexed conjunction is a genuine product and object implication is a function, so the obligation is discharged by a lambda with no truncation to eliminate, and the numeral decoding under it lands in absurdity, which is a proposition, so the truncation there is absorbed in one line.

Both readings stand at variable slots in a variable environment, and the level itself arrives as a variable numeral carrying its own defining equation. That is not a stylistic choice. With level a inlined at its occurrences the section takes 145 s; with the numeral as a parameter and refl at the call site it takes 1.8 s, and the eighty-fold difference is the classical accessibility recursion that computes the level being forced open by conversion at a slot.

LevelAt : ∀ {n} → Fin n → Fin n → Formula S n
LevelAt b x =
  (var b ∈̇ con ωʟ)
  ∧̇ ( ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) )
    ∧̇ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)
                     ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) )

module Level (a : Limit) (k : ℕ) (qk : level a ≡ k) where
  private
    aIn : ⟨ fst a ∈ Lset (# k) ⟩
    aIn = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) qk (level-in a)

    aMin : (m : ℕ) → ⟨ fst a ∈ Lset (# m) ⟩ → m < k → Empty.⊥
    aMin m h hm = levelData a .snd .snd m h
      (lift (subst (λ j → m < j) (sym qk) hm))

  module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where
    private
      Body : S → Type (ℓ-suc ℓ)
      Body c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
             × ⟨ fst (lookup x γ) ∈ fst c ⟩

    LevelAt-in : fst (lookup b γ) ≡ # k → fst (lookup x γ) ≡ fst a
               → ⟨ γ ⊨ LevelAt b x ⟩
    LevelAt-in qb qx = hω , (hex , hmin)
      where
      hω : ⟨ fst (lookup b γ) ∈ ω ⟩
      hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k)

      hex : ⟨ γ ⊨ ∃̇ ( LsetGraphAt zero (suc b) ∧̇ (var (suc x) ∈̇ var zero) ) ⟩
      hex = ∣ towerS k , (towerGraph k γ b qb , hm) ∣₁
        where
        hm : ⟨ fst (lookup x γ) ∈ fst (towerS k) ⟩
        hm = subst (λ u → ⟨ fst (lookup x γ) ∈ u ⟩) (sym (towerS-fst k))
          (subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn)

      hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)
                                  ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩
      hmin u u∈ c hg hmem = PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst u) (subst (λ w → ⟨ fst u ∈ w ⟩) qb u∈))
        where
        step : Σ[ m ∈ ℕ ] ((m < k) × (fst u ≡ # m)) → Empty.⊥
        step (m , (hm , qu)) = aMin m inStage hm
          where
          qc : fst c ≡ Lset (fst u)
          qc = Lset-only zero (suc zero) (c ∷ u ∷ γ) hg
            (subst IsOrd (sym qu) (numeral-ord m))
          inStage : ⟨ fst a ∈ Lset (# m) ⟩
          inStage = subst (λ w → ⟨ fst a ∈ Lset w ⟩) qu
            (subst (λ w → ⟨ w ∈ Lset (fst u) ⟩) qx
              (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem))

    LevelAt-out : ⟨ γ ⊨ LevelAt b x ⟩ → fst (lookup x γ) ≡ fst a
                → fst (lookup b γ) ≡ # k
    LevelAt-out (hω , (hex , hmin)) qx =
      PT.rec (setIsSet (fst (lookup b γ)) (# k)) named hω
      where
      notAbove : (m : ℕ) → fst (lookup b γ) ≡ # m → k < m → Empty.⊥
      notAbove m qb hk = hmin (numS k)
        (subst (λ w → ⟨ w ∈ fst (lookup b γ) ⟩) (sym (numS-fst k))
          (subst (λ w → ⟨ # k ∈ w ⟩) (sym qb) (#mono k m hk)))
        (towerS k) (towerGraph k (numS k ∷ γ) zero (numS-fst k))
        (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) (sym (towerS-fst k))
          (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn))

      notBelow : (m : ℕ) → fst (lookup b γ) ≡ # m → m < k → Empty.⊥
      notBelow m qb hm = PT.rec Empty.isProp⊥ atTower hex
        where
        atTower : Σ[ c ∈ S ] Body c → Empty.⊥
        atTower (c , (hg , hmem)) = aMin m inStage hm
          where
          qc : fst c ≡ Lset (# m)
          qc = Lset-only zero (suc b) (c ∷ γ) hg
                 (subst IsOrd (sym qb) (numeral-ord m))
             ∙ cong Lset qb
          inStage : ⟨ fst a ∈ Lset (# m) ⟩
          inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx
            (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem)

      named : Σ[ j ∈ Lift ℕ ] (# (lower j) ≡ fst (lookup b γ))
            → fst (lookup b γ) ≡ # k
      named (j , qj) = qb ∙ cong #_ (decide (lower j ≟ k))
        where
        qb : fst (lookup b γ) ≡ # (lower j)
        qb = sym qj
        decide : NatOrder.Trichotomy (lower j) k → lower j ≡ k
        decide (NatOrder.lt h) = Empty.rec (notBelow (lower j) qb h)
        decide (NatOrder.eq e) = e
        decide (NatOrder.gt h) = Empty.rec (notAbove (lower j) qb h)

The earliest disagreement, said inside

The second key is one step of the finite chapter's comparison, and this section writes that step down with nothing concrete in it: the base relation and the base stage are held in slots, and the two sets being compared are held in slots too. That genericity is not a flourish. The relation the step consults is the value of a recursion, so it can never be a constant at the point where the step is used; it arrives as a variable, and the whole description has to be able to stand there.

What the step says is what the finite chapter says. There is a z in the stage which belongs to y and not to x, and every member w of the stage that the base relation puts before z belongs to x exactly when it belongs to y. The one place where the object language cannot copy the meta-language verbatim is the membership of the base relation: pr w z is a pair, and a pair is described and not named, so the atom is the model chapter's appAt.

Both directions are one bookkeeping step apart. The meta-language quantifies over sets of the hierarchy and the object language over elements of the model, so each witness that crosses has to acquire or shed its constructibility proof, and the proof is available because a member of a set of L is an element of L. The pair that carries it is sealed where it is built, for the reason the previous chapter measured: it is the pair, not the set inside it, that reaches the slot.

-- perf: a member of a set of the model, paired with the constructibility proof
-- it inherits, is sealed where it is built (the previous chapter's measurement)
opaque
  memS : (A : S) (z : V ℓ) → ⟨ z ∈ fst A ⟩ → S
  memS A z h = z , isL-trans {x = fst A} {y = z} h (snd A)

  memS-fst : (A : S) (z : V ℓ) (h : ⟨ z ∈ fst A ⟩) → fst (memS A z h) ≡ z
  memS-fst A z h = refl

PrecedesAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
PrecedesAt r A x y =
  ∃̇ ( (var zero ∈̇ var (suc A))
    ∧̇ ( (var zero ∈̇ var (suc y))
      ∧̇ ( ¬̇ (var zero ∈̇ var (suc x))
        ∧̇ ∀̇∈ (var (suc A))
             ( appAt (sh2 r) zero (suc zero)
             ⇒̇ ( ((var zero ∈̇ var (sh2 x)) ⇒̇ (var zero ∈̇ var (sh2 y)))
               ∧̇ ((var zero ∈̇ var (sh2 y)) ⇒̇ (var zero ∈̇ var (sh2 x))) ) ) ) ) )

module Precedes {n : ℕ} (r A x y : Fin n) (γ : S ^ n)
                (R : V ℓ → V ℓ → Ω)
                (Rrep : (u v : S) → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩
                      → ⟨ R (fst u) (fst v) ⟩)
                (Rfill : (u v : S) → ⟨ R (fst u) (fst v) ⟩
                       → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩)
                where
  private
    Aʟ : S
    Aʟ = lookup A γ

    xv : V ℓ
    xv = fst (lookup x γ)

    yv : V ℓ
    yv = fst (lookup y γ)

    Both : V ℓ → Type (ℓ-suc ℓ)
    Both w = (⟨ w ∈ xv ⟩ → ⟨ w ∈ yv ⟩) × (⟨ w ∈ yv ⟩ → ⟨ w ∈ xv ⟩)

    Agreeing : S → Type (ℓ-suc ℓ)
    Agreeing z = (w : S) → ⟨ fst w ∈ fst Aʟ ⟩
               → ⟨ (w ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩
               → Both (fst w)

    Body : S → Type (ℓ-suc ℓ)
    Body z = ⟨ fst z ∈ fst Aʟ ⟩
           × ( ⟨ fst z ∈ yv ⟩
             × ( (⟨ fst z ∈ xv ⟩ → Empty.⊥) × Agreeing z ) )

  PrecedesAt-out : ⟨ γ ⊨ PrecedesAt r A x y ⟩
                 → ⟨ precedes R (fst Aʟ) xv yv ⟩
  PrecedesAt-out = PT.rec squash₁ atZ
    where
    atZ : Σ[ z ∈ S ] Body z → ⟨ precedes R (fst Aʟ) xv yv ⟩
    atZ (z , (z∈A , (z∈y , (z∉x , hag)))) =
      ∣ fst z , (z∈A , (z∈y , (z∉x , ag))) ∣₁
      where
      ag : Agrees R (fst Aʟ) xv yv (fst z)
      ag w w∈A hR = subst Both (memS-fst Aʟ w w∈A) (hag wS w∈A' happ)
        where
        wS : S
        wS = memS Aʟ w w∈A
        w∈A' : ⟨ fst wS ∈ fst Aʟ ⟩
        w∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym (memS-fst Aʟ w w∈A)) w∈A
        hp : ⟨ pr (fst wS) (fst z) ∈ fst (lookup r γ) ⟩
        hp = Rfill wS z
          (subst (λ u → ⟨ R u (fst z) ⟩) (sym (memS-fst Aʟ w w∈A)) hR)
        happ : ⟨ (wS ∷ z ∷ γ) ⊨ appAt (sh2 r) zero (suc zero) ⟩
        happ = subst ⟨_⟩
          (sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp

  PrecedesAt-in : ⟨ precedes R (fst Aʟ) xv yv ⟩
                → ⟨ γ ⊨ PrecedesAt r A x y ⟩
  PrecedesAt-in = PT.rec squash₁ atZ
    where
    atZ : Σ[ z ∈ V ℓ ] Witness R (fst Aʟ) xv yv z
        → ⟨ γ ⊨ PrecedesAt r A x y ⟩
    atZ (z , (z∈A , (z∈y , (z∉x , ag)))) =
      ∣ zS , (z∈A' , (z∈y' , (z∉x' , hag))) ∣₁
      where
      zS : S
      zS = memS Aʟ z z∈A
      qz : fst zS ≡ z
      qz = memS-fst Aʟ z z∈A
      z∈A' : ⟨ fst zS ∈ fst Aʟ ⟩
      z∈A' = subst (λ u → ⟨ u ∈ fst Aʟ ⟩) (sym qz) z∈A
      z∈y' : ⟨ fst zS ∈ yv ⟩
      z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y
      z∉x' : ⟨ fst zS ∈ xv ⟩ → Empty.⊥
      z∉x' h = z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h)
      hag : Agreeing zS
      hag w w∈A happ = ag (fst w) w∈A hR
        where
        hp : ⟨ pr (fst w) (fst zS) ∈ fst (lookup r γ) ⟩
        hp = subst ⟨_⟩ (appAt-adequate (sh2 r) zero (suc zero) (w ∷ zS ∷ γ)) happ
        hR : ⟨ R (fst w) z ⟩
        hR = subst (λ u → ⟨ R (fst w) u ⟩) qz (Rrep w zS hp)

The order, composed

The two keys are joined here, and the second one enters as a named hypothesis rather than a construction: a formula saying that the relation at a numeral held in a slot puts one slot before another, together with its two readings against the finite chapter's before. Everything from here on is generic in that description, and the last section says exactly what discharging it needs.

The composition is a disjunction, and its two disjuncts bind different numbers of levels. The first binds two, one for each side, and compares them by membership, which is the order on numerals. The second binds one, asserts that it is the level of both sides, and hands the comparison to the relation there. Binding one numeral rather than two is what keeps an equation between levels out of the object language, where it would have to be written with the object equality and converted back.

Reading the disjunction the other way costs one lemma, and it is the one the order table chapter already isolated for every strict well-order at once: object disjunction is truncated and the meta comparison is not, so trichotomy is consulted first, the strict case hands the comparison over untouched, and the other two cases have absurdity for a goal, where the truncation may be opened.

-- perf: the limit stage and its members, sealed where they are built
opaque
  limitS : S
  limitS = LsetS ω ω-ord

  limitS-fst : fst limitS ≡ Lset ω
  limitS-fst = refl

  limitEl : Limit → S
  limitEl a = fst a , Lset→isL ω ω-ord (fst a) (snd a)

  limitEl-fst : (a : Limit) → fst (limitEl a) ≡ fst a
  limitEl-fst a = refl

  prS : S → S → S
  prS a b = prʟ a b

  prS-fst : (a b : S) → fst (prS a b) ≡ pr (fst a) (fst b)
  prS-fst a b = prʟ-fst a b

pairsBound : Σ[ D ∈ S ] ((u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst D ⟩)
pairsBound = d .fst , onPair
  where
  ixL : ⟪ Lset ω ⟫ → S
  ixL m = ⟪ Lset ω ⟫↪ m , Lset→isL ω ω-ord (⟪ Lset ω ⟫↪ m)
    (∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m))

  d : Σ[ D ∈ S ] ((p : ⟪ Lset ω ⟫ × ⟪ Lset ω ⟫)
                  → ⟨ prʟ (ixL (fst p)) (ixL (snd p)) ∈ˢ D ⟩)
  d = smallDom (⟪ Lset ω ⟫ × ⟪ Lset ω ⟫) (λ p → prʟ (ixL (fst p)) (ixL (snd p)))

  onPair : (u v : Limit) → ⟨ pr (fst u) (fst v) ∈ fst (d .fst) ⟩
  onPair u v = subst (λ t → ⟨ t ∈ fst (d .fst) ⟩)
    (prʟ-fst (ixL (fu .fst)) (ixL (fv .fst)) ∙ cong₂ pr (fu .snd) (fv .snd))
    (d .snd (fu .fst , fv .fst))
    where
    fu = ∈-asFiber {a = fst u} {b = Lset ω} (snd u)
    fv = ∈-asFiber {a = fst v} {b = Lset ω} (snd v)

strictLimit : (a b : Limit) → ∥ a ≺ˡ b ∥₁ → a ≺ˡ b
strictLimit a b h = decide (SWO.tri∙ limitOrder a b)
  where
  decide : Tri (a ≺ˡ b) (a ≡ b) (b ≺ˡ a) → a ≺ˡ b
  decide (lt k) = k
  decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥
    (λ k → SWO.irr∙ limitOrder b (subst (λ t → t ≺ˡ b) q k)) h)
  decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥
    (λ j → SWO.irr∙ limitOrder a (SWO.trans∙ limitOrder a b a j k)) h)

module Described
  (BeforeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n)
  (BeforeAt-in : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ)
               → fst (lookup b γ) ≡ # m
               → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩
               → ⟨ γ ⊨ BeforeAt b x y ⟩)
  (BeforeAt-out : ∀ {n} (b x y : Fin n) (γ : S ^ n) (m : ℕ)
                → fst (lookup b γ) ≡ # m
                → ⟨ γ ⊨ BeforeAt b x y ⟩
                → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩)
  where

  -- perf: the composed description is sealed where it is built; unsealed, the
  -- separation's condition unfolds it under two binders and does not finish
  opaque
    LimitOrdAt : ∀ {n} → Fin n → Fin n → Formula S n
    LimitOrdAt x y =
      ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x)
             ∧̇ ( LevelAt zero (sh2 y) ∧̇ (var (suc zero) ∈̇ var zero) ) ) )
      ∨̇ ∃̇ ( LevelAt zero (suc x)
           ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) )

  module Order {n : ℕ} (x y : Fin n) (γ : S ^ n)
               (u v : Limit) (ku kv : ℕ)
               (qu : level u ≡ ku) (qv : level v ≡ kv)
               (qx : fst (lookup x γ) ≡ fst u)
               (qy : fst (lookup y γ) ≡ fst v)
               where
    private
      module Lu = Level u ku qu
      module Lv = Level v kv qv

      Split : S → S → Type (ℓ-suc ℓ)
      Split c d = ⟨ (d ∷ c ∷ γ) ⊨ LevelAt (suc zero) (sh2 x) ⟩
                × ( ⟨ (d ∷ c ∷ γ) ⊨ LevelAt zero (sh2 y) ⟩
                  × ⟨ fst c ∈ fst d ⟩ )

      Same : S → Type (ℓ-suc ℓ)
      Same c = ⟨ (c ∷ γ) ⊨ LevelAt zero (suc x) ⟩
             × ( ⟨ (c ∷ γ) ⊨ LevelAt zero (suc y) ⟩
               × ⟨ (c ∷ γ) ⊨ BeforeAt zero (suc x) (suc y) ⟩ )

      split-in : ku < kv → Split (numS ku) (numS kv)
      split-in hlt =
          Lu.LevelAt-in (suc zero) (sh2 x) (numS kv ∷ numS ku ∷ γ)
            (numS-fst ku) qx
        , ( Lv.LevelAt-in zero (sh2 y) (numS kv ∷ numS ku ∷ γ)
              (numS-fst kv) qy
          , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv))
              (#mono ku kv hlt) )

      same-in : (e : level v ≡ level u)
              → ⟨ before (level u) (fst u) (fst v) ⟩ → Same (numS ku)
      same-in e h =
          Lu.LevelAt-in zero (suc x) (numS ku ∷ γ) (numS-fst ku) qx
        , ( Level.LevelAt-in v ku (e ∙ qu) zero (suc y) (numS ku ∷ γ)
              (numS-fst ku) qy
          , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku)
              (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy)
                (subst (λ j → ⟨ before j (fst u) (fst v) ⟩) qu h)) )

      split-out : (c d : S) → Split c d → level u < level v
      split-out c d (hx , (hy , hlt)) = subst2 _<_ (sym qu) (sym qv)
        (#∈#-elim ku kv (subst2 (λ s t → ⟨ s ∈ t ⟩) qc qd hlt))
        where
        qc : fst c ≡ # ku
        qc = Lu.LevelAt-out (suc zero) (sh2 x) (d ∷ c ∷ γ) hx qx
        qd : fst d ≡ # kv
        qd = Lv.LevelAt-out zero (sh2 y) (d ∷ c ∷ γ) hy qy

      same-out : (c : S) → Same c
               → (level v ≡ level u) × ⟨ before (level u) (fst u) (fst v) ⟩
      same-out c (hx , (hy , hb)) = e , below
        where
        qc : fst c ≡ # ku
        qc = Lu.LevelAt-out zero (suc x) (c ∷ γ) hx qx
        qc' : fst c ≡ # kv
        qc' = Lv.LevelAt-out zero (suc y) (c ∷ γ) hy qy
        e : level v ≡ level u
        e = qv ∙ sym (#-inj′ (sym qc ∙ qc')) ∙ sym qu
        below : ⟨ before (level u) (fst u) (fst v) ⟩
        below = subst (λ j → ⟨ before j (fst u) (fst v) ⟩) (sym qu)
          (subst2 (λ s t → ⟨ before ku s t ⟩) qx qy
            (BeforeAt-out zero (suc x) (suc y) (c ∷ γ) ku qc hb))

    opaque
      unfolding LimitOrdAt

      LimitOrdAt-in : u ≺ˡ v → ⟨ γ ⊨ LimitOrdAt x y ⟩
      LimitOrdAt-in h = decide-in h
        where
        lower-in : ku < kv → ⟨ γ ⊨ LimitOrdAt x y ⟩
        lower-in hlt = ∣ inl ∣ numS ku , ∣ numS kv , split-in hlt ∣₁ ∣₁ ∣₁

        inner-in : (e : level v ≡ level u)
                 → ⟨ before (level u) (fst u) (fst v) ⟩
                 → ⟨ γ ⊨ LimitOrdAt x y ⟩
        inner-in e k = ∣ inr ∣ numS ku , same-in e k ∣₁ ∣₁

        decide-in : Lift {ℓ-zero} {ℓ-suc ℓ} (level u < level v)
                  ⊎ ((level v ≡ level u)
                     × ⟨ before (level u) (fst u) (fst v) ⟩)
                  → ⟨ γ ⊨ LimitOrdAt x y ⟩
        decide-in (inl k)       = lower-in (subst2 _<_ qu qv (lower k))
        decide-in (inr (e , k)) = inner-in e k

      LimitOrdAt-out : ⟨ γ ⊨ LimitOrdAt x y ⟩ → ∥ u ≺ˡ v ∥₁
      LimitOrdAt-out = PT.rec squash₁ decide
        where
        atSplit : (c : S) → Σ[ d ∈ S ] Split c d → ∥ u ≺ˡ v ∥₁
        atSplit c (d , hs) = ∣ inl (lift (split-out c d hs)) ∣₁

        atSame : Σ[ c ∈ S ] Same c → ∥ u ≺ˡ v ∥₁
        atSame (c , hs) = ∣ inr (same-out c hs) ∣₁

        decide : ⟨ γ ⊨ ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x)
                            ∧̇ ( LevelAt zero (sh2 y)
                              ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ⟩
               ⊎ ⟨ γ ⊨ ∃̇ ( LevelAt zero (suc x)
                         ∧̇ ( LevelAt zero (suc y)
                           ∧̇ BeforeAt zero (suc x) (suc y) ) ) ⟩
               → ∥ u ≺ˡ v ∥₁
        decide (inl h) = PT.rec squash₁
          (λ { (c , hd) → PT.rec squash₁ (atSplit c) hd }) h
        decide (inr h) = PT.rec squash₁ atSame h

The order, as a set

The pairs the order relates cannot escape a single set, because the members of the limit stage form a small family of elements of L and so do their pairs; the recursion chapter's bounding lemma confines them all at once. Separation with the condition below then carves out exactly the pairs wanted, and the condition is one existential pair binding the two components, with the pairing described rather than named, joined to the comparison.

The two representation lemmas are the chapter's deliverable, and they are stated in the shape the internalization chapter's Adequacy.Keys consumes: the same two arguments, the same pairing on the left, and the bundle's own comparison on the right. Their proofs are the separation's specification read in each direction, with the components recovered by injectivity of the pairing one way and supplied by the model's own pairing the other. Reading back also spends the untruncation lemma, since a membership is a proposition and the comparison is not.

  Cond₀ : Formula S 
  Cond₀ = ∃̇ ( ∃̇ ( prAtL (sh2 zero) (suc zero) zero
                 ∧̇ LimitOrdAt (suc zero) zero ) )

  -- perf: the separation is a description read at constants, so the set it
  -- carves is sealed where it is built
  opaque
    codeOrder : S
    codeOrder = hasSeparationL (pairsBound .fst) Cond₀ .fst .fst

    codeOrder-mem : (z : S) → (z ∈ˢ codeOrder)
                  ≡ ((z ∈ˢ pairsBound .fst) ⊓ ((z ∷ []) ⊨ Cond₀))
    codeOrder-mem = hasSeparationL (pairsBound .fst) Cond₀ .fst .snd

  private
    Inner : S → S → S → Type (ℓ-suc ℓ)
    Inner z c d = ⟨ (d ∷ c ∷ z ∷ []) ⊨ prAtL (sh2 zero) (suc zero) zero ⟩
                × ⟨ (d ∷ c ∷ z ∷ []) ⊨ LimitOrdAt (suc zero) zero ⟩

    Outer : S → Type (ℓ-suc ℓ)
    Outer z = Σ[ c ∈ S ] ∥ (Σ[ d ∈ S ] Inner z c d) ∥₁

    cond-in : (z c d : S) → Inner z c d → ⟨ (z ∷ []) ⊨ Cond₀ ⟩
    cond-in z c d hi = ∣ c , ∣ d , hi ∣₁ ∣₁

    cond-out : (z : S) → ⟨ (z ∷ []) ⊨ Cond₀ ⟩ → ∥ Outer z ∥₁
    cond-out z h = h

  codeOrder-fill : (u v : Limit) → u ≺ˡ v
                 → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩
  codeOrder-fill u v h =
    subst (λ t → ⟨ t ∈ fst codeOrder ⟩) qz
      (subst ⟨_⟩ (sym (codeOrder-mem (prS (limitEl u) (limitEl v))))
        (inBound , cond-in (prS (limitEl u) (limitEl v))
                     (limitEl u) (limitEl v) (hpr , hord)))
    where
    qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v)
    qz = prS-fst (limitEl u) (limitEl v)
       ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)

    inBound : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst (pairsBound .fst) ⟩
    inBound = subst (λ t → ⟨ t ∈ fst (pairsBound .fst) ⟩) (sym qz)
      (pairsBound .snd u v)

    hpr : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])
          ⊨ prAtL (sh2 zero) (suc zero) zero ⟩
    hpr = subst ⟨_⟩ (sym (prAtL-adequate (sh2 zero) (suc zero) zero
      (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])))
      (prS-fst (limitEl u) (limitEl v))

    hord : ⟨ (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])
          ⊨ LimitOrdAt (suc zero) zero ⟩
    hord = Order.LimitOrdAt-in (suc zero) zero
      (limitEl v ∷ limitEl u ∷ prS (limitEl u) (limitEl v) ∷ [])
      u v (level u) (level v) refl refl (limitEl-fst u) (limitEl-fst v) h

  codeOrder-rep : (u v : Limit)
                → ⟨ pr (fst u) (fst v) ∈ fst codeOrder ⟩ → u ≺ˡ v
  codeOrder-rep u v h = strictLimit u v
    (PT.rec squash₁ atC
      (cond-out (prS (limitEl u) (limitEl v))
        (subst ⟨_⟩ (codeOrder-mem (prS (limitEl u) (limitEl v))) inSet .snd)))
    where
    qz : fst (prS (limitEl u) (limitEl v)) ≡ pr (fst u) (fst v)
    qz = prS-fst (limitEl u) (limitEl v)
       ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)

    inSet : ⟨ fst (prS (limitEl u) (limitEl v)) ∈ fst codeOrder ⟩
    inSet = subst (λ t → ⟨ t ∈ fst codeOrder ⟩) (sym qz) h

    atD : (c d : S) → Inner (prS (limitEl u) (limitEl v)) c d → ∥ u ≺ˡ v ∥₁
    atD c d (hpr , hord) = Order.LimitOrdAt-out (suc zero) zero
      (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ []) u v (level u) (level v)
      refl refl (sym (split .fst)) (sym (split .snd)) hord
      where
      qcd : pr (fst u) (fst v) ≡ pr (fst c) (fst d)
      qcd = sym qz
        ∙ subst ⟨_⟩ (prAtL-adequate (sh2 zero) (suc zero) zero
            (d ∷ c ∷ prS (limitEl u) (limitEl v) ∷ [])) hpr
      split : (fst u ≡ fst c) × (fst v ≡ fst d)
      split = pr-inj qcd

    atC : Outer (prS (limitEl u) (limitEl v)) → ∥ u ≺ˡ v ∥₁
    atC (c , hd) = PT.rec squash₁ (λ { (d , hi) → atD c d hi }) hd

The code slot, filled

The frame the naming comparison is internalized in takes two relation slots, one for the codes and one for the parameters, each with the two directions saying what it holds. The code slot is what this chapter was written for, and here it is filled: the set is codeOrder and the two directions are the two lemmas just proved, at the same two arguments and with no adapter in between.

The parameter slot stays open, and that is not an omission. It is the order on the carrier the naming is being done over, which is a parameter of the whole construction, and the previous part supplies it at every stage through

ix-fill and ix-rep. What is filled here is exactly the half that had no supplier.

  module CodeKeys (A : V ℓ) (pA : ⟨ isL A ⟩) (w : SWO ⟪ A ⟫) where
    private
      module Ad = Adequacy A pA w

    open SWO w using () renaming ( _<∙_ to _≺ₚ_ )

    module AtParams (Ps : S)
      (Prep : (a b : ⟪ A ⟫) → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩ → a ≺ₚ b)
      (Pfill : (a b : ⟪ A ⟫) → a ≺ₚ b → ⟨ pr (Ad.ix a) (Ad.ix b) ∈ fst Ps ⟩)
      where
      open Ad.Keys codeOrder Ps codeOrder-rep codeOrder-fill Prep Pfill public

What is left, named exactly

One hypothesis of Described is open, and it is the whole of what stands between this chapter and an unconditional theorem: a formula BeforeAt saying that the earliest-disagreement order at the numeral held in one slot puts a second slot before a third, together with its two readings against the finite chapter's before.

Discharging it is one thing and not several, and the shape is settled. The relation at a numeral is the value of a recursion along the numerals, so what has to be described is an approximation, a set recording at each numeral below its domain the relation there, exactly as the tower and the order table are described: a graph quantifying over approximations, a value lemma pinning every value an approximation records, and the approximation at each numeral exhibited on the meta side. Two things make it cheaper here than either predecessor. The index is a member of ωʟ, a set, so the outer induction is on a natural number and the class-collection half of the hierarchy chapter does not arise. And the step is already written: PrecedesAt is the recursion's step condition, generic in the slot the previous relation is held in, which is exactly the form a graph must consult it in.

Two things make it dearer. The value at a numeral is a relation rather than a stage, so each step is a separation over the pairs of a finite stage rather than a definable powerset; and the previous relation reaches a slot inside the step, so it must arrive as a variable with its defining equation and never as an application, on pain of the wall that Law 1 names.

Recap

LevelAt is the level said in the object language, three conjuncts and no constant but ω: the slot holds a member of ω, the tower there holds the set, and no smaller numeral's tower does. LevelAt-in and

LevelAt-out are its two readings at variable slots in a variable environment, with the level itself arriving as a variable numeral carrying its defining equation, which is the difference between 145 s and 1.8 s: the level is a classical accessibility recursion, and conversion at a slot forces it open.

PrecedesAt is one step of the earliest-disagreement comparison with nothing concrete in it: the base relation and the base stage are held in slots, so the description can stand where the relation is the value of a recursion.

PrecedesAt-out and PrecedesAt-in are its two readings against

precedes, one bookkeeping step apart, since a witness crossing between the languages acquires or sheds its constructibility proof, and the pair carrying that proof is sealed.

strictLimit takes the truncation off a comparison, by splitting on trichotomy before eliminating anything. Described is the frame:

LimitOrdAt joins the two keys as a disjunction whose first disjunct binds two levels and compares them by membership and whose second binds one, so no equation between levels ever enters the object language;

Order.LimitOrdAt-in and Order.LimitOrdAt-out are its two readings against limitOrder's own comparison.

pairsBound confines every pair the order could relate, by the recursion chapter's bounding lemma over the small family of members of the limit stage, and

codeOrder is the separation of Cond₀ out of it, sealed where it is built. codeOrder-fill and codeOrder-rep are the two representation lemmas, and CodeKeys.AtParams is the internalization chapter's Adequacy.Keys with its code slot filled by them, at the same two arguments and with no adapter.

Two measurements are recorded, and each is a law met in a new place. A case split whose scrutinee is a bundle's comparison and whose conclusion is a satisfaction does not finish; written on an explicit sum with the branches as named helpers it costs nothing (past 300 s against 2.4 s). And the composed description must be sealed where it is built: the separation's condition unfolds it under two binders, and unsealed that reduction does not finish either (past 300 s against 2.7 s), which is the same law the previous chapter measured at 160 s per reading.