---
title: "在 L 内部构造序型"
module: L.GCH.OrderType
lang: zh
site: "Bedrock"
description: "在 L 内部构造序型"
stage: "证明 GCH"
reading_order: 109
canonical: https://bedrock.institute/zh/L.GCH.OrderType.html
html: L.GCH.OrderType.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/OrderType.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Recursion, L.Recursion.Graph, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Cardinal, L.DefinableInjection, L.Mostowski]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.OrderType.md, https://bedrock.institute/ja/L.GCH.OrderType.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 在 `L` 内部构造序型

把 `L` 中编码的关系成员表示为小类型后，便可对良基关系作塌缩。传递性进一步保证每个塌缩值都是序数，因而属于 `L`。本章把这些值收集成精确值域 `otL`，并另行收集图 `colTable`；本章没有封装 `otL` 的序数性定理。只有再加入三歧性之后，这张图才成为从原定义域到该值域的编码单射。

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

经典假设在此显式给出，因为后文的一项存在性证明必须判定候选点是否在当前点之前。良基递归本身不需要这项判定；排中律进入之处，是按关系成立与否定义一项统一的替换函数时。

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

固定宇宙层级 `ℓ`，并在可构造载体所需的层级上给定排中律实例。此模块后续的构造都继承这一项经典参数；它没有被隐藏成公理。

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

塌缩将由集合论一阶语言中的公式识别。有序对的隶属与相等提供原子检验，合取、析取、蕴含、否定及无界量词则表达表的各项条件。「对每个前驱」这类看似受限的量化，通过把关系原子放在蕴含前件中表达，而不是使用有界量词构造子。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; ∈-irrefl )
```

整个构造必须协调两种表示。为了进行良基递归，`D` 的成员通过一个小表示来处理；图的条目则仍是累积层级中编码为有序对的集合。表示与有序对编码的单射性，使后文能够从这些表示返回原成员和两个坐标。

```agda
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )
```

证明必须把递归定义的取值与 `L` 内部可满足的公式连接起来。良基递归产生塌缩，递归图把其取值与有序对收集成集合，编码公式再把这些对解释为应用。最后，层定理把每个序数塌缩值放入 `L`。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Recursion {ℓ} lem using ( Recursion; module Of; mereFunct )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; appC; appC-adequate; prʟ; prʟ-fst; svAt; domAt )
```

收集所得的图有两个不同层次的目标。首先，它必须把塌缩表示为 `D` 上全定义的单值关系；此后只有在三歧性下，它才能满足内部单射额外要求的输入唯一性条款。有序对公式表达这张图，而四项单射条件要在分别证明之后才被封装为单射码。

```agda
open import L.Coding.Expressions {ℓ} using ( module PairExpression )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap ) renaming ( module Inj to DefinableInj )
open import L.Mostowski {ℓ} using ( module Mostowski )
```

后文的唯一性论证反复通过成员来比较可构造集合。外延性把逐点的隶属等价化为底层集合的相等，而取值为命题的证据使配对而成的可构造对象之相等不依赖具体证明。这也允许命题截断下的分情形以相等为目标结束，而不抽取固定选择。

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ; isPropΣ; isSetΣSndProp )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

累积层级同时提供外围集合及其成员的小表示。因此，`D` 的一个元素既可视为外围集合，也可视为小索引；隶属关系在两种视角之间传递所需的可构造性证据。层级集合上的后继运算稍后用于把序数塌缩值定位到该序数的后继层。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; _∈ₛ_; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

良基性提供定义并分析塌缩所需的归纳原理。空类型排除不可能的关系情形；当后续论证只需知道前驱或表项存在、而不需选定见证时，命题截断记录这种存在性。

```agda
open import Cubical.Induction.WellFounded using ( WellFounded )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

以 `S` 表示可构造结构的载体。结构隶属 `_∈ˢ_` 表达 `L` 的元素之间的隶属；它不同于下文用于读取外围层级集合之表示的小隶属 `_∈ₛ_`。

```agda
open hPropStructure 𝒮ʟ using ( S; _∈ˢ_ )
```

这些公式将在 `L` 所承载的结构中解释。记号 `S ^ n` 表示由 `n` 个可构造集合组成的环境，而 `γ ⊨ φ` 表示公式 `φ` 在受限的可构造结构内部由环境 `γ` 满足。

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

底层层级载体 `V ℓ` 是 h-集合，而可构造性证据取值于命题。因此，依值对载体 `S` 也是 h-集合，即可构造集合之间的相等是命题。后文遂可把截断分情形消去到载体元素的等式中。

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
```

编码图在底层集合上读取：当 `x` 与 `y` 的底层元素构成的有序对属于 `F` 的底层集合时，记 `F` 对 `x`、`y` 成立。下文每条子句读取的都是这一形状。

```agda
Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

固定可构造集合 `D` 与编码有序对的可构造集合 `R`。假设 `Rsub` 只说明 `R` 中每个实际出现的有序对之两个端点都属于 `D`。形成塌缩时另加良基性与传递性，证明单射性时才再加三歧性。本章始终没有假设关系具有外延性。

```agda
module Collapse (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where
```

`D` 中的隶属被陈述为载体上的一元谓词。

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem x = ⟨ fst x ∈ fst D ⟩
```

该谓词是命题，因为它是被呈现集合的底层集合中的隶属。这一命题性后文有用：某构造可以依赖于隶属证明，而不因此携带任何选择数据。

```agda
  isPropMem : (x : S) → isProp (Mem x)
  isPropMem x = snd (fst x ∈ fst D)
```

`D` 的成员由一个小类型呈现；这个小类型就是该呈现的索引类型。

```agda
  Dom : Type ℓ
  Dom = ⟪ fst D ⟫
```

呈现把其索引嵌入外围层级。

```agda
  ↪ : Dom → V ℓ
  ↪ = ⟪ fst D ⟫↪
```

索引被转回可构造集合：嵌入的成员与沿 `D` 的隶属、由可构造性传递性搬运而来的可构造性证明配对。

```agda
  up : Dom → S
  up m = ↪ m , isL-trans {x = fst D} {y = ↪ m} (member (fst D) m) (snd D)
```

重建出的可构造集合是 `D` 的成员，这由呈现自身的隶属记录给出。

```agda
  up-mem : (m : Dom) → Mem (up m)
  up-mem m = member (fst D) m
```

该表示没有重复索引：两个嵌入成员相等会迫使其索引相等。后文从已知成员 `up b` 恢复索引时，这一点把恢复所得索引认同为 `b` 本身，从而证明收集所得的图含有预期的对 `(↪ b, col b)`。塌缩函数的单射性是另一项结论，并且需要三歧性。

```agda
  Dom≡ : {a b : Dom} → ↪ a ≡ ↪ b → a ≡ b
  Dom≡ {a} {b} e = ↪-inj {a = fst D} {m = a} {n = b} e
```

反过来，`D` 的成员连同其隶属证明，通过取呈现在该成员处的纤维，恢复出一个呈现索引。

```agda
  toDom : (x : S) → Mem x → Dom
  toDom x mx = fst (fiber (fst D) mx)
```

恢复出的索引恰好呈现所给的成员：纤维携带嵌入索引与该成员的同一视。

```agda
  toDom-val : (x : S) (mx : Mem x) → ↪ (toDom x mx) ≡ fst x
  toDom-val x mx = snd (fiber (fst D) mx)
```

码 `R` 在小表示上诱导一条关系：`a ≺ b` 表示由被表示成员 `↪ a` 与 `↪ b` 组成的有序对属于 `R`。良基递归正沿这条关系进行。下面两条引理把它与可构造集合上的 `Holds R (up a) (up b)` 双向连接起来。

```agda
  opaque
    _≺_ : Dom → Dom → Type ℓ
    a ≺ b = ⟨ pr (↪ a) (↪ b) ∈ₛ fst R ⟩
```

对固定索引 `a` 与 `b`，关系类型 `a ≺ b` 是命题，因为它陈述一个层级集合中的隶属。因此，这条关系只记录边是否存在，不包含由某个特定证明携带的额外数据。这项命题性本身并不判定边是否存在；只有后文真正需要这种判定时才使用排中律。

```agda
    isProp≺ : (a b : Dom) → isProp (a ≺ b)
    isProp≺ a b = snd (pr (↪ a) (↪ b) ∈ₛ fst R)
```

编码关系中的隶属给出小关系：`L` 中记录的有序对由两种隶属关系之间的桥识别。

```agda
    ≺-in : (a b : Dom) → Holds R (up a) (up b) → a ≺ b
    ≺-in a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .fst
```

反过来，小关系记录了 `R` 中真实的对，于是关系的两种读法在两个方向上一致。

```agda
    ≺-out : (a b : Dom) → a ≺ b → Holds R (up a) (up b)
    ≺-out a b = ∈∈ₛ {a = pr (↪ a) (↪ b)} {b = fst R} .snd
```

关系 `_≺_` 的良基性提供定义 `col` 所需的递归与归纳。传递性承担另一项作用：它保证前驱链仍位于其上端点之下，从而可以证明每个塌缩值传递并成为序数。这两项假设尚不能保证塌缩单射，也没有把该关系封装成良序。

```agda
  module Col (wf : WellFounded _≺_)
             (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
```

Mostowski 构造把 `col p` 定义为所有前驱 `r ≺ p` 的取值 `col r` 所成的集合。计算律 `col-eq` 把递归取值与这一显式前驱像认同。隶属引理从指定前驱得到 `col r ∈ col p`；反过来，从任意成员只得到命题截断下的前驱存在。`col-ord` 则证明每个单独的 `col p` 都是序数。

```agda
    open Mostowski Dom _≺_ wf ≺-trans public
      using ( module W; col; col-eq; col-in; col-out; col-ord )
```

每个塌缩值都可构造。引理 `col-ord` 先说明 `col p` 是序数；层引理随后把这个序数置于由其后继索引的层中，从而得到 `col-isL p`。

```agda
    opaque
      col-isL : (p : Dom) → ⟨ isL (col p) ⟩
      col-isL p = Lset→isL (sucV (col p)) (suc-ord (col-ord p)) (col p)
                    (ord∈Lset-suc (col p) (col-ord p))
```

每个塌缩值连同其可构造性证明被打包为可构造集合。塌缩因此产出的不只是外围集合，而是可构造宇宙的真实元素。

```agda
    colʟ : Dom → S
    colʟ p = col p , col-isL p
```

## 诸公式

若 `x` 的每个 `R` 前驱 `y` 都在表 `F` 中记录了某个取值 `u`，就称 `F` 在 `x` 处完备。`u` 的存在处于命题截断之下：完备性只保留表项存在这一事实，既不选定某个表项，也尚未断言取值唯一。

```agda
Complete : S → S → S → Type (ℓ-suc ℓ)
Complete F R x = (y : S) → Holds R y x → ∥ Σ[ u ∈ S ] Holds F y u ∥₁
```

谓词 `Src F R x w` 表示：`F` 在 `x` 的某个 `R` 前驱处把 `w` 记录为取值。该前驱及其表项都留在命题截断之下，因为后文只使用由此得到的隶属事实。

```agda
Src : S → S → S → S → Type (ℓ-suc ℓ)
Src F R x w = ∥ Σ[ y ∈ S ] (Holds R y x × Holds F y w) ∥₁
```

值 `v` 对 `x` 是正确的，当其成员恰为来源值：`v` 中的隶属给出一个来源，而每个来源都是成员。两个方向合起来说：`v` 就是所记录的前驱值之集，完全通过隶属读取。

```agda
ValueIs : S → S → S → S → Type (ℓ-suc ℓ)
ValueIs F R x v = (w : S) → (⟨ fst w ∈ fst v ⟩ → Src F R x w)
                          × (Src F R x w → ⟨ fst w ∈ fst v ⟩)
```

若一张表实际包含的每个有序对都在其输入处完备，并且输出恰由前驱取值组成，就称该表正确。这项条件没有指定定义域，因此既不要求覆盖整个 `D`，也不禁止在 `D` 之外出现条目。后文的唯一性定理只在被记录的输入属于 `D` 时，才把相应取值认同为塌缩值。

```agda
Correct : S → S → Type (ℓ-suc ℓ)
Correct F R = (x v : S) → Holds F x v → Complete F R x × ValueIs F R x v
```

公式 `completeAt f R x` 用无界全称量词引入候选前驱 `y`。蕴含只关注 `R` 记录有序对 `(y,x)` 的那些 `y`，其结论再用无界存在量词引入取值 `u`，要求 `F` 记录 `(y,u)`。进入存在量词后，`u` 占据新的第零槽位，原有变量相应后移。

```agda
opaque
  completeAt : ∀ {n} → Fin n → S → Fin n → Formula S n
  completeAt f R x =
    ∀̇ ( appC R zero (suc x)
      ⇒̇ ∃̇ (appAt (suc (suc f)) (suc zero) zero) )
```

要把该公式读成宿主层完备性，先固定前驱 `y` 及 `R` 记录 `(y,x)` 的证明。`appC` 的充分性路径把这一前提化为满足证明 `h` 所需的蕴含前件。应用 `h` 后得到命题截断下的候选取值；`PT.map` 保留该截断，并沿 `appAt` 的充分性路径把其中的图原子化为 `Holds F y u`。

```agda
  complete-out : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
               → ⟨ γ ⊨ completeAt f R x ⟩
               → Complete (lookup f γ) R (lookup x γ)
  complete-out f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ)) q })
```

这一方向的最后一次应用完成上述第一项转换：它沿 `appC-adequate` 搬运已给的关系事实，再把结果交给 `h y`。所得结果仍是对象语言语义产生的截断存在；前几行的映射只改变命题截断内部的内容。

```agda
    (h y (subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p))
```

反过来，假设宿主层完备性。对满足公式前件的候选前驱，先由 `appC-adequate` 把该前件化为 `Holds R y x`。完备性给出命题截断下的取值 `u`，`PT.map` 再把伴随的 `Holds F y u` 搬回存在结论所需的应用原子满足证明。

```agda
  complete-in : ∀ {n} (f : Fin n) (R : S) (x : Fin n) (γ : S ^ n)
              → Complete (lookup f γ) R (lookup x γ)
              → ⟨ γ ⊨ completeAt f R x ⟩
  complete-in f R x γ h y p = PT.map
    (λ { (u , q) → u , subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (u ∷ y ∷ γ))) q })
```

这一行把已满足的关系原子式转换为 `Holds R y x`，再把 `x` 处的完备性施用于候选前驱 `y`。这次应用给出截断取值，外围的映射随后把它转换为对象语言存在量词所需的见证。

```agda
    (h y (subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p))
```

公式 `srcAt f R x w` 用无界存在量词断言某个 `y` 同时是 `x` 的 `R` 前驱，并且 `F` 在输入 `y` 处记录 `w`。对前驱的限制由第一个合取项表达，而不是由有界存在量词表达。

```agda
opaque
  srcAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  srcAt f R x w = ∃̇ ( appC R zero (suc x) ∧̇ appAt (suc f) zero (suc w) )
```

该语义存在式已经处于命题截断之下。定义 `src-out` 的映射保留这一截断，并转换其中每个假定见证 `y`：`appC-adequate` 把第一个合取项读成 `Holds R y x`，`appAt-adequate` 把第二个读成 `Holds F y w`。

```agda
  src-out : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
          → ⟨ γ ⊨ srcAt f R x w ⟩
          → Src (lookup f γ) R (lookup x γ) (lookup w γ)
  src-out f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (appC-adequate R zero (suc x) (y ∷ γ)) p
```

前驱的图隶属闭合该读取。

```agda
      , subst ⟨_⟩ (appAt-adequate (suc f) zero (suc w) (y ∷ γ)) q ) })
```

填充来源是其反向：把前驱引入存在量词，两个原子逆着各自充分性引理搬运。

```agda
  src-in : ∀ {n} (f : Fin n) (R : S) (x w : Fin n) (γ : S ^ n)
         → Src (lookup f γ) R (lookup x γ) (lookup w γ)
         → ⟨ γ ⊨ srcAt f R x w ⟩
  src-in f R x w γ = PT.map (λ { (y , (p , q)) → y
    , ( subst ⟨_⟩ (sym (appC-adequate R zero (suc x) (y ∷ γ))) p
```

图原子最后写入，填充完成。

```agda
      , subst ⟨_⟩ (sym (appAt-adequate (suc f) zero (suc w) (y ∷ γ))) q ) })
```

公式 `valueAt f R x v` 对任意集合 `w` 量化，并同时陈述 `w ∈ v` 与 `srcAt f R x w` 之间的两个方向。因此，它给出 `v` 的外延刻画：`v` 的成员恰是 `x` 的各前驱处所记录的取值。定义展开 `srcAt`，使这一刻画成为一条完整的一阶公式。

```agda
opaque
  unfolding srcAt
  valueAt : ∀ {n} → Fin n → S → Fin n → Fin n → Formula S n
  valueAt f R x v =
    ∀̇ ( ((var zero ∈̇ var (suc v)) ⇒̇ srcAt (suc f) R (suc x) zero)
```

双条件即其两个方向的合取，而来源公式在两个方向内均已展开。

```agda
      ∧̇ (srcAt (suc f) R (suc x) zero ⇒̇ (var zero ∈̇ var (suc v))) )
```

向外读取 `valueAt` 时，要在每个 `w` 处实例化其全称量词。正向蕴含先把 `v` 中的隶属转换为来源公式的满足，`src-out` 再把这份满足读成 `Src F R x w`，从而得到 `ValueIs` 的正向一半。

```agda
  value-out : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
            → ⟨ γ ⊨ valueAt f R x v ⟩
            → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
  value-out f R x v γ h w =
      (λ w∈ → src-out (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))
```

反向对称地经来源填充读取。于是该公式恰在说：`v` 收集来源值；这正是后文唯一性论证所消耗的读法。

```agda
    , (λ s → h w .snd (src-in (suc f) R (suc x) zero (w ∷ γ) s))
```

为证明 `valueAt` 的正向蕴含，取候选取值 `v` 的一个成员 `w`。宿主级取值方程说，在命题截断下，`w` 已经作为 `x` 的某个 `R` 前驱之取值出现。把这条来源陈述向内读取，便在以 `w` 扩展的环境中给出对象语言公式所需的存在见证。

```agda
  value-in : ∀ {n} (f : Fin n) (R : S) (x v : Fin n) (γ : S ^ n)
           → ValueIs (lookup f γ) R (lookup x γ) (lookup v γ)
           → ⟨ γ ⊨ valueAt f R x v ⟩
  value-in f R x v γ h w =
      (λ w∈ → src-in (suc f) R (suc x) zero (w ∷ γ) (h w .fst w∈))
```

对逆向蕴含，先把来源公式的满足读成一种命题截断的存在：某个前驱的表值是 `w`。随后，`ValueIs` 的反向一半证明 `w` 属于所记录的值。因此，`valueAt` 恰好表达相对于候选表的递归取值方程；稍后还须借助良基归纳，才能把这个值认同为 Mostowski 塌缩。

```agda
    , (λ s → h w .snd (src-out (suc f) R (suc x) zero (w ∷ γ) s))
```

正确性只在候选表确实含有表项之处接受检验。两层全称量词遍历实参 `x` 与取值 `v`；若表中含有有序对 `(x,v)`，公式便要求这个表项满足递归步骤所需的两项条件。

```agda
opaque
  unfolding completeAt valueAt
  correctAt : ∀ {n} → Fin n → S → Formula S n
  correctAt f R =
    ∀̇ (∀̇ ( appAt (suc (suc f)) (suc zero) zero
```

这两项条件把存在性与取值方程分开。完备性说，`x` 的每个 `R` 前驱在表中都有某个表项；取值子句则说，`v` 的成员恰是这些前驱表项处出现的取值。除此以外，公式并不规定表的定义域。

```agda
          ⇒̇ ( completeAt (suc (suc f)) R (suc zero)
            ∧̇ valueAt (suc (suc f)) R (suc zero) zero ) ))
```

向外读取公式时，先取表中一个实际表项 `(x,v)`。`appAt` 的充分性把它的隶属证明转换为公式前件所需的证明。在 `x` 与 `v` 处实例化两层量词后，便得到 `x` 处的完备性及相应的取值方程；本行把其中的完备性一半读回宿主级谓词。

```agda
  correct-out : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
              → ⟨ γ ⊨ correctAt f R ⟩ → Correct (lookup f γ) R
  correct-out f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (sym (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ))) p)
    in complete-out (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c
```

第二分量由 `value-out` 读取，得到「属于 `v`」与「作为 `x` 的某个 `R` 前驱之取值出现」之间的等价。它与完备性配对后，证明所选表项在宿主级正确。由于该构造适用于表中每个表项，最终便得到 `Correct F R`。

```agda
     , value-out (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w
```

反过来，设该表在宿主级正确。选定实参 `x`、取值 `v` 与表项 `(x,v)` 后，`appAt` 的充分性把对象语言蕴含的前件转换为相应的宿主级表项。正确性随即给出该表项的完备性与取值方程；本行把其中的完备性一半填入公式。

```agda
  correct-in : ∀ {n} (f : Fin n) (R : S) (γ : S ^ n)
             → Correct (lookup f γ) R → ⟨ γ ⊨ correctAt f R ⟩
  correct-in f R γ h x v p =
    let (c , w) = h x v (subst ⟨_⟩ (appAt-adequate (suc (suc f)) (suc zero) zero (v ∷ x ∷ γ)) p)
    in complete-in (suc (suc f)) R (suc zero) (v ∷ x ∷ γ) c
```

取值方程由 `value-in` 填入，从而补全表项 `(x,v)` 所需的合取。再对选定的两个元素作抽象，便得到两层全称量词。因此，`correct-in` 与 `correct-out` 建立了 `correctAt` 和宿主级谓词 `Correct` 之间的精确对应。

```agda
     , value-in (suc (suc f)) R (suc zero) zero (v ∷ x ∷ γ) w
```

下一个公式固定关系 `R`，但仍以存在量词绑定作为见证的表。这种区分具有数学作用：在尚未构造出覆盖整个定义域的单一表之前，便可先借某张正确表局部识别一个取值。

```agda
module ColFo (R : S) where
```

在环境 `(z ∷ p ∷ [])` 中，该公式说：命题截断地存在集合 `F`，它对 `R` 正确，并含有表项 `(p,z)`。表由存在量词绑定，所以这里只是刻画 `p` 处取值的局部陈述，尚未断言有一张固定表同时适用于整个定义域。

```agda
  opaque
    unfolding correctAt
    colFo : Formula S 2
    colFo = ∃̇ ( correctAt zero R
              ∧̇ appAt zero (suc (suc zero)) (suc zero) )
```

向外读取 `colFo` 时，表见证外面的命题截断仍被保留。存在量词给出表 `F`；在同一截断内部，合取项给出 `F` 对 `R` 正确的证据，以及表示表项 `(p,z)` 的对象语言应用原子式。

```agda
    colFo-out : (z p : S) → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
              → ∥ Σ[ F ∈ S ] (Correct F R × Holds F p z) ∥₁
    colFo-out z p = PT.map (λ { (F , (hc , ha)) → F
      , ( correct-out zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (appAt-adequate zero (suc (suc zero)) (suc zero)
```

`appAt` 的充分性把余下的应用原子式转换为 `Holds F p z`。因此，结果是在命题截断下得到一张正确表及所需表项，这正是该公式的宿主级读法。

```agda
            (F ∷ z ∷ p ∷ [])) ha ) })
```

对向内方向，一张明确给定且含有 `(p,z)` 的正确表 `F` 充当存在见证。正确性证明由 `correct-in` 转入公式；余下任务是用应用原子式表达给定的表项。

```agda
    colFo-in : (z p F : S) → Correct F R → Holds F p z
             → ⟨ (z ∷ p ∷ []) ⊨ colFo ⟩
    colFo-in z p F hc hp = ∣ F
      , ( correct-in zero R (F ∷ z ∷ p ∷ []) hc
        , subst ⟨_⟩ (sym (appAt-adequate zero (suc (suc zero)) (suc zero)
```

反向使用 `appAt` 的充分性，便把 `Holds F p z` 转换为该原子式的满足。随后将表见证、其正确性与这个表项一起置于存在量词的命题截断中，即得 `colFo` 在 `(z,p)` 处的满足。

```agda
            (F ∷ z ∷ p ∷ []))) hp ) ∣₁
```

稍后需要把 `colFo` 这样的逐点取值公式用于定义有序对集合。通用构造 `PairFo` 完成这一转换：它恰在 `z` 于 `p` 处满足给定公式时识别有序对 `(p,z)`。因此，局部塌缩公式能够充当下文递归构造的取值关系。

```agda
open import L.Recursion.Graph {ℓ} lem public using ( module PairFo )
```

## 唯一性、存在性与诸表

内部构造从编码定义域 `D` 与编码关系 `R` 出发。起初唯一的附加条件是：属于 `R` 的每个有序对，其两个坐标都属于 `D`。该模块边界尚未要求良基性与传递性；塌缩论证开始时才会另行给出这两项条件。

```agda
module Internal (D R : S)
                (Rsub : (y x : S) → Holds R y x
                      → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where
```

定义域表示及其编码关系现在成为两种公式构造的共同背景。`CF` 是关系 `R` 的局部塌缩取值公式，`PF` 则识别由实参与满足该公式的取值组成的有序对。此时，这两个构造都尚未断言塌缩取值存在或唯一。

```agda
  open Collapse D R Rsub public
  module CF = ColFo R using ( colFo; colFo-in; colFo-out )
  module PF = PairFo CF.colFo using ( pair-in; pair-out; pairFo )
```

若 `q` 是 `D` 的成员，对其成员证明解码便得到索引 `toDom q mq`。由 `toDom-val`，把该索引重新嵌入后所得元素与 `q` 具有相同的底层迭代集合；又因 `S` 的可构造性分量为命题，底层集合的相等可提升为 `S` 中的相等。

```agda
  up-toDom : (q : S) (mq : Mem q) → up (toDom q mq) ≡ q
  up-toDom q mq = Σ≡Prop (λ v → snd (isL v)) (toDom-val q mq)
```

塌缩公式通过环境的第二槽依赖实参。因此，等式 `x ≡ y` 允许直接在该槽中替换：若取值 `v` 在 `x` 处满足公式，它也在 `y` 处满足公式。稍后正是借此把典范表示 `up (toDom q mq)` 与原元素 `q` 协调起来。

```agda
  colFo-at : (v : S) {x y : S} → x ≡ y
           → ⟨ (v ∷ x ∷ []) ⊨ CF.colFo ⟩ → ⟨ (v ∷ y ∷ []) ⊨ CF.colFo ⟩
  colFo-at v e = subst (λ t → ⟨ (v ∷ t ∷ []) ⊨ CF.colFo ⟩) e
```

此模块现在假定小关系既良基又传递。良基性支撑 `col` 的递归定义以及唯一性证明中的诸次归纳；传递性则用于证明所得塌缩值为序数。这两项假设作用不同，且都不由先前对 `R` 的端点条件推出。

```agda
  module Graph (wf : WellFounded _≺_)
               (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
```

在这两项假设下，Mostowski 递归为每个 `a` 指派集合 `col a`，其成员是诸前驱的塌缩值。相应的引入与消去引理刻画该集合的隶属，而 `col-ord` 证明每个单独的 `col a` 都是序数。这里说的是逐点塌缩值，尚不是稍后收集得到的集合 `otL`。

```agda
    open Col wf ≺-trans public
```

良基性排除了环 `a ≺ a`。在归纳步骤中，若有这样的环，便可把面向前驱的归纳假设施于 `a` 自身；同一份环证明既说明 `a` 比自身更小，也充当归纳假设产出矛盾时的输入。

```agda
    ≺-irrefl : (a : Dom) → a ≺ a → Empty.⊥
    ≺-irrefl = W.induction {P = λ a → a ≺ a → Empty.⊥} (λ a rec h → rec a h h)
```

此处的唯一性陈述以表项已经存在为条件：若正确表 `F` 在真实定义域点 `up a` 记录取值 `v`，则 `v` 的底层集合等于 `col a`。它并不声称每张正确表在 `D` 的每个成员处都有表项。证明对 `a` 作良基归纳，并以所示等式为归纳谓词。

```agda
    correct-val : (F : S) → Correct F R → (a : Dom) (v : S)
                → Holds F (up a) v → fst v ≡ col a
    correct-val F hc = W.induction {P = λ a → (v : S) → Holds F (up a) v → fst v ≡ col a} go
      where
      go : (a : Dom) → ((b : Dom) → b ≺ a → (v : S) → Holds F (up b) v → fst v ≡ col b)
```

证明化归为逐点等价：`w` 属于被记录取值当且仅当 `w` 属于塌缩。从正确性假设提取两个辅助事实：`up a` 处的完备性，以及取值子句。

```agda
         → (v : S) → Holds F (up a) v → fst v ≡ col a
      go a IH v hv = extensionalV {a = fst v} {b = col a} (λ w → ⇔toPath (fwd w) (bwd w))
        where
        cmp : Complete F R (up a)
        cmp = hc (up a) v hv .fst
```

`a` 处表项的正确性有两项互补后果。前面的 `cmp` 为所有前驱提供表项，而 `val` 把对 `v` 的隶属与作为某个前驱取值出现相互认同。接下来的外延性论证在两个方向中以相反次序使用这两项事实。

```agda
        val : ValueIs F R (up a) v
        val = hc (up a) v hv .snd
```

为证第一向包含，取被记录取值 `v` 的成员 `w`。由于 `v` 可构造，成员关系也使 `w` 可构造，故可将其打包为载体元素 `wS`。随后，`val` 的正向一半在命题截断下给出 `a` 的某个 `R` 前驱 `y`，表在该处记录 `wS`。

```agda
        fwd : (w : V ℓ) → ⟨ w ∈ fst v ⟩ → ⟨ w ∈ col a ⟩
        fwd w w∈ = PT.rec (snd (w ∈ col a)) read (val wS .fst w∈)
          where
          wS : S
          wS = w , isL-trans {x = fst v} {y = w} w∈ (snd v)
```

来源条目被转换为所需的两条事实：被载前驱与实参之间的关系，以及被载前驱处的表条目。前驱随后被解码为其内部索引。

```agda
          read : Σ[ y ∈ S ] (Holds R y (up a) × Holds F y wS) → ⟨ w ∈ col a ⟩
          read (y , (ry , fy)) = subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b b≺a)
            where
            my : Mem y
            my = Rsub y (up a) ry .fst
```

内部索引 `b` 由隶属下降而恢复，关系条目被运输为内部形式 `b ≺ a`。等式 `e` 记录 `w` 与 `b` 的塌缩的认同，下一步证明。

```agda
            b : Dom
            b = toDom y my
            b≺a : b ≺ a
            b≺a = ≺-in b a (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val y my)) ry)
            e : w ≡ col b
```

该等式恰是把归纳假设施于解码后的前驱：表在被载前驱处的取值等于其内部索引的塌缩，经运输即等于 `w`。

```agda
            e = IH b b≺a wS (subst (λ t → ⟨ pr t w ∈ fst F ⟩) (sym (toDom-val y my)) fy)
```

为证反向包含，设 `w ∈ col a`。塌缩的消去规则在命题截断下给出某个前驱 `r ≺ a`，并有 `col r ≡ w`。目标 `w ∈ fst v` 是命题，故可以在该截断内部推理。又因 `w` 属于可构造集合 `col a`，所以可把它连同可构造性证据打包为 `wS`。

```agda
        bwd : (w : V ℓ) → ⟨ w ∈ col a ⟩ → ⟨ w ∈ fst v ⟩
        bwd w w∈ = PT.rec (snd (w ∈ fst v)) read (col-out a w w∈)
          where
          wS : S
          wS = w , isL-trans {x = col a} {y = w} w∈ (col-isL a)
```

对 `col-out` 给出的前驱 `r`，`a` 处表项的完备性在命题截断下给出 `up r` 处的某个表值 `u`。由于目标 `w ∈ v` 是命题，可以合法地消去这个截断。接下来只须利用 `r` 处的正确性把 `u` 与 `col r` 比较，进而与 `w` 比较。

```agda
          read : Σ[ r ∈ Dom ] ((r ≺ a) × (col r ≡ w)) → ⟨ w ∈ fst v ⟩
          read (r , (ra , e)) = PT.rec (snd (w ∈ fst v)) inner (cmp (up r) (≺-out r a ra))
            where
            inner : Σ[ u ∈ S ] Holds F (up r) u → ⟨ w ∈ fst v ⟩
            inner (u , fu) = val wS .snd
```

取值方程的反向一半把来源见证转换为对 `v` 的隶属。这里的来源见证由前驱 `up r`、它与 `up a` 的关系，以及取值为 `u` 的表项组成；归纳假设把 `u` 认同为 `col r`，再由等式 `col r ≡ w` 运输该表项，使其取值成为 `w`。

```agda
              ∣ up r , (≺-out r a ra , subst (λ t → ⟨ pr (↪ r) t ∈ fst F ⟩) (IH r ra u fu ∙ e) fu) ∣₁
```

现设 `q` 确为 `D` 的成员，且 `v` 在 `q` 处满足局部塌缩公式。该公式只在命题截断下给出一张含有 `(q,v)` 的正确表；但所求集合等式是命题，故可以消去此截断。把表项从 `q` 运输到其解码表示后，`correct-val` 便把 `fst v` 认同为 `col (toDom q mq)`。

```agda
    colFo-val : (q : S) (mq : Mem q) (v : S) → ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩
              → fst v ≡ col (toDom q mq)
    colFo-val q mq v h = PT.rec (setIsSet (fst v) (col (toDom q mq)))
      (λ { (F , (hc , hv)) → correct-val F hc (toDom q mq) v
             (subst (λ t → ⟨ pr t (fst v) ∈ fst F ⟩) (sym (toDom-val q mq)) hv) })
```

塌缩公式的向外读法供给正确表与表条目，即唯一性引理的两个输入。

```agda
      (CF.colFo-out v q h)
```

局部表模块以域的实参 `a` 与在每个更小实参处提供塌缩公式的归纳假设为参数。它将为 `a` 造一张表：其实真前驱处的条目记录塌缩值，其余条目记录默认对。

```agda
    module Approx (a : Dom)
                  (IH : (b : Dom) → b ≺ a → ⟨ (colʟ b ∷ up b ∷ []) ⊨ CF.colFo ⟩) where
```

默认条目 `ea` 是被载实参与其自身塌缩组成的有序对，呈现为载体元素。

```agda
      ea : S
      ea = prʟ (up a) (colʟ a)
```

局部公式的体有两个析取支。左支说 `q` 是 `a` 的真前驱，且 `z` 把 `q` 与满足塌缩公式的取值配对。右支说 `q` 不是前驱，且 `z` 是默认条目。该情形分裂由排中律判定。

```agda
      Body : S → S → Type (ℓ-suc ℓ)
      Body z q =
          (Holds R q (up a)
             × ∥ Σ[ v ∈ S ] ((fst z ≡ pr (fst q) (fst v)) × ⟨ (v ∷ q ∷ []) ⊨ CF.colFo ⟩) ∥₁)
        ⊎ ((Holds R q (up a) → Empty.⊥) × (fst z ≡ fst ea))
```

为了在对象语言中区分前驱情形与默认情形，关系检验必须提及由变化的实参 `q` 与固定点 `a` 组成的有序对。对表达式在局部公式使用的两个自由槽位中统一给出这个词项。

```agda
      module PE = PairExpression
```

表达式 `image` 表示有序对 `(q,up a)`：第一坐标取自实参槽，第二坐标是表示 `a` 的字面载体元素。因此，`image` 属于 `R` 恰好表示 `q` 是 `a` 的 `R` 前驱；它并不描述局部表的表项。

```agda
      image : PE.Expr 2
      image = PE.pair (PE.slot (suc zero)) (PE.literal (up a))
```

公式 `ψ` 对应 `Body` 的两种情形。若 `q R a`，第一支要求输出 `z` 把 `q` 与某个在 `q` 处满足 `colFo` 的取值配成有序对。若 `q` 不是 `a` 的前驱，第二支要求 `z` 等于固定的默认表项 `ea`。在两支之间作选择的经典判定稍后才用于函数性证明，并不是析取本身的一部分。

```agda
      opaque
        ψ : Formula S 2
        ψ = (PE.member image (con R) ∧̇ PF.pairFo)
          ∨̇ ((¬̇ PE.member image (con R)) ∧̇ (var zero ≐ con ea))
```

向外读取 `ψ` 时，其析取外的命题截断仍被保留。在前驱分支中，对表达式的读式把第一合取项转换为 `q R a`，而 `PF.pair-out` 在命题截断下说明：对某个在 `q` 处满足 `colFo` 的 `v`，`z` 等于 `(q,v)`。在默认分支中，则须把对象语言否定转换为宿主级对 `q R a` 的反驳。

```agda
        ψ-out : (z q : S) → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩ → ∥ Body z q ∥₁
        ψ-out z q = PT.map
          (λ { (inl (h1 , h2)) → inl (PE.member-out image (con R) (z ∷ q ∷ []) h1
                                         , PF.pair-out z q h2)
             ; (inr (h1 , h2)) → inr
```

为得到这份宿主级反驳，暂设 `q R a`。对表达式的向内读法把该假设转换为隶属原子式的满足，而对象语言否定排除了这种满足。把 `z` 认同为默认表项的等式已经具有所需的宿主级形式，故原样保留。

```agda
                 ((λ k → lower (h1 (PE.member-in image (con R) (z ∷ q ∷ []) k))) , h2) })
```

向内读法把左支经对表达式引入与对图引入注入，并把截断取值消去到命题值的满足之中。

```agda
        ψ-in : (z q : S) → Body z q → ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
        ψ-in z q (inl (h1 , hv)) = PT.rec (snd ((z ∷ q ∷ []) ⊨ ψ))
          (λ { (v , (e , hc)) → ∣ inl (PE.member-in image (con R) (z ∷ q ∷ []) h1
                                     , PF.pair-in z q v e hc) ∣₁ }) hv
        ψ-in z q (inr (h1 , e)) =
```

右支把宿主侧反驳提升进对象语言并携带默认等式。两支都被注入公式的截断析取。

```agda
          ∣ inr ((λ k → lift (h1 (PE.member-out image (con R) (z ∷ q ∷ []) k))) , e) ∣₁
```

辅助事实 `b≺a-of` 把宿主侧关系隶属解码为内部比较：若 `q` 与 `a` 有关系，则 `q` 的内部索引低于 `a`。解码方式是沿隶属下降以恢复索引。

```agda
      private
        b≺a-of : (q : S) (mq : Mem q) → Holds R q (up a) → toDom q mq ≺ a
        b≺a-of q mq h = ≺-in (toDom q mq) a
          (subst (λ t → ⟨ pr t (↪ a) ∈ fst R ⟩) (sym (toDom-val q mq)) h)
```

归纳假设陈述在典范表示 `up (toDom q mq)` 处，而局部公式必须在原载体元素 `q` 处得到满足。往返等式认同这两种呈现，`colFo-at` 随之把满足证明从典范表示运输到 `q`。

```agda
        IHq : (q : S) (mq : Mem q) → toDom q mq ≺ a
            → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
        IHq q mq k = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (IH (toDom q mq) k)
```

替换要求：对每个 `q ∈ D`，满足 `ψ` 的取值构成可缩纤维。证明用排中律判定是否有 `q R a`。无论哪种情形，它都将在命题截断下给出一个满足公式的典范输出，并证明其他任何满足公式的输出都等于它；`mereFunct` 再把这种命题截断的唯一存在转换为可缩性。

```agda
        fc : (q : S) → ⟨ q ∈ˢ D ⟩ → isContr (Σ[ z ∈ S ] ⟨ (z ∷ q ∷ []) ⊨ ψ ⟩)
        fc q mq = mereFunct ψ q (decide (lem (pr (fst q) (↪ a) ∈ fst R)))
          where
          b : Dom
          b = toDom q mq
```

在前驱分支中，典范输出为 `zb = prʟ q (colʟ b)`，其底层集合编码 `(q,col b)`；这里的 `b` 是从 `q` 解码出的内部索引。非前驱分支则使用默认输出 `ea`。局部判定引理将在命题截断下说明：无论哪一分支成立，都有一个满足公式的输出，且其他任何满足公式的输出都与它相等。

```agda
          zb : S
          zb = prʟ q (colʟ b)
          decide : Holds R q (up a) ⊎ (Holds R q (up a) → Empty.⊥)
                 → ∥ Σ[ z ∈ S ] (⟨ (z ∷ q ∷ []) ⊨ ψ ⟩
                                × ((z' : S) → ⟨ (z' ∷ q ∷ []) ⊨ ψ ⟩ → z' ≡ z)) ∥₁
```

设 `q R a`。归纳假设说明 `col b` 在 `q` 处满足 `colFo`，而 `prʟ-fst` 给出 `fst zb` 与有序对编码 `pr (fst q) (col b)` 之间所需的等式，故典范输出 `zb` 满足左支。为证唯一性，把任意满足公式的输出仍按两种情形读取：左支见证将由 `colFo-val` 确定，右支见证则与既有假设 `q R a` 矛盾。

```agda
          decide (inl h) = ∣ zb
            , ( ψ-in zb q (inl (h , ∣ colʟ b , (prʟ-fst q (colʟ b) , IHq q mq (b≺a-of q mq h)) ∣₁))
              , λ z' hz' → PT.rec (isSetS z' zb)
                  (λ { (inl (_ , hv)) → PT.rec (isSetS z' zb)
                         (λ { (v , (e , hcol)) → Σ≡Prop (λ w → snd (isL w))
```

对左支中的竞争见证，`colFo-val` 把其第二坐标认同为 `col b`；再与该见证的有序对等式合成，便证明整个输出等于 `zb`。右支中的竞争见证含有对 `q R a` 的否定，故不可能存在。至此，前驱情形的唯一性得证。末行另行开始非前驱情形并选择默认输出 `ea`；其唯一性证明将在下一代码块继续。

```agda
                                (e ∙ cong (pr (fst q)) (colFo-val q mq v hcol) ∙ sym (prʟ-fst q (colʟ b))) })
                         hv
                     ; (inr (nh , _)) → Empty.rec (nh h) })
                  (ψ-out z' q hz') ) ∣₁
          decide (inr nh) = ∣ ea
```

否定隶属的情形闭合了唯一性论证。默认条目 `ea` 满足 `ψ`。向外读取任意竞争见证时，要么得到一条与 `nh` 矛盾的肯定隶属，要么由默认支得到 `fst z' ≡ fst ea`。在后一种情形中，可构造性证明的命题性把这条底层集合的等式提升为 `S` 中所需的等式 `z' ≡ ea`。

```agda
            , ( ψ-in ea q (inr (nh , refl))
              , λ z' hz' → PT.rec (isSetS z' ea)
                  (λ { (inl (h , _)) → Empty.rec (nh h)
                     ; (inr (_ , e)) → Σ≡Prop (λ w → snd (isL w)) e })
                  (ψ-out z' q hz') ) ∣₁
```

这项局部递归的定义域是整个 `D`。若 `q R up a`，它的唯一取值是 `q` 与 `q` 所呈现索引的塌缩值组成的有序对；否则取同一个默认条目 `ea`。把替换应用于 `ψ` 及这份唯一性证明，便将所得取值收集为一个可构造集。

```agda
        module T = Of (record { dom = D ; graph = ψ ; funct = fc }) using ( table; table-in; table-out )
```

`Fa` 表示这个由替换得到的值域。下述成员关系引理将证明，它的元素恰为满足 `b ≺ a` 的有序对 `pr(↪ b,col b)`，再加上默认分支给出的顶端有序对 `pr(↪ a,col a)`。

```agda
      Fa : S
      Fa = T.table
```

`Below b` 陈述索引 `b` 至多等于当前索引：要么严格低于，要么相等。这个两分谓词驱动局部表的引入与正确性。

```agda
      Below : Dom → Type ℓ
      Below b = (b ≺ a) ⊎ (b ≡ a)
```

若 `b` 小于或等于 `a`，`Fa-in` 就把输入为 `up b`、取值为 `colʟ b` 的图条目放入 `Fa`。严格比较的情形用归纳假设满足 `ψ` 的第一个析取支；等式 `b ≡ a` 的情形则先把这个有序对等同于 `ea`，再使用默认分支。

```agda
      Fa-in : (b : Dom) → Below b → Holds Fa (up b) (colʟ b)
      Fa-in b k = subst (λ w → ⟨ w ∈ fst Fa ⟩) (prʟ-fst (up b) (colʟ b))
        (T.table-in (up b) (prʟ (up b) (colʟ b)) (up-mem b) (ψ-in _ (up b) (bodyOf k)))
        where
        bodyOf : Below b → Body (prʟ (up b) (colʟ b)) (up b)
```

在严格情形中，公式体包含关系见证 `b ≺ a`，以及归纳假设所给出的 `colʟ b` 在 `up b` 处满足塌缩公式。在相等情形中，非自反性排除 `up b R up a`，而沿 `b ≡ a` 的传输把待证有序对等同于默认有序对。

```agda
        bodyOf (inl k) = inl (≺-out b a k , ∣ colʟ b , (prʟ-fst (up b) (colʟ b) , IH b k) ∣₁)
        bodyOf (inr e) = inr
          ( (λ h → ≺-irrefl a (≺-in a a (subst (λ t → Holds R (up t) (up a)) e h)))
          , prʟ-fst (up b) (colʟ b) ∙ cong (λ t → pr (↪ t) (col t)) e ∙ sym (prʟ-fst (up a) (colʟ a)) )
```

反过来，属于 `Fa` 仅仅给出一个满足 `b ≺ a` 或 `b ≡ a` 的索引 `b`，以及把该成员等同于 `pr(↪ b,col b)` 的等式。索引仍处于命题截断之下，因此这个结论没有选定一个代表元。

```agda
      Fa-out : (y : S) → ⟨ y ∈ˢ Fa ⟩
             → ∥ Σ[ b ∈ Dom ] (Below b × (fst y ≡ pr (↪ b) (col b))) ∥₁
      Fa-out y hy = PT.rec squash₁
        (λ { (q , (mq , hψ)) → PT.rec squash₁
          (λ { (inl (h , hv)) → PT.map
```

在前驱分支中，`colFo-val` 把公式给出的取值等同于 `toDom q mq` 处的塌缩值，随后 `q` 的呈现等式把有序对改写为典范形式。在默认分支中，记录的有序对就是以 `a` 自身为索引的那一个。

```agda
                 (λ { (v , (e , hcol)) → toDom q mq
                    , (inl (b≺a-of q mq h)
                      , e ∙ cong₂ pr (sym (toDom-val q mq)) (colFo-val q mq v hcol)) })
                 hv
             ; (inr (_ , e)) → ∣ a , (inr refl , e ∙ prʟ-fst (up a) (colʟ a)) ∣₁ })
```

替换的读取引理与 `ψ-out` 都只返回经命题截断的见证。由于目标本身也经过命题截断，证明可以依次消去外层与内层截断，而无需在全局选定任何一个见证。

```agda
          (ψ-out y q hψ) })
        (T.table-out y hy)
```

把上一结论用于 `x` 与 `v` 的有序对编码，便可恢复它的两个坐标。因此，图条目 `Holds Fa x v` 仅仅确定某个 `b ≤ a`，使 `fst x ≡ ↪ b` 且 `fst v ≡ col b`。

```agda
      Fa-pair : (x v : S) → Holds Fa x v
              → ∥ Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v)) ∥₁
      Fa-pair x v h = PT.map step
        (Fa-out (prʟ x v) (subst (λ w → ⟨ w ∈ fst Fa ⟩) (sym (prʟ-fst x v)) h))
        where
```

传输把等式重新指向内部对；辅助引理经有序对的单射性把它拆成索引的命名等式与塌缩值的命名等式。

```agda
        step : Σ[ b ∈ Dom ] (Below b × (fst (prʟ x v) ≡ pr (↪ b) (col b)))
             → Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
        step (b , (k , e)) = b , (k , sym (fst q) , sym (snd q))
          where
          q : (fst x ≡ ↪ b) × (fst v ≡ col b)
```

把 `pr-inj` 应用于复合后的有序对等式，便得到 `fst x ≡ ↪ b` 与 `fst v ≡ col b`。`Fa-pair` 所需的结果把典范坐标置于等式左边，因此 `step` 返回前先反转这两条分量等式。

```agda
          q = pr-inj (sym (prʟ-fst x v) ∙ e)
```

若 `c ≺ b` 且 `b ≺ a`，传递性给出 `c ≺ a`。若改为 `b ≡ a`，把这个等式代入 `c ≺ b` 也得到同一结论。这正是 `Below b` 的两种情形。

```agda
      below-trans : {c b : Dom} → c ≺ b → Below b → c ≺ a
      below-trans cb (inl k) = ≺-trans cb k
      below-trans {c} cb (inr e) = subst (c ≺_) e cb
```

为证明 `Correct Fa R`，先固定 `Fa` 中一个实际条目 `(x,v)`。配对读取引理只给出一个经命题截断的索引来表示该条目，但 `Complete Fa R x` 与 `ValueIs Fa R x v` 都是命题。因此，可以合法地向它们的合取消去这层截断。

```agda
      Fa-correct : Correct Fa R
      Fa-correct x v hxv = PT.rec
        (isProp× (isPropΠ (λ _ → isPropΠ (λ _ → squash₁)))
                 (isPropΠ (λ w → isProp× (isPropΠ (λ _ → squash₁))
                                          (isPropΠ (λ _ → snd (fst w ∈ fst v))))))
```

设所选条目由某个 `b ≤ a` 表示，于是 `x` 呈现 `b`，而 `v` 的底层集合是 `col b`。完备性要求 `x` 的每个 `R` 前驱都在 `Fa` 中有取值；取值条件则要求对每个 `w` 证明：`w ∈ v` 当且仅当某个这样的前驱在 `Fa` 中与 `w` 配对。

```agda
        build (Fa-pair x v hxv)
        where
        build : Σ[ b ∈ Dom ] (Below b × (↪ b ≡ fst x) × (col b ≡ fst v))
              → Complete Fa R x × ValueIs Fa R x v
        build (b , (k , ex , ev)) = cmp , (λ w → fwd w , bwd w)
```

这里的关键转换，是把编码关系中的前驱 `y R x` 化为 `Dom` 中的严格比较。条目的表示把 `fst x` 与被表示成员 `↪ b` 等同，并不把载体元素 `x` 与外围索引 `b` 等同。`Rsub` 先证明 `y` 属于 `D`，随后 `toDom` 才恢复出可与 `b` 比较的索引。

```agda
          where
```

由 `y R x`，端点包含假设先给出 `y ∈ D`，故 `toDom y my` 定义了一个索引 `c`。沿 `y` 与 `x` 的呈现等式传输关系见证，即得 `c ≺ b`；第二个分量则记录 `↪ c` 是 `y` 的底层集合。

```agda
          pred : (y : S) → Holds R y x → Σ[ c ∈ Dom ] ((c ≺ b) × (↪ c ≡ fst y))
          pred y hy = c , (≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩)
                              (sym (toDom-val y my)) (sym ex) hy) , toDom-val y my)
            where
            my : Mem y
```

证明 `my` 正是 `Rsub` 给出的第一个端点成员关系，也是构造 `toDom y my` 所需的证据。由于属于 `D` 是一个命题，使用这份证据不会额外选择一种呈现。

```agda
            my = Rsub y x hy .fst
            c : Dom
            c = toDom y my
```

对前驱 `y R x`，令 `c` 为刚恢复的索引。完备性的取值见证是 `colʟ c`；`Fa-in` 先给出输入为 `up c` 的典范条目，再沿 `↪ c ≡ fst y` 传输为输入在 `y` 处的所需条目。经由 `b ≤ a` 的传递性保证 `c` 严格低于 `a`。

```agda
          cmp : Complete Fa R x
          cmp y hy = ∣ colʟ c , subst (λ t → ⟨ pr t (col c) ∈ fst Fa ⟩) ec
                                 (Fa-in c (inl (below-trans cb k))) ∣₁
            where
            c = pred y hy .fst
```

现在把 `pred y hy` 的两个投影记作 `cb` 与 `ec`：`cb` 是严格比较 `c ≺ b`，`ec` 则把典范代表 `↪ c` 等同于实际输入 `y`。前者提供 `Fa-in` 所需的界，后者负责把条目传输到 `y`。

```agda
            cb = pred y hy .snd .fst
            ec = pred y hy .snd .snd
```

为证明 `ValueIs` 的正向一半，先把 `w ∈ v` 改写为 `fst w ∈ col b`。塌缩的向外引理仅仅给出 `r ≺ b` 与 `col r ≡ fst w`；这些数据构造出从 `up r` 到 `x` 的一条 `R` 边，以及在表中把 `up r` 与 `w` 配对的条目。

```agda
          fwd : (w : S) → ⟨ fst w ∈ fst v ⟩ → Src Fa R x w
          fwd w w∈ = PT.map read (col-out b (fst w) (subst (λ t → ⟨ fst w ∈ t ⟩) (sym ev) w∈))
            where
            read : Σ[ r ∈ Dom ] ((r ≺ b) × (col r ≡ fst w)) → Σ[ y ∈ S ] (Holds R y x × Holds Fa y w)
            read (r , (rb , er)) = up r
```

两条隶属沿索引的等式与严格比较传输，把关系与表的隶属都落在被点名的前驱处。

```agda
              , ( subst (λ t → ⟨ pr (↪ r) t ∈ fst R ⟩) ex (≺-out r b rb)
                , subst (λ t → ⟨ pr (↪ r) t ∈ fst Fa ⟩) er (Fa-in r (inl (below-trans rb k))) )
```

在反向一半中，`Src Fa R x w` 的见证仅仅给出某个 `y`，满足 `y R x`，并且表中有从 `y` 到 `w` 的条目。目标 `fst w ∈ fst v` 是命题，因此可以向它依次消去来源见证与表读取结果中的命题截断。

```agda
          bwd : (w : S) → Src Fa R x w → ⟨ fst w ∈ fst v ⟩
          bwd w = PT.rec (snd (fst w ∈ fst v)) (λ { (y , (hy , fy)) →
            PT.rec (snd (fst w ∈ fst v)) (read y hy) (Fa-pair y w fy) })
            where
            read : (y : S) → Holds R y x
```

读取表条目得到一个索引 `c`、把 `y` 等同于 `↪ c` 的等式，以及把 `w` 等同于 `col c` 的等式。把第一个等式、`y R x` 与 `x` 由 `b` 表示这一事实合并，便得到 `c ≺ b`；于是 `col-in` 给出 `col c ∈ col b`，其余等式再把这条成员关系传输为 `w ∈ v`。

```agda
                 → Σ[ c ∈ Dom ] (Below c × (↪ c ≡ fst y) × (col c ≡ fst w))
                 → ⟨ fst w ∈ fst v ⟩
            read y hy (c , (_ , ey , ew)) =
              subst2 (λ s t → ⟨ s ∈ t ⟩) ew ev (col-in b c cb)
              where
```

`c` 与 `b` 之间的严格比较由两条命名等式与关系见证填充，前驱数据随之完备。

```agda
              cb : c ≺ b
              cb = ≺-in c b (subst2 (λ s t → ⟨ pr s t ∈ fst R ⟩) (sym ey) (sym ex) hy)
```

局部表在顶端元素处满足图公式，默认条目见证取值子句。这是本节的归纳步。

```agda
      approx-step : ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
      approx-step = CF.colFo-in (colʟ a) (up a) Fa Fa-correct (Fa-in a (inr refl))
```

现在用良基归纳证明塌缩公式在每个 `a : Dom` 处成立。归纳假设为每个严格前驱给出该公式的满足见证，`Approx.approx-step` 再用这些见证在 `a` 处构造一张正确的局部表。结论遍及 `Dom` 中的每个索引，并不要求事先把 `D` 等同于某个序数。

```agda
    approx : (a : Dom) → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩
    approx = W.induction {P = λ a → ⟨ (colʟ a ∷ up a ∷ []) ⊨ CF.colFo ⟩}
      (λ a IH → Approx.approx-step a IH)
```

给定 `q : S` 与 `mq : Mem q`，前面的归纳先在典范表示 `up (toDom q mq)` 处给出公式。往返等式 `up-toDom q mq` 把该表示与 `q` 等同，`colFo-at` 再把满足证明运输到 `D` 的这个原成员处。

```agda
    approx-at : (q : S) (mq : Mem q) → ⟨ (colʟ (toDom q mq) ∷ q ∷ []) ⊨ CF.colFo ⟩
    approx-at q mq = colFo-at (colʟ (toDom q mq)) (up-toDom q mq) (approx (toDom q mq))
```

递归 `otR` 以 `D` 为定义域，以 `CF.colFo` 为取值关系。对成员 `q ∈ D`，选定的取值是小索引 `toDom q mq` 处的塌缩值；前面的逼近结果证明这个取值在 `q` 处满足公式。

```agda
    private
      otR : Recursion
      otR = record
        { dom   = D
        ; graph = CF.colFo
```

字段 `funct` 必须证明：对每个 `q ∈ D`，满足 `CF.colFo` 的取值所成纤维是可缩的。其中心由 `colʟ (toDom q mq)` 与 `approx-at q mq` 组成。对任意竞争元素 `(v,hv)`，`colFo-val` 把 `v` 的底层集合与同一个塌缩值等同；可构造性证明与满足证明的命题性再依次把这条等式提升到 `v`，最后提升到整个纤维元素。

```agda
        ; funct = λ q mq → (colʟ (toDom q mq) , approx-at q mq)
            , λ { (v , hv) → Σ≡Prop (λ w → snd ((w ∷ q ∷ []) ⊨ CF.colFo))
                (sym (Σ≡Prop (λ w → snd (isL w)) (colFo-val q mq v hv))) } }
```

通用的替换构造 `Of` 现在把这项函数性递归变成它的取值表，并给出成员关系刻画的两个方向：满足递归关系的取值进入该表，而表的每个成员都来自 `D` 中某个输入，并带有所需的公式见证。

```agda
      module OT = Of otR using ( table; table-in; table-out )
```

`otL` 是 `otR` 经替换得到的值域，因此是 `L` 的一个元素。它的底层集合收集所有 `b : Dom` 的塌缩值 `col b`，无需这些取值来自互不相同的索引。这里的构造只使用这一精确值域刻画；整个值域的序数性是还需进一步推出的结论。

```agda
    otL : S
    otL = OT.table
```

对每个 `b : Dom`，逼近引理证明 `colʟ b` 是 `otR` 在 `up b` 处的取值。因此，替换的引入方向给出 `col b ∈ fst otL`。

```agda
    otL-in : (b : Dom) → ⟨ col b ∈ fst otL ⟩
    otL-in b = OT.table-in (up b) (colʟ b) (up-mem b) (approx b)
```

反过来，每个 `y ∈ fst otL` 仅仅具有某个索引 `b : Dom`，满足 `col b ≡ y`。结论特意保留命题截断，因此它刻画了精确值域，却没有为每个成员选定一个原像。

```agda
    otL-out : (y : V ℓ) → ⟨ y ∈ fst otL ⟩ → ∥ Σ[ b ∈ Dom ] (col b ≡ y) ∥₁
    otL-out y hy = PT.map (λ { (q , (mq , h)) → toDom q mq , sym (colFo-val q mq yS h) })
      (OT.table-out yS hy)
      where
      yS : S
```

为了应用替换的读取引理，需要把外围集合 `y` 看作可构造论域中的元素。由 `y ∈ fst otL` 以及 `otL` 的可构造性，可构造性的向下封闭正好给出这一打包。

```agda
      yS = y , isL-trans {x = fst otL} {y = y} hy (snd otL)
```

把递归图构造应用于 `otR`，所收集的是有序对而非裸取值。它为 `D` 中每个输入记录该输入及其唯一确定的塌缩值，并给出相应的内向与外向读取、单值性以及精确定义域陈述。

```agda
    module CT = RecursionGraph otR using ( F; F-in; F-out; pair-out; sv; dm )
```

`colTable` 是在 `L` 内由 `otR` 构造出的函数图集合。对 `b : Dom`，其典范条目是 `pr(↪ b,col b)`：表中存储的输入是 `D` 的被表示成员 `↪ b`，而 `b` 本身仍是外围小表示中的索引。

```agda
    colTable : S
    colTable = CT.F
```

在典范代表 `up b` 处，递归图最初记录的取值是 `col (toDom (up b) (up-mem b))`。呈现等式诱导出这个恢复索引与 `b` 的相等；沿该等式在 `col` 下的像传输第二坐标，便得到所陈述的有序对 `pr(↪ b,col b)`。

```agda
    colTable-in : (b : Dom) → ⟨ pr (↪ b) (col b) ∈ fst colTable ⟩
    colTable-in b = subst (λ t → ⟨ pr (↪ b) t ∈ fst colTable ⟩)
      (cong col (Dom≡ (toDom-val (up b) (up-mem b)))) (CT.F-in (up b) (up-mem b))
```

反过来，`colTable-out` 说明：对函数图的任意成员 `y`，仅仅存在某个 `b : Dom`，使 `fst y ≡ pr(↪ b,col b)`。该索引仍处于命题截断之下，因此这项向外读法只刻画函数图，并未为每个成员选定一个表示索引。

```agda
    colTable-out : (y : S) → ⟨ y ∈ˢ colTable ⟩
                 → ∥ Σ[ b ∈ Dom ] (fst y ≡ pr (↪ b) (col b)) ∥₁
    colTable-out y hy = PT.map (λ { (q , mq , e) → toDom q mq
      , e ∙ cong (λ t → pr t (col (toDom q mq))) (sym (toDom-val q mq)) }) (CT.F-out (fst y) hy)
```

纤维谓词说：与 `x` 配对的成员 `v` 是 `x` 所呈现索引的塌缩值，并以呈现隶属为数据。

```agda
    Fib : S → S → Type (ℓ-suc ℓ)
    Fib x v = Σ[ mx ∈ Mem x ] (fst v ≡ col (toDom x mx))
```

固定 `x` 与 `v` 后，`Fib x v` 是命题。成员关系 `mx : Mem x` 取值于命题；对每个这样的 `mx`，由于 `V` 是集合，等式 `fst v ≡ col (toDom x mx)` 也是命题。因此，这个依值和不携带额外的选择数据。

```agda
    isPropFib : (x v : S) → isProp (Fib x v)
    isPropFib x v = isPropΣ (isPropMem x) (λ mx → setIsSet (fst v) (col (toDom x mx)))
```

因此，`x` 与 `v` 的编码有序对属于 `colTable` 时，可以得到不带截断的信息：`x` 属于 `D`，且 `v` 的底层集合等于 `x` 所呈现索引处的塌缩值。正是 `Fib x v` 的命题性允许消去图读取结果中的截断。

```agda
    colTable-pair : (x v : S) → Holds colTable x v → Fib x v
    colTable-pair = CT.pair-out
```

## 作为编码单射的图

为研究塌缩图何时编码一条单射，固定 `D`、`R` 以及端点条件 `Rsub`。这个条件只说明每条被 `R` 记录的边，其两个端点都属于 `D`；良基性、传递性与三歧性仍是彼此独立的假设。

```agda
module Code (D R : S)
            (Rsub : (y x : S) → Holds R y x
                  → ⟨ fst y ∈ fst D ⟩ × ⟨ fst x ∈ fst D ⟩) where
```

这里沿用上文的小表示 `Dom`、其编码关系 `_≺_`，以及 `D` 的成员与索引之间的转换。接下来的编码论证建立在同一塌缩构造上，并不引入第二条关系。

```agda
  open Internal D R Rsub public
```

这些假设各有不同作用。良基性通过递归定义 `col`，传递性证明每个塌缩值是序数，因而可构造；局部表的装配还使用本章的经典参数 `lem`。这些材料共同构造出精确值域 `otL` 与函数图 `colTable`，并给出单值性、精确定义域，以及所有函数图取值都属于 `otL`。三歧性只在下一个模块中加入，用于证明单射性。

```agda
  module Conjuncts (wf : WellFounded _≺_)
                   (≺-trans : {a b c : Dom} → a ≺ b → b ≺ c → a ≺ c) where
```

固定这两个假设后，前面的图构造给出 `col`、`otL` 与 `colTable`，以及它们的成员关系刻画。在这一阶段，相同输入具有相同的记录取值，但尚未证明记录取值相等能够推出输入相等。

```agda
    open Graph wf ≺-trans public
```

在二槽位环境 `γ` 中，零号槽放置 `colTable`，一号槽放置 `D`。单值性与精确定义域公式因而可以通过这两个固定位置引用函数图及其预定定义域。

```agda
    γ : S ^ 2
    γ = colTable ∷ D ∷ []
```

第一项条件是单值性：若 `colTable` 含有输入相同、取值分别为 `y` 与 `y'` 的两个有序对，则 `fst y ≡ fst y'`。这来自递归取值的唯一性，本身并不断言每个输入都有取值。

```agda
    sv : ⟨ γ ⊨ svAt zero ⟩
    sv = CT.sv
```

定义域条件是一条等价：一个输入在 `colTable` 中具有某个取值，当且仅当它属于 `D`。因此，它既排除定义域外的条目，也断言 `D` 的每个成员都有取值；后一个方向中的存在取值仍保留命题截断。

```agda
    dm : ⟨ γ ⊨ domAt zero (suc zero) ⟩
    dm = CT.dm
```

值域条件来自函数图的配对读取：从 `x` 到 `y` 的条目给出 `x` 属于定义域的见证，并把 `fst y` 等同于相应的塌缩值，而 `otL-in` 证明该塌缩值属于 `otL`。这里仅证明函数图的取值都落在 `otL` 中；`colTable` 的单射性仍需下一步引入的三歧性假设。

```agda
    ran : (x y : S) → Holds colTable x y → ⟨ fst y ∈ fst otL ⟩
    ran x y h = subst (λ t → ⟨ t ∈ fst otL ⟩) (sym (snd (colTable-pair x y h)))
      (otL-in (toDom x (fst (colTable-pair x y h))))
```

塌缩表已经在 `D` 上全域且单值，其取值也已落在精确值域 `otL` 中。要得到编码单射，只余下输入唯一性这一项条件。现在假设小定义域上的三歧性：对任意 `a` 与 `b`，或者 `a ≺ b`，或者 `a ≡ b`，或者 `b ≺ a`。结合外层模块已经固定的良基性与传递性，这项比较将使相等的塌缩值迫使索引相等。

```agda
    module Inj (tri : (a b : Dom) → (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a))) where
```

为证明 `col` 单射，固定满足 `col a ≡ col b` 的 `a` 与 `b`，并按二者的三歧性分类。相等情形已经给出所需结论。两个严格情形则各自把两个塌缩值之间真实成立的隶属关系沿该等式搬运成自隶属，故只需反驳这一不可能的隶属关系。

```agda
      col-inj : (a b : Dom) → col a ≡ col b → a ≡ b
      col-inj a b e = go (tri a b)
        where
        go : (a ≺ b) ⊎ ((a ≡ b) ⊎ (b ≺ a)) → a ≡ b
        go (inl k)       = Empty.rec (∈-irrefl (col b)
```

左支中 `a` 先于 `b`，故 `col a` 属于 `col b`；沿取值等式运输使 `col b` 属于自身，被非自反性反驳。中支直接返回等式。右支对称：`col a` 将属于自身。

```agda
          (subst (λ t → ⟨ t ∈ col b ⟩) e (col-in b a k)))
        go (inr (inl q)) = q
        go (inr (inr k)) = Empty.rec (∈-irrefl (col a)
          (subst (λ t → ⟨ t ∈ col a ⟩) (sym e) (col-in a b k)))
```

对象语言子句 `injAt` 要求：具有同一输出的两条图表项必须具有同一输入。用 `colTable-pair` 读取 `p` 与 `q`，便得到两个输入属于 `D` 的证明 `m` 与 `m'`，以及把共同输出 `y` 分别认同为两个恢复所得塌缩值的等式。复合这两条等式，就得到应用 `col-inj` 所需的前提。

```agda
      ij : ⟨ γ ⊨ injAt zero ⟩
      ij = injAt-in zero γ (λ y x x' p q →
        let (m , e)   = colTable-pair x y p
            (m' , e') = colTable-pair x' y q
        in sym (toDom-val x m)
```

恢复的索引由 `col-inj` 相等，而往返引理把该等式搬回原载体元素的底层集合。三条等式复合成所需等式。

```agda
         ∙ cong ↪ (col-inj (toDom x m) (toDom x' m') (sym e ∙ e'))
         ∙ toDom-val x' m')
```

这四个字段来自不同的论证。递归图给出单值性与精确定义域子句；`colTable-pair` 和 `otL-in` 给出值域界；三歧性则补上缺少的单射性子句。把这些证明封装起来便得到 `InjCode colTable D otL`。因此，只有在携带 `tri` 的模块内部，`colTable` 才是编码单射；这份记录没有另行断言本章已经把 `otL` 封装为序数。

```agda
      code : InjCode colTable D otL
      code = sv , dm , ij , ran
```

反向构造只针对选定的源集 `X` 与目标集 `Y`。对每个 `x ∈ X`，`pre` 必须选出索引 `b : Dom` 并满足 `col b ≡ fst x`；它是塌缩原像，不一定是这条关系中某个固定点的前驱。第二项参数 `bound` 证明所表示的原输入 `↪ b` 属于 `Y`。每次使用逆向接口时都必须另行提供这些数据，它们不能仅由 `otL-out` 自动得到。

```agda
      module Inverse (X Y : S)
        (pre : (x : S) → ⟨ fst x ∈ fst X ⟩ → Σ[ b ∈ Dom ] (col b ≡ fst x))
        (bound : (x : S) (mx : ⟨ fst x ∈ fst X ⟩) → ⟨ ↪ (pre x mx .fst) ∈ fst Y ⟩) where
```

源集的隶属被记录为类型，使论证能把它与被映射的每个元素并肩携带。

```agda
        SourceMem : S → Type (ℓ-suc ℓ)
        SourceMem x = ⟨ fst x ∈ fst X ⟩
```

对 `x ∈ X`，令 `b` 为 `pre` 选出的塌缩原像。逆函数返回 `up b`，即底层集合为原定义域中被表示成员 `↪ b` 的可构造载体元素。这里需要证明参数 `mx`，因为所选原像可以依赖于 `x` 属于指定源集的证据。

```agda
        fn : (x : S) → SourceMem x → S
        fn x mx = up (pre x mx .fst)
```

定义公式沿反方向读取已有的表。在环境 `y ∷ x ∷ []` 中，`y` 是逆映射的候选输出，`x` 是其输入，而 `appC colTable zero (suc zero)` 断言原表项 `Holds colTable y x`。这里没有假设一张新的塌缩表，只是让旧图的两个坐标承担逆向角色。

```agda
        opaque
          graph : Formula S 2
          graph = appC colTable zero (suc zero)
```

充分性等式把交换后图公式的满足等同于该对在塌缩表中的隶属，使表的两种读法可互换。

```agda
          at : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ ≡ Holds colTable y x
          at y x = cong ⟨_⟩ (appC-adequate colTable zero (suc zero) (y ∷ x ∷ []))
```

还需证明反向公式只能取到所选的值。由 `Holds colTable y x`，`colTable-pair` 恢复一个表示候选输出 `y` 的索引，并给出该索引的塌缩值等于逆映射输入 `x` 的等式。`pre` 选出的索引也塌缩到 `x`；因此 `col-inj` 认同这两个索引，`up-toDom` 再把索引等式搬回 `y ≡ fn x mx`。

```agda
        only : (x : S) (mx : SourceMem x) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x mx
        only x mx y hy = sym (up-toDom y my)
          ∙ cong up (col-inj (toDom y my) (pre x mx .fst) (sym (f .snd) ∙ sym (pre x mx .snd)))
          where
          f = colTable-pair y x (transport (at y x) hy)
```

`f` 的第一投影是成员关系证明 `my : Mem y`。这份证据用于构造恢复所得的索引 `toDom y my` 并应用往返引理；它本身并不是该索引。

```agda
          my = f .fst
```

这些材料组成一项从 `X` 到 `Y` 的 `DefinableMap`。其外围函数是 `fn`，而 `bound` 提供陪域字段。为证明定义子句，先对所选原像 `b` 使用 `colTable-in b`；再沿 `col b ≡ fst x` 替换输出坐标，最后反向使用 `at`，把所得表隶属关系变成反向图公式的满足证明。

```agda
        M : DefinableMap
        M = record
          { dom = X ; cod = Y ; fn = fn ; into = bound ; graph = graph
          ; defines = λ x mx → transport (sym (at (fn x mx) x))
              (subst (λ w → ⟨ pr (↪ (pre x mx .fst)) w ∈ fst colTable ⟩)
```

字段 `defines` 从典范条目 `colTable-in b` 出发，沿原像等式 `col b ≡ fst x` 运输其输出坐标。充分性等式 `at` 随后把这条表成员关系变成反向图公式的满足，而 `only` 则给出所需的取值唯一性。

```agda
                (pre x mx .snd)
                (colTable-in (pre x mx .fst)))
          ; only = only }
```

逆函数的单射性有一项直接理由。若 `fn x mx` 与 `fn x' mx'` 的底层集合相等，那么这两个集合分别是 `pre` 所选索引 `b` 与 `b'` 的 `↪ b` 和 `↪ b'`；表示的单射性 `Dom≡` 因而给出 `b ≡ b'`。对该等式应用 `col`，再与 `pre` 保存的两条等式复合，便得到 `fst x ≡ fst x'`。这段证明在 `Dom≡` 处使用小表示的单射性；`col-inj` 已在前文用于证明反向公式的取值唯一性，并未出现在这条等式链中。

```agda
        inj : (x : S) (mx : SourceMem x) (x' : S) (mx' : SourceMem x')
            → fst (fn x mx) ≡ fst (fn x' mx') → fst x ≡ fst x'
        inj x mx x' mx' e = sym (pre x mx .snd) ∙ cong col (Dom≡ e) ∙ pre x' mx' .snd
```

把一般的可定义单射构造应用于 `M` 与 `inj`，便把这项受限反向映射封装为 `InjL X Y`，即编码单射存在性的命题截断陈述。它的范围恰由所给数据限定：`X` 的每个成员都有一个选定的塌缩原像，并且所表示的原输入属于 `Y`。它既不提供整个 `otL` 上的无条件逆映射，也不提供双射记录。

```agda
        injL : InjL X Y
        injL = DefinableInj.injL M inj
```