---
title: "把可定义单射化为内部编码"
module: L.DefinableInjection
lang: zh
site: "Bedrock"
description: "把可定义单射化为内部编码"
stage: "序数、单射与基数"
reading_order: 90
canonical: https://bedrock.institute/zh/L.DefinableInjection.html
html: L.DefinableInjection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/DefinableInjection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Recursion.Graph, L.Coding.Injection, L.Cardinal]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.DefinableInjection.md, https://bedrock.institute/ja/L.DefinableInjection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 把可定义单射化为内部编码

在 `L` 外部描述一条取值规则，并不等于已经有了一个可供 `L` 量化的对象。要在模型内部比较基数，需要一个由有序对组成的可构造集合来记录这些取值。因此，本章的中心问题是：可定义性与逐点唯一性怎样使替换定理能够收集这张函数图。

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

唯一的经典参数是层级 `ℓ-suc ℓ` 上的排中律。本章中的初等步骤，例如证明唯一性、运输成员关系，以及把命题截断消去到命题中，都是构造性的。这个参数在一般替换定理把函数图收集成 `L` 的元素时起作用；全程不使用任何形式的选择公理。

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

固定宇宙层级 `ℓ` 与这一排中律实例。这里的数学问题，是怎样从宿主层的取值规则得到一个可由 `L` 量化的集合。取值规则本身不会被放入 `L`；一条公式在 `L` 的某个集合上描述它的值，替换据此形成可构造的函数图，再由单射性证明为该图配上内部基数比较所需的编码。

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

这里须区分三类对象。公式属于一阶语言，其常元是可构造论域的元素；满足关系在 `L` 上的结构中解释该公式；`pr` 则是在外围层级中编码底层集合有序对的柯拉托夫斯基对。稍后读取定义公式时，值在前、输入在后；收集所得函数图的条目则是 `pr(输入,值)`。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

证明依次经过三种数学形式。递归由定义域、取值公式，以及定义域每一点的满足值纤维可缩这一证明组成。函数图构造用替换收集有序对，并证明单值性与恰当定义域。最后，`injAt` 表达尚缺的单射条件：两个条目若有相同输出，其输入便相等。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )
```

对集合 `a` 与 `b`，`InjCode F a b` 恰有四个分量：函数图 `F` 是单值的，其定义域恰为 `a`，它满足单射性，并且其中出现的每个值都属于 `b`。前三项是对象语言公式的满足判断，第四项是宿主层的取值范围条件。`InjL a b` 则把这样的 `F` 及其编码之存在作命题截断。

```agda
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
```

两项类型论事实控制着这段证明。若依值对的第二分量取值于命题，`Σ≡Prop` 就能把第一分量之间的路径提升为整对之间的路径。命题截断只保留是否有元素。函数图的读回引理 `pair-out` 可以消去一个经命题截断的来源见证，因为它的目标纤维是命题；最后一步则用 `∣_∣₁` 隐去具体的函数图与编码。这两次操作都没有全局选出一族见证。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
```

论域 `S` 来自 `L` 上的结构：元素 `x : S` 由外围集合 `fst x` 与它可构造的命题性证书组成。成员记号取自外围层级，所以记录中的表达式明确比较底层集合，例如 `fst x ∈ˢ fst dom`。当构造必须返回 `L` 的元素时，可构造性证书仍保留在第二分量中。

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

记号 `_⊨_` 表示外围层级限制到可构造集合所得结构中的满足关系。因此，`(y ∷ x ∷ []) ⊨ graph` 用 `L` 的元素填入 `graph` 的两个自由槽位来解释它。名称 `AbsL` 并不声称任意公式在 `L` 与外围层级之间绝对；本章使用的是限制结构的语义与已经证明的替换定理。

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

## 函数可定义的含义

一项 `DefinableMap` 首先指定 `L` 的两个元素 `dom` 与 `cod`，并不假设它们是序数或基数。宿主层取值规则 `fn` 只对一对数据有定义：`x : S` 以及 `x` 属于 `dom` 的证据 `m`；定义域之外无需给出值。类型允许 `fn x m` 提及 `m`。由于成员关系是命题，任意两份此类证明都相等，再由合同性可知相应取值相等。字段 `into` 证明每个选定值都属于 `cod`。

```agda
record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ fst x ∈ˢ fst dom ⟩ → S
    into    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) → ⟨ fst (fn x m) ∈ˢ fst cod ⟩
```

其余字段把宿主层取值与对象语言公式联系起来。`graph` 有两个自由槽位，可以含有来自 `S` 的常元，并不要求是 Δ₀ 公式。对每个 `x ∈ dom`，`defines` 证明以所选值在前、`x` 在后的环境满足该公式；`only` 则证明任何满足公式的 `y` 都在 `S` 中等于该所选值。这些条件不约束 `dom` 之外的输入，`only` 也不假设候选 `y` 属于 `cod`。所选值落入陪域由独立的字段 `into` 给出。

```agda
    graph   : Formula S 2
    defines : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m
```

## 把图的表项编码成有序对

函数图由一个集合表示，因此每个输入输出表项都要先表示为有序对。定义公式在第一个语义槽位中读取函数值，在第二个槽位中读取输入；集合编码则把相应表项存为 `pr(输入,函数值)`。构造函数图并在随后读回其内容时，必须始终区分这两种次序。

## 在 L 内部构造函数图

第一项构造只假设可定义性与函数性。它从 `M` 形成一个属于 `L` 的完整函数图，并给出准确写入与读取有序对条目的方法。单射性留到下一阶段：同一函数图构造也适用于无需单射的可定义映射，例如最小见证表。

```agda
module Graph (M : DefinableMap) where
  open DefinableMap M public
```

为满足递归所需的假设，保留 `dom` 与 `graph`，并证明定义域每一点的满足值纤维都有中心。该中心是 `(fn x m, defines x m)`，即给定取值及其满足证明。成员证据 `m` 直接传给 `fn`，所以这一步不会把取值规则扩张到 `dom` 之外。此处既不需要 `into`，也不需要单射性。

```agda
  private
    R : Recursion
    R = record
      { dom = dom ; graph = graph
      ; funct = λ x m → (fn x m , defines x m)
```

还须把每个候选 `(y,h)` 收缩到该中心。字段 `only` 给出 `y ≡ fn x m`，而可缩性要求一条从中心到候选的路径，因此代码使用 `sym`。第二分量是满足证明，因而为命题；所以 `Σ≡Prop` 能把反向后的取值相等提升为整个依值对的相等。这样便构造性地证明了所需的唯一存在。

```agda
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph)) (sym (only x m y h)) } }
```

现在由替换把有序对取值收集成可构造集合 `F`。辅助配对公式协调两种次序：原关系按 `(值,输入)` 解释，而 `F` 的成员是 `pr(输入,值)`。`F-in` 写入每个指定条目，`F-out` 则在命题截断下说明每个成员都来自这样的条目。固定 `x` 与 `y` 后，`pair-out` 把 `pr(x,y)` 属于 `F` 加强为一份定义域证明与等式 `y = fn(x)`。这次消去是合法的，因为 `Fib x y` 是命题，其中用到成员证明的证明无关性以及 `V` 中相等取值于命题。由这些读式可证明 `sv` 所表达的单值性，以及 `dm` 所表达的定义域恰为 `dom`。形成 `F` 的步骤使用替换定理，因而依赖给定的排中律；后续读取没有引入选择。

```agda
  open RecursionGraph R public
    using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )
```

最终编码的第四项条件是取值落入陪域。给定实际函数图条目 `pr(fst x,fst y) ∈ fst F`，`pair-out` 给出 `m : x ∈ dom` 与 `e : fst y ≡ fst(fn x m)`。字段 `into x m` 证明 `fst(fn x m)` 属于 `fst cod`。因此，成员关系必须沿 `sym e` 从所选值运输回 `y`，从而得到 `y ∈ cod`。这只证明像包含于陪域，并不证明陪域的每个元素都会出现。

```agda
  ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst cod ⟩
  ran x y h = subst (λ w → ⟨ w ∈ fst cod ⟩) (sym e) (into x m)
    where
    m = fst (pair-out x y h)
    e = snd (pair-out x y h)
```

## 从外部单射性得到编码单射

要把这张函数图变成单射编码，还须加入真正新的单射性假设。对两个各自带有 `dom` 成员证明的输入，它断言：若所选取值的底层集合相等，则输入的底层集合相等。成员实参仍然显式出现，因为 `fn` 的类型依值地依赖于它们。证明无关性保证不同成员证明之间相容，但这条假设仍按两个输入处实际给出的证据陈述。其结论的强度恰好符合 `injAt` 的相等条款。

```agda
module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ fst x ∈ˢ fst (DefinableMap.dom M) ⟩)
                  (x' : S) (m' : ⟨ fst x' ∈ˢ fst (DefinableMap.dom M) ⟩)
                → fst (DefinableMap.fn M x m) ≡ fst (DefinableMap.fn M x' m')
                → fst x ≡ fst x') where
```

打开 `Graph M` 后，已经构造出的 `F` 及其性质可用于单射情形。于是同时保留两种数学上有用的结论：当后续构造必须指名或组合函数图时，可以保留这个具体的 `F` 及其编码；也可以使用 `injL`，只记住某个编码单射存在。两者的区别在于具体数据与其命题性存在。

```agda
  open Graph M public
```

公式 `injAt zero` 固定输出 `y`，比较两个输入 `x` 与 `x'`：若 `pr(x,y)` 和 `pr(x',y)` 都属于 `F`，则两个输入相等。对第一条目应用 `pair-out` 得到 `e : y = fn(x)`，对第二条目应用它则得到 `e' : y = fn(x')`，并同时得到所需的两份定义域证明。因此，`sym e ∙ e'` 正是路径 `fn(x) = fn(x')`；宿主层假设 `inj` 把它化为 `x = x'`，`injAt-in` 再把这一性质转成满足判断 `ij`。这段论证使用的是单射性，而不仅是 `only`；`only` 比较固定输入处的输出，它支持的是单值性。

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

四元组 `sv , dm , ij , ran` 依次填入 `InjCode F dom cod` 的四个字段。其中，`sv` 证明单值性，`dm` 证明函数图的定义域恰为 `dom`，`ij` 证明对象语言中的单射性；三者都在环境 `F ∷ dom ∷ []` 中陈述。最后的 `ran` 在宿主层断言 `F` 中出现的值属于 `cod`。这份编码没有断言满射性，所以它描述的是到 `cod` 的单射，而不是双射。

```agda
  code : InjCode F dom cod
  code = sv , dm , ij , ran
```

最后，把具体的对 `(F,code)` 放入命题截断。所得项 `injL : InjL dom cod` 断言存在一张带单射编码的可构造函数图，同时忘去所构造的是哪一张图。基数比较需要的正是这个命题，并可在目标仍为命题时对它作消去。若某项构造需要具体数据，实例化后的模块中仍可分别使用 `F` 与 `code`。因此，被内化到 `L` 中的是编码后的函数图，而不是外部取值规则本身。

```agda
  injL : InjL dom cod
  injL = ∣ F , code ∣₁
```