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

本部的每一章都把自己的债务归约成一笔更小的，而上一章点出了剩下的那笔：内化命名比较的那个框架持有一个为诸码所设的关系位，而那一位所要的，是极限阶段诸成员上的序 limitOrder 作为模型的一个集合。至今无人造出它。本章造。

那个序以层号为主键。极限阶段的成员首次现身于某个有穷阶段，最小的这种数码就是它的层号，而层号不同的两个成员仅凭层号比较。同层的两个成员按那一层自己的序比较，而后者是在最先分歧处的比较：两个集合总在某处相异，而在上一个阶段自己的序之下最小的那个相异点作出裁决，持有它的那个集合排在后面。

于是有两个键，而每一个都得在对象语言里说出来。第一个很短，而为它准备的器械已经存在：一个数码是某集合的层号，当那里的塔装着这个集合、而没有更小数码的塔装它。第二个是沿诸数码的一场递归，其取值是关系，而取值为集合的递归没法被一个词项点名，故被描述的是逼近，与塔、与序之表被描述的方式一模一样。两个键随后由一个析取接合起来，而模型自家的分离把那个集合从「诸对逃不出的一个界」上雕出来。

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

层号，在内部说出

三个合取项，且除 ω 自身外不点名任何常元。位 b 持有 ω 的一个成员，故它持有一个数码；b 处有一座塔，而位 x 属于它；并且对 b 的每个成员、亦即每个更小的数码，那里的塔不装 x。塔经序列那一章的图抵达，而那是抵达它的唯一办法，因为层级是被描述的、不是被某个词项点名的。

第三个合取项是本部任何地方头一次用上全称量词。它不花分文，而理由值得记下：指标合取是货真价实的乘积，对象蕴含是函数，故这笔债由一个 lambda 交割，没有任何截断要消去；而它之下的数码解码落在荒谬里，荒谬是命题，故那里的截断一行就被吸收。

两条读式都站在变元环境的变元位上，而层号自身以变元数码的身份到场、携带它自己的定义等式。这不是文体上的取舍。把 level a 就地内联在它出现的各处，本节要跑 145 秒；把数码取作参数、在调用处填 refl，则是 1.8 秒；而这八十倍之差，正是算出层号的那场经典可及性递归被槽位处的转换检查撬开所致。

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)

最先的分歧，在内部说出

第二个键是有穷那一章那次比较的单独一步，而本节把这一步写下来，且其中不含任何具体之物：基底关系与基底阶段被握在槽位里，被比较的那两个集合也被握在槽位里。这种通用性不是花架子。那一步所查阅的关系是一场递归的取值，故在这一步被使用之处，它绝不可能是常元；它以变元身份到场，而整条描述必须站得住。

那一步所说的，就是有穷那一章所说的。阶段中存在一个 z，它属于 y 而不属于 x，且阶段中凡被基底关系排在 z 之前的成员 w，属于 x 当且仅当属于 y。对象语言唯一无法逐字抄写元语言之处，是基底关系的那次隶属：pr w z 是一个对，而对是被描述的、不是被点名的，故那个原子是模型那一章的 appAt。

两个方向只差一步记账。元语言在层级的诸集合上量化，对象语言在模型的诸元素上量化，故每一个过界的见证都得取得或卸下它的可构造性证明，而那份证明是有的，因为 L 的集合的成员就是 L 的元素。携带它的那个对在造出之处被封印，理由上一章已实测过：抵达槽位的是那个对，而不是它里面的集合。

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

那个序，接合起来

两个键在此接合，而第二个以具名假设的身份进场、不是作为一个构造：一条公式，说「某个槽位所持有的数码处的关系把一个槽位排在另一个之前」，连同它对着有穷那一章的 before 的两条读式。自此往下的一切都对那条描述保持通用，而最后一节将说准：兑现它需要什么。

接合是一个析取，而它的两支绑定的层号个数不同。第一支绑两个，每边一个，并按隶属比较它们，那就是数码上的序。第二支绑一个，断言它是两边的层号，并把比较交给那里的关系。绑一个数码而不是两个，正是把「层号之间的等式」挡在对象语言之外的办法；否则那个等式就得用对象等词写出、再换回来。

反着读那个析取要花一条引理，而它正是序之表那一章早已为每一个严格良序一举隔离出来的那一条：对象析取是截断的，元层面的比较不是，故先请出三歧，严格那一情形原封不动交出比较，另外两种情形的目标是荒谬，而截断可以在那里打开。

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

那个序，作为一个集合

被那个序关联的诸对逃不出单一的一个集合，因为极限阶段的诸成员构成 L 元素的一个小族，它们的诸对也是；递归那一章的界层引理一举把它们全部禁闭。随后，用下面这条条件作分离，就恰好把想要的那些对雕出来，而那条条件是一对存在量词绑住两个分量，配对是被描述的而非被点名的，再接上那次比较。

两条表示引理是本章的交付物，而它们陈述成内化那一章的 Adequacy.Keys 所消费的形状：同样两个实参、左边同样的配对、右边那个束自己的比较。它们的证明就是分离的规格分两个方向读出来，一个方向由配对的单射性取回两个分量，另一个方向由模型自家的配对供上它们。读回来还要花掉那条脱截断引理，因为隶属是命题而比较不是。

  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

那个为诸码所设的位，已填上

内化命名比较的那个框架取两个关系位，一个为诸码、一个为诸参数，各自带着「它持有什么」的两个方向。为诸码所设的那一位正是本章为之而写的东西，而它在此处被填上：集合是 codeOrder，两个方向就是刚证完的那两条引理，实参相同，中间不设任何转接。

为诸参数所设的那一位仍然敞着，而这不是遗漏。它是「命名所依托的那个载体上的序」，是整个构造的一个参数，而上一部经 ix-fill 与 ix-rep 在每个阶段处供给它。此处填上的，恰是那没有供给方的一半。

  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

剩下什么，点准了名

Described 有一条假设仍然敞着，而它就是横在本章与一条无条件定理之间的全部：一条公式 BeforeAt，说「某个槽位所持有的数码处、按最先分歧处的那个序，把第二个槽位排在第三个之前」，连同它对着有穷那一章的 before 的两条读式。

兑现它是一件事、不是几件，而形状已经定了。某个数码处的关系是沿诸数码的一场递归的取值，故要被描述的是一个逼近：一个集合，在它定义域以下的每个数码处记录那里的关系；与塔、与序之表被描述的方式一模一样：一个对诸逼近作量化的图、一条把逼近所记录的每个取值钉住的值引理，以及在元层面把每个数码处的逼近当场拿出来。有两件事使它比两位前辈都更便宜。索引是 ωʟ 的成员，而 ωʟ 是个集合，故外层归纳是对一个自然数作的，层级那一章那半场真类收集根本不会出现。而那一步已经写好：PrecedesAt 就是这场递归的步进条件，且对「上一个关系被握在哪一位」保持通用，而那恰是一个图查阅它时必须采取的形式。

也有两件事使它更贵。某个数码处的取值是关系而非阶段，故每一步是在一个有穷阶段的诸对之上作分离、而不是取可定义幂集；而上一个关系要抵达那一步内部的一个槽位，故它必须以变元身份携带自己的定义等式到场，绝不可以是一个应用，否则就撞上第一条定律所点名的那堵墙。

小结

LevelAt 是层号在对象语言中的说法，三个合取项，且除 ω 外不点名任何常元：那一位持有 ω 的一个成员、那里的塔装着这个集合、而没有更小数码的塔装它。LevelAt-in 与 LevelAt-out 是它落在变元环境的变元位上的两条读式，而层号自身以变元数码的身份到场、携带它的定义等式，这正是 145 秒与 1.8 秒之差：层号是一场经典可及性递归，而槽位处的转换检查把它撬开。

PrecedesAt 是最先分歧处那次比较的单独一步，其中不含任何具体之物：基底关系与基底阶段被握在槽位里，故这条描述能站在「关系是某场递归之取值」的地方。PrecedesAt-out 与 PrecedesAt-in 是它对着 precedes 的两条读式，只差一步记账，因为在两种语言之间过界的见证要取得或卸下它的可构造性证明，而携带那份证明的对被封印。

strictLimit 把一次比较上的截断脱下来，办法是在消去任何东西之前先按三歧分情形。Described 是那个框架：LimitOrdAt 把两个键接成一个析取，第一支绑两个层号并按隶属比较它们，第二支绑一个，于是层号之间的等式根本不进对象语言；Order.LimitOrdAt-in 与 Order.LimitOrdAt-out 是它对着 limitOrder 自己那次比较的两条读式。

pairsBound 把那个序可能关联的每一个对都禁闭起来，靠的是递归那一章的界层引理施于极限阶段诸成员的那个小族；而 codeOrder 是从它上面用 Cond₀ 分离出来的，在造出之处封印。codeOrder-fill 与 codeOrder-rep 是两条表示引理，而 CodeKeys.AtParams 就是内化那一章的 Adequacy.Keys，其为诸码所设的位由它们填上，实参相同，中间不设转接。

记下两次实测，每一条都是在新地方遇上的旧规矩。一次分情形，若其被检者是某个束的比较、而其结论是一个满足关系，就跑不完；写在一个显式的和上、诸支取作具名辅助，则不花分文 (超过 300 秒对 2.4 秒)。而那条接合起来的描述必须在造出之处封印：分离的那条条件会在两层绑定之下把它展开，而不封印时那次归约同样跑不完 (超过 300 秒对 2.7 秒)，这与上一章实测为每条读式 160 秒的是同一条定律。