---
title: "L 内部的极限层序"
module: L.Choice.LimitStageOrder
lang: zh
site: "Bedrock"
description: "L 内部的极限层序"
stage: "典范良序与选择公理"
reading_order: 81
canonical: https://bedrock.institute/zh/L.Choice.LimitStageOrder.html
html: L.Choice.LimitStageOrder.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/LimitStageOrder.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Full, L.Recursion, L.Coding.Model, L.Coding.Expressions, L.Coding.HierarchySequence, L.Hierarchy, L.Choice.FiniteStageOrders, L.Choice.NameComparison, L.WellOrder.Base, FOL.Absoluteness]
routes: [choice-completion]
translations: [https://bedrock.institute/en/L.Choice.LimitStageOrder.md, https://bedrock.institute/ja/L.Choice.LimitStageOrder.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 内部的极限层序

`Lset ω` 的诸成员在外部已经带有严格良序。本章的问题是：怎样让 `L`内部的公式使用这个比较？答案要依次经过三种彼此有别的形态：元层面的比较、对象语言中对该比较的描述，以及在有穷层描述已经给出后实现该关系的可构造集合。

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

本章的全部构造都相对于层级 `ℓ-suc ℓ` 上一个显式的排中律实例。前文已用这条假设取得极限层成员首次出现的最小有穷层，本章还把同一实例传给所用的分离结果与取界结果。它在这些构造需要时判定命题，却不为任意集合族提供选择函数。

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

固定宇宙层级 `ℓ` 与刚才说明的排中律实例。此时后文的内部关系仍是条件式构造：只有给出描述有穷层序的公式及其两个语义方向后，它才在模块 `Described`
内部得到定义。下一章会提供这个实例，并把 `codeOrder` 公开给后续构造使用。

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

对象语言必须描述比较，同时不把语法与它在层级中的意义混为一谈。公式使用变元、常元、隶属、联结词与量词；由于常元域就是可构造载体，一个常元已经指称某个确定的可构造集合。后文所需的两个基本检验由编码引理提供。有序对的等式决定两个分量，数码编码也是单射的，而 `#mono` 把 `k < m` 变为 `# k` 属于
`# m`。因此，集合论隶属能够忠实承载有穷指标的严格比较。

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

这里采用的结构是可构造宇宙。其载体元素把一个集合与可构造性证据打包在一起，而传递性又为该集合的每个成员提供同类证据。这样，普通层级隶属中的见证便能进入对象语言的环境。特别地，`finiteStage n` 是 `Lset (# n)`，极限层则是
`Lset ω`；关于数码与序数的事实使这些指标始终区别于它们所指名的层。经过包装的层与常元 `ωʟ` 随后使公式能够从结构内部谈论这条层级。

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

三座桥把语义上的比较变成 `L` 的一个集合。首先，`smallDom` 把一个小族放进同一个可构造集合，却不声称这个界恰好等于该族的像。其次，分离从这样的界中精确取出满足一元公式的元素。最后，描述有序对、关系隶属与层级序列的编码公式都带有充分性定律，把满足关系翻译成相应的集合事实。这三件工具把寻找公共定义域与在该域上陈述精确关系这两个问题分开处理。

```agda
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; prAtL; prAtL-adequate; prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( numL )
open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt )
```

要表示的比较在外部已经定义。到了后继层，`before (suc n)` 用
`before n` 排列更早的点，并在最先分歧处比较 `finiteStage n`
的两个子集。`precedes R A x y` 的见证属于 `A`，属于 `y` 而不属于 `x`，并记录 `x` 与 `y` 在每个更早点处一致；该见证的存在带有命题截断。类型
`Limit` 打包 `Lset ω` 的成员，而它们的最小出现层号构成
`limitOrder` 的主键；只有层号相同才调用相应的 `before` 比较。所得关系集的两个表示方向，形状正好符合 `Adequacy.Keys` 的要求。

```agda
open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines )
open import L.Choice.FiniteStageOrders {ℓ} lem
  using ( Limit; level; level-in; levelData; limitOrder
        ; before; precedes; Agrees; Witness; finiteStage )
open import L.Choice.NameComparison {ℓ} lem using ( module Adequacy )
```

`limitOrder` 以 `SWO` 束的形式给出：除比较本身外，还包含三歧性、非自反性、传递性与良基性。内部化论证不会重新证明这些定律。后文只为一个特定目的使用前三条：从对象语言析取读回时只能先得到带命题截断的严格比较，三歧性指出可能的分支，非自反性与传递性则排除不相容的分支。

```agda
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
```

极限比较具有后文所需的字典序形状。第一支说第一个成员的层号更小；第二支说双方层号相同，并在共同层号处用 `before` 比较底层集合。自然数的三歧分析第一把键，`subst2` 则在等式识别出编码层号或端点时运输二元关系。与之相伴的
`Lift` 与 `lower` 只处理宇宙层级，其中 `lower` 对应命题降级；它们都不消除命题截断。

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

对象语言的存在量词与析取分别解释为带命题截断的存在与分支选择。因此，只有当目标是命题时才能使用其中的见证，例如不可能性、层级集合的等式或另一项命题截断。这不表示本章每个存在类型都带命题截断：当类型要求显式数据时，打包后的载体元素与公共界之类的数据仍然可见。从命题截断恢复严格比较也不是消除命题截断的一般原则；它专门依赖 `limitOrder` 的三歧性与序定律。

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

为了应用取界引理，`Lset ω` 的成员需要一个小索引类型。纤维
`⟪ Lset ω ⟫` 提供这种指标，而 `∈-asFiber` 把给定的成员证明变成一个指标，其像就是原来的成员。因此，两个这种纤维的积索引了极限层成员的所有有序对。后文的 `pairsBound` 会包含这些对中的每一个；精确性要到分离以后才得到。

```agda
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; ω )
```

现在有三种隶属记号，各自承担不同角色。对载体元素，`x ∈ˢ y` 是可构造结构中取命题值的隶属；对底层的层级集合，`fst x ∈ fst y` 使用外围隶属；在公式内部，`_∈̇_`
只是句法上的隶属原子。下一步引入的满足关系把第三种形式解释成前两种。分清这些层次，就不会把描述一个序的公式误当成「其实现集合在内部已被证明为良序」。

```agda
open hPropStructure 𝒮ʟ
```

判断 `_⊨_` 是把外围层级结构限制到可构造类后得到的内层满足关系。它的载体由集合及其可构造性证据组成，因此常元与量化取值都遍及可构造对象。原子隶属通过第一投影解释，而传递性保证可构造界的成员仍能包装成载体元素。于是，满足关系在对象语言公式与其底层集合的普通隶属事实之间给出精确的桥梁。

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

把 `limitOrder` 携带的比较记作 `_≺ˡ_`。它先按最小出现层号比较两个极限层成员；层号相同，再按共同有穷层中的最先分歧比较。接下来的目标是条件式的：假设有一条对象语言公式在预定定义域上表示每个有穷层的 `before` 关系，便在
`Described` 内部构造集合 `codeOrder`，使 `u` 与 `v` 的有序对属于它当且仅当 `u ≺ˡ v`。下一章会给出所需的有穷层公式，从而得到可实际使用的实例。

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

约束变元用 de Bruijn 位置表示。打开两个嵌套的绑定后，外围环境中的每个位置都要越过两个新条目，`sh2` 正好记录这次移位。最先分歧公式先绑定候选分歧点、再绑定其下的点时会用到它；不同层号分支绑定两个层号数码时也会用到它。移位只改变既有自由变元的寻址方式，不改变该变元所指称的集合或关系。

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

环境包含的是可构造载体的元素，而不是未包装的层级集合。因此，对自然数 `k`，`towerS k` 把层 `Lset (# k)` 与其可构造性证据打包在一起。该定义保持不透明，使后续证明通过公开的投影等式使用它，而不展开层级构造。不透明性只控制归约，不会增加任何数学假设。

```agda
opaque
  towerS : ℕ → S
  towerS k = LsetS (# k) (numeral-ord k)
```

等式 `towerS-fst k` 把这个载体元素的底层集合认同为 `Lset (# k)`。它连接同一层的两种视角：公式接收包装后的元素 `towerS k`，外部层级引理则陈述底层层级集合中的隶属。后续证明在这两种视角之间运输成员事实时，都会经过这条等式。

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

指标自身还需要一个单独的载体元素。`numS k` 把数码 `# k` 与其可构造性证据打包。把 `numS k` 与 `towerS k` 分开可避免一种常见混淆：前者指称序数指标，后者指称由它索引的可构造层。`LevelAt` 将通过层级序列的描述把这两个对象联系起来。

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

投影等式 `numS-fst k` 从包装后的数码中恢复 `# k`。它与
`towerS-fst k` 配合，使同一个自然数能够协调地承担两种角色：一方面作为环境中的层号取值，另一方面作为见证所展示之层的指标。这两条等式为对象语言取值与外部的数码、层事实之间的运输提供依据。

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

设环境位置 `i` 的底层集合是 `# j`。引理 `towerGraph` 把
`towerS j` 放进新位置，并证明 `LsetGraphAt` 联系这两个位置。它的内容恰是层级序列的规格：与数码 `# j` 对应的取值是层 `Lset (# j)`。因此，同一条引理既为真实层号处的存在性提供塔见证，也为用该层检验最小性提供塔见证。

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

## 层号，在内部说出

公式 `LevelAt b x` 开始刻画第一把键。它先要求位置 `b` 的取值属于 `ω`，因而可解码为数码；随后要求存在一个由 `LsetGraphAt` 在该数码处描述的取值，并要求位置 `x` 的取值属于所得的层。这些子句说明 `b` 是 `x` 的一个出现层；余下的子句将说明它还是最小的出现层。

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

最小性遍及候选数码 `b` 的每个成员 `u`，而不只检查它的直接前驱。对每个在这样的`u` 处被描述出来的层，位置 `x` 的取值都不得属于该层。由于 `# k` 的成员恰是更小的数码，候选 `b = # k` 因而排除了从 `0` 到 `k-1` 的所有层。两个嵌套绑定解释了 `x` 的移位。语义上，这些全称子句是函数类型；附近对数码成员的命题截断解码只在命题目标下使用，并不会选定一个更小指标。

```agda
                     ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) )
```

为证明 `LevelAt` 的两个读法，固定一个真实的极限层成员 `a`、一个自然数 `k`，以及把 `k` 认同为其最小出现层号的等式 `qk : level a ≡ k`。把
`levelData a` 的正面分量沿 `qk` 运输，便得到 `aIn`：`a` 的底层集合属于 `Lset (# k)`。负面分量则说，对任何 `m < k`，它不可能属于
`Lset (# m)`。这恰是证明公式识别真实层号所需的存在性与最小性事实；随后还会用它们证明公式识别出的任何层号都等于 `# k`。

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

`levelData a` 的第二个投影给出后续论证所需的最小性。若 `a` 的底层集合已经属于 `Lset (# m)`，且 `m < k`，等式 `qk`
就把后一条不等式化为 `m < level a`，与该最小性矛盾。`levelData` 所需的比较位于更高一层宇宙，因此这里用
`lift` 包装它。这只是宇宙层级的调整，不涉及命题截断。

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

`LevelAt` 的两条读式都在任意环境的任意位置 `b` 与 `x` 上证明。为了向外读取公式，先为存在量词所隐藏的信息命名会很方便：一个载体元素`c` 在 `b` 的值处满足层级图，并且 `x` 的值属于 `c` 的底层集合。私有类型
`Body` 恰好就是施加命题截断之前的这份见证数据。

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

向内读取时，设 `b` 表示数码 `# k`，而 `x` 表示 `a` 的底层集合。结论包含 `LevelAt` 的三个部分：`b` 的值属于 `ω`；`b` 处有一个层级取值包含 `x` 的值；由 `b` 的成员所索引的每个层级取值都不包含它。证明把这三部分分别命名为 `hω`、`hex` 与 `hmin`，从而分开建立存在性与最小性。

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

第一部分来自每个数码都属于 `ω` 这一基本事实。等式 `qb` 把位置 `b`所存的值与 `# k` 认同；沿该等式的反向运输 `#∈ω k`，便得到所需的成员证明。这次运输把关于显式数码的事实接到关于环境位置的同一事实上。

```agda
      hω = subst (λ u → ⟨ u ∈ ω ⟩) (sym qb) (#∈ω k)
```

对于存在部分，取包装后的有穷层 `towerS k` 为见证。引理
`towerGraph` 借助 `qb` 证明这个见证就是 `b` 处的层级取值。由 `towerS-fst k`，其底层集合是 `Lset (# k)`，所以只需再用 `qx` 对齐端点，即可应用已知的成员事实 `aIn`。

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

事实 `aIn` 已经说明 `a` 的底层集合属于 `Lset (# k)`。沿
`qx` 的反向运输，把其中的成员从 `a` 的底层集合改成 `x` 处的值。再与前面的投影运输合并，便证明了 `hm`，并在命题截断之下完成存在见证。

```agda
          (subst (λ u → ⟨ u ∈ Lset (# k) ⟩) (sym qx) aIn)
```

这个有界全称表达全局最小性。给定 `b` 的值中的成员 `u`、一个在 `u` 处满足层级图的候选 `c`，以及一份声称 `x` 的值属于 `c` 的证明，目标是导出矛盾。用 `qb` 把 `u` 的成员身份改写到 `# k` 后，`∈#-elim` 在命题截断之下给出某个 `m < k`，使 `u` 等于 `# m`。由于目标是空类型，因而是命题，可以消去这个命题截断。所得矛盾只为匹配对象语言否定所在的宇宙层级而被抬升。

```agda
      hmin : ⟨ γ ⊨ ∀̇∈ (var b) (∀̇ ( LsetGraphAt zero (suc zero)
                                  ⇒̇ ¬̇ (var (sh2 x) ∈̇ var zero) )) ⟩
      hmin u u∈ c hg hmem = lift (PT.rec Empty.isProp⊥ step
        (∈#-elim k (fst u) (subst (λ w → ⟨ fst u ∈ w ⟩) qb u∈)))
        where
```

固定一次显式解码，得到 `m < k` 与 `fst u ≡ # m`。图证明
`hg` 不仅说明 `c` 是某个可能的见证；把数码 `# m` 的序数证明运输过去后，`Lset-only` 会把 `c` 的底层集合认同为
`Lset (fst u)`。因此，公式不能在存在见证后藏入任意集合，层级图会确定相应的有穷层。

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

现在沿三条认同运输那份假设的成员证明。先由 `qc` 把 `x` 的值放入
`Lset (fst u)`，再由 `qx` 把该值替换为 `a` 的底层集合，最后由 `qu` 把 `fst u` 替换为 `# m`。所得结论是
`fst a ∈ Lset (# m)`；当 `m < k` 时，这正是 `aMin` 所排除的陈述。因此，没有由小于 `k` 的数码索引的有穷层包含 `a`。

```agda
            (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 b x` 成立，并仍把 `x` 的值认同为固定成员`a` 的底层集合。目标是证明 `b` 处的候选正是真实数码 `# k`。候选属于 `ω` 只能在命题截断之下揭示其自然数索引。目标是累积层级中的一条等式，而 `setIsSet` 表明这个等式类型是命题，因此可以把截断的数码数据消去到其中。

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

先排除解码所得索引 `m` 高于真实层号的情形，即假设 `k < m`，且 `b` 的值是
`# m`。由 `#mono`，`# k` 属于 `# m`；于是包装
`numS k` 与 `towerS k` 让我们能在真正的有穷层
`Lset (# k)` 处使用 `LevelAt` 的最小性子句。该子句说 `x` 的值不在那里，与 `aIn` 矛盾。它返回抬升后的矛盾，`lower` 只移除这个宇宙抬升；这是命题降级，而不是命题截断。

```agda
      notAbove : (m : ℕ) → fst (lookup b γ) ≡ # m → k < m → Empty.⊥
      notAbove m qb hk = lower (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))
```

传给该最小性子句的最后一个实参，正是它即将反驳的正面成员证明。从
`aIn` 出发，沿 `qx` 的反向把 `a` 的底层集合替换成 `x` 的值，再沿 `towerS-fst k` 的反向把 `Lset (# k)` 替换成其载体包装的底层集合。这样，公式与外部的最小层号论证便在谈论同一个有穷层中的同一个成员。

```agda
        (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) (sym (towerS-fst k))
          (subst (λ w → ⟨ w ∈ Lset (# k) ⟩) (sym qx) aIn)))
```

再排除解码所得索引低于真实层号的情形。若 `m < k`，`LevelAt` 的存在部分就在命题截断之下给出一个载体 `c`：它在 `b` 处满足层级图，并包含 `x` 的值。这恰是 `Body` 所命名的数据。由于目标是导出矛盾，可以把命题截断消去到空类型；每个显式见证都将迫使 `a` 已在第 `m` 个有穷层出现。

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

对于这样的见证，`Lset-only` 先把 `c` 的底层集合认同为由 `b` 的值索引的层级阶段。它所需的序数前提来自 `numeral-ord m`，并沿「`b` 的值是 `# m`」这条等式运输。再把所得等式与 `cong Lset qb` 复合，便得到具体认同 `fst c ≡ Lset (# m)`。

```agda
          where
          qc : fst c ≡ Lset (# m)
          qc = Lset-only zero (suc b) (c ∷ γ) hg
                 (subst IsOrd (sym qb) (numeral-ord m))
             ∙ cong Lset qb
```

现在可以在具体的有穷层读取见证中保存的成员事实。沿 `qc` 运输后，它变成 `x` 的值属于 `Lset (# m)`；再沿 `qx` 运输，该值变成 `a`的底层集合。因此 `a` 已在第 `m` 个有穷层出现；结合 `m < k`，这与
`aMin` 矛盾。故候选索引不可能低于真实层号。

```agda
          inStage : ⟨ fst a ∈ Lset (# m) ⟩
          inStage = subst (λ w → ⟨ w ∈ Lset (# m) ⟩) qx
            (subst (λ w → ⟨ fst (lookup x γ) ∈ w ⟩) qc hmem)
```

还需认同从 `ω` 的成员身份中解码出的数码。一份显式解码数据包含`j : Lift ℕ`，以及从 `# (lower j)` 到 `b` 处之值的等式。反转该等式便得到 `qb`。一旦自然数比较证明 `lower j ≡ k`，对这条等式应用数码映射并作复合，就得到所需结论 `fst (lookup b γ) ≡ # k`。

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

自然数的三歧性恰好给出所需等式。`lower j < k` 的情形与
`notBelow` 矛盾，`k < lower j` 的情形与 `notAbove` 矛盾；相等情形则原样返回其证明。因此，两条读式在真值层面互相对应：真实的最小有穷层满足 `LevelAt`，而该公式为固定成员 `a` 报告的任何候选都必是它的真实层号。

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

## 最先的分歧，在内部说出

要用公式比较集合，必须先把可构造载体的外部成员表示成语义载体 `S` 的元素。若 `A : S` 且 `z` 属于它的底层集合，可构造性的传递性就会把 `A` 中保存的证书化为 `z` 可构造的证书。`memS` 把 `z` 与这份继承来的证明包装起来。它构造的是依值载体的一个元素，不是集合论的有序对。

```agda
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` 说明这次包装保留了正在讨论的集合：`memS A z h` 的底层集合就是 `z`。该等式由自反性成立，但把它显式写成引理后，后续运输便能在量化所得的载体元素与它所表示的外部集合之间往返，而无须展开包装。

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

`PrecedesAt` 相对于已存于 `r` 的关系和已存于 `A` 的载体，表达一步最先分歧比较。对于 `x` 与 `y` 处的集合，它要求存在载体成员 `z`，使 `z` 属于`y` 而不属于 `x`。这个方向决定比较结果：在作出裁决的点上，右侧集合的成员值为一，左侧集合的成员值为零，所以 `x` 先于 `y`。

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

这个见证还必须是关系 `r` 所判定的最先分歧点。对载体 `A` 中的每个 `w`，若该关系把 `w` 排在 `z` 之前，则 `w` 属于 `x` 与属于 `y` 必须双向一致。公式通过 `appAt` 查阅关系；在语义上，这询问由 `w` 与 `z` 组成的集合论有序对是否属于存放在 `r` 的关系集。约束 `z` 的存在量词与约束 `w` 的全称量词，正好说明旧变量为何要移过两个位置。

```agda
        ∧̇ ∀̇∈ (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))) ) ) ) ) )
```

模块 `Precedes` 准确列出读取这条公式所需的数据。除四个位置及其环境外，它还固定一个元层关系 `R`。定律 `Rrep` 把集合论有序对属于 `r`处关系集的事实读成一个 `R` 事实，`Rfill` 则把这种事实写回成员关系。两条定律只需处理可构造端点，因为每个量化端点本来就在 `S` 中，而外部的载体成员可由 `memS` 包装。这里不假设 `R` 满足任何序公理；公式只表示一步比较的定义，不依赖后来对某个具体关系为良序的证明。

```agda
module Precedes {n : ℕ} (r A x y : Fin n) (γ : S ^ n)
                (R : V ℓ → V ℓ → hProp (ℓ-suc ℓ))
                (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) ⟩
```

先固定载体。关于早于分歧点之元素的每个断言，都由环境中 `A` 处取值所指的可构造集合限定，因此比较不会越出基底关系所作用的那一层。

```agda
                       → ⟨ pr (fst u) (fst v) ∈ fst (lookup r γ) ⟩)
                where
  private
    Aʟ : S
    Aʟ = lookup A γ
```

用 `xv` 表示环境中 `x` 处取值所指的集合。这样便能直接陈述左侧集合中的隶属，而不必在每个子句中重复环境查找。

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

同样，`yv` 表示环境中 `y` 处取值所给的集合。这两个名称的次序很重要，因为首个分歧点属于右侧集合而不属于左侧集合。

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

在首个分歧点之前，两个集合必须对隶属给出相同答案。`Both w` 精确记录这一等价：`w` 属于 `xv` 蕴含它属于 `yv`，反向亦然。

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

对候选分歧见证 `z`，`Agreeing z` 考察载体中被编码基底关系排在 `z` 之前的每个 `w`。原子 `appAt r w z` 表示关系集含有 `w` 与 `z` 的有序对；在此前提下，`xv` 与 `yv` 必须在 `w` 处一致。

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

见证本身必须属于载体和 `yv`，但不属于 `xv`；载体中每个按基底关系更早的成员都必须满足一致条件。因此这个方向表示 `xv` 先于 `yv`。这里并未假设所给基底关系满足任何序律，所以只有当该关系确实是序时，才能称此见证为「最早」分歧。

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

要把公式向外读，就把它的命题截断存在消去到命题 `precedes R A xv yv`。只需把每个给出的模型见证变成宿主层定义的见证，因为目标也只保留其命题截断。

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

`z` 的底层集给出宿主层见证，前三个分量已经给出它的载体隶属与有向分歧。剩下的任务是在任意宿主层元素 `w` 被排在它之前时证明两边一致。

```agda
    atZ (z , (z∈A , (z∈y , (z∉x , hag)))) =
      ∣ fst z , (z∈A , (z∈y , ((λ h → lower (z∉x h)) , 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)
```

由于 `w` 属于可构造载体，它继承可构造性，因而可打包为模型元素 `wS`。其投影等式把原来的载体隶属证明搬运成对象语言有界子句所需的形式。

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

当前前提在宿主层表示 `R w z`。把 `w` 与 `wS` 对齐后，`Rfill` 将这个事实写成有序对属于关系集，这恰是建立应用原子所需的信息。

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

`appAt` 的充分性把这个有序对隶属陈述变成在由 `wS` 与 `z` 延拓的环境中的满足。现在即可应用对象语言中的一致假设。

```agda
          (sym (appAt-adequate (sh2 r) zero (suc zero) (wS ∷ z ∷ γ))) hp
```

反向从 `precedes` 中的命题截断见证开始。由于 `PrecedesAt` 的满足本身是命题，可以消去该截断，并把每个宿主层见证转成对象语言的存在见证。

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

展开宿主层见证 `z`，连同它的载体隶属、右侧隶属、左侧排除以及在更早点处的一致。它属于载体，因而具有可构造性，所以 `zS` 可以充当公式的量化见证。

```agda
        → ⟨ γ ⊨ 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
```

投影 `fst zS` 等于原来的 `z`。沿此等式搬运可知，打包后的见证仍属于载体，所以打包只改变它的呈现，不改变其数学作用。

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

同一投影等式也搬运 `yv` 中的隶属和 `xv` 中的非隶属。还需把公式中的关系前提读回 `R`，才能使用宿主层的一致假设。

```agda
      z∈y' : ⟨ fst zS ∈ yv ⟩
      z∈y' = subst (λ u → ⟨ u ∈ yv ⟩) (sym qz) z∈y
      z∉x' : ⟨ fst zS ∈ xv ⟩ → Lift {j = ℓ-suc ℓ} Empty.⊥
      z∉x' h = lift (z∉x (subst (λ u → ⟨ u ∈ xv ⟩) qz h))
      hag : Agreeing zS
```

给定载体中的模型元素 `w`，`appAt` 的充分性先把满足读成 `w` 与 `zS` 的有序对属于编码关系。这正是向外证明中所用转换的反向。

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

现在 `Rrep` 把关系集隶属读回 `R (fst w) zS`；再把第二个端点从 `fst zS` 搬运到 `z`，便得到原一致证明所需的前提，从而取得 `Both` 中的两条隶属蕴含。

```agda
        hR = subst (λ u → ⟨ R (fst w) u ⟩) qz (Rrep w zS hp)
```

## 那个序，接合起来

元素 `a : Limit` 携带其底层集属于 `Lset ω` 的证明。属于这个可构造层便给出所需的 `isL` 证据，使同一个底层集可作为模型元素 `limitEl a`。

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

打包并不改变集合：按定义投影 `limitEl a` 就得到 `fst a`。这个等式随后会把模型内构造的有序对与表示定理中使用的外围有序对对齐。

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

要把一条关系放入 `L`，相关的两个端点必须由一个本身也是模型元素的有序对表示。`prS` 为任意两个可构造端点给出这个内部有序对。

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

`prS` 的投影律把其底层集认同为两个底层端点的外围有序对。因此，内部配对构造与外部关系隶属谈论的是同一个集合。

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

在分离选出满足比较的有序对之前，所有候选对需要一个集合大小的共同界。先用小纤维呈现 `Lset ω` 的成员，把每个呈现出的成员打包为可构造元素，再用两个小纤维的积为有序对编索引。

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

每个呈现索引确实指向 `Lset ω` 的一个成员。隶属桥把呈现事实变成通常的隶属，而属于该层又给出 `ixL` 打包所需的可构造性证明。

```agda
    (∈∈ₛ {a = ⟪ Lset ω ⟫↪ m} {b = Lset ω} .snd (∈ₛ⟪ Lset ω ⟫↪ m))
```

把 `smallDom` 用于这个小积，得到一个含有所有内部构造有序对的可构造集合。它只是共同界，可以含有额外对象；精确的比较关系要靠在其中施行分离获得。

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

对任意 `u,v : Limit`，它们的底层集在 `Lset ω` 的小纤维中都有呈现索引。由这些索引形成的有序对属于共同界，再沿投影等式搬运，就得到外围有序对 `pr (fst u) (fst v)` 的隶属。

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

两条纤维见证恰好恢复上面使用的呈现索引，并附带把所呈现成员分别认同为 `fst u` 与 `fst v` 的等式。正因这些等式，小呈现才足以覆盖每个实际的极限层端点。

```agda
    fu = ∈-asFiber {a = fst u} {b = Lset ω} (snd u)
    fv = ∈-asFiber {a = fst v} {b = Lset ω} (snd v)
```

从公式读取时，有时只能得到极限严格比较的命题截断。`strictLimit` 先使用已经证明的严格良序 `limitOrder` 的三歧性来恢复比较；若三歧性给出 `a ≺ˡ b`，就无需再作任何选择。

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

在已有截断的正向比较时，三歧性的另外两种情形不可能成立。若 `a = b`，搬运会给出自比较；若 `b ≺ˡ a`，它与隐藏的正向比较经传递性也会给出自比较。非自反性反驳这两个命题，因此这里只把命题截断消去到矛盾中。

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

`level a` 的定义性质把 `fst a` 放在 `finiteStage (level a)` 中。等式 `level a ≡ k` 把这一隶属搬运到 `finiteStage k`，恰好给出调用有限层比较时所需的层边界。

```agda
levelStage : (a : Limit) (k : ℕ) → level a ≡ k → ⟨ fst a ∈ finiteStage k ⟩
levelStage a k q = subst (λ j → ⟨ fst a ∈ Lset (# j) ⟩) q (level-in a)
```

`Described` 是一个条件式框架。它接收一条用来描述 `before m` 的公式 `BeforeAt`，以及一个向内方向；只有当 `b` 处的取值表示 `# m`，且第一个端点属于 `finiteStage m` 时，才能使用这个方向。

```agda
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
               → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩
```

向内假设还要求第二个端点属于同一有限层，并要求实际比较 `before m x y`；由这些数据，它产出 `BeforeAt` 的满足。因此，这个框架既不构造有限层关系，也不推出它的序律。

```agda
               → ⟨ fst (lookup y γ) ∈ finiteStage 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
```

向外假设具有相同的数码与层边界，并把满足读回 `before m x y`。只有同时满足两个方向的公式才能实例化这个框架；实际的 `BeforeAt` 以及由此得到的 `codeOrder` 由 `EarliestDisagreement` 提供，此处并没有无条件得到它们。

```agda
                → ⟨ fst (lookup x γ) ∈ finiteStage m ⟩
                → ⟨ fst (lookup y γ) ∈ finiteStage m ⟩
                → ⟨ γ ⊨ BeforeAt b x y ⟩
                → ⟨ before m (fst (lookup x γ)) (fst (lookup y γ)) ⟩)
  where
```

`LimitOrdAt` 的第一支处理层号不等的情形。它绑定两个候选数码，分别证明它们是 `x` 与 `y` 的最小层号，并要求 `x` 的数码属于 `y` 的数码，从而表达自然数层号的严格不等。

```agda
  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` 子句都把同一数码认作最小层号，然后由假设的 `BeforeAt` 在该有限层内比较两个端点。共享一个见证便表达了相等，无须另加对象语言等式。

```agda
      ∨̇ ∃̇ ( LevelAt zero (suc x)
           ∧̇ ( LevelAt zero (suc y) ∧̇ BeforeAt zero (suc x) (suc y) ) )
```

为证明这条公式的充分性，先固定环境中的两个位置 `x` 与 `y`，并把其取值分别认同为实际的 `u,v : Limit`。显式指数 `ku,kv` 及其与真实层号的等式，使证明能在自然数比较、数码隶属与层隶属之间清楚转换。

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

两个 `Level` 实例不只是提供方便的名称：每个实例都为相应的实际端点及其最小层号给出 `LevelAt` 的已验证读法。向外读取时，正是这座桥排除了伪造的数码见证。

```agda
               where
    private
      module Lu = Level u ku qu
      module Lv = Level v kv qv
```

`Split c d` 是层号不等分支的语义内容。它表示 `c` 是左端点的最小层数码，`d` 是右端点的最小层数码，并且 `c ∈ d`；最后一项把方向固定为左侧层号小于右侧层号。

```agda
      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 c` 是层号相等分支的语义内容。同一个 `c` 必须描述两个端点的最小层号，只有随后才能由 `BeforeAt c x y` 给出它们在该共同有限层内的比较。

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

设 `ku < kv`。选择打包为模型元素的真实数码 `# ku` 与 `# kv` 作为两个存在见证。两次 `LevelAt-in` 验证这些数码确实描述了已对齐端点的实际最小层号。

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

自然数的严格不等经数码单调性给出 `# ku ∈ # kv`。沿两个打包数码的投影等式搬运，就得到 `Split` 所需的隶属 `fst (numS ku) ∈ fst (numS kv)`。

```agda
              (numS-fst kv) qy
          , subst2 (λ s t → ⟨ s ∈ t ⟩) (sym (numS-fst ku)) (sym (numS-fst kv))
              (#mono ku kv hlt) )
```

在同层分支中，等式 `level v ≡ level u` 使同一个数码 `# ku` 能描述两个端点。左侧的 `LevelAt` 读法直接使用 `qu`，右侧则利用该等式把 `v` 的层号也表示为同一指数 `ku`。

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

只有先建立所需边界，才能使用条件式假设 `BeforeAt-in`。层号等式把查得的两个端点都放入 `finiteStage ku`，而 `numS ku` 的投影等式表明作为共同数码给出的取值确实表示 `# ku`。

```agda
              (numS-fst ku) qy
          , BeforeAt-in zero (suc x) (suc y) (numS ku ∷ γ) ku (numS-fst ku)
              (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx)
                (levelStage u ku qu))
              (subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)
```

最后，把给定比较从指数 `level u` 搬运到 `ku`，并把它的两个端点与环境中的值对齐。连同两条层隶属证明，这满足 `BeforeAt-in` 的全部前提，从而完成 `Same (numS ku)`。

```agda
                (levelStage v ku (e ∙ qu)))
              (subst2 (λ s t → ⟨ before ku s t ⟩) (sym qx) (sym qy)
                (subst (λ j → ⟨ before j (fst u) (fst v) ⟩) qu h)) )
```

向外读取 `Split c d` 时，先由两条 `LevelAt-out` 引理把 `c` 认同为 `# ku`、把 `d` 认同为 `# kv`。沿这些认同搬运 `c ∈ d` 后，消去数码隶属便得到 `ku < kv`，再由保存的层号等式转成 `level u < level v`。

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

每个数码认同都在正确的延拓环境中取得：第一条 `LevelAt` 越过两个新见证指向 `x`，第二条则指向 `y`。这种绑定者对齐保证最终比较的是原来两个端点的真实层号，而不是见证本身。

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

在同层支中，同一个模型元素 `c` 同时充当 `u` 与 `v` 的候选层号数码。读取它的两份 `LevelAt` 证书会得到两个结论：双方的真实层号必定相等，而给定的有穷层公式也可以读成公共层内 `u` 在 `v` 之前。

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

第一份证书把 `c` 的底层集合认作数码 `# ku`，第二份则把它认作 `# kv`。数码编码的单射性于是给出 `ku = kv`；再与定义 `ku`、`kv` 的层号等式复合，便得到 `level v = level u`。因此，层号相等是从共同见证中恢复的，并未作为等式写进对象语言公式。

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

要使用假定的 `BeforeAt` 读取方向，必须先知道被比较的两个集合都属于同一个有穷层。`u` 的层号隶属给出它位于第 `ku` 层，新得到的层号等式则把 `v` 也放入这一层；环境等式再把这两个集合分别认作 `x` 与 `y` 处的取值。

```agda
        xIn : ⟨ fst (lookup x γ) ∈ finiteStage ku ⟩
        xIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qx) (levelStage u ku qu)
        yIn : ⟨ fst (lookup y γ) ∈ finiteStage ku ⟩
        yIn = subst (λ t → ⟨ t ∈ finiteStage ku ⟩) (sym qy)
          (levelStage v ku (e ∙ qu))
```

现在可以在 `c` 所表示的数码处应用抽象假设 `BeforeAt-out`。它先给出两个环境值之间的 `before ku`；把这两个值换成 `fst u` 与 `fst v`，再把 `ku` 换成 `level u`，便得到极限序同层支所需的有穷层比较。整个论证只在假设规定的层边界内使用 `BeforeAt`，不要求它在边界外具有任何语义。

```agda
        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 xIn yIn hb))
```

`LimitOrdAt` 的两条充分性律保留了两个数学分支的意义：层号不同时比较其数码，同层时使用外部提供的有穷层公式。不透明边界使这一定义的每次使用都经过这两条定律。因此，`Described` 内的每项结果都以它的三个输入为条件。

```agda
    opaque
      unfolding LimitOrdAt
```

先设 `u` 首次出现的有穷层严格早于 `v`。对象语言中的两个见证是模型数码 `# ku` 与 `# kv`；它们的 `LevelAt` 证书分别认出两个对象的层号，而第一个数码属于第二个数码正好表达 `ku < kv`。这些资料共同构成 `LimitOrdAt` 的异层支。

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

若双方层号相等，只需一个数码 `# ku` 同时证明两条 `LevelAt` 陈述。外部比较中的有穷层部分随后被写入这一公共层处的 `BeforeAt` 公式。共同使用一个见证本身就表达两个层号相等，因此对象语言里不需要另写两个层号数码之间的等式。

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

外部极限比较恰好给出这两个选项。在第一支中，`Lift` 只把命题放入更高的宇宙；`lower` 所做的是命题降级，从中取回普通的自然数不等式。再用 `ku` 与 `kv` 的定义等式对齐索引，便可应用异层支的构造。

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

外部比较的第二个选项已经包含同层构造所需的两项资料：层号相等，以及该层中的 `before` 比较。把二者交给同层构造便完成填充方向。因此，`LimitOrdAt-in` 只是依照既有极限序的字典式定义行事，并未引入一条新序。

```agda
        decide-in (inr (e , k)) = inner-in e k
```

读取 `LimitOrdAt` 时，两个分支的选择已经处在命题截断之中，所以最初只能得到命题截断的比较。在异层支中，两层存在见证由 `split-out` 读取；数码隶属由此还原为真实层号之间的严格不等式。所得不等式进入外部极限比较的第一支，并继续保留在命题截断内。

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

在同层支中，`same-out` 返回真实层号相等以及该有穷层中的 `before` 比较。这两项正好构成外部极限比较的第二支。这里不会导出任何层号不等式；次序信息完全来自层内比较。

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

语义析取先把两个数学情形分开，再处理各自的见证。左侧含有两层嵌套的层号存在见证与数码隶属，右侧则含有一个共同层号及有穷层公式。这一结构正对应极限序先比较层号、同层时再作层内比较的字典式次序。

```agda
        decide : ⟨ γ ⊨ ∃̇ ( ∃̇ ( LevelAt (suc zero) (sh2 x)
                            ∧̇ ( LevelAt zero (sh2 y)
                              ∧̇ (var (suc zero) ∈̇ var zero) ) ) ) ⟩
               ⊎ ⟨ γ ⊨ ∃̇ ( LevelAt zero (suc x)
                         ∧̇ ( LevelAt zero (suc y)
```

每个存在见证都只被消去到命题截断的目标中。异层情形局部取出两个候选层号并应用 `atSplit`，同层情形局部取出唯一的共同候选并应用 `atSame`。这些见证只用于证明当前比较，没有任何层号数码的选择逸出命题截断。

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

## 那个序，作为一个集合

要把比较化为关系集，分离条件必须先辨认候选元素是否为有序对。`Cond₀` 绑定可能的分量 `c` 与 `d`，要求候选元素是二者的编码有序对，并要求 `LimitOrdAt c d` 成立。因此，这个条件同时规定元素的配对形状与其所表示比较的方向。

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

在 `Described` 的一个实例内部，分离以 `Cond₀` 筛选包含所有极限层元素对的公共界。所得模型元素 `codeOrder` 恰好包含这个界内满足比较条件的候选元素。它的存在以给定的 `BeforeAt` 公式及其两条充分性方向为条件；下一章才提供具体实例。

```agda
  opaque
    codeOrder : S
    codeOrder = hasSeparationL (pairsBound .fst) Cond₀ .fst .fst
```

分离规格给出可直接使用的隶属刻画：一个候选元素属于 `codeOrder`，当且仅当它属于 `pairsBound` 并满足 `Cond₀`。公共界本身可能还含有额外元素，因此只负责给出集合大小的包容；精确性来自第二个合取项，它辨认有序对并验证相应的极限比较。

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

固定 `z`、`c`、`d` 后，`Inner` 集中记录分离公式所需的两个事实：`z` 是 `c` 与 `d` 的编码有序对，并且 `LimitOrdAt` 判定 `c` 在 `d` 之前。把二者放在一起，便能确保比较所用的端点正是候选对编码的两个分量。

```agda
  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 z` 展示两层嵌套存在量词的见证结构：先给出第一个分量 `c`，再在命题截断中给出满足 `Inner z c d` 的第二个分量 `d`。这种嵌套与 `Cond₀` 的语义一致，既保留见证之间的依赖，也不为 `z` 选择一个规范分解。

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

给定实际分量以及 `Inner` 中的两个事实，只要把这些分量依次放入嵌套存在量词，就能满足分离条件。两个存在见证都处在命题截断中，因为对象语言的存在只记录合适分量确实存在。分离所得集合的隶属本身是命题，所以这些资料已经足够。

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

反过来，满足 `Cond₀` 的证据已经具有 `Outer` 所记录的截断嵌套结构，所以读取时可以直接保留这份证据，不必选择任何一个分量。借助这一点，后面的隶属证明可以展开分离条件，同时始终留在命题截断的存在之内。

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

填充律从外部比较 `u ≺ˡ v` 出发，目标是证明二者底层集合的普通有序对属于 `codeOrder`。论证先使用真正位于模型中的 `limitEl u`、`limitEl v` 及其模型内编码对；最后再用一条等式把这一内部呈现与 `pr (fst u) (fst v)` 对齐。

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

分离规格把隶属目标归约为两个数学义务。模型内编码对必须属于公共界，而 `Cond₀` 必须以 `limitEl u` 与 `limitEl v` 为两个见证成立。完成这两项后，分离规格给出隶属，再沿两个配对呈现之间的等式得到原目标。

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

对齐等式由两个直接步骤组成。模型内配对的投影等于两个投影的外部有序对，而每个 `limitEl` 又投影回原极限层元素的底层集合。复合这两个事实可知，改变呈现既不改变任何端点，也不改变端点的顺序。

```agda
       ∙ cong₂ pr (limitEl-fst u) (limitEl-fst v)
```

第一个分离义务使用 `pairsBound` 的定义性质：任取两个极限层元素，由它们形成的有序对都受这个界覆盖。应用覆盖证书前，先把模型内编码对与相应的外部有序对对齐。这里不需要公共界的反向刻画，因为精确的比较标准由 `Cond₀` 提供。

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

`Cond₀` 的配对合取项由 `prAtL` 的充分性建立。模型内配对的投影已经是所需的有序对，因此这条充分性律把投影等式转成配对原子的满足证据。由此，公共界所用的集合论有序对与分离条件所用的对象语言描述连接起来。

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

比较合取项由 `LimitOrdAt-in` 在含有候选对及其两个分量的环境中给出。把分量取为 `limitEl u` 与 `limitEl v` 后，所需的对齐等式都是自反等式，而原假设 `u ≺ˡ v` 正好提供比较。至此完成条件式表示的正向证明。

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

读取律从 `pr (fst u) (fst v)` 属于 `codeOrder` 出发。分离条件会给出一对处于命题截断中的分量，并证明它们满足配对与比较条件；读取这些条件最初只能得到 `∥ u ≺ˡ v ∥₁`。最后由既已证明的严格良序 `limitOrder` 应用 `strictLimit`，利用三歧性排除相等与反向比较，才得到未截断的结论。

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

与填充方向相同，先把模型内编码对认作两个底层集合的外部有序对。把隶属转到这一呈现后，`codeOrder-mem` 展开分离的两个合取项，其中第二项正是满足 `Cond₀`。从此可以不再使用公共界合取项，因为端点及比较的全部信息都在分离条件中。

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

已知隶属针对外部有序对，而分离规格要应用于 `prS` 产生的模型元素。配对对齐等式说明二者的底层集合相等，因此可以把隶属转到模型内呈现。只有完成这一步，才能在该模型元素所形成的环境中读取对象语言条件。

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

对给定见证 `c`、`d`，配对原子先证明它们正是原有序对所编码的两个端点。把所得端点等式调整到所需方向后，`LimitOrdAt-out` 才能把随附的比较公式读成命题截断的 `u ≺ˡ v`。因此，比较合取项不能脱离配对合取项单独读取，后者负责认定公式所比较的究竟是哪两个外部极限层元素。

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

配对原子的充分性把其满足证据转成候选元素底层集合与 `pr (fst c) (fst d)` 之间的等式。先前的对齐又把同一个候选元素认作 `pr (fst u) (fst v)`。复合这两个等式便得到两个有序对相等，并为读取 `LimitOrdAt` 准备好所需的端点等式。

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

有序对编码的单射性把配对等式拆成 `fst u = fst c` 与 `fst v = fst d`。两个分量的位置与方向都被保留，左端不会与右端交换。把这两条等式反向，正好得到 `LimitOrdAt` 读取定理所需的对齐假设。

```agda
      split = pr-inj qcd
```

外层读取按照 `Cond₀` 的绑定次序处理嵌套见证：先处理 `c`，再在命题截断内处理 `d` 及其 `Inner` 证据。每次消去的目标都是 `atD` 已给出的命题截断比较，所以整个过程始终遵守截断限制。所有可能分解都被映到这个命题后，再由 `strictLimit` 给出最终未截断的比较。

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

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

`CodeKeys` 记录了在任意可构造载体 `A` 上进行名字比较时，使用这条条件式码关系的一种方式。除了 `A` 及其可构造性证明，它还固定 `A` 的小成员类型上的严格良序 `w`。名字比较的充分性结果于是可用 `w` 比较参数，并用当前 `Described` 实例比较码。这个嵌套模块是表示定理的一项可复用推论，主构造并不依赖它。

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

`w` 的严格关系在局部获得一个专用记号，以便把参数比较与码所用的极限层比较 `u ≺ˡ v` 区分开来。两条关系位于不同载体上，也由不同的内部关系集表示。它们的充分性律形状相同，但数学输入彼此独立。

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

若模型关系 `Ps` 从两个方向表示参数序，`AtParams` 就把它连同 `codeOrder` 及码序的两条表示律一起交给 `Adequacy.Keys`；这两条被表示的关系在数学上仍彼此独立。真实的下游路线在 `EarliestDisagreement` 中实例化 `Described`，公开 `codeOrder`、`codeOrder-fill` 与 `codeOrder-rep`，再由 `InternalWellOrder` 把这三项连同另行表示的参数序直接交给 `NameComparisonAdequacy.At.Least`。

```agda
    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` 及其两条读式。这两条读式只要求处理如下情形：第一个取值是数码 `# m`，两个端点都属于 `finiteStage m`；在这些假设下，公式成立当且仅当 `before m` 比较这两个端点。模块 `EarliestDisagreement` 恰好给出这些资料：`relAt m` 表示 `before m`，`beforeFam` 沿内部自然数收集这些已经表示的关系，而其中的 `BeforeAt` 先取出给定数码处的关系，再把它应用于两个端点。以这些结果实例化 `Described`，便得到公开的关系集 `codeOrder` 及其两条表示律 `codeOrder-fill` 与 `codeOrder-rep`。

## 小结

`LevelAt` 认出给定极限层成员首次出现的有穷层所对应的数码，`PrecedesAt` 则相对于任意已经表示的基底关系，表示一次最先分歧比较。给定 `BeforeAt` 在规定边界内的双向读法后，`Described` 用 `LimitOrdAt` 组合异层比较与同层比较，为所有候选有序对取界，再由分离得到条件式关系集 `codeOrder`。对每个 `u,v : Limit`，填充律与读取律给出 `u ≺ˡ v` 和 `pr (fst u) (fst v)` 属于该集合之间的两个方向；读取方向使用 `strictLimit` 与既有严格良序，从命题截断恢复比较。`EarliestDisagreement` 兑现有穷层假设，但本章既不在对象语言中断言 `codeOrder` 是良序，也不证明选择公理。