--- title: "内部层序关系" module: L.Choice.InternalWellOrder lang: zh site: "Bedrock" description: "内部典范良序" stage: "典范良序与选择公理" reading_order: 83 canonical: https://bedrock.institute/zh/L.Choice.InternalWellOrder.html html: L.Choice.InternalWellOrder.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/InternalWellOrder.lagda.md prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, V.Hierarchy, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.Choice.CanonicalNames, L.Choice.NameComparison, L.Choice.OrderTable, L.Choice.StageOrderAdequacy, L.Choice.NameComparisonAdequacy, L.Choice.EarliestDisagreement, L.Coding.HierarchySequence, L.Coding.DefinablePowerSet, L.Coding.Model, L.Coding.CodeSet, L.Hierarchy, L.WellOrder.Base, FOL.Absoluteness] routes: [choice-completion] translations: [https://bedrock.institute/en/L.Choice.InternalWellOrder.md, https://bedrock.institute/ja/L.Choice.InternalWellOrder.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 内部层序关系 在每个可构造层，`orderAt` 已经给出其成员上的宿主层严格良序。本章的任务是让解释于 `L` 中的公式也能使用其底层比较：对每个序数层，得到一个关系集，使其中的有序对成员与 `relOf (orderAt α oα)` 逐对双向对应。这里既不构造新的良序，也不证明断言该关系为良序的对象语言公式。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} ``` 本章始终区分两个层面。良序是宿主理论中的数学结构，而它在 `L` 内的表示必须是第一阶语言能够指称的集合。 ```agda open import Base.Prelude open import Base.Classical using ( LEM ) ``` 构造在任意宇宙层级上进行，只假设所标明后继层级上的排中律。后文所得的关系集恰好继承这一常设假设。 ```agda module L.Choice.InternalWellOrder {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where ``` 要在内部描述一次比较步，只须用隶属、等词、合取与存在量化连接变元和常元。下文的六个存在绑定，是对同一个逻辑构造器的反复使用。 ```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 ) open import L.Constructible {ℓ} ``` 这个关系以序数层为指标。因此，它的见证必须被辨认为可构造集合，而后继层中的隶属必须与前一层上的可定义性联系起来。 ```agda using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( suc-ord ) open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc ) open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ; Lset-suc ) open import L.Choice.FirstIntersectionStage {ℓ} lem using ( stageBound ) ``` 语义目标分属两个层面。`orderAt δ od` 是 `Lset δ` 的成员上的宿主层严格良序。为了描述其递归构造中的同生步进，`Under δ (stepOrder δ od) u v` 记录 `u`、`v` 属于 `Lset (sucV δ)`，并记录由此得到的两个成员满足 `stepOrder δ od`。`Lset δ` 上的最小名字把这项宿主层步进连接到下文构造的公式。 ```agda open import L.Choice.StageOrders {ℓ} lem using ( Mem; New; relOf; carry; orderAt; Under ; stepAt-fill; stepAt-read; IsLeastName; leastNameOf ) open import L.Choice.CanonicalNames {ℓ} lem using ( module Naming ) open import L.Choice.NameComparison {ℓ} lem using ( StepAt ) ``` 递归序表已经知道怎样把一条充分的步进描述变成关系集。剩下的工作是给出一条具体公式，并证明它的两个语义方向，从而消去序表对抽象步进参数的依赖。 ```agda open import L.Choice.OrderTable {ℓ} lem using ( IsRel; ixRel-fill; ixRel-rep ) open import L.Choice.StageOrderAdequacy {ℓ} lem using ( CodesAt; CodesAt-in; CodesAt-out; stepOrder; module Ordered ; towerS; towerS-fst; powS; powS-fst; sh2; sh3; StpOut; StpIn ) open import L.Choice.NameComparisonAdequacy {ℓ} lem using ( module At ) ``` 该公式必须辨认四个随层变化的对象：层塔、它的可定义子集、表在该层的取值，以及塔上的码。借助这些辨认子句，任意满足赋值都能被还原为预期的数学资料。 ```agda open import L.Choice.EarliestDisagreement {ℓ} lem using ( codeOrder; codeOrder-fill; codeOrder-rep ) open import L.Coding.HierarchySequence {ℓ} lem using ( LsetGraphAt ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( DefAt; DefAt-stage ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) ``` 另有两个见证被固定为常元：码上的比较关系与空字母表的码集。它们与序表给出的可变关系值一道，提供比较最小名字时所需的辅助关系与定义域。 ```agda open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Hierarchy {ℓ} lem using ( Lset-only; Lset-defines ) open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO ) ``` 满足关系解释在可构造集合的命题结构中。因此，每个存在子句都产生一个经过命题截断的依值对：见证可以支撑证明，却不能作为已选资料从命题之外取出。 ```agda import FOL.Absoluteness open import Cubical.Data.Sigma using ( Σ≡Prop ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ ) ``` 比较发生在某个后继层的成员之间。把层呈现为小类型，使宿主良序能够作用于其成员；`sucV` 则记录定位两个被比较对象所用的后继序数。 ```agda open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( sucV ) ``` 从这里起，公式都解释在 `L` 所携带的第一阶结构中。因此，放入槽位的元素既包含底层集合，也包含该集合可构造这一命题。 ```agda open hPropStructure 𝒮ʟ ``` 以下用 `γ ⊨ φ` 表示这种解释。绝对性使各条辨认公式能够被读成关于底层集合的具体事实，这正是后文能够拆出见证的原因。 ```agda module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ ) ``` ## 描述所绑定的诸元素 六槽移位把每个变元移过步进公式的六个存在见证。 ```agda private sh6 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc (suc n)))))) sh6 i = suc (suc (suc (suc (suc (suc i))))) ``` 六个见证全部绑定后，`StepAt` 直接引用其中五个：塔 `tw`、表关系 `rl`、码集 `cs`、码序 `ro` 与空字母表码集 `c0`。可定义幂集见证 `pw` 用于外围的隶属子句，并不传给 `StepAt`。 ```agda iTow iRel iCod iOrd iNil : ∀ {n} → Fin (suc (suc (suc (suc (suc (suc n)))))) iTow = suc (suc (suc (suc (suc zero)))) iRel = suc (suc (suc zero)) iCod = suc (suc zero) ``` 最内侧的两个指标选取 `ro` 与 `c0`。它们不引入新的绑定，只记录这两个已绑定见证在完全扩张的环境中所处的位置。 ```agda iOrd = suc zero iNil = zero ``` ## 那条描述 `Stp d f u v` 的六个见证按依赖顺序引入。首先是被辨认为 `d` 所指层的塔；其次是它的可定义幂集，其中的隶属子句将证明 `u` 与 `v` 所指对象可以参加后继层比较。 ```agda opaque Stp : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S n Stp d f u v = ∃̇ ( LsetGraphAt zero (suc d) ∧̇ ∃̇ ( DefAt zero (suc zero) ``` 第三个见证是序表在该层记录的取值 `rl`，第四个是塔上的码集。最后两个见证是由对象等词约束的变元，分别被固定为典范码序与空字母表的码集。 ```agda ∧̇ ( (var (sh2 u) ∈̇ var zero) ∧̇ ( (var (sh2 v) ∈̇ var zero) ∧̇ ∃̇ ( appAt (sh3 f) (sh3 d) zero ∧̇ ∃̇ ( CodesAt zero (sh3 zero) ∧̇ ∃̇ ( (var zero ≐ con codeOrder) ``` 到达最内层时，`StepAt` 看见七个语义槽位：上面选出的五个辅助见证，以及越过全部六个绑定后的两个原有对象。它断言二者最小名字之间的比较，并不在 `L` 内断言所表示的关系满足良序公式。 ```agda ∧̇ ∃̇ ( (var zero ≐ con (AllCodes ∅ʟ)) ∧̇ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ) ) ) ) ) ) ) ) ``` ## 六个绑定，逐层展开 读取模块固定四个槽位、环境，以及被解码层的序数性，因为宿主序需要该序数性。 ```agda module Reading {n : ℕ} (d f u v : Fin n) (γ : S ^ n) (od : IsOrd (fst (lookup d γ))) where private δ : V ℓ δ = fst (lookup d γ) ``` 宿主序被搬运到层的呈现上：成员的严格序可在小索引类型上取用。 ```agda ordW : SWO ⟪ Lset δ ⟫ ordW = carry (Lset δ) (orderAt δ od) ``` `Lset (sucV δ)` 中集合的名字在 `Lset δ` 上形成，并且只有相对于前一层上搬运后的序 `ordW` 才能被选定为最小名字。谓词 `IsLeastName` 同时记录该名字解释为给定集合，以及没有更小的竞争名字。这正是后继层中的集合与 `StepAt` 所用名字比较之间的精确桥梁。 ```agda module NM = Naming (Lset δ) ordW ``` 语义目标是经过命题截断的 `Under` 陈述。它同时包含两个后继层隶属事实与步进比较，但读取存在公式只会证明这类证据存在，并不会把名字或六个绑定对象中的任何一个选作资料。 ```agda Goal : Type (ℓ-suc ℓ) Goal = ∥ Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) ∥₁ ``` 六个见证全部扩张环境后，`StepHolds tw pw rl cs ro c0` 恰好表示最内层 `StepAt` 公式的满足。它是六层存在结构内部的最终语义条件。把各层见证置于命题截断之下的是外围绑定，而不是 `StepHolds` 本身。 ```agda opaque StepHolds : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) StepHolds tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ StepAt iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) ⟩ ``` 最内层载荷包含固定 `c0` 的等式与步进满足本身。二者在载荷内部是普通的合取证据；命题截断由外围存在层引入。 ```agda Six : (tw pw rl cs ro c0 : S) → Type (ℓ-suc ℓ) Six tw pw rl cs ro c0 = ⟨ (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con (AllCodes ∅ʟ)) ⟩ × StepHolds tw pw rl cs ro c0 ``` 向外一层，`ro` 被固定为典范码序，而合适的 `c0` 的存在经过命题截断。等式确定了预期的底层集合，但证明不会暴露一个已选的存在见证。 ```agda Five : (tw pw rl cs ro : S) → Type (ℓ-suc ℓ) Five tw pw rl cs ro = ⟨ (ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ (var zero ≐ con codeOrder) ⟩ × ∥ (Σ[ c0 ∈ S ] Six tw pw rl cs ro c0) ∥₁ ``` 码集子句刻画绑定塔上的 `cs`。读取公式时，它的充分性与先前对塔的辨认共同确定 `cs` 的底层集合；其余内层见证仍留在命题截断之下。 ```agda Four : (tw pw rl cs : S) → Type (ℓ-suc ℓ) Four tw pw rl cs = ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ × ∥ (Σ[ ro ∈ S ] Five tw pw rl cs ro) ∥₁ ``` 序表应用子句说明 `rl` 是被解码层处记录的某个取值。在读取方向，`rl` 可以是该处任意一个被记录值，因此后面的关系假设必须对该处每个取值作全称陈述；在填充方向，则使用调用方给出的某个特定 `rl`。 ```agda Three : (tw pw rl : S) → Type (ℓ-suc ℓ) Three tw pw rl = ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ × ∥ (Σ[ cs ∈ S ] Four tw pw rl cs) ∥₁ ``` 可定义幂集子句辨认 `pw`，随后的两个合取项把两个被比较对象都放入其中。一旦 `tw` 与 `pw` 被确定，这两条隶属便转化为对 `Lset (sucV δ)` 的隶属，给出 `Under` 所需的两个定义域分量。 ```agda Two : (tw pw : S) → Type (ℓ-suc ℓ) Two tw pw = ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ × ( ⟨ fst (lookup u γ) ∈ fst pw ⟩ × ( ⟨ fst (lookup v γ) ∈ fst pw ⟩ ``` 在两条隶属之后，剩余载荷从表值 `rl` 的截断存在开始。最终目标 `Goal` 本身是命题，因此证明可以把每层截断消去到这个目标中，而不会抽取出可重复使用的见证选择。 ```agda × ∥ (Σ[ rl ∈ S ] Three tw pw rl) ∥₁ ) ) ``` 最外层载荷从满足层图的见证 `tw` 开始。序数性使这条描述在底层集合层面唯一，因此任意满足它的 `tw` 都能与 `Lset δ` 同一视；后续所有见证的嵌套存在仍经过命题截断。 ```agda One : (tw : S) → Type (ℓ-suc ℓ) One tw = ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ × ∥ (Σ[ pw ∈ S ] Two tw pw) ∥₁ ``` ## 层处的那一步之充分性 六个绑定元素中只有五个进入 `StepAt`；`pw` 用于外围的两项隶属子句。因此，`Slots` 把塔与码集认同为预期对象，假设 `rl` 具有逐对表示性质 `IsRel δ rl`，并把 `ro` 与 `c0` 固定为所需的两个常元。这些事实恰是先前名字比较充分性定理所需的条件。 ```agda module Slots (tw pw rl cs ro c0 : S) (qtw : fst tw ≡ Lset δ) (hrel : IsRel δ rl) (qcs : fst cs ≡ fst (AllCodes (LsetS δ od))) (qro : fst ro ≡ fst codeOrder) ``` 在对齐内部，命名充分性在该层处实例化；其局部步进比较以码序与关系值打开，而关系表示的两个方向一并供给。 ```agda (qc0 : fst c0 ≡ fst (AllCodes ∅ʟ)) where private module A6 = At (Lset δ) (snd (LsetS δ od)) ordW module L6 = A6.Least codeOrder rl codeOrder-rep codeOrder-fill (ixRel-rep δ od rl hrel) (ixRel-fill δ od rl hrel) ``` 有了这些证明，名字比较定理便可在完全扩张的环境中实例化。它的七个语义槽位由两个被比较对象与五个辅助见证组成，后者分别由 `iTow`、`iRel`、`iCod`、`iOrd`、`iNil` 选出。 ```agda module St = L6.Step iOrd iRel iTow iCod iNil (sh6 u) (sh6 v) (c0 ∷ ro ∷ cs ∷ rl ∷ pw ∷ tw ∷ γ) qro refl (Σ≡Prop (λ x → snd (isL x)) qtw) qcs qc0 ``` 对第一个对象，`LeastFst t` 是「`t` 是它的最小名字」这一断言的局部形式。其中的解释等式与 `IsLeastName` 中相应等式方向相反；下文的转换引理反转该等式，同时保留同一项极小性断言。 ```agda LeastFst : NM.Name → Type (ℓ-suc ℓ) LeastFst = St.LeastOf (sh6 u) ``` `LeastSnd` 为第二个对象给出同样的桥梁。保持两个谓词平行很重要，因为 `StepAt` 比较的是两个最小名字，而不只是断言最小名字存在。 ```agda LeastSnd : NM.Name → Type (ℓ-suc ℓ) LeastSnd = St.LeastOf (sh6 v) ``` 导出的谓词 `IsLeastName` 与充分性定理以相反方向陈述解释等式。路径对称性转换第一个对象的等式，而极小性子句则用同样方式反转每条竞争等式来搬运。 ```agda leastFst-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup u γ)) → LeastFst t leastFst-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 第二个对象的转换形式完全相同。它只改变等式方向，并保留极小性的数学内容。 ```agda leastSnd-in : (t : NM.Name) → IsLeastName δ ordW t (fst (lookup v γ)) → LeastSnd t leastSnd-in t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 在读取方向，同一个对称性操作恢复第一个对象的 `IsLeastName`。由于路径反转两次会恢复原方向，这一转换不损失信息。 ```agda leastFst-out : (t : NM.Name) → LeastFst t → IsLeastName δ ordW t (fst (lookup u γ)) leastFst-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 第二个最小名字谓词以同样方式读回，于是得到两条普通的最小名字事实，可供宿主层步进引理使用。 ```agda leastSnd-out : (t : NM.Name) → LeastSnd t → IsLeastName δ ordW t (fst (lookup v γ)) leastSnd-out t (q , mn) = sym q , λ t' q' → mn t' (sym q') ``` 最内层公式的两个语义方向有意保持不对称。给定两条具体的最小名字及其比较，`holds-in` 证明 `StepHolds`。反过来，`holds-out` 从 `StepHolds` 只得到命题截断下的存在性，即存在两条合适的最小名字及其比较，因此没有一对已选名字逸出公式。 ```agda opaque unfolding StepHolds ``` 在向内方向，`t₁`、`t₂` 的局部最小名字事实连同 `t₁ ≺ₙ t₂`，给出最内层公式所需的全部语义内容。名字比较充分性定理恰把这三项事实转成 `StepHolds`。 ```agda holds-in : (t₁ t₂ : NM.Name) → LeastFst t₁ → LeastSnd t₂ → NM._≺ₙ_ t₁ t₂ → StepHolds tw pw rl cs ro c0 holds-in = St.StepAt-fill ``` 反过来，读取最内层满足会在命题截断之下得到两个最小名字及其名字比较。这个截断不可省略：结果断言合适名字存在，却不导出一对已选名字。 ```agda holds-out : StepHolds tw pw rl cs ro c0 → ∥ Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] (LeastFst t₁ × (LeastSnd t₂ × NM._≺ₙ_ t₁ t₂)) ∥₁ holds-out = St.StepAt-read ``` ## 拆开 总体读取必须适用于满足赋值所给出的任意六个见证。最先的假设说明：`tw` 满足被解码层的图描述，`pw` 满足其上的可定义幂集描述，并且第一个被比较对象属于 `pw`；随后将用唯一性与充分性结果，把这些条件转成关于具体层的事实。 ```agda private atAll : (tw pw rl cs ro c0 : S) → ⟨ (tw ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ → ⟨ (pw ∷ tw ∷ γ) ⊨ DefAt zero (suc zero) ⟩ → ⟨ fst (lookup u γ) ∈ fst pw ⟩ ``` 接下来的假设给出第二条隶属、序表应用与码集描述。关键在于，关系前提遍历序表在 `δ` 处记录的每个 `r`，因为在读取方向，存在公式可能绑定其中任意一个 `rl`；这里最后显示的等式把 `ro` 固定为典范码序。 ```agda → ⟨ fst (lookup v γ) ∈ fst pw ⟩ → ⟨ (rl ∷ pw ∷ tw ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ → ⟨ (cs ∷ rl ∷ pw ∷ tw ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ → ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → fst ro ≡ fst codeOrder ``` 向外论证现在到达最内层条件。六个存在见证辨认完毕后，`atAll` 从 `StepAt` 的满足读出两条最小名字及其名字比较的仅仅存在。下一步在这项命题截断上作映射，把名字比较转成所需的宿主层 `Under` 比较，而不会从截断之外选出名字。 ```agda → fst c0 ≡ fst (AllCodes ∅ʟ) → StepHolds tw pw rl cs ro c0 → Goal atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep = PT.map atNames (K.holds-out hstep) where ``` 塔认同等式说公式中绑定的塔等于实参序数处的可构造层，由层充分性引理读取。 ```agda qtw : fst tw ≡ Lset δ qtw = Lset-only zero (suc d) (tw ∷ γ) hg od ``` 可定义子集认同说被绑定的集合是该层的可定义幂集，沿塔等式运输。 ```agda qpw : fst pw ≡ 𝒟ₒ (Lset δ) qpw = subst ⟨_⟩ (DefAt-stage δ od zero (suc zero) (pw ∷ tw ∷ γ) qtw) hdef ``` 后继层隶属由两次运输恢复：第一次沿可构造层后继恒等式认同可定义幂集与后继层，第二次沿被绑定集合认同为该可定义幂集的等式改写。二者共同把被比较对象放进后继层 `Lset (sucV δ)` 中。 ```agda inSuc : (x : V ℓ) → ⟨ x ∈ fst pw ⟩ → ⟨ x ∈ Lset (sucV δ) ⟩ inSuc x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (Lset-suc δ)) (subst (λ z → ⟨ x ∈ z ⟩) qpw h) ``` 第一个比较候选是槽位 `u` 处的底层集合，经恢复引理呈现为后继段的成员。 ```agda a : New δ a = fst (lookup u γ) , inSuc (fst (lookup u γ)) hu ``` 第二个比较候选是槽位 `v` 处的底层集合，同样呈现。 ```agda b : New δ b = fst (lookup v γ) , inSuc (fst (lookup v γ)) hv ``` 应用公式的满足说明 `rl` 是表在 `δ` 处记录的一个取值。向外假设 `vals` 特意覆盖每个这样的记录值，所以也为 `Stp` 内部选出的这个见证提供 `IsRel δ rl`。这是对所有可能表见证的可靠性条件，并非表取值的唯一性断言。 ```agda hrel : IsRel δ rl hrel = vals rl (subst ⟨_⟩ (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ pw ∷ tw ∷ γ)) happ) ``` 码集描述的向外读式把 `cs` 认同为 `AllCodes (LsetS δ od)`，即当前层 `Lset δ` 上的码集。被比较对象属于后继层，但其名字相对于前一层形成，所以这里的码集以 `δ` 为指标，而不是以 `sucV δ` 为指标。 ```agda qcs : fst cs ≡ fst (AllCodes (LsetS δ od)) qcs = cong fst (CodesAt-out (LsetS δ od) zero (sh3 zero) (cs ∷ rl ∷ pw ∷ tw ∷ γ) qtw hcs) ``` 塔、层关系、码集以及两个固定码对象现在都已辨认，`Slots` 因而把六个见证接到先前证明的名字比较充分性定理上。借助这一共同实例，余下论证可以在最内层公式与相应最小名字资料之间往返。 ```agda module K = Slots tw pw rl cs ro c0 qtw hrel qcs qro qc0 ``` 在名字充分性定理返回的命题截断内部，设 `t₁`、`t₂` 分别是两个被比较集合的最小名字，且 `t₁ ≺ₙ t₂`。目标 `Under` 不只含最终比较，还记录两个集合都属于 `Lset (sucV δ)`；这两项隶属已经由 `a` 与 `b` 建立。 ```agda atNames : Σ[ t₁ ∈ NM.Name ] Σ[ t₂ ∈ NM.Name ] ( K.LeastFst t₁ × ( K.LeastSnd t₂ × NM._≺ₙ_ t₁ t₂ ) ) → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) atNames (t₁ , (t₂ , (l₁ , (l₂ , lt)))) = a .snd ``` 两条最小名字的向外读式把局部谓词还原为 `IsLeastName`。随后 `stepAt-fill` 说明，这两条最小名字之间的比较蕴含其所表示新元素之间的 `stepOrder δ od` 关系。再合并上一组的两项隶属，即得到完整的 `Under`。 ```agda , ( b .snd , stepAt-fill δ ordW a b t₁ t₂ (K.leastFst-out t₁ l₁) (K.leastSnd-out t₂ l₂) lt ) ``` ## 装回 反向论证固定一个实际表取值 `rl`，以及表在 `δ` 处记录它和它表示所需层关系的证据；同时固定一项 `Under` 比较携带的两条后继层隶属。与向外方向不同，这个构造手中已有一个具体的局部表取值，可以把它用作 `Stp` 的第三个存在见证。 ```agda module Pack (rl : S) (hpr : ⟨ pr δ (fst rl) ∈ fst (lookup f γ) ⟩) (hrel : IsRel δ rl) (hx : ⟨ fst (lookup u γ) ∈ Lset (sucV δ) ⟩) (hy : ⟨ fst (lookup v γ) ∈ Lset (sucV δ) ⟩) where ``` 装回论证按 `Stp` 规定的次序使用六个见证：`towerS δ od`、`powS δ od`、给定的表取值 `rl`、`AllCodes (LsetS δ od)`、`codeOrder` 与 `AllCodes ∅ʟ`。特别地，第四个见证是当前层 `Lset δ` 上的码集；只有被比较的两个对象属于其后继层。 ```agda private module K = Slots (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) (towerS-fst δ od) hrel refl refl refl ``` 第一个比较候选由其在后继段中的隶属呈现。 ```agda a : New δ a = fst (lookup u γ) , hx ``` 第二个比较候选同样呈现。 ```agda b : New δ b = fst (lookup v γ) , hy ``` 相对于固定的宿主层良序 `ordW`，每个新元素都有最小名字，因此第一个候选给出一条名字及其 `IsLeastName` 证明所成的对。这是填入公式时使用的显式局部见证，并不声称 `Stp` 唯一确定某条名字。 ```agda n₁ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup u γ)) n₁ = leastNameOf δ ordW a ``` 同一条定理为第二个候选提供一条最小名字。论证在局部比较这两条选出的名字，再把它们交给 `StepAt` 的向内充分性定理。该公式的存在语义以及 `Stp` 外围的六个存在绑定随后重新隐藏这些名字；此构造不会导出一对已选名字。 ```agda n₂ : Σ[ t ∈ NM.Name ] IsLeastName δ ordW t (fst (lookup v γ)) n₂ = leastNameOf δ ordW b ``` 第一个见证取 `towerS δ od`。其定义定理证明它在扩展环境中满足 `LsetGraphAt`，因而底层集合是第一个绑定所要求的 `Lset δ`。 ```agda hg : ⟨ (towerS δ od ∷ γ) ⊨ LsetGraphAt zero (suc d) ⟩ hg = Lset-defines zero (suc d) (towerS δ od ∷ γ) od (towerS-fst δ od) ``` 第二个见证取 `powS δ od`，其底层集合是可定义子集集 `𝒟ₒ (Lset δ)`。`DefAt-stage` 给出的等式刻画 `DefAt` 的满足；沿这一刻画运输 `powS-fst`，便得到所需的满足陈述。这里使用的是该层的可定义子集集，而不是它的完整幂集。 ```agda hdef : ⟨ (powS δ od ∷ towerS δ od ∷ γ) ⊨ DefAt zero (suc zero) ⟩ hdef = subst ⟨_⟩ (sym (DefAt-stage δ od zero (suc zero) (powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od))) (powS-fst δ od) ``` 为了填入 `Stp` 的两项隶属合取，这里需要的方向是从后继层进入选定的可定义子集对象。恒等式 `Lset-suc δ` 把 `Lset (sucV δ)` 中的隶属改写为 `𝒟ₒ (Lset δ)` 中的隶属，`powS-fst` 再把后者改写为 `powS δ od` 的底层集合。 ```agda inPow : (x : V ℓ) → ⟨ x ∈ Lset (sucV δ) ⟩ → ⟨ x ∈ fst (powS δ od) ⟩ inPow x h = subst (λ z → ⟨ x ∈ z ⟩) (sym (powS-fst δ od)) (subst (λ z → ⟨ x ∈ z ⟩) (Lset-suc δ) h) ``` 应用满足由表条目证明沿应用编码的充分性运输。 ```agda happ : ⟨ (rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ appAt (sh3 f) (sh3 d) zero ⟩ happ = subst ⟨_⟩ (sym (appAt-adequate (sh3 f) (sh3 d) zero (rl ∷ powS δ od ∷ towerS δ od ∷ γ))) hpr ``` 对第四个见证，`CodesAt` 的向内读式证明 `AllCodes (LsetS δ od)` 满足塔 `Lset δ` 上的码集描述。这里不需要后继层上的码集。 ```agda hcs : ⟨ (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) ⊨ CodesAt zero (sh3 zero) ⟩ hcs = CodesAt-in (LsetS δ od) zero (sh3 zero) (AllCodes (LsetS δ od) ∷ rl ∷ powS δ od ∷ towerS δ od ∷ γ) (towerS-fst δ od) refl ``` 现假设宿主层的 `stepOrder` 比较成立。经向内的等式方向调整，先前选出的两条最小名字满足局部最小名字谓词；余下只需把宿主比较转成最内层 `StepAt` 公式所需的名字比较。 ```agda hstep : relOf (stepOrder δ od) a b → StepHolds (towerS δ od) (powS δ od) rl (AllCodes (LsetS δ od)) codeOrder (AllCodes ∅ʟ) hstep cmp = K.holds-in (n₁ .fst) (n₂ .fst) (K.leastFst-in (n₁ .fst) (n₁ .snd)) (K.leastSnd-in (n₂ .fst) (n₂ .snd)) ``` 定理 `stepAt-read` 正好完成这一转换，并使用 `n₁` 与 `n₂` 的最小性证明。把所得名字比较交给 `holds-in`，便证明最内层满足陈述。论证使用已经存在的宿主层 `stepOrder`，并未构造新的良序。 ```agda (stepAt-read δ ordW a b (n₁ .fst) (n₂ .fst) (n₁ .snd) (n₂ .snd) cmp) ``` 对象语言的六个存在量词被解释为六层嵌套的命题截断依值对。`packAll` 先装入 `towerS δ od` 及其 `LsetGraphAt` 证明。尽管证明在局部构造了具体见证，最外层存在边界立即只保留它的命题截断。 ```agda packAll : relOf (stepOrder δ od) a b → ∥ (Σ[ tw ∈ S ] One tw) ∥₁ packAll cmp = ∣ towerS δ od , ( hg , ∣ powS δ od ``` 第二个见证是 `powS δ od`，并附有它对 `DefAt` 的满足，以及从后继层运输来的两条隶属。第三个见证是给定的表取值 `rl`；它的有序对成员证明给出所需的 `appAt` 满足。因此，填充方向使用调用方已经给出的特定关系值，而不是从表中选取一个值。 ```agda , ( hdef , ( inPow (fst (lookup u γ)) hx , ( inPow (fst (lookup v γ)) hy , ∣ rl , ( happ ``` 码集满足之后是码序元素及其认同等式，再后是空字母表码集。 ```agda , ∣ AllCodes (LsetS δ od) , ( hcs , ∣ codeOrder , ( refl , ∣ AllCodes ∅ʟ ``` 最后几层包装装入空字母表码集、辨认它的等式以及最内层步进公式的满足。封闭全部六层截断后即证明 `Stp`，同时不会向后续使用者暴露所选的塔、关系、码或名字见证。 ```agda , ( refl , hstep cmp ) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ ) ) ) ∣₁ ) ∣₁ ``` ## 两条读式 两条读式现在给出递归序表所需的精确接口，而其类型记录了关键的不对称性。向外方向必须接受该层所记录的每个关系值，并且只返回 `∥ Under ... ∥₁`。向内方向则接收一个指定的已记录取值及其 `IsRel` 证明，再接收一项未经截断的 `Under` 比较，由此构造 `Stp` 的满足。 ```agda opaque unfolding Stp StepHolds ``` 向外读取时，假设表在 `δ` 处记录的每个取值都表示所需层关系。`Stp` 的满足只给出命题截断下的存在见证，因此 `read` 逐层消去六项截断，目标则是本身经过命题截断的 `Goal`。 ```agda read : ((r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r) → ⟨ γ ⊨ Stp d f u v ⟩ → Goal read vals = PT.rec PT.squash₁ (λ { (tw , (hg , hpw)) → PT.rec PT.squash₁ (λ { (pw , (hdef , (hu , (hv , hrl)))) → PT.rec PT.squash₁ ``` 消去遵循绑定次序：塔、可定义子集集、表取值、码集、码序以及空字母表码集。每一层的见证只在下一层截断的续体内部可用；整个构造从不返回一个选定的六元组。 ```agda (λ { (rl , (happ , hcs)) → PT.rec PT.squash₁ (λ { (cs , (hcs , hro)) → PT.rec PT.squash₁ (λ { (ro , (qro , hc0)) → PT.rec PT.squash₁ (λ { (c0 , (qc0 , hstep)) → atAll tw pw rl cs ro c0 hg hdef hu hv happ hcs vals qro qc0 hstep }) ``` 六个见证及其条件在局部全部可用后，`atAll` 产出命题截断的 `Under` 比较。嵌套消去器随后按相反的语法次序闭合，从而保留对象语言存在量词所要求的截断边界。 ```agda hc0 }) hro }) hcs }) hrl }) hpw }) ``` 向内读法消耗特定表取值连同其隶属与关系证明，连同两条隶属证明与宿主侧比较，并把一切打包进六层存在量词。 ```agda fill : (r : S) → ⟨ pr δ (fst r) ∈ fst (lookup f γ) ⟩ → IsRel δ r → Under δ (stepOrder δ od) (fst (lookup u γ)) (fst (lookup v γ)) → ⟨ γ ⊨ Stp d f u v ⟩ fill r hpr hrel (hx , (hy , cmp)) = Pack.packAll r hpr hrel hx hy cmp ``` 步进公式的向外读法作为第一条充分性方向导出：满足蕴含截断的步进比较。 ```agda stp-out : StpOut Stp stp-out = Reading.read ``` ## 框架被打开 步进公式的向内读法作为第二条充分性方向导出：特定表条目连同正确关系与宿主侧比较共同蕴含公式满足。 ```agda stp-in : StpIn Stp stp-in = Reading.fill ``` 把 `Stp` 及其两条读式交给抽象构造，层序表便完整实例化。特别地，对每个序数层都会得到一个内部集合 `relL`，以及 `relL-fill` 与 `relL-rep`；二者逐对在 `orderAt` 的宿主关系和相应有序对属于 `relL` 之间转换。这里得到的是关系图的表示，并未证明一条对象语言陈述，声称 `relL` 满足某个良序公式。 ```agda open Ordered Stp stp-out stp-in public ``` ## 上界序数处的序 对可构造集合 `a`，`stageBound` 选取一个同时高于 `ω` 与 `a` 首次出现之层的序数。因此，`Lset boundOrd` 足以容纳 `a` 的成员以及这些成员的成员，这正是后续横截论证所需的局部论域。所选界足以完成这项工作；本章不声称它是 `a` 的最小界或唯一确定的界。 ```agda module Bound (a : V ℓ) (p : ⟨ isL a ⟩) where boundOrd : V ℓ boundOrd = stageBound a p .fst ``` 同一项界结果还证明 `boundOrd` 是序数。凭这项证明，先前已经构造的宿主层良序族 `orderAt` 才能专用于层 `Lset boundOrd`。 ```agda boundOrd-ord : IsOrd boundOrd boundOrd-ord = stageBound a p .snd .fst ``` 为了在这个指标处取得内部关系对象，序表构造还需要指标本身可构造。序数属于它自身的后继层，因此 `boundOrd ∈ Lset (sucV boundOrd)` 正好给出见证，使 `Lset→isL` 能证明 `isL boundOrd`。 ```agda boundOrd-isL : ⟨ isL boundOrd ⟩ boundOrd-isL = Lset→isL (sucV boundOrd) (suc-ord boundOrd-ord) boundOrd (ord∈Lset-suc boundOrd boundOrd-ord) ``` 待表示的关系是已经存在的宿主层严格良序 `orderAt boundOrd boundOrd-ord`，其载体为 `Mem (Lset boundOrd)`。良序结构由这个 `SWO` 值携带；以下各行只把它的二元关系实现为 `L` 内的集合。 ```agda boundOrder : SWO (Mem (Lset boundOrd)) boundOrder = orderAt boundOrd boundOrd-ord ``` 序表在所选序数处给出这个内部集合 `relL`。因此 `orderL` 是模型中的一个元素，其成员用来表示关系图中的有序对。它不是一项新的良序构造，本章也没有为它附上一份对象理论内部对良序公理的满足证明。 ```agda orderL : S orderL = relL boundOrd boundOrd-isL boundOrd-ord ``` 正向表示引理从宿主层比较 `relOf boundOrder x y` 出发，把编码有序对 `pr (fst x) (fst y)` 放入 `orderL`。这建立已有 `SWO` 关系与其内部关系图之间逐对对应的一个方向。 ```agda orderL-fill : (x y : Mem (Lset boundOrd)) → relOf boundOrder x y → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ orderL-fill = relL-fill boundOrd boundOrd-isL boundOrd-ord ``` 反过来，编码有序对属于 `orderL` 可恢复宿主层比较。`orderL-fill` 与 `orderL-rep` 合起来，逐对刻画哪些有序对出现在内部关系图中；它们既不声称表示该图的集合具有唯一性，也不在对象语言内部证明它是良序。 ```agda orderL-rep : (x y : Mem (Lset boundOrd)) → ⟨ pr (fst x) (fst y) ∈ fst orderL ⟩ → relOf boundOrder x y orderL-rep = relL-rep boundOrd boundOrd-isL boundOrd-ord ``` ## 小结 严格良序仍是 `Mem (Lset α)` 上的宿主层结构 `orderAt α oα`。集合 `relL α hα oα` 是 `L` 的一个元素，它把该二元关系表示为关系图；`relL-fill` 与 `relL-rep` 对每一对元素证明这项表示的两个方向。六重绑定公式及其充分性读式使后续对象语言公式能够使用这个关系图，但既不证明新的良序，也不证明对象语言中的良序断言。