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

在可构造序数层索引 `α` 处，先前的构造已经给出 `Lset α` 的成员上的宿主层严格良序。本章要把它的二元比较表示为 `L` 内部的一个集合，使模型中解释的公式能够量化这条关系。所得结果以单步递归已有充分的对象语言描述为条件，并且只适用于既是序数又可构造的 `α`。它表示已有序的底层关系，而尚未在对象语言中断言这条关系是良序。

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

全章唯一的经典假设，是构造所处宇宙层级上的排中律。先前的层序已经需要它，后文使用的替换与分离也由它供给；关于截断、搬运与外延唯一性的局部论证不再加入第二项经典假设。

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

在模块边界固定 `lem : LEM (ℓ-suc ℓ)`，使这项依赖始终一致。特别地，下文所有构造都继承同一个带层级索引的假设，而不会暗中诉诸任意大小上的排中律。

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

这里必须区分两个论述层次。待表示的关系定义在宿主类型论中，而它的递归描述是一条在 `L` 中解释的一阶公式。成员归纳连接各层：它的动机可以取值于任意依值类型族，因此后文同时包含表与关系的资料包无须先被证明为命题，递归本身便已合法。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
```

最终关系位于可构造模型中，但它的端点起初是宿主集合 `Lset α` 的成员。固定序数性证明 `oα` 后，`Lset→isL` 把每个端点打包为模型元素；这一步使用 `α` 的序数性，而不使用 `α` 本身可构造的另一份证明。`α` 的可构造性见证在后文承担不同作用：它把层索引本身打包为模型元素 `A`，供替换作为定义域、供分离作为参数。序数成员法则给出较小索引的序数性，而对编码的单射性与外延性分别恢复端点、按成员认同集合。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset→isL; IsOrd; isPropIsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )
open import L.Axioms.Basic {ℓ} using ( extensionalL )
```

构造将把两条集合存在原理用于不同目的。命题截断下的存在与外延唯一性先使每个图纤维可缩，替换随后把所有较小索引处的关系取值收集成一张表。分离则从一个公共包含集中切出当前关系。因此，界下的表与界处的关系虽被同时产生，却来自两种不同的论证。

```agda
open import L.Axioms.Full {ℓ} lem using ( hasReplacementL; hasSeparationL )
open import L.Recursion {ℓ} lem using ( mereFunct; smallDom )
open import L.Coding.Model {ℓ} using ( domAt-intro; prʟ; prʟ-fst )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-in; extAt-out; extAt-in-both )
open import L.Coding.HierarchySequence {ℓ} lem using ( module RecShape )
```

序本身已经由 `orderAt α oα` 给出，它是 `Mem (Lset α)` 上的严格良序。本章使用其底层比较、三岐性、非自反性与传递性，后面还把同一个序搬运到该层的小呈现上。这里不引入新的比较规则，也不重新证明良基性。

```agda
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf; orderAt; memOf; carry )
open import L.WellOrder.Base {ℓ-suc ℓ} using ( SWO; Tri; lt; eq; gt )
```

后文许多等式比较的是依值对，其第二分量是成员证明。由于成员关系与序数性都是命题，底层集的相等便决定打包成员的相等，而更换证书不会产生不同的数学端点。因此，可以沿对分量的等式搬运比较，而不会把证明变成额外的选择。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop; _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
```

命题截断将标出每个只需存在而不选定见证之处。小呈现承担另一种任务：它用一个小索引类型呈现可能较大的成员纤维，再由嵌入返回所表示的成员。二者必须分清，因为前者隐藏选择，后者控制大小。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber )
```

从这里起，命题与量词都在 `L` 的成员结构中读取。因此，说一个模型元素实现某个类，是对其成员作出的命题，而不是借元理论的概括另行组装一个外部集合。

```agda
open hPropStructure 𝒮ʟ
```

后面使用的内部集合构造接口，将陈述某个候选集合恰以满足一条公式的对象为成员。这只是集合的外延规格；集合的存在仍须在递归的相应位置由替换或分离给出。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

公式的满足关系通过绝对性与宿主层谓词相比较。公式本身并不含有 `orderAt`；充分性等式将在语义上把公式的真值与编码比较对所成的宿主层类认同起来。

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

后文公式会在既有环境外再引入两个绑定。这个私有移位把每个旧变元的索引越过两个新绑定，从而保留原有含义；借此，取值、索引与表的数学角色在扩展环境中仍保持不变。

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

## 把比较整个读回来

模型中的类必须取命题值，但尚未证明 `relOf (orderAt α oα) a b` 的见证具有唯一性。因此，`Ordering` 只保留该见证的命题截断。这把比较化为适合类成员关系的逻辑形式，同时保留比较是否有见证这一事实。

```agda
Ordering : (α : V ℓ) → IsOrd α → Mem (Lset α) → Mem (Lset α) → hProp (ℓ-suc ℓ)
Ordering α oα a b = ∥ relOf (orderAt α oα) a b ∥₁ , squash₁
```

对于这一特定比较，稍后可以消去截断。理由是已有严格序的三岐性：一旦把 `a` 与 `b` 分成正向相关、相等或反向相关三种情形，后两种就会与截断后的正向比较矛盾。这是严格全序比较的特殊性质，并非从任意命题截断中提取见证的一般方法。

```agda
strict : (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α))
       → ⟨ Ordering α oα a b ⟩ → relOf (orderAt α oα) a b
strict α oα a b h = decide (SWO.tri∙ W a b)
  where
  W = orderAt α oα
```

在正向分支中，三岐性已经给出所需的未截断见证，因而无须打开截断假设。在相等分支中，只把该见证消去到空类型：沿 `a ≡ b` 搬运后，它将使 `a` 先于自身，与非自反性矛盾。所需结果再由该矛盾消去得到。

```agda
  decide : Tri (relOf W a b) (a ≡ b) (relOf W b a) → relOf W a b
  decide (lt k) = k
  decide (eq q) = Empty.rec (PT.rec Empty.isProp⊥
    (λ k → SWO.irr∙ W a (subst (relOf W a) (sym q) k)) h)
  decide (gt k) = Empty.rec (PT.rec Empty.isProp⊥
```

在反向分支中，若有正向见证，把它与反向比较按传递性复合，也会使 `a` 先于自身。此处打开截断只为证明这个矛盾。因此，`strict` 虽返回一项比较见证，却没有证明比较见证本身构成命题，也没有选出某个优先证明。

```agda
    (λ j → SWO.irr∙ W a (SWO.trans∙ W a b a j k)) h)
```

## 层处的关系是什么

对索引 `α`，`Related α z` 在命题截断意义下断言：`z` 是 `Lset α` 的两个成员所成的 Kuratowski 对，且这两个成员由层序关联。序数性证书在类的内部量化，因此该类不依赖于一份选定的 `α` 为序数的证明。端点分解与比较见证都留在各自的截断边界内。

```agda
Related : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
Related α z = ∃[ oα ∶ IsOrd α ] (∃[ a ∶ Mem (Lset α) ] (∃[ b ∶ Mem (Lset α) ]
  ((z ≡ pr (fst a) (fst b)) , setIsSet z (pr (fst a) (fst b))) ⊓ Ordering α oα a b))
```

模型集合 `r` 实现这个类，是指对每个模型元素 `z`，`r` 的成员关系与 `Related α` 双向一致。向外蕴含排除无关或形状错误的成员，向内蕴含纳入每个被关联的对。这里只量化模型元素已经足够，因为可构造性具有传递性，可构造集的每个成员都能再次打包为模型元素。

```agda
Realizes : V ℓ → S → hProp (ℓ-suc ℓ)
Realizes α r = ∀[ z ∶ S ] ((fst z ∈ fst r) ⇒ Related α (fst z))
                        ⊓ (Related α (fst z) ⇒ (fst z ∈ fst r))
```

`IsRel α r` 是上述精确成员规格的证据类型。它断言 `r` 实现宿主层定义的类；它既不为 `r` 添加严格序结构，也不声称该关系满足某条对象语言良序公式。

```agda
IsRel : V ℓ → S → Type (ℓ-suc ℓ)
IsRel α r = ⟨ Realizes α r ⟩
```

实现证明中的两条蕴含，在「`z` 属于 `r`」与「`z` 在 `α` 处被关联」这两个命题之间确定一条路径。后文每当需要在任意实现者的成员关系与语义类之间转换时，就使用这条逐点路径改写。

```agda
rel-path : (α : V ℓ) (r : S) → IsRel α r
         → (z : S) → (fst z ∈ fst r) ≡ Related α (fst z)
rel-path α r p z =
  ⇔toPath {P = fst z ∈ fst r} {Q = Related α (fst z)} (p z .fst) (p z .snd)
```

若 `r` 与 `r'` 都实现该类，则两者的成员命题逐点一致，`L` 中的外延性遂认同这两个集合。这里证明的是实现集合的唯一性；它并不把 `Related` 中经过截断的序数证书、端点分解或比较见证变成唯一选定的资料。

```agda
rel-unique : (α : V ℓ) (r r' : S) → IsRel α r → IsRel α r' → r ≡ r'
rel-unique α r r' p q = extensionalL
  (λ z → rel-path α r p z ∙ sym (rel-path α r' q z))
```

正向读式从指定的成员 `a,b` 与一项实际的层序比较出发。其底层集组成编码对，而序数证书、两个打包成员与截断后的比较共同给出 `Related` 的见证。见证是在各层截断内部构造的，因此这里没有从截断信息中提取选择。

```agda
module _ (α : V ℓ) (oα : IsOrd α) (a b : Mem (Lset α)) where
  related-in : relOf (orderAt α oα) a b → ⟨ Related α (pr (fst a) (fst b)) ⟩
  related-in h = ∣ oα , ∣ a , ∣ b , (refl , ∣ h ∣₁) ∣₁ ∣₁ ∣₁
```

反向读式刻意采用更窄的形状。输入对象已经被呈现为固定端点 `a,b` 的编码对；只有在这种呈现下，证明才能把存在性表示中的对与这两个端点比较，并恢复它们的层序比较。它不会把任意被关联对象分解成一对选定端点。

```agda
  related-out : ⟨ Related α (pr (fst a) (fst b)) ⟩ → relOf (orderAt α oα) a b
  related-out h = strict α oα a b (PT.rec squash₁ atOrd h)
    where
    atPair : (o : IsOrd α) (a' b' : Mem (Lset α))
           → (pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
```

设截断记录给出端点 `a',b'` 与序数性证明 `o`。两条编码对的相等分别认同 `a` 与 `a'`、`b` 与 `b'`；序数性的命题性则认同 `o` 与固定证明 `oα`。沿这三项认同搬运被记录的比较，便得到固定端点处的截断比较。

```agda
           → ⟨ Ordering α o a' b' ⟩ → ⟨ Ordering α oα a b ⟩
    atPair o a' b' q = PT.map
      (λ k → subst2 (relOf (orderAt α oα)) (sym ea) (sym eb)
        (subst (λ o' → relOf (orderAt α o') a' b') (isPropIsOrd α o oα) k))
      where
```

对编码的单射性先恢复底层端点集的相等。每个端点都是由集合及其属于 `Lset α` 的证明组成的依值对；由于该证明是命题，第一分量的相等可以提升为完整成员的相等。比较因而能在正确的依值类型中搬运。

```agda
      ea : a ≡ a'
      ea = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .fst)
      eb : b ≡ b'
      eb = Σ≡Prop (λ x → snd (x ∈ Lset α)) (pr-inj q .snd)
```

外层序数证书是显式的，而两个端点都只在命题截断下存在。因此，消去逐层进入命题 `Ordering α oα a b`。这个目标允许证明临时使用代表，却不会让任一端点作为选定资料逸出。

```agda
    atOrd : Σ[ o ∈ IsOrd α ] ⟨ ∃[ a' ∶ Mem (Lset α) ] (∃[ b' ∶ Mem (Lset α) ] ((pr (fst a) (fst b) ≡ pr (fst a') (fst b'))
                 , setIsSet _ (pr (fst a') (fst b'))) ⊓ Ordering α o a' b') ⟩
          → ⟨ Ordering α oα a b ⟩
    atOrd (o , h₁) = PT.rec squash₁
      (λ { (a' , h₂) → PT.rec squash₁
```

两个临时端点都被打开后，对齐有序对的论证给出 `a,b` 处的截断比较；随后 `strict` 把这一特定截断比较化为所需见证。复合后的证明完成反向读式，同时保留所有存在量词的截断边界，只有经三岐性论证的比较见证被恢复出来。

```agda
        (λ { (b' , (q , hr)) → atPair o a' b' q hr }) h₂ }) h₁
```

## 凡实现那个类者，读在两种形状上

真正有用的表示引理针对任意实现 `Related α` 的 `r`，而不限于递归最终构造的关系。这样，较低层表中已经记录的关系取值便能立即被读取。固定序数性证明 `oα` 后，`Lset α` 的每个成员都是可构造的，因而可以打包成模型元素。

```agda
module _ (α : V ℓ) (oα : IsOrd α) (r : S) (hr : IsRel α r) where
  private
    memL : Mem (Lset α) → S
    memL c = fst c , Lset→isL α oα (fst c) (snd c)
```

模型中由打包端点组成的内部有序对，与其底层集在宿主层组成的 Kuratowski 对在命题上相等，但二者不被当作定义性相同。把「属于 `r`」施于这条等式，便得到第一条搬运桥。

```agda
    atRel : (a b : Mem (Lset α))
          → (fst (prʟ (memL a) (memL b)) ∈ fst r)
          ≡ (pr (fst a) (fst b) ∈ fst r)
    atRel a b = cong (λ x → x ∈ fst r) (prʟ-fst (memL a) (memL b))
```

把 `Related α` 施于同一条有序对等式，得到语义一侧的配套桥。两条桥结合起来，便可先在内部有序对处使用实现证明，再把结论改述为底层集的朴素有序对，反向亦然。

```agda
    atRelated : (a b : Mem (Lset α))
              → ⟨ Related α (fst (prʟ (memL a) (memL b))) ⟩
              ≡ ⟨ Related α (pr (fst a) (fst b)) ⟩
    atRelated a b = cong (λ x → ⟨ Related α x ⟩) (prʟ-fst (memL a) (memL b))
```

填充方向从两个成员的一项宿主层比较出发。`Related` 的正向读式把它化为编码对的关联性，实现证明再把关联性化为属于 `r`，最后由有序对桥把陈述搬回宿主对。因此，`orderAt` 所比较的每一对都属于任意实现集合。

```agda
  rel-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
           → ⟨ pr (fst a) (fst b) ∈ fst r ⟩
  rel-fill a b h = subst ⟨_⟩ (atRel a b)
    (hr (prʟ (memL a) (memL b)) .snd
      (transport (sym (atRelated a b)) (related-in α oα a b h)))
```

读取方向反向走过同一条路径。宿主对的成员关系先搬到内部对处，经实现证明向外读成 `Related` 事实，再搬回固定的宿主对，最终由 `related-out` 化为未截断的层序比较。

```agda
  rel-rep : (a b : Mem (Lset α))
          → ⟨ pr (fst a) (fst b) ∈ fst r ⟩ → relOf (orderAt α oα) a b
  rel-rep a b h = related-out α oα a b
    (transport (atRelated a b)
      (hr (prʟ (memL a) (memL b)) .fst (subst ⟨_⟩ (sym (atRel a b)) h)))
```

后续有些论证使用小呈现 `⟪ Lset α ⟫`，而不直接使用依值成员对。呈现中的索引嵌入底层集合，并携带恰好足以组成 `Mem (Lset α)` 元素的成员证明。

```agda
  private
    atIx : ⟪ Lset α ⟫ → Mem (Lset α)
    atIx m = ⟪ Lset α ⟫↪ m , memOf (Lset α) m
```

沿这个呈现搬运 `orderAt`，得到小索引类型上的严格序。这只是同一比较经嵌入后的读法，因此相应的表示定理无须新的序论论证。

```agda
  open SWO (carry (Lset α) (orderAt α oα)) using () renaming ( _<∙_ to _≺ᶜ_ )
```

对呈现索引 `u,v`，搬运后的比较先被读成相应层成员之间的比较。先前的填充定理随后把嵌入端点所成的 Kuratowski 对放入 `r`。这就是从比较到成员关系的小索引形式。

```agda
  ixRel-fill : (u v : ⟪ Lset α ⟫) → u ≺ᶜ v
             → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩
  ixRel-fill u v = rel-fill (atIx u) (atIx v)
```

反过来，嵌入端点所成的对属于 `r`，经先前定理读成相应层成员的比较。按照搬运序的定义，这恰是小呈现中 `u` 与 `v` 的严格比较。

```agda
  ixRel-rep : (u v : ⟪ Lset α ⟫)
            → ⟨ pr (⟪ Lset α ⟫↪ u) (⟪ Lset α ⟫↪ v) ∈ fst r ⟩ → u ≺ᶜ v
  ixRel-rep u v = rel-rep (atIx u) (atIx v)
```

## 一张表记录了什么

第一项表条件是已记录取值的可靠性。若索引 `c` 位于 `B` 以下，且编码条目 `(c,r)` 属于 `h`，则 `r` 必须实现 `Related c`。这项条件不约束第一分量位于 `B` 之外的条目，因而不能单独刻画表的定义域。

```agda
Values : S → V ℓ → Type (ℓ-suc ℓ)
Values h B = (c r : S) → ⟨ fst c ∈ B ⟩
           → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → IsRel (fst c) r
```

第二项条件是界下的全定义性。每个 `c ∈ B` 都有某个被记录取值 `r`，但这项存在经过命题截断。因此，`Entries` 恰好供给命题性步进论证所需的信息，却不提供在每个索引处选取一个取值的全局函数。

```agda
Entries : S → V ℓ → Type (ℓ-suc ℓ)
Entries h B = (c : S) → ⟨ fst c ∈ B ⟩
            → ∥ (Σ[ r ∈ S ] ⟨ pr (fst c) (fst r) ∈ fst h ⟩) ∥₁
```

第三项条件排除界外条目：`h` 中每个编码对的第一分量都属于 `B`。它与 `Entries` 合用，给出把一张完成的表反建为逼近时所需的精确定义域。正向证明已记录取值正确时只需前两项条件，所以 `Domain` 被单独保留。

```agda
Domain : S → V ℓ → Type (ℓ-suc ℓ)
Domain h B = (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩ → ⟨ fst c ∈ B ⟩
```

## 那一步，取作参数

递归构造现在假设两条具有同一语义的公式。`Cond b f` 是变元槽形式，用于逼近表在图中被绑定时；`Cond₀ B F` 是常元形式，用于固定序数与完成的表作为分离的参数时。第一条充分性等式假设序数性以及 `Values` 与 `Entries`，随后对每个被检验对象，把变元形式的满足关系与相应的 `Related` 认同起来。

```agda
module Described
  (Cond : ∀ {n} → Fin n → Fin n → Formula S (suc n))
  (Cond₀ : S → S → Formula S 1)
  (cond-spec : ∀ {n} (b f : Fin n) (γ : S ^ n) → IsOrd (fst (lookup b γ))
             → Values (lookup f γ) (fst (lookup b γ))
```

变元形式的假设是逐点且真正双向的：它既把满足公式的编码对象读成被关联的对，也从关联性构造公式的满足。这里仅要求序数以下条目的正确性与命题截断下的存在性，并不假设精确定义域，因此可能的界外条目不参与这项语义认同。

```agda
             → Entries (lookup f γ) (fst (lookup b γ))
             → (z : S)
             → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z))
  (cond₀-spec : (b f : S) → IsOrd (fst b)
              → Values f (fst b) → Entries f (fst b)
```

当序数与表已成为固定模型元素后，常元形式的等式给出同样的逐点等价。分离所用的定义公式只为可能的关系成员保留一个自由槽，因此需要这种第二种呈现。该等式认同两种语境的含义，而不声称 `Cond` 与 `Cond₀` 在语法上相等。

```agda
              → (z : S) → ((z ∷ []) ⊨ Cond₀ b f) ≡ Related (fst b) (fst z))
  where
```

给定变元条件后，`StepAt v b f` 外延地刻画候选取值：一个对象属于槽位 `v` 中的取值，当且仅当它满足 `Cond b f`。这是一项双向成员规格，而不是存在定理。实现该规格的实际集合将在后面的递归中由替换与分离产生。

```agda
  StepAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  StepAt v b f = extAt v (Cond b f)
```

固定候选取值、序数索引与较低层表的三个槽位，并给定一个满足序数性、取值可靠性与命题截断下表项存在性的环境。在这些假设下，充分性等式为条件给出统一的逐点含义。随后的两条读式将从相反方向使用它：外延步进规格产生候选取值的 `IsRel` 证明，而已有的 `IsRel` 证明填充该规格。在后续章节给出具体实例以前，整个构造始终以这条假设的步进描述为参数。

```agda
  module _ {n : ℕ} (v b f : Fin n) (γ : S ^ n)
           (ob : IsOrd (fst (lookup b γ)))
           (vals : Values (lookup f γ) (fst (lookup b γ)))
           (ents : Entries (lookup f γ) (fst (lookup b γ))) where
    private
```

固定序数界、健全的表以及每个较小实参处的条目后，条件的变元形式便有了精确的数学含义：一个集合满足它，当且仅当它是该层序所关联的有序对之一。这条等价是对象语言步进与宿主层关系之间的语义桥梁。

```agda
      same : (z : S) → ((z ∷ γ) ⊨ Cond b f) ≡ Related (fst (lookup b γ)) (fst z)
      same = cond-spec b f γ ob vals ents
```

设一个候选取值满足此外延步进。对该取值的隶属先推出条件成立，再由语义桥得到关联性；反过来，关联性推出条件成立，继而推出隶属。两条蕴含合在一起，恰好说明候选取值实现所选序数处的关系。

```agda
    step-rel : ⟨ γ ⊨ StepAt v b f ⟩ → IsRel (fst (lookup b γ)) (lookup v γ)
    step-rel h z =
        (λ hz → subst ⟨_⟩ (same z) (extAt-out v (Cond b f) γ h z hz))
      , (λ hz → extAt-in v (Cond b f) γ h z (subst ⟨_⟩ (sym (same z)) hz))
```

同一论证也可反向使用。若一个集合已经实现该层关系，就能把它的两条隶属蕴含沿语义等价搬运，得到此外延步进。因此，在序数与表的假设齐备时，步进公式的满足与关系的实现携带相同的信息。

```agda
    step-table : IsRel (fst (lookup b γ)) (lookup v γ) → ⟨ γ ⊨ StepAt v b f ⟩
    step-table sp = extAt-in-both v (Cond b f) γ
      (λ z hz → subst ⟨_⟩ (sym (same z)) (sp z .fst hz))
      (λ z h → sp z .snd (subst ⟨_⟩ (same z) h))
```

## 诸逼近，与那个图

现在把通用递归形状专用于这条步进。逼近是集合编码的表，它具有指定定义域，并使每个已记录条目满足相应步进；图断言存在这样的逼近来支撑当前实参处的取值；成对图则把实参与该取值一起记录。相应的引入和消去原则使后文能按这些含义推理，而不必从命题截断的存在中选出见证。

```agda
  module A = RecShape StepAt
  open A using ( ApproxAt; GraphAt; ApproxAt-dom; ApproxAt-value; ApproxAt-step
               ; ApproxAt-in; GraphOf; Graph-in; Graph-out
               ; PairGraphAt; PairOf; PairGraph-in; PairGraph-out )
```

## 逼近所记录的每个取值

为了证明逼近只记录正确取值，先固定其表与定义域，再考察一个可能的实参 `u`。归纳性质说：若 `u` 可构造且为序数，则每个已记录对 `(u,r)` 的取值 `r` 都实现 `u` 处的关系。这里有意对所有已记录取值量化，因此没有预先假设单值性。

```agda
  module _ {n : ℕ} (f a : Fin n) (γ : S ^ n) where
    private
      Value : V ℓ → Type (ℓ-suc ℓ)
      Value u = ⟨ isL u ⟩ → IsOrd u → (r : S)
              → ⟨ pr u (fst r) ∈ fst (lookup f γ) ⟩ → IsRel u r
```

证明对已记录实参 `c` 的底层集合作沿成员关系的归纳。上述性质取值于一般的类型，仍可使用这条原则，因为沿成员关系的归纳允许任意依值类型族，并不只允许命题。逼近的定义域另有序数性假设，以保证一个已记录实参以下的成员仍落在该定义域内。

```agda
    approx-val : ⟨ γ ⊨ ApproxAt f a ⟩ → IsOrd (fst (lookup a γ))
               → (c : S) → IsOrd (fst c) → (r : S)
               → ⟨ pr (fst c) (fst r) ∈ fst (lookup f γ) ⟩ → IsRel (fst c) r
    approx-val h oa c = ∈-induction {P = Value} go (fst c) (snd c)
      where
```

在归纳步中，设 `r` 是记录在 `u` 处的取值。逼近本身断言这个条目满足由同一张表计算出的递归步进。要把该步进读成 `u` 处关系的实现，还需给出表在 `u` 以下的健全性与完备性；这两项义务分别由归纳假设和定义域信息解决。

```agda
      go : (u : V ℓ) → ((t : V ℓ) → ⟨ t ∈ u ⟩ → Value t) → Value u
      go u IH hu ou r p = step-rel zero (suc zero) (sh2 f) (r ∷ d ∷ γ) ou vals ents
        (ApproxAt-step f a γ h d r p)
        where
        d : S
```

实参 `u` 与其可构造性证明打包后，便可作为模型中的元素使用。由于 `(u,r)` 已被记录，逼近的精确定义域子句推出 `u` 属于逼近的序数定义域。正是在这里，关于一个表条目的事实转化成了所有更小递归调用所需的界。

```agda
        d = u , hu
        u∈a : ⟨ u ∈ fst (lookup a γ) ⟩
        u∈a = ApproxAt-dom f a γ h d r p
        vals : Values (lookup f γ) u
        vals e t e∈ q =
```

对于满足 `e∈u` 的条目 `(e,t)`，归纳假设证明 `t` 实现 `e` 处的关系；序数的成员法则同时给出 `e` 的序数性。完备性的来源不同：逼近定义域的传递性把 `e∈u` 与 `u` 属于定义域合成为 `e` 属于定义域，随后逼近以命题截断形式给出那里存在某个取值。因此，`u` 处的递归步进得到了全部所需前提。特别地，同一实参处的两个已记录取值都实现同一个类，故以后可由外延唯一性认同它们；此处并未引入另一个具名的唯一性引理。

```agda
          IH (fst e) e∈ (snd e) (mem-ord {A = u} ou (fst e) e∈) t q
        ents : Entries (lookup f γ) u
        ents e e∈ = ApproxAt-value f a γ h e (oa .fst {x = u} {y = fst e} e∈ u∈a)
```

## 图对别的什么都不成立

图的断言只以命题截断形式包含支撑它的逼近见证。不过，所需结论「图中取值实现序数实参处的关系」本身是命题，因此可以把该命题截断消去到此结论中。这一步确立图取值的正确性；若要得到唯一性，仍须再用外延性比较两个实现集合。

```agda
  module _ {n : ℕ} (w b : Fin n) (γ : S ^ n) where
    graph-only : ⟨ γ ⊨ GraphAt w b ⟩ → IsOrd (fst (lookup b γ))
               → IsRel (fst (lookup b γ)) (lookup w γ)
    graph-only h ob = PT.rec (snd (Realizes (fst (lookup b γ)) (lookup w γ)))
      read (Graph-out w b γ h)
```

在这个命题目标内打开图见证后，可以得到逼近 `f` 以及界处的外层步进。只要知道 `f` 在界下每个实参处都有正确取值与条目，就能把该步进读成关系实现。这两项事实从逼近本身恢复，无须重新假设。

```agda
      where
      read : GraphOf w b γ → IsRel (fst (lookup b γ)) (lookup w γ)
      read (f , (ha , hs)) = step-rel (suc w) (suc b) zero (f ∷ γ) ob vals ents hs
        where
        vals : Values f (fst (lookup b γ))
```

`f` 所记录每个取值的正确性来自前面的沿成员关系归纳结论，并逐一应用于序数界的成员；`mem-ord` 保证这些成员仍是序数。界下的完备性则正是逼近精确定义域规格中「存在取值」的方向。因此，外层步进给出所需的关系实现。

```agda
        vals c r c∈ p = approx-val zero (suc b) (f ∷ γ) ha ob c
          (mem-ord {A = fst (lookup b γ)} ob (fst c) c∈) r p
        ents : Entries f (fst (lookup b γ))
        ents = ApproxAt-value zero (suc b) (f ∷ γ) ha
```

反方向从一张表 `h` 开始：它在某个序数界上健全，在界下每点都有条目，而且没有第一分量落在界外的已记录对。若所提议的当前取值实现界处关系，这些资料便足以把 `h` 展示为图所隐藏的逼近，并验证图的外层步进。

```agda
    graph-table : (h : S) → IsOrd (fst (lookup b γ))
                → Values h (fst (lookup b γ)) → Entries h (fst (lookup b γ))
                → Domain h (fst (lookup b γ))
                → IsRel (fst (lookup b γ)) (lookup w γ) → ⟨ γ ⊨ GraphAt w b ⟩
    graph-table h ob vals ents dom sp = Graph-in w b γ h approx
```

外层步进由关系实现假设经反向语义桥直接得到，余下任务是构造逼近。逼近的定义域必须精确：某个第一分量出现在表的某条记录中，当且仅当它属于该界。两个方向分别使用不同的表假设，从而不把健全性、完备性与有界性混为一谈。

```agda
      (step-table (suc w) (suc b) zero (h ∷ γ) ob vals ents sp)
      where
      onDom : (c : S)
            → (⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩
               → ⟨ fst c ∈ fst (lookup b γ) ⟩)
```

若某个取值记录在 `c` 处，该取值的见证位于命题截断中。由于结论「`c` 属于该界」是命题，可以把命题截断消去到这个结论，再由有界性完成证明。反过来，完备性为界中的每个 `c` 给出仅存在意义下的已记录取值。两方向合起来，得到逼近所需的精确定义域。

```agda
            × (⟨ fst c ∈ fst (lookup b γ) ⟩
               → ⟨ ∃[ r ∶ S ] pr (fst c) (fst r) ∈ fst h ⟩)
      onDom c = (λ hr → PT.rec (snd (fst c ∈ fst (lookup b γ)))
                          (λ { (r , p) → dom c r p }) hr)
              , ents c
```

逼近的第二个子句在每个已记录对 `(c,r)` 处检查递归步进。它仍使用同一张表 `h`，但只使用与 `c` 以下部分有关的资料。因此，每个现有条目都要局部考察：`c` 必须是序数，其下所有已记录取值都必须正确，并且每个更小实参都必须有条目。

```agda
      onStep : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
             → ⟨ (r ∷ c ∷ h ∷ γ) ⊨ StepAt zero (suc zero) (suc (suc zero)) ⟩
      onStep c r p = step-table zero (suc zero) (suc (suc zero)) (r ∷ c ∷ h ∷ γ)
        oc vals' ents' (vals c r c∈ p)
        where
```

有界性先把已记录对转化为 `c` 属于外围界。由于该界是序数，`c` 也为序数。此时可以把健全性限制到 `c` 以下：只要条目 `(e,t)` 确实被记录，有界性便把 `e` 放回外围界，原来的健全性陈述因而适用。

```agda
        c∈ : ⟨ fst c ∈ fst (lookup b γ) ⟩
        c∈ = dom c r p
        oc : IsOrd (fst c)
        oc = mem-ord {A = fst (lookup b γ)} ob (fst c) c∈
        vals' : Values h (fst c)
```

局部健全性与局部完备性的来源并不对称。健全性只需知道某条目已被记录，因为有界性可恢复其对外围定义域的隶属。完备性则从 `e∈c` 出发，利用外围序数的传递性和 `c` 属于该界得到 `e` 属于该界，随后原来的完备性假设在 `e` 处给出条目。

```agda
        vals' e t _ q = vals e t (dom e t q) q
        ents' : Entries h (fst c)
        ents' e e∈ = ents e (ob .fst {x = fst c} {y = fst e} e∈ c∈)
```

精确定义域等价与逐条目的局部步进恰是逼近的两个合取项。把它们合在一起，`h` 就成为图中所隐藏逼近的见证。再结合已经验证的外层步进，便完成从健全、完备且有界的表到图断言的方向。

```agda
      approx : ⟨ (h ∷ γ) ⊨ ApproxAt zero (suc b) ⟩
      approx = ApproxAt-in zero (suc b) (h ∷ γ)
        (domAt-intro zero (suc b) (h ∷ γ) onDom) onStep
```

## 成对的那个图

替换作用于一张以完整表项为取值的图。因而，`PairGraphAt` 断言所显示的取值是当前索引与某个关系集组成的 Kuratowski 对，并且该关系集在此索引处满足 `GraphAt`。它的两条读式都把关系集见证保留在命题截断之内。这就把取值为关系集的递归连接到由带索引条目组成的替换图像。

## 那张表，与界上的那个关系

类 `Recorded B` 描述界 `B` 以下一张表应有的成员。一个对象属于该类，是指以命题截断形式存在模型元素 `c` 与 `r`，其中 `c` 属于 `B`，`r` 实现 `c` 处的关系，而且该对象等于二者底层集合组成的有序对。定义本身不要求 `B` 为序数；在序数界上使用这个类时，序数性才发挥作用。

```agda
  Recorded : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  Recorded B z = ∃[ c ∶ S ] (fst c ∈ B) ⊓ (∃[ r ∶ S ]
    ((z ≡ pr (fst c) (fst r)) , setIsSet z (pr (fst c) (fst r)))
    ⊓ Realizes (fst c) r)
```

模型中的集合若要成为 `B` 的表，它的隶属必须逐点等价于属于 `Recorded B`。两个方向都不可缺少：一个排除不相关对象和定义域外对象，另一个纳入每个满足 `c∈B` 且 `r` 实现 `c` 处关系的对 `(c,r)`。因此，`IsTable` 表达的是精确表示，而不只是对正确条目的封闭性。

```agda
  IsTable : V ℓ → S → Type (ℓ-suc (ℓ-suc ℓ))
  IsTable B h = (z : S) → (fst z ∈ fst h) ≡ Recorded B (fst z)
```

`α` 处的递归资料包含模型中的两个集合：一张精确表示 `α` 以下所有正确条目的表，以及一个实现 `α` 本身之关系的集合。处理更大实参时，第一个分量提供验证逼近所需的既有表，第二个分量提供要写入后续表的关系取值。这个包是沿成员关系递归返回的数据。这里没有证明其类型是命题，也不需要这样的证明，因为沿成员关系的归纳接受任意 Type 值类型族。

```agda
  Bundle : V ℓ → Type (ℓ-suc (ℓ-suc ℓ))
  Bundle α = Σ[ h ∈ S ] Σ[ r ∈ S ] (IsTable α h × IsRel α r)
```

固定界 `B` 的一张精确表 `h`。要在具体条目处使用其规格，必须对齐两种有序对：模型元素构成的内部对，以及其底层集合构成的宿主层 Kuratowski 对。内部配对的投影律把表的隶属等价搬运到 `(c,r)` 的底层有序对处。

```agda
  module _ (B : V ℓ) (oB : IsOrd B) (h : S) (sp : IsTable B h) where
    private
      atPair : (c r : S)
             → (pr (fst c) (fst r) ∈ fst h) ≡ Recorded B (pr (fst c) (fst r))
      atPair c r = subst (λ x → (x ∈ fst h) ≡ Recorded B x) (prʟ-fst c r)
```

先把精确表规格应用于内部有序对，再经上述投影律阅读所得等价。外围读式虽把 `B` 固定为序数，这一步对齐本身却只使用表规格与有序对的表示，并没有额外的序数论论证。

```agda
        (sp (prʟ c r))
```

现在可以同时从两个方面读取一个实际表条目 `(c,r)`。精确性给出它的已记录分解，由此恢复定义域事实 `c∈B`，以及取值健全性事实「`r` 实现 `c` 处关系」。把这个读式应用于每个条目，就得到 `Domain h B` 与 `Values h B`。

```agda
    table-out : Domain h B × Values h B
    table-out = (λ c r p → read c r p .fst) , (λ c r _ p → read c r p .snd)
      where
      read : (c r : S) → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
           → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
```

`Recorded` 给出的分解位于命题截断中，所以消去它时目标必须为命题。这里的目标是「属于 `B`」与「实现该关系」的积；隶属是命题，关系实现也是命题，二者的积仍是命题。消去的合法性来自这个局部目标，而不是整个包的任何性质。

```agda
      read c r p = PT.rec isPropBoth outer (subst ⟨_⟩ (atPair c r) p)
        where
        isPropBoth : isProp (⟨ fst c ∈ B ⟩ × IsRel (fst c) r)
        isPropBoth = isProp× (snd (fst c ∈ B)) (snd (Realizes (fst c) r))
```

在命题消去的内部，设已记录分解使用的是另一对 `(d,t)`。Kuratowski 对 `(c,r)` 与 `(d,t)` 相等，便迫使它们的第一底层分量相等，也迫使第二底层分量相等。第一条等式用于搬运定义域隶属，第二条等式用于把待读取值与分解中的实现取值对齐。

```agda
        inner : (d t : S) → ⟨ fst d ∈ B ⟩
              → (pr (fst c) (fst r) ≡ pr (fst d) (fst t)) → IsRel (fst d) t
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        inner d t d∈ q hr =
            subst (λ x → ⟨ x ∈ B ⟩) (sym (pr-inj q .fst)) d∈
```

沿第一分量等式可把 `d∈B` 搬运为 `c∈B`。第二底层集合的等式还能提升为模型元素 `r` 与 `t` 的等式，因为二者的可构造性证明都是命题，不携带额外选择。随后同时沿索引等式与取值等式搬运关系实现，便得到恰在 `(c,r)` 处的实现事实。

```agda
          , subst2 IsRel (sym (pr-inj q .fst)) (sym rt) hr
          where
          rt : r ≡ t
          rt = Σ≡Prop (λ x → snd (isL x)) (pr-inj q .snd)
```

最外层的已记录见证先给出 `B` 中的指数 `d`，以及关于其实现取值的另一层命题截断见证。最终所求的两项事实构成命题，所以可以依次消去这两层命题截断；刚才建立的端点等式论证负责处理最内层分解。

```agda
        outer : Σ[ d ∈ S ] ( ⟨ fst d ∈ B ⟩
                  × ⟨ ∃[ t ∶ S ] ((pr (fst c) (fst r) ≡ pr (fst d) (fst t))
                        , setIsSet _ (pr (fst d) (fst t))) ⊓ Realizes (fst d) t ⟩ )
              → ⟨ fst c ∈ B ⟩ × IsRel (fst c) r
        outer (d , (d∈ , hs)) = PT.rec isPropBoth
```

对每个可能的实现取值 `t`，有序对等式都把该见证化为关于 `c` 与 `r` 的所需事实。由于结果不保留 `t`，这里对命题截断的使用并未从表中选择取值；它只证明给定条目具有所需定义域性质与关系实现性质这一命题。

```agda
          (λ { (t , (q , hr)) → inner d t d∈ q hr }) hs
```

表读式的反方向较为直接。给定 `c∈B` 以及实现 `c` 处关系的模型元素 `r`，有序对 `(c,r)` 便具有 `Recorded` 所需的命题截断见证。表的精确性再把这项类隶属转成对 `h` 的隶属，而内部有序对的投影律负责对齐两种表示。

```agda
    table-in : (c r : S) → ⟨ fst c ∈ B ⟩ → IsRel (fst c) r
             → ⟨ pr (fst c) (fst r) ∈ fst h ⟩
    table-in c r c∈ hr = subst ⟨_⟩ (sym (atPair c r))
      ∣ c , (c∈ , ∣ r , (refl , hr) ∣₁) ∣₁
```

在通过分离得到序数 `α` 处的关系之前，需要先在 `L` 中找到一个集合，容纳所有可能的相关有序对。所需的界返回模型集合 `D`，使 `Related α` 中的每个对象都属于 `D`。它只是共同容器，可能含有无关成员；此时并不声称精确性。

```agda
  bound : (α : V ℓ) (oα : IsOrd α)
        → Σ[ D ∈ S ] ((z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst D ⟩)
  bound α oα = d .fst , confine
    where
    ixL : ⟪ Lset α ⟫ → S
```

`Lset α` 的小呈现为其所有成员提供索引。每个索引所呈现的底层集合与其可构造性证明打包，成为模型元素；该证明来自它对可构造层的隶属。于是，每个被呈现端点都可用于内部有序配对。

```agda
    ixL m = ⟪ Lset α ⟫↪ m , Lset→isL α oα (⟪ Lset α ⟫↪ m) (memOf (Lset α) m)
```

呈现索引的有序对形成一个小索引类型。把共同定义域原则应用于这些索引所对应的内部有序对族，便得到模型集合 `D`，其中包含该族的每个成员。这条原则只给出包含关系，既不计算精确像，也不按照层序筛选有序对。

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

共同界不仅要适用于呈现索引，还要适用于 `Lset α` 的普通成员 `a,b`。先用各自的纤维索引表示这两个成员，再对相应内部有序对使用共同界，并沿「被呈现有序对等于宿主层有序对 `pr(fst a,fst b)`」的等式搬运隶属。因此，该层任意两个成员组成的有序对都属于 `D`。

```agda
    onPair : (a b : Mem (Lset α)) → ⟨ pr (fst a) (fst b) ∈ fst (d .fst) ⟩
    onPair a b = subst (λ x → ⟨ x ∈ fst (d .fst) ⟩)
      (prʟ-fst (ixL (fa .fst)) (ixL (fb .fst))
        ∙ cong₂ pr (fa .snd) (fb .snd))
      (d .snd (fa .fst , fb .fst))
```

`a` 与 `b` 的隶属证明把它们分别认同为小呈现中的元素，所得纤维等式对齐两个端点；有序配对的合同性进而对齐两个宿主层有序对。再结合内部配对的投影律，就得到上一段搬运所需的等式。

```agda
      where
      fa = ∈-asFiber {a = fst a} {b = Lset α} (snd a)
      fb = ∈-asFiber {a = fst b} {b = Lset α} (snd b)
```

现取 `Related α` 中的任意对象。它的定义通过三层嵌套且经过命题截断的存在量词，给出序数性证明、`Lset α` 的两个成员 `a,b`，以及把该对象认同为二者有序对的等式；层序比较本身还保留在命题截断之内。目标「属于 `D`」是命题，因此可以逐层消去三层存在量词的命题截断。这个粗略界只依赖两个端点及有序对等式，连截断后的比较事实也无须使用。

```agda
    confine : (z : S) → ⟨ Related α (fst z) ⟩ → ⟨ fst z ∈ fst (d .fst) ⟩
    confine z = PT.rec (snd (fst z ∈ fst (d .fst)))
      (λ { (_ , h₁) → PT.rec (snd (fst z ∈ fst (d .fst)))
        (λ { (a , h₂) → PT.rec (snd (fst z ∈ fst (d .fst)))
          (λ { (b , (q , _)) →
```

由前面的结论，恢复出的两个端点所成有序对已经属于 `D`。沿所恢复有序对等式的反向搬运这项隶属，就得到原对象属于 `D`。这些见证只留在命题证明内部，所以该界并没有为每个相关对象选择端点。

```agda
            subst (λ x → ⟨ x ∈ fst (d .fst) ⟩) (sym q) (onPair a b) }) h₂ }) h₁ })
```

表与当前关系通过沿成员关系的递归同时构造。它的实际输入范围是配有可构造性证明的序数：`α` 同时带有属于 `L` 的证明和序数性证明。递归取值是前述包，而定义被封装，使后文通过规格使用它。该递归允许 Type 值类型族，并不依赖 `Bundle α` 是命题。

```agda
  opaque
    tableAt : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → Bundle α
    tableAt = ∈-induction {P = λ α → ⟨ isL α ⟩ → IsOrd α → Bundle α}
      (build (PairGraphAt zero (suc zero)) refl)
      where
```

在 `α` 处的归纳步中，递归假设说：对 `α` 的每个成员 `δ`，只要给出其可构造性与序数性，就有相应的包。当前任务是产生 `α` 以下的表以及 `α` 处的关系。成对图公式作为显式参数保留，并带有它等于预期公式的证明；这不增加数学假设，只保证替换论证使用的正是那张图。

```agda
      build : (φ : Formula S 2) → φ ≡ PairGraphAt zero (suc zero)
            → (α : V ℓ)
            → ((δ : V ℓ) → ⟨ δ ∈ α ⟩ → ⟨ isL δ ⟩ → IsOrd δ → Bundle δ)
            → ⟨ isL α ⟩ → IsOrd α → Bundle α
      build φ qφ α IH hα oα = rep .fst .fst , (sep .fst .fst , (spec , rspec))
```

序数 `α` 与其可构造性证明组成模型元素 `A`。它将作为考察成对图的内部定义域；其中的成员正是那些更小集合，只要建立其序数性，沿成员关系的递归假设便可处理它们。

```agda
        where
        A : S
        A = α , hα
```

序数 `α` 的每个成员 `c` 本身仍是序数。这项继承的序数性不可缺少，因为递归构造只定义在可构造序数上，而不是任意可构造成员上。取得这份序数性证明不涉及命题截断。

```agda
        ordOf : (c : S) → ⟨ fst c ∈ α ⟩ → IsOrd (fst c)
        ordOf c c∈ = mem-ord {A = α} oα (fst c) c∈
```

对于 `c∈α`，模型元素 `c` 已携带其可构造性证明，而序数成员法则给出其序数性。这些正是应用归纳假设所需的输入。所得结果是 `c` 处的完整包，其中同时含有 `c` 以下的精确表和 `c` 处的关系实现集合。

```agda
        bun : (c : S) → ⟨ fst c ∈ α ⟩ → Bundle (fst c)
        bun c c∈ = IH (fst c) c∈ (snd c) (ordOf c c∈)
```

从 `c` 处的递归包中取出当前关系分量，并把它作为 `c` 处的取值。它是一个具体的模型元素，并非从表的命题截断 `Entries` 字段中抽出的见证。递归之所以把定义域内每个可构造序数处的关系与其下的表一同携带，正是为了得到这样的具体取值。

```agda
        value : (c : S) → ⟨ fst c ∈ α ⟩ → S
        value c c∈ = bun c c∈ .snd .fst
```

与该分量一同存储的规格断言：所选取值实现 `Related c`。这恰是归纳假设所提供的语义正确性。仅凭这项事实，既不能断言该取值满足成对图，也不能断言它与 `c` 组成的有序对已属于一张完成的表。

```agda
        relOK : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → IsRel (fst c) (value c c∈)
        relOK c c∈ = bun c c∈ .snd .snd .snd
```

对每个底层序数属于 `α` 的 `c`，归纳假设已经给出 `c` 处的关系集。替换必须保留产生该关系的索引，因此它的候选取值是 `c` 与这个关系集组成的内部有序对，而不是裸关系集。

```agda
        entry : (c : S) → ⟨ fst c ∈ α ⟩ → S
        entry c c∈ = prʟ c (value c c∈)
```

还须证明这个候选取值落在替换所用的图上。在组成有序对之前，选定的关系集必须满足 `c` 处的递归图。`c` 处的包同时给出其下方的表与该处已实现的关系，而 `c` 属于序数 `α` 又保证 `c` 本身是序数，因而可以应用从表到图的一般论证。

```agda
        below : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
              → ⟨ (value c c∈ ∷ k ∷ c ∷ []) ⊨ GraphAt zero (suc (suc zero)) ⟩
        below c c∈ k = graph-table zero (suc (suc zero))
          (value c c∈ ∷ k ∷ c ∷ []) (bun c c∈ .fst) (ordOf c c∈)
          (reads .snd) ents (reads .fst) (relOK c c∈)
```

下方那张表的精确规格给出该论证所需三项事实中的两项：`c` 以下每个被记录的取值都实现相应关系，并且没有索引在 `c` 之外的有序对被记录。余下的是完备性，即 `c` 的每个成员处都有某个被记录的取值。

```agda
          where
          reads : Domain (bun c c∈ .fst) (fst c) × Values (bun c c∈ .fst) (fst c)
          reads = table-out (fst c) (ordOf c c∈) (bun c c∈ .fst)
                    (bun c c∈ .snd .snd .fst)
          ents : Entries (bun c c∈ .fst) (fst c)
```

若 `e` 是 `c` 的成员，环境序数的传递性便把 `e ∈ c ∈ α` 推成 `e ∈ α`。于是归纳假设给出 `e` 处已实现的关系，而 `c` 处表的精确规格把 `e` 与该关系组成的有序对放入下方表中。这个见证置于命题截断之下返回，恰好符合表完备性的要求。

```agda
          ents e e∈ = ∣ value e e∈' , table-in (fst c) (ordOf c c∈) (bun c c∈ .fst)
                         (bun c c∈ .snd .snd .fst) e (value e e∈') e∈ (relOK e e∈') ∣₁
            where
            e∈' : ⟨ fst e ∈ α ⟩
            e∈' = oα .fst {x = fst c} {y = fst e} e∈ c∈
```

现在可以把关系取值的递归图证明与内部有序对的标准同一视合并。由此，候选条目在 `c` 处满足成对图公式，也就对 `α` 以下每个索引建立了函数性所需的存在方向。

```agda
        holds : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) → ⟨ (entry c c∈ ∷ c ∷ []) ⊨ φ ⟩
        holds c c∈ = PairGraph-in zero (suc zero) (entry c c∈ ∷ c ∷ []) φ qφ
          (value c c∈) (prʟ-fst c (value c c∈)) (below c c∈ (entry c c∈))
```

函数性还要求整个成对取值的唯一性。若另一个 `k` 在 `c` 处满足成对图，读出该公式便会在命题截断之下给出关系集 `r`、`k` 的底层集合与有序对 `(c,r)` 的同一视，以及 `r` 的图证明。可构造论域中的相等是命题，因此可以把这些截断资料消去到所需的相等中。

```agda
        only : (c : S) (c∈ : ⟨ fst c ∈ α ⟩) (k : S)
             → ⟨ (k ∷ c ∷ []) ⊨ φ ⟩ → k ≡ entry c c∈
        only c c∈ k h = PT.rec (isSetS k (entry c c∈)) read
          (PairGraph-out zero (suc zero) (k ∷ c ∷ []) φ qφ h)
          where
```

图证明说明 `r` 实现 `c` 处的关系类；另一方面，归纳假设说明在 `c` 处选定的取值也实现同一个类。因此，实现关系类的集合之外延唯一性把 `r` 与选定取值认同。唯一性是在图的正确性已经建立之后才进入论证的，并不是对下方表所作的假设。

```agda
          read : PairOf zero (suc zero) (k ∷ c ∷ []) φ qφ → k ≡ entry c c∈
          read (r , (q , hg)) = Σ≡Prop (λ x → snd (isL x))
            ( q
            ∙ cong (pr (fst c)) (cong fst (rel-unique (fst c) r (value c c∈)
                (graph-only zero (suc (suc zero)) (r ∷ k ∷ c ∷ []) hg (ordOf c c∈))
```

把已知的 `k` 与 `(c,r)` 的同一视、两个关系集的相等，以及可构造有序对的标准投影路径依次复合，便认同了 `k` 与候选条目的底层集合。可构造性是命题，所以这条底层相等可提升为论域中的相等，唯一性证明至此完成。

```agda
                (relOK c c∈)))
            ∙ sym (prʟ-fst c (value c c∈)) )
```

对每个 `c ∈ α`，刚才的存在性与唯一性在「图取值连同其满足证明」所成的纤维中确定唯一一点。这份唯一存在见证处在命题截断之下，但可缩性本身是命题；因此 `mereFunct` 无须作任何额外选择，就能把该见证转换成替换所要求的可缩纤维。

```agda
        fc : (c : S) → ⟨ c ∈ˢ A ⟩
           → isContr (Σ[ k ∈ S ] ⟨ (k ∷ c ∷ []) ⊨ φ ⟩)
        fc c c∈ = mereFunct φ c ∣ entry c c∈ , (holds c c∈ , only c c∈) ∣₁
```

于是替换可以在内部定义域 `α` 上收集成对图的取值。其结论是一个可缩类型，其中的元素由一个可构造集合及该图像的精确成员关系规格组成。因此得到的是具有唯一规格的图像集，并不是说这个集合的成员构成可缩类型。

```agda
        rep : isContr (SetOf (λ z → ∃[ c ∶ S ] (c ∈ˢ A) ⊓ ((z ∷ c ∷ []) ⊨ φ)))
        rep = hasReplacementL A φ fc
```

表 `H` 取为这项可缩替换结果之中心所给出的可构造集合。与它同行的成员关系规格仍然可用，下面将据此证明 `H` 恰好记录预期的「索引与关系」有序对。

```agda
        H : S
        H = rep .fst .fst
```

所需的表规格是两个命题之间的相等：一边是属于 `H`，另一边是「某个 `α` 以下的索引与一个实现该处关系的集合组成有序对」。这条相等由两个蕴含得到。正向读出替换的成员关系，反向则把任何这样的被记录有序对变回替换图的取值。

```agda
        spec : IsTable α H
        spec z = ⇔toPath toRec fromRec
          where
          toRec : ⟨ fst z ∈ fst H ⟩ → ⟨ Recorded α (fst z) ⟩
          toRec hz = PT.rec squash₁
```

在正向中，替换的成员关系只在命题截断之下给出 `α` 以下的索引 `c`，以及 `z` 在该处满足成对图的证明。先前的唯一性结果把 `z` 与 `c` 处的标准条目认同，而该条目的关系分量已知实现 `c` 处的类。这些事实给出所需的被记录有序对见证，并继续保留命题截断边界。

```agda
            (λ { (c , (c∈ , hp)) → ∣ c , (c∈ , ∣ value c c∈
               , ( cong fst (only c c∈ z hp) ∙ prʟ-fst c (value c c∈)
                 , relOK c c∈ ) ∣₁) ∣₁ })
            (subst ⟨_⟩ (rep .fst .snd z) hz)
```

在反向蕴含中，被记录有序对的见证可以包含任意实现 `c` 处关系类的集合 `r`，未必是上文递归选定的取值。为了复用已经为标准条目建立的成对图证明，论证先把截断见证消去到命题性的满足目标中，再沿两个条目之间的相等搬运该证明。

```agda
          fromRec : ⟨ Recorded α (fst z) ⟩ → ⟨ fst z ∈ fst H ⟩
          fromRec hz = subst ⟨_⟩ (sym (rep .fst .snd z)) (PT.map
            (λ { (c , (c∈ , hr)) → c , (c∈ , PT.rec (snd ((z ∷ c ∷ []) ⊨ φ))
              (λ { (r , (q , hs)) → subst (λ t → ⟨ (t ∷ c ∷ []) ⊨ φ ⟩)
                (sym (Σ≡Prop (λ x → snd (isL x))
```

这条搬运路径始于 `z` 随被记录见证给出的相等，经由外延唯一性把 `r` 换成标准关系取值，最后接上内部有序对的标准投影路径。由于可构造性证明是命题，底层集合的相等即可确定论域中的相等。沿此路径搬运后的图证明把 `z` 放入替换图像，从而完成反向蕴含。

```agda
                  (q ∙ cong (pr (fst c)) (cong fst
                     (rel-unique (fst c) r (value c c∈) hs (relOK c c∈)))
                     ∙ sym (prʟ-fst c (value c c∈)))))
                (holds c c∈) }) hr) }) hz)
```

现在，表的精确规格给出 `H` 在 `α` 以下所记录全部取值的正确性。若 `(c,r)` 属于 `H` 且 `c ∈ α`，读出该规格便知 `r` 实现 `c` 处的关系类。此处无须再作归纳或唯一性论证。

```agda
        tvals : Values H α
        tvals = table-out α oα H spec .snd
```

完备性逐点取得。对每个 `c ∈ α`，`c` 处的递归取值已知实现所需的类，因此表规格把它与 `c` 组成的有序对放入 `H`。所得存在陈述经过命题截断：它证明每个索引处都有条目，却不把某个指定条目纳入完备性陈述。

```agda
        tents : Entries H α
        tents c c∈ = ∣ value c c∈
                    , table-in α oα H spec c (value c c∈) c∈ (relOK c c∈) ∣₁
```

这张表现已给出在 `α` 处读取常元形式步进条件所需的取值正确性与完备性。分离公理在先前构造的共同界内应用该条件，得到具有唯一规格的可构造子集，其成员恰为界中满足该条件的元素。作为 `α` 处候选关系的是这个子集，而不是共同界本身。

```agda
        sep : isContr (SetOf (λ x → (x ∈ˢ bound α oα .fst)
                                  ⊓ ((x ∷ []) ⊨ Cond₀ A H)))
        sep = hasSeparationL (bound α oα .fst) (Cond₀ A H)
```

为证明分离所得集合实现预期的类，先取它的一个成员。分离规格同时给出该元素属于共同界并满足常元条件；这个方向只需第二分量。条件的充分性把该满足证明转换成 `Related α`，从而得到从成员关系到关系类的蕴含。

```agda
        rspec : IsRel α (sep .fst .fst)
        rspec z =
            (λ hz → subst ⟨_⟩ (cond₀-spec A H oα tvals tents z)
                      (subst ⟨_⟩ (sep .fst .snd z) hz .snd))
          , (λ hz → subst ⟨_⟩ (sym (sep .fst .snd z))
```

反过来，满足 `Related α` 的元素由共同界的限制性质可知属于该界。充分性的反向又把同一关系事实转换为对常元条件的满足。这两个分量共同符合分离规格，因而把该元素放入分离所得集合，完成双向的精确实现。

```agda
                      ( bound α oα .snd z hz
                      , subst ⟨_⟩ (sym (cond₀-spec A H oα tvals tents z)) hz ))
```

对同时配有可构造性与序数性证明的层索引 `α`，递归包包含下方的表以及刚由分离得到的关系集。关系 `relL` 选取后者。因此，它的适用范围是 `L` 中所用的可构造序数层索引，而不是没有可构造性见证的任意序数。

```agda
  relL : (α : V ℓ) → ⟨ isL α ⟩ → IsOrd α → S
  relL α hα oα = tableAt α hα oα .snd .fst
```

同行的规格来自同一个包。它精确断言：属于 `relL` 与满足类 `Related α` 相一致；每个成员都表示一个被关联的有序对，而每个被关联的有序对都属于其中。因此，后续论证可以直接使用这条等价，无须重新展开替换与分离的构造。

```agda
  relL-spec : (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) → IsRel α (relL α hα oα)
  relL-spec α hα oα = tableAt α hα oα .snd .snd .snd
```

## 成员就是那个序所关联的诸对

对 `Lset α` 的两个成员 `a` 与 `b`，填充方向把一般的实现引理专用于 `relL`。因此，已经构造好的严格良序 `orderAt α` 中的一条宿主层比较，会把二者底层集合组成的编码有序对放入 `relL`。

```agda
  module _ (α : V ℓ) (hα : ⟨ isL α ⟩) (oα : IsOrd α) where
    relL-fill : (a b : Mem (Lset α)) → relOf (orderAt α oα) a b
              → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
    relL-fill = rel-fill α oα (relL α hα oα) (relL-spec α hα oα)
```

读取方向对同一对层成员给出逆命题：二者编码有序对属于 `relL`，便可恢复 `orderAt α` 中的宿主层比较。两个方向合起来逐点表示这张关系图，供后续的最小性论证使用。它们既不构造新的名字比较，也不在对象语言中断言这张图是良序。

```agda
    relL-rep : (a b : Mem (Lset α))
             → ⟨ pr (fst a) (fst b) ∈ fst (relL α hα oα) ⟩
             → relOf (orderAt α oα) a b
    relL-rep = rel-rep α oα (relL α hα oα) (relL-spec α hα oα)
```

## 小结

在可构造序数层索引 `α` 处，宿主类型论已经给出 `Lset α` 的成员上的严格良序 `orderAt α oα`。`Ordering` 通过命题截断把它的比较化为命题值谓词，`Related` 再把被关联端点的有序对组织成宿主层定义的类。三岐性只允许 `strict` 在端点已经指定时恢复比较；`IsRel`、`relL-fill` 与 `relL-rep` 随后逐点给出这项比较与实现集合之成员关系的精确对应。

实现集合通过间接方式得到。逼近只在其定义域以下记录命题截断意义下存在的取值，而沿成员关系的归纳在不假设单值性的情况下，证明每个已记录取值都实现其自身实参处的类。比较成对图的纤维时，实现集合的外延唯一性才认同相互竞争的取值。`mereFunct` 把所得命题截断下的唯一存在转成可缩性，替换收集 `α` 以下的带索引条目，分离再从共同包含集中切出 `α` 处的关系。递归包同时携带完成的下方表与当前关系，而递归并不要求这个包是命题。

整个构造仍以交给 `Described` 的两种充分对象语言步进形式为参数，后续章节才给出具体描述并解除这个参数。这里的 `relL` 只适用于同时配有 `isL` 与 `IsOrd` 证据的 `α`。它表示已有序的关系图；它既不完成新的名字比较，也不在对象语言中证明这张图是良序。