The description is faithful

上一章把每个阶段处的序变成了 L 的一个对象，而那个构造是撑在两条假设上的，它们说清那条步进条件是什么意思。填它们不是一笔债、而是三笔：步进描述对着元层面那一步的适足性；诞生阶段在对象语言里的说法，至今无人说过；以及在一个随诞生阶段移动的载体上的码集。本章了结第二笔与第三笔，并把那两条假设变成一条，即单个载体处的那一步。

这次归约正是本章的用意所在，故值得说准。序之族以诞生阶段为主键：一个阶段的两个成员，按它们各自被雕出的时刻比较，只有在同一时刻被雕出的两个，才由那个时刻的机器来比较。于是上一章所索取的那条条件裂开了，而诞生阶段那一半是较大的一半。写下来，它不需要后继运算：一个集合的诞生阶段，是这样的序数，它的塔不装这个集合、而那座塔的可定义幂集装它；这两件事都是原子，且都架在早已存在的描述之上。

不能了结的是那一步自身。本章以一个具名参数把这句话说出来，参数自带它的含义作为假设，而绝不用近似物顶替。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( ∈sucV-elim )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; IsOrd; isPropIsOrd; Lset-mono; Lset→isL; 𝒟ₒ )
open import L.Ordinal {ℓ} using ( suc-ord; mem-ord )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Axioms.Basic {ℓ} using ( Lset-suc; LsetS; 𝒟ₒS; extensionalL )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem; stage-earliest )
open import L.Choice.Stage {ℓ} lem using ( ord-suc-inj )
open import L.Choice.Step {ℓ} lem
  using ( birth; birth-ord; birth-suc; birth-mem; birth-stage; birth-proof
        ; Mem; New; relOf; carry; Under; stepAt
        ; orderAt; orderAt-step; module Family )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO )
open import L.Coding.Model {ℓ}
  using ( extAt; extAt-in; extAt-out; extAt-in-both; prAtL; prAtL-adequate )
open import L.Coding.Sequence {ℓ} lem using ( LsetGraphAt )
open import L.Coding.Powerset {ℓ} lem using ( DefAt; DefAt-stage )
open import L.Coding.CodeSet {ℓ} lem
  using ( arityNumAtL; arityNumAtL-in; arityNumAtL-out; hasWitnessAt
        ; witnessAt-in; witnessAt-out; keyS; codeS
        ; AllCodes; AllCodes-in; AllCodes-out; IsKeyOverAny )
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Choice.Table {ℓ} lem
  using ( Ordering; strict; Related; IsRel; Values; Entries
        ; related-in; module Described )
open import V.Coding {ℓ} using ( pr )

import FOL.Absoluteness
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( J; subst2 )
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 ( ⟪_⟫ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( sucV; #_ )

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

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

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

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

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

  tm4 : ∀ {n} → Term S n → Term S (suc (suc (suc (suc n))))
  tm4 (con k) = con k
  tm4 (var i) = var (sh4 i)

  tm4-val : ∀ {n} (t : Term S n) (a b c d : S) (γ : S ^ n)
          → ⟦ tm4 t ⟧ (d ∷ c ∷ b ∷ a ∷ γ) ≡ ⟦ t ⟧ γ
  tm4-val (con k) a b c d γ = refl
  tm4-val (var i) a b c d γ = refl

-- perf: the two witnesses the birth description is satisfied at are sealed;
-- unsealed, the chapter's first section alone runs 178 s instead of 2 s
opaque
  towerS : (β : V ℓ) → IsOrd β → S
  towerS β ob = LsetS β ob

  towerS-fst : (β : V ℓ) (ob : IsOrd β) → fst (towerS β ob) ≡ Lset β
  towerS-fst β ob = refl

  powS : (β : V ℓ) → IsOrd β → S
  powS β ob = 𝒟ₒS β ob

  powS-fst : (β : V ℓ) (ob : IsOrd β) → fst (powS β ob) ≡ 𝒟ₒ (Lset β)
  powS-fst β ob = refl

诞生阶段，在内部说出

这条描述绑定两个集合，且不点名任何常元。存在一个 c，它是 b 处的塔；x 不属于它；并且存在一个 d，它是 c 的可定义幂集，而 x 属于它。使这两条条件等价于「b 比包含 x 的最小阶段低一级」的，是 Lset-suc，而它只花在元层面这一侧。这正是那个句子不需要自备后继运算的原因，也是塔之图用在 b 那一位自身、而不是用在它的一个后继上的原因。

两条读式都站在变元环境的变元位上，唯一的假设是 b 那一位的序数性。可靠性是一次对着最小阶段的三歧分情形，而它是一个把结论写出来的具名辅助：第一支由 stage-earliest 驳倒，第二支是 ord-suc-inj 对着 birth-suc，第三支是 ∈sucV-elim 分成两条与非隶属相冲的矛盾。完备性更短，因为 Lset-defines 与 DefAt-stage 各自反着跑一行。

这条描述所满足于其上的那两个元素被封印，而那条标记记录的是实测、不是偏好：不封印，仅这一节就跑 178 秒，封印后是 2 秒。Lset 与 𝒟ₒ 在它们被造出之处早已封印，但携带它们可构造性证明的那两个对没有，而抵达槽位的正是那个对。

BirthAt : ∀ {n} → Fin n → Fin n → Formula S n
BirthAt b x =
  ∃̇ ( LsetGraphAt zero (suc b)
    ∧̇ ( ¬̇ (var (suc x) ∈̇ var zero)
      ∧̇ ∃̇ ( DefAt zero (suc zero) ∧̇ (var (sh2 x) ∈̇ var zero) ) ) )

module _ {n : ℕ} (b x : Fin n) (γ : S ^ n) where
  private
    β : V ℓ
    β = fst (lookup b γ)

    z : S
    z = lookup x γ

    Inner : S → Type (ℓ-suc ℓ)
    Inner c = Σ[ d ∈ S ]
      ( ⟨ (d ∷ c ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ⟨ fst z ∈ fst d ⟩ )

    Outer : S → Type (ℓ-suc ℓ)
    Outer c = ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
            × ( (⟨ fst z ∈ fst c ⟩ → Empty.⊥) × ∥ Inner c ∥₁ )

    decideBirth : IsOrd β → ⟨ fst z ∈ 𝒟ₒ (Lset β) ⟩
                → (⟨ fst z ∈ Lset β ⟩ → Empty.⊥)
                → β ≡ birth (fst z) (snd z)
    decideBirth ob hin hout = go (ord-tri (sucV β) (suc-ord ob)
                                          (stage (fst z) (snd z))
                                          (stage-ord (fst z) (snd z)))
      where
      mem : ⟨ fst z ∈ Lset (sucV β) ⟩
      mem = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (Lset-suc β)) hin

      early : ⟨ stage (fst z) (snd z) ∈ sucV β ⟩ → Empty.⊥
      early h = Empty.rec* (∈sucV-elim {A = β} {x = stage (fst z) (snd z)}
        Empty.isProp⊥* h below same)
        where
        below : ⟨ stage (fst z) (snd z) ∈ β ⟩ → Empty.⊥*
        below k = Empty.rec (hout
          (Lset-mono {α = β} {β = stage (fst z) (snd z)} k
            {x = fst z} (stage-mem (fst z) (snd z))))
        same : stage (fst z) (snd z) ≡ β → Empty.⊥*
        same e = Empty.rec (hout (subst (λ u → ⟨ fst z ∈ Lset u ⟩) e
          (stage-mem (fst z) (snd z))))

      go : ⟨ sucV β ∈ stage (fst z) (snd z) ⟩
         ⊎ ((sucV β ≡ stage (fst z) (snd z)) ⊎ ⟨ stage (fst z) (snd z) ∈ sucV β ⟩)
         → β ≡ birth (fst z) (snd z)
      go (inl h) = Empty.rec
        (stage-earliest (fst z) (snd z) (sucV β) (suc-ord ob) mem h)
      go (inr (inl e)) = ord-suc-inj β (birth (fst z) (snd z)) ob
        (e ∙ sym (birth-suc (fst z) (snd z)))
      go (inr (inr h)) = Empty.rec (early h)

  BirthAt-out : ⟨ γ ⊨ BirthAt b x ⟩ → IsOrd β → β ≡ birth (fst z) (snd z)
  BirthAt-out h ob =
    PT.rec (setIsSet β (birth (fst z) (snd z))) atCarrier h
    where
    atInner : (c : S) → ⟨ (c ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
            → (⟨ fst z ∈ fst c ⟩ → Empty.⊥)
            → Inner c → β ≡ birth (fst z) (snd z)
    atInner c hg hn (d , (hd , hm)) = decideBirth ob
      (subst (λ u → ⟨ fst z ∈ u ⟩) qd hm)
      (λ k → hn (subst (λ u → ⟨ fst z ∈ u ⟩) (sym qc) k))
      where
      qc : fst c ≡ Lset β
      qc = Lset-only zero (suc b) (c ∷ γ) hg ob
      qd : fst d ≡ 𝒟ₒ (Lset β)
      qd = subst ⟨_⟩ (DefAt-stage β ob zero (suc zero) (d ∷ c ∷ γ) qc) hd

    atCarrier : Σ[ c ∈ S ] Outer c → β ≡ birth (fst z) (snd z)
    atCarrier (c , (hg , (hn , hi))) =
      PT.rec (setIsSet β (birth (fst z) (snd z))) (atInner c hg hn) hi

  BirthAt-in : IsOrd β → β ≡ birth (fst z) (snd z) → ⟨ γ ⊨ BirthAt b x ⟩
  BirthAt-in ob e = ∣ towerS β ob
    , (hg , (hn , ∣ powS β ob , (hd , hm) ∣₁)) ∣₁
    where
    hg : ⟨ (towerS β ob ∷ γ) ⊨ LsetGraphAt zero (suc b) ⟩
    hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob)

    hn : ⟨ fst z ∈ fst (towerS β ob) ⟩ → Empty.⊥
    hn k = stage-earliest (fst z) (snd z) β ob
      (subst (λ u → ⟨ fst z ∈ u ⟩) (towerS-fst β ob) k)
      (subst (λ u → ⟨ u ∈ stage (fst z) (snd z) ⟩) (sym e)
        (birth-stage (fst z) (snd z)))

    hd : ⟨ (powS β ob ∷ towerS β ob ∷ γ) ⊨ DefAt zero (suc zero) ⟩
    hd = subst ⟨_⟩
      (sym (DefAt-stage β ob zero (suc zero)
              (powS β ob ∷ towerS β ob ∷ γ) (towerS-fst β ob)))
      (powS-fst β ob)

    hm : ⟨ fst z ∈ fst (powS β ob) ⟩
    hm = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (powS-fst β ob))
      (subst (λ u → ⟨ fst z ∈ u ⟩) (Lset-suc β)
        (subst (λ u → ⟨ fst z ∈ Lset (sucV u) ⟩) (sym e)
          (birth-mem (fst z) (snd z))))

任意元数处的诸码，落在一个作为槽位的载体上

第三笔债索取的是「在一个随诞生阶段移动的载体上的码集」。它是实例化、不是构造，而把这句话说出来值这一段。幂集那一章早已把「载体握在一位上」的码谓词 isCodeAt 写成两个合取项：实参是元数一处的一个键，且它在那一位所持有的载体上有一个既封闭又成形的见证。码集那一章也早已写下第一个合取项的元数绑定变体 arityNumAtL，因为对诸子码的递归必须以每个元数处的诸键为索引。两者之间再无别的差异。

于是此处所要的谓词，就是第二个合取项接上元数绑定的第一个，而它的两条读式就是现成的那两条读在一位上：元数那一项交出一个数码与一条码，见证那一项把这一对变成载体之上的一条公式。没有新机器，没有新的旁条件，而载体自始至终是一位。

isCodeAnyAt : ∀ {n} → Fin n → Fin n → Formula S n
isCodeAnyAt c w = arityNumAtL c ∧̇ hasWitnessAt w c

module _ (A : S) where
  codeAnyAt-in : ∀ {n k} (c w : Fin n) (γ : S ^ n)
               → fst (lookup w γ) ≡ fst A
               → (ψ : Formula ⟪ fst A ⟫ k) → fst (lookup c γ) ≡ fst (keyS A ψ)
               → ⟨ γ ⊨ isCodeAnyAt c w ⟩
  codeAnyAt-in {k = k} c w γ qw ψ qc =
    arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc

  codeAnyAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n)
                → fst (lookup w γ) ≡ fst A
                → ⟨ γ ⊨ isCodeAnyAt c w ⟩
                → ⟨ IsKeyOverAny A (lookup c γ) ⟩
  codeAnyAt-out c w γ qw (hk , hw) =
    PT.rec squash₁ step (arityNumAtL-out c γ hk)
    where
    step : Σ[ m ∈ ℕ ] Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# m) (fst z))
         → ⟨ IsKeyOverAny A (lookup c γ) ⟩
    step (m , (z , qz)) = PT.map (λ { (ψ , q) → m , (ψ , q) })
      (witnessAt-out A w c γ qw hw m z qz)

那个集合，一次外延

那个集合是一次 extAt，理由与这条路线上每一条取值为集合的子句相同：一个取值恰是满足某条件的那些东西之集，而若写成一对包含，那个条件就要说两遍。它的两条读式把谓词那两条接到码集自家的隶属等价上，出来的是一条元素之间的等式：在一个经等式抵达的载体上，那一位所持有的就是该载体之上的码集、别无他物。

这正是「随诞生阶段移动」所索取的东西。命名那条描述把它的码集取作一位，由外部供来的一条等式钉住；有了这个合取项在旁，那一位改由描述自己钉住，于是调用方可以先绑定载体，再让码集跟着它走。

CodesAt : ∀ {n} → Fin n → Fin n → Formula S n
CodesAt c w = extAt c (isCodeAnyAt zero (suc w))

module _ (A : S) {n : ℕ} (c w : Fin n) (γ : S ^ n)
         (qw : fst (lookup w γ) ≡ fst A) where
  CodesAt-out : ⟨ γ ⊨ CodesAt c w ⟩ → lookup c γ ≡ AllCodes A
  CodesAt-out h = extensionalL step
    where
    step : (x : S) → (x ∈ˢ lookup c γ) ≡ (x ∈ˢ AllCodes A)
    step x = ⇔toPath
      (λ hx → AllCodes-in A x
        (codeAnyAt-out A zero (suc w) (x ∷ γ) qw
          (extAt-out c (isCodeAnyAt zero (suc w)) γ h x hx)))
      (λ hx → extAt-in c (isCodeAnyAt zero (suc w)) γ h x
        (PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)))
          (λ { (k , (ψ , q)) →
                 codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ q })
          (AllCodes-out A x hx)))

  CodesAt-in : lookup c γ ≡ AllCodes A → ⟨ γ ⊨ CodesAt c w ⟩
  CodesAt-in q = extAt-in-both c (isCodeAnyAt zero (suc w)) γ into back
    where
    into : (x : S) → ⟨ fst x ∈ fst (lookup c γ) ⟩
         → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
    into x hx = PT.rec (snd ((x ∷ γ) ⊨ isCodeAnyAt zero (suc w)))
      (λ { (k , (ψ , qk)) →
             codeAnyAt-in A {k = k} zero (suc w) (x ∷ γ) qw ψ qk })
      (AllCodes-out A x (subst (λ u → ⟨ fst x ∈ fst u ⟩) q hx))

    back : (x : S) → ⟨ (x ∷ γ) ⊨ isCodeAnyAt zero (suc w) ⟩
         → ⟨ fst x ∈ fst (lookup c γ) ⟩
    back x hx = subst (λ u → ⟨ fst x ∈ fst u ⟩) (sym q)
      (AllCodes-in A x (codeAnyAt-out A zero (suc w) (x ∷ γ) qw hx))

阶段处的序，展开一次

三个元语言的定义，其中之一是本章的支点。order-unfold 是那一族的定义方程读在一个阶段处：两个成员的比较，就是它们诞生阶段之间的比较，或者，在同一诞生阶段处，就是那里的那一步。它是在递归的计算规则上作的一次 cong，而对象语言要对上的一切，如今都站在它的右边。

bornIn 是 birth-in 的逆：诞生阶段落在某个序数以下的集合，落在那个序数处的塔中。正是它使这条描述得以丢掉「被比较的两个集合都属于这个阶段」那条条件，只留下「两个诞生阶段都落在它以下」，而那是落在反正要绑定的两位上的两个隶属原子，还省下一层绑定。

stepMoved 沿载体之间的一条等式搬运一次步进比较，靠路径归纳，基底情形用序数性的证明无关性。上一章私有地持有同一条引理。此处是重建而不是导出，因为从另一个模块够到数据正是这条路线要付代价的地方，而解药是就地。

stepOrder : (δ : V ℓ) → IsOrd δ → SWO (New δ)
stepOrder δ oδ = stepAt δ (carry (Lset δ) (orderAt δ oδ))

stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ)
          → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y
stepMoved δ δ' e = J Motive base e
  where
  Motive : (δ' : V ℓ) → δ ≡ δ' → Type (ℓ-suc ℓ)
  Motive δ' _ = (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ)
              → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y
  base : Motive δ refl
  base o o' x y = subst (λ w → Under δ (stepOrder δ w) x y) (isPropIsOrd δ o o')

bornIn : (α : V ℓ) → IsOrd α → (x : V ℓ) (p : ⟨ isL x ⟩)
       → ⟨ birth x p ∈ α ⟩ → ⟨ x ∈ Lset α ⟩
bornIn α oα x p h = reach (suc∈or≡ (birth x p) α (birth-ord x p) oα h)
  where
  reach : ⟨ sucV (birth x p) ∈ α ⟩ ⊎ (sucV (birth x p) ≡ α) → ⟨ x ∈ Lset α ⟩
  reach (inl k) = Lset-mono {α = α} {β = sucV (birth x p)} k
    {x = x} (birth-mem x p)
  reach (inr e) = subst (λ w → ⟨ x ∈ Lset w ⟩) e (birth-mem x p)

module _ (α : V ℓ) (oα : IsOrd α) where
  private
    module Fam = Family α (λ δ _ → orderAt δ) oα

  memberL : (a : Mem (Lset α)) → ⟨ isL (fst a) ⟩
  memberL a = Lset→isL α oα (fst a) (snd a)

  bornOf : (a : Mem (Lset α)) → V ℓ
  bornOf a = birth (fst a) (memberL a)

  bornOrd : (a : Mem (Lset α)) → IsOrd (bornOf a)
  bornOrd a = birth-ord (fst a) (memberL a)

  bornMem : (a : Mem (Lset α)) → ⟨ bornOf a ∈ α ⟩
  bornMem a = Fam.bornAt a .snd

  order-unfold : (a b : Mem (Lset α))
               → relOf (orderAt α oα) a b
               ≡ ( ⟨ bornOf a ∈ bornOf b ⟩
                 ⊎ ( (bornOf b ≡ bornOf a)
                   × Under (bornOf a) (stepOrder (bornOf a)
                       (mem-ord {A = α} oα (bornOf a) (bornMem a)))
                       (fst a) (fst b) ) )
  order-unfold a b = cong (λ z → relOf (z oα) a b) (orderAt-step α)

另有四个元素抵达满足关系内部的诸位，它们出于同一条实测理由被封印。封印所暴露的诸等式，恰是这条描述要消费的那三条：一个成员的底集、一个诞生阶段的底集，以及那条说「某个诞生阶段就是它旁边那个成员的诞生阶段」的等式，于是诞生描述在每个调用点由 refl 解除。

-- perf: the four elements the order description is satisfied at are sealed;
-- unsealed, the reading back into the object language runs past 400 s
opaque
  memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S
  memS α oα a = fst a , memberL α oα a

  memS-fst : (α : V ℓ) (oα : IsOrd α) (a : Mem (Lset α))
           → fst (memS α oα a) ≡ fst a
  memS-fst α oα a = refl

  bornS : (α : V ℓ) (oα : IsOrd α) → ⟨ isL α ⟩ → Mem (Lset α) → S
  bornS α oα pα a = bornOf α oα a
                  , isL-trans {x = α} {y = bornOf α oα a} (bornMem α oα a) pα

  bornS-fst : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α))
            → fst (bornS α oα pα a) ≡ bornOf α oα a
  bornS-fst α oα pα a = refl

  bornS-birth : (α : V ℓ) (oα : IsOrd α) (pα : ⟨ isL α ⟩) (a : Mem (Lset α))
              → fst (bornS α oα pα a)
              ≡ birth (fst (memS α oα a)) (snd (memS α oα a))
  bornS-birth α oα pα a = refl

那个序，被描述出来，而那一步取作参数

自此往下的一切都对那条步进条件保持通用，它以参数身份进场，含义两个方向都说清：在一个经一位抵达的载体上，手里握着表在那里的取值时，该条件对两个集合成立，当且仅当那个载体处的步进序把它们关联起来。那个参数就是本章仍然欠着的全部，而它是有意做成一件事、而不是三件。

两个方向取用表在那个载体处的取值的方式不同，而这个不同不是装点。完备性被交到手上的是某一个取值，附带「它实现那里的序」这条假设，因为那正是它要塞进那条条件里去的东西。可靠性被交到手上的，是对表在那里所记录的每一个取值都成立的那条假设，因为它所读的那条条件可能自己绑定了一个取值，而只有「无论找到哪一个都能证其实现」的供给方，才说得清那个取值是什么。两边都是上面那个框架交出来的东西，即 Values 读在单个实参上。

主体只绑定四个集合，不多。其中两个是被比较的成员，它们的对就是那个实参，另外两个是它们的诞生阶段。然后是五条条件：每个诞生阶段都是它那个成员的诞生阶段，每个诞生阶段都落在该阶段以下，以及比较自身，即两个诞生阶段之间的一个隶属原子，或者，在同一诞生阶段处，就是那一步。阶段是以词项、而不是以槽位的身份到场的，而这不是装饰：下一章要跑的那次分离，要的是整条条件落在诸常元上，而词项无须绑定就能接住一个常元，槽位则要花掉一层。实测下来，那一层绑定就是 3 秒与 160 秒之差。

module Ordered
  (Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n)
  (stp-out : ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ)))
           → ((r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩
              → IsRel (fst (lookup d γ)) r)
           → ⟨ γ ⊨ Stp d f u v ⟩
           → ∥ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od)
                 (fst (lookup u γ)) (fst (lookup v γ)) ∥₁)
  (stp-in : ∀ {n} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ)))
          → (r : S) → ⟨ pr (fst (lookup d γ)) (fst r) ∈ fst (lookup f γ) ⟩
          → IsRel (fst (lookup d γ)) r
          → Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od)
              (fst (lookup u γ)) (fst (lookup v γ))
          → ⟨ γ ⊨ Stp d f u v ⟩)
  where

  OrdBody : ∀ {n} → Term S n → Fin n → Formula S (suc (suc (suc (suc n))))
  OrdBody tb f =
      BirthAt (suc zero) (sh3 zero)
    ∧̇ ( BirthAt zero (sh2 zero)
      ∧̇ ( (var (suc zero) ∈̇ tm4 tb)
        ∧̇ ( (var zero ∈̇ tm4 tb)
          ∧̇ ( (var (suc zero) ∈̇ var zero)
            ∨̇ ( (var zero ≐ var (suc zero))
              ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) )

  -- perf: the order description is sealed where it is built; unsealed, its two
  -- readings at the constants the separation wants run 160 s each instead of 2 s
  opaque
    CondCore : ∀ {n} → Fin n → Term S n → Fin n → Formula S n
    CondCore z tb f =
      ∃̇ ( ∃̇ ( prAtL (sh2 z) (suc zero) zero ∧̇ ∃̇ (∃̇ (OrdBody tb f)) ) )

这条描述说了什么，两个方向

这条读式取用阶段的序数性，以及表在它以下的两条正确性条件，而那恰是它所供养的那个框架交出来的东西。二者是分开花掉的。可靠性只花正确性那一条，花在被比较成员的诞生阶段处，并原样把它递给步进参数。完备性经 value 把两条一并花掉：在阶段以下的一个诞生阶段处，表「仅仅」有一个取值，而那个取值实现那里的序，于是那个参数可以被填上。单值性自始至终用不上，因为步进条件是命题，而一个「仅仅存在」的取值可以在其中被打开。

  module _ {n : ℕ} (z : Fin n) (tb : Term S n) (f : Fin n) (γ : S ^ n)
           (oα : IsOrd (fst (⟦ tb ⟧ γ)))
           (vals : Values (lookup f γ) (fst (⟦ tb ⟧ γ)))
           (ents : Entries (lookup f γ) (fst (⟦ tb ⟧ γ))) where
    private
      α : V ℓ
      α = fst (⟦ tb ⟧ γ)

      shift : (u v du dv : S) → ⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ) ≡ ⟦ tb ⟧ γ
      shift u v du dv = tm4-val tb u v du dv γ

      value : (d : S) → ⟨ fst d ∈ α ⟩ → (P : Ω)
            → ((r : S) → ⟨ pr (fst d) (fst r) ∈ fst (lookup f γ) ⟩
               → IsRel (fst d) r → ⟨ P ⟩)
            → ⟨ P ⟩
      value d hd P k = PT.rec (snd P)
        (λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd)

      Deep : (u v du : S) → S → Type (ℓ-suc ℓ)
      Deep u v du dv = ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ OrdBody tb f ⟩

      Mid : (u v : S) → S → Type (ℓ-suc ℓ)
      Mid u v du = ∥ (Σ[ dv ∈ S ] Deep u v du dv) ∥₁

      Pair : (u : S) → S → Type (ℓ-suc ℓ)
      Pair u v = ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
               × ∥ (Σ[ du ∈ S ] Mid u v du) ∥₁

      Top : S → Type (ℓ-suc ℓ)
      Top u = ∥ (Σ[ v ∈ S ] Pair u v) ∥₁

可靠性把那四个被绑定的集合读回来。对的等式认定那个实参；两条诞生读式把两个被绑定的序数钉在两个成员的诞生阶段上；bornIn 把「落在该阶段以下」的两条隶属变成「属于该阶段」，而那正是那个类所量化的东西；随后那次比较就是那一族自家的比较，沿 order-unfold 而来。这条描述在此处是封印着的，故这份证明里没有任何东西去归一化它所谈论的那个句子。

    opaque
     unfolding CondCore

     CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α (fst (lookup z γ)) ⟩
     CondCore-out = PT.rec (snd (Related α (fst (lookup z γ)))) atTop
       where
       Goal : Type (ℓ-suc ℓ)
       Goal = ⟨ Related α (fst (lookup z γ)) ⟩

       atDeep : (u v du dv : S)
              → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
              → Deep u v du dv → Goal
       atDeep u v du dv hp (hbu , (hbv , (hmu₀ , (hmv₀ , hcmp)))) =
         subst (λ w → ⟨ Related α w ⟩) (sym qz)
           (PT.rec (snd (Related α (pr (fst u) (fst v)))) atCase hcmp)
         where
         qz : fst (lookup z γ) ≡ pr (fst u) (fst v)
         qz = subst ⟨_⟩ (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)) hp

         hmu : ⟨ fst du ∈ α ⟩
         hmu = subst (λ w → ⟨ fst du ∈ fst w ⟩) (shift u v du dv) hmu₀

         hmv : ⟨ fst dv ∈ α ⟩
         hmv = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (shift u v du dv) hmv₀

         odu : IsOrd (fst du)
         odu = mem-ord {A = α} oα (fst du) hmu

         odv : IsOrd (fst dv)
         odv = mem-ord {A = α} oα (fst dv) hmv

         qu : fst du ≡ birth (fst u) (snd u)
         qu = BirthAt-out (suc zero) (sh3 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbu odu

         qv : fst dv ≡ birth (fst v) (snd v)
         qv = BirthAt-out zero (sh2 zero) ((dv ∷ du ∷ v ∷ u ∷ γ)) hbv odv

         a : Mem (Lset α)
         a = fst u , bornIn α oα (fst u) (snd u)
               (subst (λ w → ⟨ w ∈ α ⟩) qu hmu)

         c : Mem (Lset α)
         c = fst v , bornIn α oα (fst v) (snd v)
               (subst (λ w → ⟨ w ∈ α ⟩) qv hmv)

         qa : bornOf α oα a ≡ fst du
         qa = birth-proof (fst u) (memberL α oα a) (snd u) ∙ sym qu

         qc : bornOf α oα c ≡ fst dv
         qc = birth-proof (fst v) (memberL α oα c) (snd v) ∙ sym qv

         fill : relOf (orderAt α oα) a c → ⟨ Related α (pr (fst u) (fst v)) ⟩
         fill = related-in α oα a c

         atCase : ⟨ fst du ∈ fst dv ⟩
                ⊎ ( (fst dv ≡ fst du)
                  × ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ⟩ )
                → ⟨ Related α (pr (fst u) (fst v)) ⟩
         atCase (inl h) = fill (transport (sym (order-unfold α oα a c))
           (inl (subst2 (λ p q → ⟨ p ∈ q ⟩) (sym qa) (sym qc) h)))
         atCase (inr (e , hs)) = PT.rec
           (snd (Related α (pr (fst u) (fst v)))) atUnder
           (stp-out (suc zero) (sh4 f) (sh3 zero) (sh2 zero)
             ((dv ∷ du ∷ v ∷ u ∷ γ)) odu (λ r hr → vals du r hmu hr) hs)
           where
           atUnder : Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v)
                   → ⟨ Related α (pr (fst u) (fst v)) ⟩
           atUnder und = fill (transport (sym (order-unfold α oα a c))
             (inr (qc ∙ e ∙ sym qa
               , stepMoved (fst du) (bornOf α oα a) (sym qa) odu
                   (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))
                   (fst u) (fst v) und)))

       atMid : (u v du : S)
             → ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
             → Mid u v du → Goal
       atMid u v du hp = PT.rec (snd (Related α (fst (lookup z γ))))
         (λ { (dv , hd) → atDeep u v du dv hp hd })

       atPair : (u v : S) → Pair u v → Goal
       atPair u v (hp , hm) = PT.rec (snd (Related α (fst (lookup z γ))))
         (λ { (du , hd) → atMid u v du hp hd }) hm

       atTop : Σ[ u ∈ S ] Top u → Goal
       atTop (u , h) = PT.rec (snd (Related α (fst (lookup z γ))))
         (λ { (v , hv) → atPair u v hv }) h

完备性把它们填回去。那个类被拆成一对成员加一次比较，比较由 strict 脱去截断，而那四个见证就是两个成员与它们的两个诞生阶段，各自封印。对那次比较的两路分情形是一个具名辅助，绝不是 with：写成 with，仅这一次分情形就跑过 300 秒，因为它所作的抽象是对着一个满足关系的，而那个满足关系是全章最大的词项。

     private
       Pairs : IsOrd α → Type (ℓ-suc ℓ)
       Pairs o = Σ[ a ∈ Mem (Lset α) ] ∥ (Σ[ c ∈ Mem (Lset α) ]
         ( (fst (lookup z γ) ≡ pr (fst a) (fst c)) × ⟨ Ordering α o a c ⟩ )) ∥₁

     CondCore-in : ⟨ Related α (fst (lookup z γ)) ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩
     CondCore-in = PT.rec (snd (γ ⊨ CondCore z tb f)) atOrd
       where
       atRel : (o : IsOrd α) (a c : Mem (Lset α))
             → fst (lookup z γ) ≡ pr (fst a) (fst c)
             → ⟨ Ordering α o a c ⟩ → ⟨ γ ⊨ CondCore z tb f ⟩
       atRel o a c q hord =
         value (bornS α oα pα a) hmu (γ ⊨ CondCore z tb f) atValue
         where
         pα : ⟨ isL α ⟩
         pα = snd (⟦ tb ⟧ γ)

         u v du dv : S
         u = memS α oα a
         v = memS α oα c
         du = bornS α oα pα a
         dv = bornS α oα pα c

         hmu : ⟨ fst du ∈ α ⟩
         hmu = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα a))
           (bornMem α oα a)

         hmv : ⟨ fst dv ∈ α ⟩
         hmv = subst (λ w → ⟨ w ∈ α ⟩) (sym (bornS-fst α oα pα c))
           (bornMem α oα c)

         odu : IsOrd (fst du)
         odu = mem-ord {A = α} oα (fst du) hmu

         odv : IsOrd (fst dv)
         odv = mem-ord {A = α} oα (fst dv) hmv

         cmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩
             ⊎ ( (bornOf α oα c ≡ bornOf α oα a)
               × Under (bornOf α oα a) (stepOrder (bornOf α oα a)
                   (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
                   (fst a) (fst c) )
         cmp = transport (order-unfold α oα a c)
           (strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩)
             (isPropIsOrd α o oα) hord))

         hp : ⟨ (v ∷ u ∷ γ) ⊨ prAtL (sh2 z) (suc zero) zero ⟩
         hp = subst ⟨_⟩
           (sym (prAtL-adequate (sh2 z) (suc zero) zero (v ∷ u ∷ γ)))
           (q ∙ cong₂ pr (sym (memS-fst α oα a)) (sym (memS-fst α oα c)))

         hbu : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt (suc zero) (sh3 zero) ⟩
         hbu = BirthAt-in (suc zero) (sh3 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odu
           (bornS-birth α oα pα a)

         hbv : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ BirthAt zero (sh2 zero) ⟩
         hbv = BirthAt-in zero (sh2 zero) (dv ∷ du ∷ v ∷ u ∷ γ) odv
           (bornS-birth α oα pα c)

         moved : Under (bornOf α oα a) (stepOrder (bornOf α oα a)
                   (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
                   (fst a) (fst c)
               → Under (fst du) (stepOrder (fst du) odu) (fst u) (fst v)
         moved und = subst2 (λ p r → Under (fst du) (stepOrder (fst du) odu) p r)
           (sym (memS-fst α oα a)) (sym (memS-fst α oα c))
           (stepMoved (bornOf α oα a) (fst du) (sym (bornS-fst α oα pα a))
             (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)) odu
             (fst a) (fst c) und)

         atValue : (r : S) → ⟨ pr (fst du) (fst r) ∈ fst (lookup f γ) ⟩
                 → IsRel (fst du) r → ⟨ γ ⊨ CondCore z tb f ⟩
         atValue r hr hrel = ∣ u , ∣ v , (hp , ∣ du , ∣ dv
           , (hbu , (hbv , (hmu₀ , (hmv₀ , side)))) ∣₁ ∣₁) ∣₁ ∣₁
           where
           hmu₀ : ⟨ fst du ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩
           hmu₀ = subst (λ w → ⟨ fst du ∈ fst w ⟩) (sym (shift u v du dv)) hmu

           hmv₀ : ⟨ fst dv ∈ fst (⟦ tm4 tb ⟧ (dv ∷ du ∷ v ∷ u ∷ γ)) ⟩
           hmv₀ = subst (λ w → ⟨ fst dv ∈ fst w ⟩) (sym (shift u v du dv)) hmv

           -- perf: law of the route: a two-way split concluding in a
           -- satisfaction is a named helper, never a `with`; as a `with` this
           -- one alone runs past 300 s
           atCmp : ⟨ bornOf α oα a ∈ bornOf α oα c ⟩
                 ⊎ ( (bornOf α oα c ≡ bornOf α oα a)
                   × Under (bornOf α oα a) (stepOrder (bornOf α oα a)
                       (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a)))
                       (fst a) (fst c) )
                 → ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero)
                     ∨̇ ( (var zero ≐ var (suc zero))
                       ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩
           atCmp (inl h) = ∣ inl (subst2 (λ p q → ⟨ p ∈ q ⟩)
             (sym (bornS-fst α oα pα a)) (sym (bornS-fst α oα pα c)) h) ∣₁
           atCmp (inr (e , und)) = ∣ inr
             ( bornS-fst α oα pα c ∙ e ∙ sym (bornS-fst α oα pα a)
             , stp-in (suc zero) (sh4 f) (sh3 zero) (sh2 zero)
                 (dv ∷ du ∷ v ∷ u ∷ γ) odu r hr hrel (moved und) ) ∣₁

           side : ⟨ (dv ∷ du ∷ v ∷ u ∷ γ) ⊨ ( (var (suc zero) ∈̇ var zero)
                     ∨̇ ( (var zero ≐ var (suc zero))
                       ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ⟩
           side = atCmp cmp

       atPairs : (o : IsOrd α) → Pairs o → ⟨ γ ⊨ CondCore z tb f ⟩
       atPairs o (a , h) = PT.rec (snd (γ ⊨ CondCore z tb f))
         (λ { (c , (q , hord)) → atRel o a c q hord }) h

       atOrd : Σ[ o ∈ IsOrd α ] ∥ Pairs o ∥₁ → ⟨ γ ⊨ CondCore z tb f ⟩
       atOrd (o , h) = PT.rec (snd (γ ⊨ CondCore z tb f)) (atPairs o) h

     CondCore-spec : (γ ⊨ CondCore z tb f) ≡ Related α (fst (lookup z γ))
     CondCore-spec = ⇔toPath CondCore-out CondCore-in

那个框架的两条假设，已解除

上一章索取的是同一含义的两种形式：落在诸位上，因为图必须绑定它所查阅的那张表；以及落在诸常元上，因为分离是用单自由变量的公式去雕的。两者是同一个主体。落在诸位上时，阶段是词项 var b，什么也不绑定；落在诸常元上时，阶段是词项 con B，只有表被绑定，用一个存在量词，由那层绑定处的等式钉住。

这两条一填上，Described 便可施用，而它所证的一切在此处都可取用：逼近、图、每个序数处的表、每个阶段处作为 L 之元素的那个关系，以及它的隶属读在「阶段的成员到场时的两种形状」上。这一切都以那个步进参数为条件，且再无其他条件。

  Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n)
  Cond b f = CondCore zero (var (suc b)) (suc f)

  Cond₀ : S → S → Formula S 
  Cond₀ B F =
    ∃̇ ( (var zero ≐ con F) ∧̇ CondCore (suc zero) (con B) zero )

  cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ))
            → Values (lookup f γ) (fst (lookup b γ))
            → Entries (lookup f γ) (fst (lookup b γ))
            → (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z)
  cond-spec b f γ ob vals ents z =
    CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents

  module _ (B F : S) (oB : IsOrd (fst B))
           (vals : Values F (fst B)) (ents : Entries F (fst B)) (z : S) where
    private
      Held : S → Type (ℓ-suc ℓ)
      Held c = (fst c ≡ fst F)
             × ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩

    cond₀-out : ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩ → ⟨ Related (fst B) (fst z) ⟩
    cond₀-out = PT.rec (snd (Related (fst B) (fst z))) atHeld
      where
      atHeld : Σ[ c ∈ S ] Held c → ⟨ Related (fst B) (fst z) ⟩
      atHeld (c , (qc , hc)) =
        CondCore-out (suc zero) (con B) zero (c ∷ z ∷ []) oB
          (λ x r hx hp → vals x r hx
            (subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) qc hp))
          (λ x hx → PT.map (λ { (r , hr) → r
              , subst (λ w → ⟨ pr (fst x) (fst r) ∈ w ⟩) (sym qc) hr })
            (ents x hx))
          hc

    cond₀-in : ⟨ Related (fst B) (fst z) ⟩ → ⟨ (z ∷ []) ⊨ Cond₀ B F ⟩
    cond₀-in h = ∣ F , (refl
      , CondCore-in (suc zero) (con B) zero (F ∷ z ∷ []) oB vals ents h) ∣₁

  cond₀-spec : (B F : S) → IsOrd (fst B)
             → Values F (fst B) → Entries F (fst B)
             → (z : S) → ((z ∷ []) ⊨ Cond₀ B F) ≡ Related (fst B) (fst z)
  cond₀-spec B F oB vals ents z =
    ⇔toPath (cond₀-out B F oB vals ents z) (cond₀-in B F oB vals ents z)

  open Described Cond Cond₀ cond-spec cond₀-spec public

小结

BirthAt 是诞生阶段在对象语言中的描述，不含后继运算，也不点名任何常元：那一位处的塔不装这个集合，而那座塔的可定义幂集装它。BirthAt-out 与 BirthAt-in 是它落在变元位上的两条读式，唯一的假设是序数位处的序数性，而它所满足于其上的那两个元素被封印，实测为 178 秒对 2 秒。

isCodeAnyAt 是任意元数处、落在一位所持载体上的码谓词，而它是实例化、不是构造：元数绑定那个合取项与见证那个合取项都早已存在，一个在码集那一章、一个在幂集那一章，新的只是它们的会合。CodesAt 是它们雕出的那个集合，一次 extAt，而 CodesAt-out 与 CodesAt-in 在两个方向上把那一位钉在该载体之上的码集上，于是命名描述的码集那一位可以由描述钉住、而不必由外部的一条等式钉住。这就是第三笔债。

order-unfold 是序之族在一个阶段处的定义方程，即在递归的计算规则上作的一次 cong；bornIn 是 birth-in 的逆，正是它为这条描述省下一层绑定；stepMoved 沿载体之间的一条等式搬运一次步进比较，此处是重建、而不是伸手去够。

CondCore 是阶段处的序被完整描述出来，以诞生阶段为主键，对步进条件保持通用。它绑定四个集合，把阶段取作词项，使得常元那一形式不花绑定；而它在被造出之处封印：不封印，它落在诸常元上的两条读式各跑 160 秒。CondCore-out 与 CondCore-in 是它的两半，而 Cond、Cond₀、cond-spec 与 cond₀-spec 是上一章那个框架所索取的两种形式连同它们的含义。有了它们，Described 便可施用。

不在此处的，是那一步自身的适足性，即 L.Choice.Internal 的 StepAt 对着 stepAt。它以参数 Stp 的身份进场，stp-out 与 stp-in 是它的含义，前者取用表在该载体处所记录的每一个取值上的正确性，后者取用「实现那里的序」的单个取值；而它是对着早已存在的诸章记账的一整章：把参数序列读回成向量、把指称与元层面名字的指称认同、把这条描述诸名字中的最小者与元层面诸名字中的最小者认同。那个框架的两条假设已经没了；剩下这一条，就是横在这个构造与一条无条件定理之间的东西。