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

后续的基数论证反复在单射的两种表示之间往返：一种是公式可以量化的图，另一种是集合的小成员类型之间的实际函数。两者之间的缝隙分三层填补。对象语言首先需要一条表达图是单射的公式，它是已有单值性条款的对偶。其次，在单值性与恰当定义域的假设下，图可以读成一个真正的函数，取值仍是可构造模型的元素。最后，该函数可转移到指定定义域与值域的典范小呈现上。本章补上单射性公式，并完成 Cantor-Bernstein 与 GCH 构造所用的两层读回。

这一构造本身是构造性的。周遭论证虽带有 `LEM (ℓ-suc ℓ)`，下面的证明却不调用它：图的取值只以截断存在给出，但单值性使整个像原像成为命题，因此可以消去截断并取得其唯一元素，而无须选择原理。

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

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

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

设 `S` 为可构造模型的载体。`S` 的元素由 `V ℓ` 中的周遭集合及其可构造性证明组成，因此图的断言都针对第一投影陈述。表示图取值、单值性与恰当定义域的公式，恰好把内部满足关系与这些投影后的图事实联系起来。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _≐_; _⇒̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

第二层读回需要典范呈现的工具：集合由索引类型与索引映射呈现，`member` 把索引变成显式的隶属证明，`fiber` 做相反的事，返回一个实际的索引而非截断的存在。`Σ≡Prop` 会在第二分量是命题时把依赖对的相等化归为第一分量的相等，像的原像与模型载体的对正是这样处理的。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; svAt; svAt-out; domAt; domAt-in )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
```

这里的真值是带着「其为命题」证明的命题，满足关系直接使用 `hProp` 上的逻辑联结词。满足判断 `_⊨_` 是对可构造结构 `𝒮ʟ` 陈述的，因此像 `γ ⊨ svAt zero` 这样的判断经充分性等同化后谈的是投影后的集合，而非对某个周遭结构的裸满足。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )
```

有界绝对性把可构造模型中的满足与赋值经 `fst` 投影后的满足联系起来。这座桥只在应用充分性定理时使用，并不会自行使 `Extract.toFun` 成为单射；单射性稍后以独立假设 `ij` 加入。

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

## 对象语言中的单射性

单值性的图固定一个输入、比较输出：若两条目有相同的第一分量，其第二分量一致。单射性是它的镜像：固定一个输出、比较输入。具体地，若 `(x, y)` 与 `(x', y)` 都属于图，则 `x` 与 `x'` 的第一分量必须相等。把它写成对象语言的公式，基数论证才能在模型内部对单射图作量化。本节定义 `injAt`，并证明：在应用的充分性等同下，该公式成立当且仅当投影后的图具有单射性质。

公式绑定赋值 `x′ ∷ x ∷ y ∷ γ`：槽位 0 是 `x′`，槽位 1 是 `x`，槽位 2 是 `y`，原来的图槽位 `f` 则变为 `f + 3`。两个前提分别说 `(x,y)` 与 `(x′,y)` 属于该图，结论把 `x` 与 `x′` 等同。因此它固定输出并比较输入，恰是单值性的对偶。

```agda
injAt : ∀ {n} → Fin n → Formula S n
injAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc zero) (suc (suc zero))
  ⇒̇ (appAt (suc (suc (suc f))) zero (suc (suc zero))
  ⇒̇ (var (suc zero) ≐ var zero)))))
```

读回时固定变元索引 `f` 与模型元素组成的赋值 `γ`。`Holds₀ x y` 是投影后的事实：`x` 与 `y` 的底层集合组成的有序对属于底层图，即变元 `f` 在 `γ` 中选出的那一项。下面的两个方向都是把某条应用条款的满足判断与这个 `Holds₀` 相比较，充分性路径是整个论证的枢纽。

```agda
module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds₀ : S → S → Type (ℓ-suc ℓ)
    Holds₀ x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at₁ : (y x x' : S)
```

路径 `at₁` 记录第一条应用条款在扩张赋值 `x' ∷ x ∷ y ∷ γ` 处的充分性：那里的满足被等同于对 `(x, y)` 属于图的投影事实。这一等同是命题之间的相等，由 `appAt-adequate` 在所给变元索引处给出，因此可以向两个方向运输。

```agda
        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)))
        ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

    at₂ : (y x x' : S)
```

路径 `at₂` 是另一条条款的同样陈述：变元 `0` 与 `2` 处的应用的满足等同于 `(x', y)` 属于图的投影事实。两条路径只在对码中输入哪个第一分量上不同，而这正是单射性所利用的不对称。

```agda
        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero)))
        ≡ (pr (fst x') (fst y) ∈ fst (lookup f γ))
    at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

  injAt-out : ⟨ γ ⊨ injAt f ⟩
```

向外的方向 `injAt-out` 从公式在 `γ` 处成立的证明与两个隶属事实 `Holds₀ x y`、`Holds₀ x' y` 出发。把三个量词实例化，得到含取式体在扩张赋值处的满足证明；再把隶属事实沿 `at₁`、`at₂` 的反向运输，变成两条前件条款的满足证明。最后的 `fst x ≡ fst x'` 在模型的相等中读出。

```agda
            → (y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x'
  injAt-out h y x x' p q = h y x x'
    (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q)

  injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x')
           → ⟨ γ ⊨ injAt f ⟩
```

向内的方向 `injAt-in` 沿同样的路径正向运输：把投影的单射性质作为关于 `Holds₀` 的假设，沿 `at₁`、`at₂` 本身运输两个隶属事实，得到两条前件的满足，假设随后给出公式结论所需的等式。两个方向合起来说明：该公式对单射性是充分的，既不强也不弱。

```agda
  injAt-in h y x x' p q = h y x x'
    (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)
```

## 提取一个取值于模型的单射

假设图是单值的且有恰当定义域，定义域的每个元素在图中都有某个像，但那只是仅仅存在的像：定义域隶属给出的是命题截断，而非选定的见证。单值性改变了局面。它表明对一个固定的输入，「一个输出连同该对属于图的证明」构成的类型是命题，而截断的值总能消去到命题中。于是图给出一个真正的、取值在模型中的函数；再假设单射性，便得到真正的单射。这第一层读回把取值保留为载体的元素，是后续证明仍需对编码图作推理时使用的形式。

本节把图 `F` 与定义域 `D` 作为模型元素，连同两个满足假设：变元零处图的单值性，以及断言 `D` 的每个元素在 `F` 下有取值的恰当定义域条款。环境 `γ` 按满足判断所期望的固定顺序把它们打包。

```agda
module Extract (F D : S)
               (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) where

  γ : S ^ 2
  γ = F ∷ D ∷ []
```

`Holds x y` 是底层对属于底层图的投影隶属。原像 `Fib x` 把一个输出 `y` 与这样的证明配成一对；它的元素就是图在 `x` 处的候选值，每个候选都带着「它确实是取值」的证书。

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

  Fib : S → Type (ℓ-suc ℓ)
  Fib x = Σ[ y ∈ S ] Holds x y

  isPropFib : (x : S) → isProp (Fib x)
```

要证明 `Fib x` 是命题，比较 `(y,p)` 与 `(y′,q)`。单值性先给出路径 `fst y ≡ fst y′`。内层 `Σ≡Prop` 利用 `S` 元素的第二分量即 `isL` 证书为命题，把该路径提升为 `y ≡ y′`；外层 `Σ≡Prop` 再利用图隶属证明为命题，把这一相等提升为 `Fib x` 的两个元素相等。这是两个不同的证明无关性步骤，并不是说周遭集合的相等仅由可构造性推出。

```agda
  isPropFib x (y , p) (y' , q) =
    Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst F))
      (Σ≡Prop (λ z → snd (isL z)) (svAt-out zero γ sv x y y' p q))

  toVal : (x : S) → ∥ Fib x ∥₁ → Fib x
  toVal x = PT.rec (isPropFib x) (λ z → z)
```

由于 `Fib x` 是命题，`toVal` 能把取值的截断存在 `∥ Fib x ∥₁` 消去为实际的原像。选择似乎藏在这里，其实没有：命题截断可以消去到任何命题值的目标，既不需要排中律也不需要选典范代表。定义域 `Dom` 把输入与其属于 `D` 的投影证明打包，`fib` 把由 `domAt-in` 得到的每个输入的截断像送入 `toVal`。

```agda
  Dom : Type (ℓ-suc ℓ)
  Dom = Σ[ x ∈ S ] ⟨ fst x ∈ fst D ⟩

  fib : (u : Dom) → Fib (fst u)
  fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m)

  toFun : Dom → S
```

函数 `toFun` 把定义域元素送到其唯一原像中的输出 `y : S`。它只舍去随附的图隶属证明；输出仍是模型元素，因此保留其可构造性证书。定理 `toFun-graph` 恰把这份被舍去的隶属证据作为原像的第二分量取回。

```agda
  toFun u = fst (fib u)

  toFun-graph : (u : Dom) → Holds (fst u) (toFun u)
  toFun-graph u = snd (fib u)

  module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where

    toFun-inj : (u v : Dom) → fst (toFun u) ≡ fst (toFun v)
```

再假设图的单射性，`toFun-inj` 把输出的相等变成输入的相等。若 `toFun u` 与 `toFun v` 的底层集合相等，就把 `u` 的图等式沿该路径运输，使两条目都谈及同一个输出即 `toFun v`；`injAt-out` 随后比较两个输入，给出 `fst u` 与 `fst v` 的第一分量之相等。结论是对投影后的第一分量陈述的，下游基数论证比较 `Dom` 的元素时用的正是这一形式。

```agda
              → fst (fst u) ≡ fst (fst v)
    toFun-inj u v e = injAt-out zero γ ij (toFun v) (fst u) (fst v)
      (subst (λ w → ⟨ pr (fst (fst u)) w ∈ fst F ⟩) e (toFun-graph u))
      (toFun-graph v)
```

## 限制到小载体

函数 `toFun` 作用在「模型元素连同隶属证明」的对上，这样的载体无法用于基数计数。最后一步把两端都换成典范的小呈现：定义域换成 `D` 的索引类型，值域换成调用方提供的集合 `C` 的索引类型，调用方只需证明图的每个取值都落在 `C` 中。图的三个条款，单值性、恰当定义域与单射性，在此一并假设。呈现层的贡献在于显式性：因为典范嵌入有命题值的原像，属于 `D` 或 `C` 都能从索引读出，也能读回索引。

参数点名了起作用的三个可构造集合：图 `F`、定义域 `D` 与值域 `C`。前三个假设正是 Extract 与 toFun-inj 所用的满足陈述。最后一条 `ran` 是新的：对任意输入 `x` 与使 `(x, y)` 属于图的取值 `y`，它证书化 `y` 的底层集合属于 `C` 的底层集合。这是作为调用方假设陈述的取值限制，因此本节本身从不假设图是以某个特定值域造出的。

```agda
module Small (F D C : S)
             (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
             (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩)
             (ij : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
             (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
```

内层模块以 `F`、`D` 与前两个满足证明重新打开 Extract，于是上一节的所有构造都以带前缀的名字可用。接着 `toS` 把 `D` 的典范呈现的一个索引 `m` 变成模型元素。第一分量就是被呈现的集合本身；第二分量是其可构造性证书，由 `isL-trans` 从显式隶属 `member (fst D) m` 与 `D` 自身可构造的证书得出。传递性正是所需的原理：可构造集合的成员是可构造的。

```agda
                  → ⟨ fst y ∈ fst C ⟩) where

  module E = Extract F D sv dm

  toS : ⟪ fst D ⟫ → S
  toS m = ⟪ fst D ⟫↪ m
        , isL-trans {x = fst D} {y = ⟪ fst D ⟫↪ m} (member (fst D) m) (snd D)
```

每个小索引还须被看作 Extract 意义下定义域的成员，`at` 提供这一对：模型元素 `toS m` 连同显式隶属证明 `member (fst D) m`。把 `at m` 经 `E.toFun` 喂给图得到一个取值，取值假设证书化该值属于 `C`。由于典范呈现中的隶属 `⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m))` 是具有命题值原像的嵌入的原像，`fiber` 返回的是实际的索引 `k` 连同一条路径，而非仅仅是截断的存在。

```agda
  at : ⟪ fst D ⟫ → E.Dom
  at m = toS m , member (fst D) m

  fib : (m : ⟪ fst D ⟫)
      → Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m)))
  fib m = fiber (fst C)
```

舍去路径便得到 `small`：从 `D` 的索引类型到 `C` 的索引类型的函数。每个定义域索引被送到「在图下的像」所对应的索引。至此两种表示会合：`small` 是固定宇宙层级上类型之间的映射，正是计数论证所需的形状，而它经由保留的路径与图联系在一起。

```agda
    (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m)))

  small : ⟪ fst D ⟫ → ⟪ fst C ⟫
  small m = fst (fib m)

  small-inj : (m n : ⟪ fst D ⟫) → small m ≡ small n → m ≡ n
  small-inj m n e = ↪-inj {a = fst D} {m = m} {n = n}
```

`small` 的单射性由索引的相等沿呈现往返证得。由 `small m ≡ small n`，反向取 `snd (fib m)` 得到 `m` 处的呈现值，嵌入下的同余把相等传过去，`snd (fib n)` 落到 `n` 处的呈现值；三条路径按这个确切方向拼接，使两个输出的底层集合相等。Extract 的单射性随之给出两个输入的底层集合相等，而 `↪-inj`，即定义域呈现嵌入在索引上的单射性，最终给出 `m ≡ n`。这里有两个不同的单射性事实在起作用，一个关于图，一个关于典范嵌入，二者不可互相替代。

```agda
    (E.toFun-inj ij (at m) (at n)
      (sym (snd (fib m)) ∙ cong ⟪ fst C ⟫↪ e ∙ snd (fib n)))
```

## 小结

`injAt` 在模型内部表达编码图的单射性。单值性与恰当定义域使 `Extract.toFun` 能把图读成取值于 `L` 的函数；独立假设 `ij` 才给出 `Extract.toFun-inj`。加上指定的值域条件后，`Small.small` 把该单射转移到定义域和值域的典范小成员类型上。截断步骤使用像原像的唯一性，呈现步骤则使用嵌入原像为命题这一性质。