---
title: "层序描述的充分性"
module: L.Choice.StageOrderAdequacy
lang: zh
site: "Bedrock"
description: "层序描述的充分性"
stage: "典范良序与选择公理"
reading_order: 79
canonical: https://bedrock.institute/zh/L.Choice.StageOrderAdequacy.html
html: L.Choice.StageOrderAdequacy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/StageOrderAdequacy.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Linear, L.Ordinal.Stages, L.Axioms.Basic, L.Stage, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.WellOrder.Base, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Coding.DefinablePowerSet, L.Coding.CodeSet, L.Hierarchy, L.Choice.OrderTable, V.Coding, FOL.Absoluteness]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.StageOrderAdequacy.md, https://bedrock.institute/ja/L.Choice.StageOrderAdequacy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 层序描述的充分性

元理论已经在每个可构造层携带一个严格良序，但 `L` 的对象语言只能通过公式说话。本章把这一层序翻译成公式：描述每个集合的诞生层、随载体变化的码集，以及层序的比较规则，并证明这些描述忠实于其元语言含义。其中有一件被刻意留作参数：固定诞生层内部的比较。

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

经典推理只经由一个显式假设 `lem` 进入。比较序数层时会用到它，而本章构造的公式仍是对象语言的普通公式。因此，语义论证可以使用排中律，却不会把新公理写进被解释的语言。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM )
```

从一开始就要区分两个话语层次。此前构造的 `orderAt` 是元语言中的严格良序。本章的目标是构造一些公式，使其满足关系表达该良序的底层比较；本章没有任何公式重新构造 `SWO` 结构，也不重证其良基性。

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

这次翻译只使用对象语言的普通原子与联结词。隶属原子陈述候选见证属于某层或码集，相等原子认同两个被表示的对象，而存在量词隐藏描述所需的辅助集合。后文的证明会在可构造结构中解释这些公式，再把所得命题与相应的元语言命题比较。

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

这里所需的层级几何很简单。序数线性排列各层，序数指标之间的隶属使塔保持单调，而一个序数的后继把该层与下一可定义幂集层分开。借助这些事实，我们可以比较候选诞生序数的后继与集合首次出现的层，从而认定该候选序数。

```agda
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≡ )
```

对可构造集合 `x`，包含它的最早层是一个后继层，而 `birth x` 是紧邻其下的序数。因此，`x` 不属于 `Lset (birth x)`，却属于 `Lset (sucV (birth x))`，后者正是前一层的可定义幂集。公式 `BirthAt` 将表达这两条隶属事实；最小性本身仍来自元语言定理。

```agda
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.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj )
open import L.Choice.StageOrders {ℓ} lem
  using ( birth; birth-ord; birth-suc; birth-mem; birth-stage; birth-proof
```

既有的层序按诞生层对两个成员作字典式比较。较早的诞生层立即决定比较；诞生层相等时，比较交给该层新生元素上的局部序。后面的公式将精确对应这一次展开方程，因此其充分性只关乎 `orderAt` 已经携带的关系，并不关乎该序的构造。

```agda
        ; 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 ( prAtL; prAtL-adequate )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both )
```

同层比较需要使用定义在某个载体上的公式，而该载体随共同诞生序数变化。因此，相关语法不能预先固定在单一层上。下文的码谓词相对于一个由变元槽位持有的载体，涵盖每个有限元数，使载体及其公式码能够一同变化。

```agda
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage )
open import L.Coding.CodeSet {ℓ} lem
  using ( arityNumAtL; arityNumAtL-in; arityNumAtL-out; hasWitnessAt
        ; witnessAt-in; witnessAt-out; keyS; codeS
```

最终目标是在 `L` 中把关系表示为有序对之集。环境层以下的一张表提供局部关系取值，而公式必须对每个编码有序对都与元语言比较一致。证明这种一致既需要表项的正确性，也需要表项的存在性，并且始终以局部步进公式的两条充分性读式为条件。

```agda
        ; AllCodes; AllCodes-in; AllCodes-out; IsKeyOverAny )
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Choice.OrderTable {ℓ} lem
  using ( Ordering; strict; Related; IsRel; Values; Entries
        ; related-in; module Described )
```

被表示关系的一个元素读作编码 `pr u v`。因此，充分性有两个方向：从这种对码恢复某些被比较成员 `u`、`v` 并证明其层序比较成立；反过来，从一次已知比较把相应对码放入被表示集合。这里的存在经过命题截断，因而不会选出规范的分解。

```agda
open import V.Coding {ℓ} using ( pr )
```

证明中的若干认同会沿相等的层指标或对码搬运关系。由于序数性与可构造性证据都是命题，更换这些证据不会改变被表示的数学对象。正是这种证明无关性允许我们进行搬运，而不会把证书变成额外的选择。

```agda
import FOL.Absoluteness
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

存在量词的满足关系始终经过命题截断。证明只有在目标仍是命题时，才能使用某个层取值、可定义幂集取值、解码公式或表项。因此，下文任何一次消去都不会给出规范见证、选定的解码器，或为局部关系指定取值的选择函数。

```agda
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 ( ⟪_⟫ )
```

这里有两种作用不同的后继构造。`sucV` 推进一个序数层，而数码在层级内部编码有限元数。区分二者，就不会把「集合在诞生层的后继处进入」与公式码的元数分量混为一谈。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( sucV; #_ )
```

这些公式将在可构造结构 `𝒮ʟ` 中解释，所以其含义取值于命题：满足关系记录被描述的隶属、相等或存在是否在 `L` 内成立，而比较这些含义的证明则生活在外围的 Cubical Agda 元理论中。

```agda
open hPropStructure 𝒮ʟ
```

我们以 `γ ⊨ φ` 表示公式在环境中的满足，以 `⟦ t ⟧ γ` 表示项的取值。每条充分性陈述都通过这套记号架桥：左侧读取对象语言语法，右侧认定元理论中相应的集合、序数或关系。

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

第一个移位把变元命名到外移两槽的位置，为绑定四个对象的公式做准备。

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

第二个移位把变元外移三槽。

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

一个私有移位把变元外移四槽，预留给下一节绑定四个对象的公式。

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

项的移位把一个项移过四个新绑定：常数保持其值，每个变元按同一移位改名。

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

移位后的项的求值不受四个新绑定影响；这一定义性一致被记录一次，此后静默复用。

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

为了把 `Lset β` 放入公式环境，我们将该层连同其可构造性证明打包为 `S` 的元素。序数性假设提供这份证明。数学上要紧的是下文的第一投影等式：这个封装仍恰好指称 `Lset β`，因而可以在向内读取 `BirthAt` 时充当层见证。

```agda
opaque
  towerS : (β : V ℓ) → IsOrd β → S
  towerS β ob = LsetS β ob
```

打包后的层的底层集按定义就是层本身。

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

`BirthAt` 所需的第二个见证是该层的可定义幂集。我们以同样方式封装 `𝒟ₒ (Lset β)`；它的可构造性来自序数 `β` 处已有的层事实，而其第一投影正是公式所需的集合。

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

其底层集按定义就是该序数处层的可定义幂集。

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

## 诞生层的内部表述

`BirthAt b x` 绑定两个辅助集合。第一个必须是候选槽位 `b` 所描述的塔层 `Lset β`，且 `x` 不属于它；第二个必须是前者的可定义幂集，且 `x` 属于它。因此，该公式表达两个相继层之间的边界。它既不断言 `β` 是序数，也不包含对象语言内部的最小性子句。

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

固定一个环境 `γ`。候选序数是槽位 `b` 中元素的底层集合，而待检验诞生层的集合是槽位 `x` 中的元素。后续推理都相对于这两个解释进行，所以定理适用于任意变元赋值，而非特选常元。

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

元素 `z` 同时携带其底层集合与它属于 `L` 的证据。元语言函数 `birth` 使用这份证据形成一个序数，但证明无关性保证所得序数不会编码对某份可构造性证明的选择。

```agda
    z : S
    z = lookup x γ
```

内层记录收集候选层 `c` 之上的可定义幂集值 `d`，连同幂集描述的满足，以及参数属于 `d` 的隶属。

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

外层记录再加上「层图在抬升指数处的满足」「参数不属于候选层」的反驳，以及内层记录的截断。三者合起来恰是诞生公式所断言的内容。

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

关键语义引理假设 `β` 是序数，并且 `x` 属于 `𝒟ₒ (Lset β)` 而不属于 `Lset β`。它恰从这些边界事实证明 `β ≡ birth x`。序数性是这条读式的输入，并非从 `BirthAt` 的满足关系中恢复。

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

借助 `Lset-suc`，`𝒟ₒ (Lset β)` 中的隶属转化为 `Lset (sucV β)` 中的隶属。这说明包含 `x` 的最早层不晚于 `β` 的后继；证明还必须排除所有更早的可能。

```agda
                                          (stage-ord (fst z) (snd z)))
      where
      mem : ⟨ fst z ∈ Lset (sucV β) ⟩
      mem = subst (λ u → ⟨ fst z ∈ u ⟩) (sym (Lset-suc β)) hin
```

假设 `x` 的最早层属于 `sucV β`。后继序数中的隶属分成两种情形：该层属于 `β`，或该层等于 `β`。前一种由单调性、后一种由直接搬运，都会推出 `x` 属于 `Lset β`，与所假设的非隶属矛盾。

```agda
      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.⊥*
```

若 `stage x ∈ β`，层的单调性会把已知的 `x ∈ Lset (stage x)` 推到 `x ∈ Lset β`。若 `stage x ≡ β`，沿该等式搬运即可直接得到同一结论。两种情形都与边界假设 `x ∉ Lset β` 矛盾。

```agda
        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 x ≡ β` 把已知的隶属 `x ∈ Lset (stage x)` 搬运成 `x ∈ Lset β`。这是证明最早层不可能位于 `β` 或其下所需的第二个矛盾。

```agda
          (stage-mem (fst z) (snd z))))
```

现在用序数三歧律比较 `sucV β` 与 `stage x`。若前者严格更早，则 `x ∈ Lset (sucV β)` 与 `stage x` 的定义性最小性矛盾；若 `stage x` 更早，则前述论证与 `x ∉ Lset β` 矛盾。因此，只可能剩下相等情形。

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

由 `sucV β ≡ stage x` 与等式 `stage x ≡ sucV (birth x)`，序数后继的单射性给出 `β ≡ birth x`。结论来自对两个严格情形的排除；证明并未从公式中选取诞生见证。

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

读取引理携带槽位的序数性假设：公式自身并不证明该槽位是序数。证明拆开截断的存在量化，抵达外层记录。

```agda
  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) ⟩
```

在每个候选层处，内层记录供给包含参数的可定义幂集值，以及参数不属于候选层的反驳；判定引理应用于这三份数据。

```agda
            → (⟨ 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))
```

抬升指数处的层图由层级描述的唯一性认同为候选序数处的层；幂集值由描述的层等式认同为该层的可定义幂集。

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

外层记录被消去到内层读取，内层读取喂给判定引理；整个证明把截断消去为序数的相等，而序数相等是命题。

```agda
    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 (λ k → lower (hn k))) hi
```

反向证明假设槽位 `b` 中的序数等于 `x` 的元语言诞生层。两个存在见证分别是打包后的层 `Lset β` 及其打包后的可定义幂集。按照存在满足关系的要求，它们被置于命题截断之下，所以这项构造并不声称公式具有唯一确定的见证。

```agda
  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) ⟩
```

抬升指数处的层图成立，因为打包后的层按呈现的定义等式就是该指数处的层。

```agda
    hg = Lset-defines zero (suc b) (towerS β ob ∷ γ) ob (towerS-fst β ob)
```

若 `x` 属于 `Lset β`，把 `β` 换成 `birth x` 后，它就会出现在严格低于 `stage x = sucV (birth x)` 的层。这与 `stage-earliest` 矛盾，从而给出 `BirthAt` 所需的非隶属。

```agda
    hn : ⟨ fst z ∈ fst (towerS β ob) ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥
    hn k = lift (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))))
```

`DefAt` 的层等式把它的满足命题认同为与 `𝒟ₒ (Lset β)` 的相等。`powS β ob` 的投影等式恰好给出这项相等，因此封装后的可定义幂集满足所需子句。

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

最后，`birth-mem` 把 `x` 放入 `Lset (sucV (birth x))`。先把候选序数换成诞生序数，再使用 `Lset-suc`，最后使用打包可定义幂集的投影等式，就把这条隶属搬运到第二个见证中。结合向外读式，这证明了在候选槽位被假设为序数时，`BirthAt` 精确描述诞生序数；它既不在内部添加序数性，也不给出规范的存在见证。

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

## 任意元数处的诸码，位于槽位所持的载体上

逐码识别式合并两个子句：第一个从码读取元数数码，第二个检查该码见证工作字母表上的一条公式。二者合起来说该码是某个元数处的真公式码。

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

向内读式以工作集 `A`、两个槽位、与 `A` 对齐的环境、元数 `k` 的公式、以及认同码槽与该公式键的等式为参数。它填充两个合取项。

```agda
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 ⟩
```

两个合取项由各自的向内读式填充：元数读法名指自然数与码，见证读式确认该公式在已对齐的字母表上。

```agda
  codeAnyAt-in {k = k} c w γ qw ψ qc =
    arityNumAtL-in c γ k (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc
```

向外读法恢复截断的码见证：某个元数与某条公式产生此键。截断数据保持在命题截断之内。

```agda
  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) =
```

证明消去元数读取为自然数与码的对，再把见证读法映入码层级的截断存在。

```agda
    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) })
```

见证读法的消去在正确元数处恢复公式与码等式，完成截断存在。

```agda
      (witnessAt-out A w c γ qw hw m z qz)
```

## 那个集合，一次外延

`CodesAt c w` 并不构造码集。它借助 `extAt` 描述已经占据槽位 `c` 的集合：一个元素属于该集合，当且仅当它是槽位 `w` 所持载体上某个有限元数公式的键。这样便在外延意义上把槽位取值确定为 `AllCodes A`，而隶属读式所用的每个公式见证仍处于命题截断之下。

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

码集的向外读法说：该槽位恰持有工作字母表的码集。证明沿两个方向作外延性。

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

对第一项包含，`codeAnyAt-out` 把描述槽位中的隶属读成「该元素是某条公式之键」的命题截断。`AllCodes-in` 恰把这项断言化为对固定元语言集合 `AllCodes A` 的隶属，并不选出某个特定解码。

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

为证明反向包含，`AllCodes A` 中的隶属只给出一个元数与一条公式的命题截断，并说明给定元素是该公式的键。逐码公式的满足本身是命题，所以证明可以在此处消去该截断并应用 `codeAnyAt-in`，但不会提取出一份指定的解码。

```agda
      (λ 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)))
```

反过来，设槽位 `c` 的取值等于 `AllCodes A`。要证明 `CodesAt`，只需给出外延公式要求的两条隶属蕴含：槽位中的成员满足逐码谓词，而满足该谓词的对象属于槽位。

```agda
  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) ⟩
```

对第一条蕴含，集合等式把槽位隶属化为 `AllCodes A` 中的隶属。后者只在命题截断下给出公式见证；由于目标是 `isCodeAnyAt` 的满足命题，可以把截断消去到这个目标中。

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

对反向蕴含，`codeAnyAt-out` 把满足关系读成「候选对象是某条公式之键」的命题截断。`AllCodes-in` 正用这条截断断言证明对象属于 `AllCodes A`，随后集合等式把结论搬回槽位 `c`。

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

## 层处的序，展开一次

在序数 `δ` 处，前章已经构造的 `orderAt δ` 比较 `Lset δ` 的成员。把该序搬到命名构造所需的小载体后，`stepAt δ` 据此在 `New δ`，即 `Lset (sucV δ)` 的成员上构造局部严格良序 `stepOrder δ`。

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

若 `δ ≡ δ'`，则 `δ` 处的 `Under` 比较可搬运到 `δ'` 处。依赖对的路径同时认同两份序数性证明；这是因为 `IsOrd` 是命题。因此，搬运后的比较不依赖于所选的序数性证书。

```agda
stepMoved : (δ δ' : V ℓ) (e : δ ≡ δ') (o : IsOrd δ) (o' : IsOrd δ') (x y : V ℓ)
          → Under δ (stepOrder δ o) x y → Under δ' (stepOrder δ' o') x y
stepMoved δ δ' e o o' x y =
  subst (λ p → Under (fst p) (stepOrder (fst p) (snd p)) x y)
    (Σ≡Prop isPropIsOrd {u = δ , o} {v = δ' , o'} e)
```

设可构造集合 `x` 的诞生序数属于序数 `α`。那么该诞生序数的后继要么属于 `α`，要么等于 `α`。由于 `x` 属于以该后继为指标的层，这两种情形都会把 `x` 放入 `Lset α`。

```agda
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 α ⟩
```

`suc∈or≡` 给出的两种情形完成了论证。若诞生序数的后继属于 `α`，单调性把 `birth-mem` 推到 `Lset α`；若该后继等于 `α`，沿等式搬运即可直接得到同一隶属。

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

现在固定环境序数 `α`。`Lset α` 的每个成员都有一个低于 `α` 的诞生序数，因此 `orderAt α` 的递归方程所需的较早层序恰在相应指标处可用。于是，我们可以把该方程直接表成两个成员的诞生层比较。

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

每个层成员可构造，由层的可构造性与沿隶属的传递性而来。

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

由于 `Lset α` 的每个成员 `a` 都可构造，它都有诞生序数。把这个序数记为 `bornOf a`；展开 `α` 处的序时，它将作为第一比较键。

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

事实 `bornOf a ∈ α` 有两项作用。它先确认该诞生序数可在展开 `orderAt α` 时充当较早指标；随后又使 `bornIn` 能从对象语言的诞生描述恢复 `a` 对环境层的隶属。

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

展开等式是本章的连接点。它说：`α` 处的序在 `a` 与 `b` 之间成立，恰当 `a` 的诞生序数严格低于 `b` 的诞生序数，或二者共享同一诞生序数且该诞生序数处的局部步进序把 `a` 置于 `b` 之下。

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

证明用 `orderAt-step` 展开一层隶属递归，再对其底层关系应用同余。因此，这个两分等式来自前章已经构造的序；此处既不重新构造也不重新证明该严格良序。

```agda
                       (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 α)
```

成员到载体的包装把每个层成员打包为载体元素，使公式环境能容纳它。

```agda
opaque
  memS : (α : V ℓ) (oα : IsOrd α) → Mem (Lset α) → S
  memS α oα a = fst a , memberL α oα a
```

第一投影等式确认包装保持底层集合。

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

诞生呈现把诞生序数连同从外围序数 `α` 运来的可构造性打包。

```agda
  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α
```

第一投影等式确认包装保持诞生序数。

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

诞生等式确认打包的诞生与打包成员的计算诞生一致。

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

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

步进公式类型是四槽公式族，以载体槽、表槽与两个比较槽为参数。

```agda
StpFo : Type (ℓ-suc ℓ)
StpFo = ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n
```

步进公式的向外充分性读式相对于序数载体 `d`、表 `f` 与两个被比较对象陈述。它对表的假设是：在 `d` 处记录的每个取值 `r` 都实现层关系 `IsRel d r`。由 `Stp` 的满足只能推出相应 `Under` 比较的命题截断。

```agda
StpOut StpIn : StpFo → Type (ℓ-suc ℓ)
StpOut Stp = ∀ {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 ... ∥₁`，所以它只给出局部比较的存在，而不选择规范见证。向内方向的输入不同：调用方给出一个特定取值 `r`、表在 `d` 处记录它的证据，以及 `r` 实现当地关系的证明。

```agda
           → ∥ Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od)
                 (fst (lookup u γ)) (fst (lookup v γ)) ∥₁
StpIn Stp = ∀ {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` 比较产出公式满足。

```agda
          → Under (fst (lookup d γ)) (stepOrder (fst (lookup d γ)) od)
              (fst (lookup u γ)) (fst (lookup v γ))
          → ⟨ γ ⊨ Stp d f u v ⟩
```

模块 `Ordered` 假设一条抽象步进公式及其两条读式。因此，下文给出的是诞生层优先规则的有条件翻译：它从同生比较的充分性推出整个层比较的充分性，却不在本章声称任何具体步进公式已经满足该接口。

```agda
module Ordered (Stp : StpFo) (stp-out : StpOut Stp) (stp-in : StpIn Stp) where
```

新绑定的四个对象是被比较集合 `u,v` 及其候选诞生序数 `du,dv`。前两项断言 `BirthAt du u` 与 `BirthAt dv v`；只有后续读式提供 `du`、`dv` 的序数性时，这两项才把候选者认同为相应诞生层。

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

接下来的两项要求两个候选诞生层都属于词项 `tb` 所指称的阶段。最后的析取复现诞生层优先规则：要么 `du ∈ dv`，要么 `dv ≡ du` 且外部给出的步进公式在这个共同载体处比较 `u` 与 `v`。这里没有断言 `u` 与 `v` 之间的集合隶属关系。

```agda
        ∧̇ ( (var zero ∈̇ tm4 tb)
          ∧̇ ( (var (suc zero) ∈̇ var zero)
            ∨̇ ( (var zero ≐ var (suc zero))
              ∧̇ Stp (suc zero) (sh4 f) (sh3 zero) (sh2 zero) ) ) ) ) )
```

`CondCore` 先以存在量词绑定两个被比较对象 `u` 与 `v`，对公式要求槽位 `z` 中的实参是二者的有序对。随后两个存在量词绑定它们的候选诞生层，再由 `OrdBody` 检查诞生层优先的比较。四个见证都位于存在公式的满足语义下，因此都经过命题截断。

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

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

为读取 `CondCore`，固定由 `tb` 指称的序数阶段及其上的一张表。`Values` 保证每个已记录取值都实现相应的局部关系；`Entries` 则只说阶段以下每个载体处都记录着某个取值。这正是后面两个方向所用的假设。

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

阶段序数被命名以便直接引用。

```agda
      α : V ℓ
      α = fst (⟦ tb ⟧ γ)
```

平移引理确认四槽改名保持阶段词项的指称。

```agda
      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 γ
```

对 `α` 以下的载体 `d`，`Entries` 只给出一项经过命题截断的表取值。这个辅助引理可以把该截断消去到任意命题 `P` 中：对恢复出的每个 `r`，`Values` 证明 `IsRel d r`，续至函数再用已记录的有序对及这份证明得到 `P`。

```agda
      value : (d : S) → ⟨ fst d ∈ α ⟩ → (P : hProp (ℓ-suc ℓ))
            → ((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)
```

具体地说，`ents d hd` 给出由取值 `r` 及其表条目组成的命题截断。这里只因 `P` 是 `hProp` 才能消去命题截断；随后 `vals` 提供续至函数所需的关系实现证明。该构造不会在这个命题之外选定一个表取值。

```agda
        (λ { (r , hr) → k r hr (vals d r hd hr) }) (ents d hd)
```

深层满足类型读取有序体在由两个比较对象及其诞生序数组成的四槽环境处的满足。

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

两条读式以相反方向使用 `CondCore` 的同一个定义方程。向外时，四个存在绑定被读成一对成员及两个候选诞生层；向内时，一项已有的 `Related` 比较提供这些绑定。只有同生分支会用到对 `Stp` 的两条假设读式。

```agda
    opaque
     unfolding CondCore
```

向外读式依次打开四层存在见证：先是被比较对象 `u,v`，再是候选诞生层 `du,dv`。每个见证都只能通过命题截断取得，而每次消去的目标都是命题 `Related α ...`。最内层数据随后交给数学比较论证。

```agda
     CondCore-out : ⟨ γ ⊨ CondCore z tb f ⟩ → ⟨ Related α (fst (lookup z γ)) ⟩
     CondCore-out = PT.rec (snd (Related α (fst (lookup z γ))))
       (λ { (u , hv) → PT.rec (snd (Related α (fst (lookup z γ))))
         (λ { (v , (hp , hdu)) → PT.rec (snd (Related α (fst (lookup z γ))))
           (λ { (du , hdv) → PT.rec (snd (Related α (fst (lookup z γ))))
```

局部名称 `Goal` 记录这样一个命题：槽位 `z` 中的实参满足元语言谓词 `Related α`。恢复出的四个见证给出有序对等式与 `OrdBody` 的满足，这两项被交给 `atDeep`；余下证明将把它们转化为该关联命题。

```agda
             (λ { (dv , hd) → atDeep u v du dv hp hd }) hdv }) hdu }) hv })
       where
       Goal : Type (ℓ-suc ℓ)
       Goal = ⟨ Related α (fst (lookup z γ)) ⟩
```

四个存在见证被消去到命题 `Related` 之后，向外证明取得两部分信息：`hp` 说明实参是 `u` 与 `v` 的编码有序对；深层记录则说明 `du,dv` 是环境层以下的候选诞生层，并满足诞生层优先的比较。这些见证只在命题目标中使用；证明并未选出规范的有序对或规范的诞生数据。

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

配对公式的充分性把槽位 `z` 中的集合认同为 `pr (fst u) (fst v)`。正是这条等式，而非 `u` 与 `v` 之间的等式，使证明能把目标改写为该表示对的 `Related α`，再分析其中的诞生层比较。

```agda
           (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
```

第一个诞生层在序数中的隶属沿环境移位搬运：诞生层的移位读法与非移位读法在底层集合上一致。

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

第二个诞生层由同一移位搬运，于是两个诞生层都属于该序数。

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

第一个诞生层是序数：它属于该序数，而序数的成员是序数。

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

第二个诞生层由同样论证是序数。

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

诞生公式的读取引理现在适用于第一个诞生层：在其序数性下，诞生公式的满足把被记录的层认同为第一个对象的真正诞生序数。

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

同样的读取适用于第二个诞生层与第二个对象。

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

现在可以把第一个对象视为 `Lset α` 的成员。其可构造性证据已由 `u` 携带；新增的事实是它属于环境层，而这由 `bornIn` 从「已经认出的诞生序数属于 `α`」推出。

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

第二个对象以同样方式打包。

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

打包成员 `a` 与 `u` 有相同的底层集合，但其可构造性证明来自层隶属。`birth-proof` 表达这份证据的证明无关性，说明从 `a` 算出的诞生层与从 `u` 算出的诞生层相同；再与 `qu` 复合，便把它认同为记录的层 `du`。

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

打包后的第二个对象的诞生序数与被记录的第二个诞生层一致。

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

此时只需证明元语言比较 `relOf (orderAt α oα) a c`。序表接口随后把这项比较送到命题：两个底层集合的编码有序对属于 `Related α`。这一步尚未选取任何对象语言关系集合。

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

`OrdBody` 编码的比较恰有 `orderAt` 一次展开所得的两支。若 `du ∈ dv`，同一视 `qa` 与 `qc` 把它改写成 `a` 与 `c` 的「诞生更早」分支；沿 `order-unfold` 搬运后，即得二者的层序比较。

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

在同生分支中，`OrdBody` 给出抽象公式 `Stp` 的满足。把公共诞生层的序数性与 `Values` 假设交给 `stp-out`，只能得到一项经过命题截断的 `Under` 比较。由于 `Related` 是命题，可以把这项截断消去到其中；该论证既不考察 `Stp` 如何取得表值，也不从中提取表值。

```agda
           (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)
```

给定记录的公共诞生层处的一项 `Under` 比较，证明还须把它与打包成员 `a` 所带的诞生层对齐。对齐之后，它给出 `order-unfold` 的同生分支；所得 `orderAt` 比较再由 `Related` 表示。

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

这次对齐使用两条载体序数之间的等式 `qa`。`stepMoved` 沿该等式搬运局部比较，并借助证明无关性认同两份序数性证明；这里既不使用公共序数的传递性，也不构造新的局部序。

```agda
               , stepMoved (fst du) (bornOf α oα a) (sym qa) odu
                   (mem-ord {A = α} oα (bornOf α oα a) (bornMem α oα a))
                   (fst u) (fst v) und)))
```

在向内方向，`Related α z` 包含一份序数性证明，以及命题截断下的如下数据：`Lset α` 的两个成员 `a,c`、说明 `z` 是二者编码有序对的等式，以及二者的 `Ordering` 比较。`Pairs` 恰为这份载荷取名，使它只能被消去到正在构造的满足命题中。

```agda
     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 ⟩ )) ∥₁
```

向内读式把 `Related` 的截断内容消去到 `CondCore` 的满足命题中。局部取得序数性证明与一对被表示的成员后，`atRel` 重建四个存在见证及诞生层优先比较；证明不会产出对表示成员的全局选择。

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

环境序数性 `oα` 已是整条读式的假设。此处的局部证明从层词项的取值中取出的是可构造性分量 `pα`，随后向表索取第一个成员诞生层处的一个取值。由于目标是满足命题，表值的仅仅存在可以消去到其中。

```agda
             → ⟨ 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 α ⟩
```

每个词项都在结构 `𝒮ʟ` 中解释，而该结构的元素由底层集合及其可构造性证据组成。因此，`⟦ tb ⟧ γ` 的第二投影给出 `isL α`；这是词项语义值的一部分，并非另一项满足假设。

```agda
         pα = snd (⟦ tb ⟧ γ)
```

现在局部给出 `CondCore` 的见证：`u,v` 把两个层成员封装为 `𝒮ʟ` 的元素，`du,dv` 则封装它们真正的诞生序数。它们只是这次命题证明所用的见证，并非从 `Related` 导出的规范选择。

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

`Lset α` 的每个成员，其真正诞生序数都低于 `α`。由于 `bornS` 的第一投影就是该序数，同一隶属陈述也适用于放入槽位 `du` 的值；对象语言子句读取的正是这个形式。

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

第二个成员的诞生层经同样搬运属于该序数。

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

第一个诞生层是序数，因为它落在该序数之内。

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

第二个诞生层由同样读取是序数。

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

展开已经构造好的层序，得到其两分的字典序规则：要么 `a` 的诞生严格早于 `c`，要么二者诞生层相同，且该公共诞生层处的局部 `stepOrder` 把 `a` 的底层集合排在 `c` 的底层集合之前。

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

该比较沿「两份序数性证明的同一视」搬运严格读法而得，因为序数性是命题，两份证明描述的是同一个序数。

```agda
         cmp = transport (order-unfold α oα a c)
           (strict α oα a c (subst (λ o' → ⟨ Ordering α o' a c ⟩)
             (isPropIsOrd α o oα) hord))
```

`Related` 所含的等式把实参认同为 `a` 与 `c` 的底层集合所成的有序对。`memS` 的第一投影等式把这两个端点改写为放入槽位 `u` 与 `v` 的值，从而恰好得到 `CondCore` 所需的配对子句。

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

为填入第一条 `BirthAt` 子句，向内读式给出其充分性引理所需的两项事实：`du` 是序数，且其底层集合恰是 `u` 的诞生序数。公式本身仍不断言序数性，也不选择最小层。

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

第二个诞生层的诞生公式在同一深环境中填充。

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

在同生分支中，`cmp` 给出一项 `Under` 比较，其载体是 `a` 的真正诞生层，两个端点是 `a,c` 的底层集合。但步进公式读在封装值 `du,u,v` 上，因此必须把载体与两个端点都搬到这些表示中。

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

两个端点的搬运使用 `memS` 的底层集合外显等式。载体的搬运使用 `bornS-fst` 与 `stepMoved`；后者的依赖路径还利用 `IsOrd` 是命题来认同两份序数性证明。这里不涉及传递性论证。

```agda
           (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)
```

`Entries` 在第一个诞生层处给出一个仅仅存在的表值 `r`，而 `Values` 证明任一这样的记录值都实现 `IsRel`。对每份局部载荷，`atValue` 插入两个成员及其两个诞生层，构造 `CondCore` 的满足。同生分支把该表值专门传给 `stp-in`；它不会成为全局选定的取值。

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

在 `OrdBody` 内，原环境之前增加了四个绑定，故层词项写成 `tm4 tb`。移位等式证明这个提升后的词项仍指称 `α`，于是把第一诞生层的已知隶属搬成对象语言子句所需的确切形式。

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

第二个诞生层经同一移位等式搬运。

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

余下的子句必须复现 `order-unfold` 给出的同一两支：诞生更早，或诞生相同后采用局部步进比较。辅助函数把这次分情形保持在满足命题内部，使见证与任何截断的表项都只在允许的命题目标中使用。

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

在诞生更早分支中，`bornS` 的外显等式把真正诞生层之间的元语言隶属改写为 `du` 与 `dv` 之间的隶属。所得证明进入对象语言析取的左支，而该析取的满足经过命题截断。

```agda
                 → ⟨ (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) ∣₁
```

在同生分支中，诞生层等式被改写为 `dv` 与 `du` 之间的等式。随后，向内充分性假设 `stp-in` 使用这个特定的记录值 `r`、它在表中的隶属、它的 `IsRel` 证明，以及搬运后的 `Under` 比较，填入局部步进公式。正是在这一方向上，证明手中有一个具体的局部表值。

```agda
           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) ) ∣₁
```

把这项两分翻译施于 `cmp`，便完成 `OrdBody` 的比较子句。它与两条诞生描述及两条低于 `α` 的界条件共同给出 `CondCore` 所需的深层记录，并未增加新的选择或序论断言。

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

对级组装消去第二个成员的截断存在：对与 `a` 关联的每个候选 `c`，局部组装产出核心子句的满足。

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

`Related` 的外层载荷给出一份序数性证明 `o`，以及 `Pairs o` 的命题截断。由于 `CondCore` 的满足是命题，`atOrd` 可以消去这项截断，并把每个表示对交给 `atPairs`。对特定序数性证明的无关性已在更早处使用：借助 `isPropIsOrd`，把 `o` 与环境证明 `oα` 认同。

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

该规格把核心子句的满足与编码对的关联等同为命题路径，双向成立。

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

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

当层与表已经占据环境中的变元槽位时，使用 `Cond` 这一形式。新增的第零槽留给待检验的编码有序对，原有的层与表索引则越过它而提升。因此，`Cond` 不为层引入见证，而是引用外围语境已经提供的层。

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

`Cond₀ B F` 是分离所需的常元层形式。它唯一的存在绑定给出一个表值，等式子句把该值固定为常元 `F`；层本身已经是常元词项 `B`。余下的自由槽保存待检验的编码有序对。后续规格证明这一形式与 `Cond` 描述同一个 `Related` 比较，而这仍相对于给定的 `StpOut` 与 `StpIn`；两种形式都不构造层序本身。

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

变元形式检验一个可能的有序对 `z`，而层与序表仍留在周围环境中。假设该层是序数，且序表具有给定的取值读式与表项读式，其充分性等式便把 `Cond` 的满足关系与宿主层的类 `Related` 对应起来。因此，这条公式描述的是已经构造好的层序比较，并不构造新的序。

```agda
  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 =
```

把 `z` 加到环境首部后，原有的每个槽位都向后移动一位。因此，核心在零号槽位读取 `z`，经 `var (suc b)` 读取层，并经 `suc f` 读取序表。作出这些平移后，`CondCore` 的一般等式直接给出所需的变元形式等式。

```agda
    CondCore-spec zero (var (suc b)) (suc f) (z ∷ γ) ob vals ents
```

作分离时，周围环境只含候选者 `z`，所以常元形式必须绑定它所查阅的序表。若一个被绑定的元素 `c` 的底层集合等于固定序表 `F` 的底层集合，并且以 `c` 占据序表槽位时核心比较成立，那么 `c` 就是合适的见证。辅助命题 `Held c` 恰好合并这两项事实；`c` 是序表的代表，并非公式码。

```agda
  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 ∷ []` 中，零号槽位是被绑定的序表代表，一号槽位是可能的有序对，而层由常元词项 `con B` 给出。这样的安排使同一个核心也能表达常元情形；向外读取时，必须把 `F` 的序表读式转移给与它外延相等的代表 `c`。

```agda
             × ⟨ (c ∷ z ∷ []) ⊨ CondCore (suc zero) (con B) zero ⟩
```

向外方向从被绑定序表的命题截断存在见证出发。由于 `Related` 本身是命题，可以把这层命题截断消去到该目标中。辅助定义 `atHeld` 只在局部使用一个临时代表 `c` 及其两项 `Held` 事实；没有任何代表逸出这段证明，所以该论证既不产生规范见证，也不产生选择函数。

```agda
    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)) =
```

等式 `qc` 使两条序表读式可以在被绑定的代表与 `F` 之间转换，但方向相反。先把假设属于 `c` 的表项运输到 `F`，再由 `vals` 判定其取值实现该层关系。反过来，`ents` 给出 `F` 中一个经过命题截断的表项，而在这层截断之下作映射，把该表项运回 `c`。

```agda
        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 })
```

这些经过运输的读式正是向外读取核心比较所需的假设。把它们用于 `hc`，便得到关于 `z` 的 `Related` 事实。在整个转换中，表项见证始终处于命题截断之下；这已经足够，因为核心满足关系与所得关系断言都是命题。

```agda
            (ents x hx))
          hc
```

向内方向已经给定序表 `F`，所以可直接用它作存在见证，而它与常元序表的等式就是自反性。核心的向内读式随后把给定的 `Related` 事实化为以 `F` 占据序表槽位时的满足证明。这里是在命题截断内部构造见证，并非从截断信息中提取见证，也没有断言序表代表是唯一选定的。

```agda
    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₀ B F` 的满足命题与 `Related (fst B) (fst z)` 之间的路径。因此，在同样的序数性、取值与表项假设下，常元公式具有与变元形式完全相同的数学读法。该等式涉及命题值含义，并不在语法上等同两条公式，也不为序表选择一个特出的呈现。

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

通用序表构造现在可以在层与序表占据变元槽位时使用 `Cond`，并在二者作为固定常元时使用 `Cond₀`。由此得到的关系对象表示先前已构造的严格良序 `orderAt` 的底层比较；这里没有重新构造良序。所有结果仍然相对于抽象步进公式的 `StpOut` 与 `StpIn`。随后，`InternalWellOrder` 为具体步进提供这两条读式，从而消去最后这个参数。

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

## 小结

本章在对象语言中描述了先前所构造层序的底层关系。`BirthAt` 只有在外部给出序数性假设时才认定诞生序数，`CodesAt` 只在外延意义上确定随载体变化的码集，而 `CondCore` 只有相对于 `StpOut`、`StpIn`、`Values` 与 `Entries` 才与诞生层优先的比较相符。存在、解码、表值与 `Under` 的见证始终留在命题截断之内。下一章将给出具体步进公式及其两条读式。