---
title: "小呈现上的 Cantor–Schröder–Bernstein 定理"
module: V.CantorBernstein
lang: zh
site: "Bedrock"
description: "小呈现上的 Cantor–Schröder–Bernstein 定理"
stage: "序数、单射与基数"
reading_order: 93
canonical: https://bedrock.institute/zh/V.CantorBernstein.html
html: V.CantorBernstein.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/CantorBernstein.lagda.md
prerequisites: [Base.Prelude, Base.Classical]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/V.CantorBernstein.md, https://bedrock.institute/ja/V.CantorBernstein.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 小呈现上的 Cantor–Schröder–Bernstein 定理

两个集合的小呈现之间若有双向单射，便可得到双射。证明先在排中律下为小类型构造双射，再给出通用形式，把任意可双向读出的编码单射转成这类双射。

经典的 Cantor–Schröder–Bernstein 定理说，单射 $f : A → B$ 与 $g : B → A$ 给出双射 $A → B$。本章中两个类型共享同一个宇宙层级 ℓ，而唯一的额外假设是该层级上的排中律：对住在层级 ℓ 的每个命题，给出证明或反驳。论证本身属于指标类型 $A$ 与 $B$，而不属于累积层级中的集合；正因如此，后面才能把它原样搬到任意小呈现的成员类型上。证明需要用命题截断造出一些命题，然后对它们作判定；下面的设置因此同时固定了经典假设，以及将要施加于其上的命题值词汇。

层级 ℓ 上的判定在这里被打包一次并全章复用：`LEM ℓ` 取命题 `P : hProp ℓ`，返回 `⟨ P ⟩` 的证明，或一个反驳，即从 `⟨ P ⟩` 映入空类型的映射。因此模块参数 `lem` 只是这一个层级上的实例，而不是对所有层级都成立的全局原理。本章构造的一切都对它保持参数化，所以每当需要经典裁决时，这一假设都会显式出现。

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

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

module V.CantorBernstein {ℓ : Level} (lem : LEM ℓ) where

open import Cubical.Functions.Embedding using ( Embedding-into-isSet→isSet )
```

证明将用对存在命题作命题截断来构造若干命题：x 属于 g 的像这一陈述是 ∥ Σ[ y ∈ B ] (g y ≡ x) ∥₁，它仅保留原像存在这一事实，而不携带选定的原像。这类命题截断陈述借助 `squash₁` 成为命题，且其证明只能消解到命题值的目标中，不能得到任意数据。这一限制正是需要经典假设的原因：当论证需要选定原像时，把单纯的存在性变成选定的原像。

```agda
import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Empty.Properties using ( isProp⊥ )
import Cubical.HITs.PropositionalTruncation as PT
```

本章由两类命题主导：属于 g 的像，以及经由有限交错链可达。二者都存为 `hProp ℓ` 的元素，它把底层类型与「它是命题」的证明打包在一起；`⟨ P ⟩` 投影出底层类型，而命题性证明留在第二个分量。其余导入提供围绕它们的机制：坏/好情形分裂用的不交和、反驳一侧的 `isProp⊥`、对第二分量为命题值的序对作识别的 `Σ≡Prop`，以及累积层级本身与「集合的成员类型 `⟪ a ⟫` 嵌入到一个集合、因而它是 h-集合」这一事实。

```agda
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪ )
```

两个方向各一条单射，给出一个双射。本节在层级 ℓ 的排中律下，对同一宇宙层级的两个类型 $A$ 与 $B$(其中 $A$ 是 h-集合) 证明这一点。构造把 $A$ 的每个元素分为坏的或好的：坏元素是那些可由一条从 g 的像之外出发的有限交错原像链到达的元素。坏元素经 $f$ 向前送，好元素沿 g 的选定逆像送回。排中律进入两次：一次判定坏性命题 `C`，一次从命题截断的像陈述中提取选定的原像；链本身是谓词族 `Cₙ`，它唯一需要的结构事实是 $x ↦ g (f x)$ 保持坏性。

整个构造被打包进模块 `Bernstein`，它恰好接受经典的数据：两个类型、$A$ 的 h-集合结构，以及两条单射，每条由函数与其单射性证明共同给出。第一个成分是像谓词 `imG x`，它仅仅断言存在某个 $y ∈ B$ 使 $g y ≡ x$。这里不选定任何原像；命题截断 ∥ ⋯ ∥₁ 抹去见证而留下一个命题，`squash₁` 就是该命题性的证书。

```agda
module Bernstein {A B : Type ℓ} (setA : isSet A)
                 (f : A → B) (fi : (x y : A) → f x ≡ f y → x ≡ y)
                 (g : B → A) (gi : (x y : B) → g x ≡ g y → x ≡ y) where

  imG : A → hProp ℓ
  imG x = (∥ Σ[ y ∈ B ] (g y ≡ x) ∥₁ , squash₁)
```

坏性层级的基础说：当 x 完全不在 g 的像中时，x 在第零层是坏的。由于 `imG x` 的反驳是从 `⟨ imG x ⟩` 到空类型的映射，`C₀ x` 是函数类型；因为映入命题的函数仍是命题，所以它是命题。步进算子 `C₊ C x` 说：x 可从某个坏元素经一步后退到达，即仅仅存在 $y ∈ B$ 与 $z ∈ A$ 使 $g y ≡ x$、$f z ≡ y$、且 z 对 C 已经是坏的。从 `C₀` 出发迭代该算子得到 `Cₙ`，于是 `Cₙ n x` 的一个元记录了一条长为 n 的交错链：x = g y，y = f z，而 z 在低一层已是坏的。

```agda
  C₀ : A → hProp ℓ
  C₀ x = ((⟨ imG x ⟩ → Empty.⊥) , isPropΠ (λ _ → isProp⊥))

  C₊ : (A → hProp ℓ) → A → hProp ℓ
  C₊ C x = (∥ Σ[ y ∈ B ] Σ[ z ∈ A ] ((g y ≡ x) × ((f z ≡ y) × ⟨ C z ⟩)) ∥₁ , squash₁)

  Cₙ : ℕ → A → hProp ℓ
```

`Cₙ` 的两条定义等式是计算规则：指标为零时是基础谓词，后继时施加一步。完整的坏性命题 `C x` 则对所有链长一次命题截断：只要某个 `Cₙ n x` 单纯成立，x 就是坏的。这里的命题截断是本质的，它把层级中无穷多个层折叠成一个命题，排中律随后可以施加于其上。

```agda
  Cₙ zero = C₀
  Cₙ (suc n) = C₊ (Cₙ n)

  C : A → hProp ℓ
  C x = (∥ Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ ∥₁ , squash₁)
```

在使用该层级之前，先记录一条小型簿记引理：任意固定层 n 上的坏性证明给出坏性证明。其内容只是：序对 (n , proof) 是定义 `C` 的命题截断存在式的见证，而 ∣ ⋯ ∣₁ 把该见证注入命题截断。此后每个产出某长度链的论证都要经过这个映射。

```agda
  c-in : {x : A} {n : ℕ} → ⟨ Cₙ n x ⟩ → ⟨ C x ⟩
  c-in {x} {n} h = ∣ n , h ∣₁
```

引言承诺的那条结构事实现在得证：若 x 是坏的，则 g (f x) 也是坏的。给定一条长为 n、终于 x 的链，只需向后延伸一步：x 自身充当元素 z，f x 充当元素 y，所需的路径 g (f x) ≡ g (f x) 与 f x ≡ f x 都是自反性，而旧链是尾部。结果是一条长为 suc n、终于 g (f x) 的链。由于输入是命题截断的，消去 `PT.rec` 以输出的命题性为目标，这在 `C (g (f x))` 是命题时是合法的。

```agda
  gf-closed : {x : A} → ⟨ C x ⟩ → ⟨ C (g (f x)) ⟩
  gf-closed {x} = PT.rec (snd (C (g (f x)))) go
    where
    go : Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ → ⟨ C (g (f x)) ⟩
    go (n , cx) = c-in {x = g (f x)} {n = suc n} ∣ f x , x , (refl , (refl , cx)) ∣₁
```

g ∘ f 下的封闭性告诉我们坏性向前传播，但为了把元素经 h 路由，我们还需要向回看一层：每个坏性证明要么在第零层见底，要么 x 形如 g (f z) 且 z 是坏的。这正是 `C-view` 所交付的。目标本身是命题截断的，因此即便对链长 n 的情形分析是真正的数据，向其中消去也没有问题。

```agda
  C-view : {x : A} → ⟨ C x ⟩
         → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
  C-view {x} = PT.rec squash₁ go
    where
```

证明对记录的长度作情形分裂。长度为零时，链只是断言 x 在 g 的像之外，这恰是左析取支。长度为 suc n 时，保存的见证是三元组 y, z，满足 g y ≡ x、f z ≡ y 以及 z 的长为 n 的坏性证明；两条路径经 g 复合得 g (f z) ≡ x，更短的链由 `c-in` 纳入。右析取支恰是序对 (z，该路径，该更短证明) 的命题截断。这条引理是后面满性证明的核心：用在 g y 处，它要么直接反驳坏性，要么给出原像 z。

```agda
    go : Σ[ n ∈ ℕ ] ⟨ Cₙ n x ⟩ → ∥ (⟨ C₀ x ⟩ ⊎ (Σ[ z ∈ A ] ((g (f z) ≡ x) × ⟨ C z ⟩))) ∥₁
    go (zero , c0) = ∣ inl c0 ∣₁
    go (suc n , cs) = PT.map inr (PT.map (λ { (y , z , gy , fz , cz) →
        z , ((cong g fz ∙ gy) , c-in {x = z} {n = n} cz) }) cs)
```

排中律的第二次使用把好性转成像属于关系。设 x 是好的，取强意义：`C x` 容许一个反驳。判定命题 `imG x` 要么给出原像，这正是我们想要的，要么给出像属于的反驳，即 `C₀ x` 的证明。但第零层经 `c-in` 蕴含坏性，与假设的 `C x` 的反驳矛盾；由该矛盾可推出任何东西。于是 `notC→imG` 产出 `⟨ imG x ⟩` 的一个元，仍只表明原像存在，还没有选定原像。

```agda
  notC→imG : {x : A} → (⟨ C x ⟩ → Empty.⊥) → ⟨ imG x ⟩
  notC→imG {x} nC = Sum.rec {A = ⟨ imG x ⟩} {B = ⟨ imG x ⟩ → Empty.⊥} {C = ⟨ imG x ⟩}
    (λ h → h) (λ nC₀ → Empty.rec (nC (c-in {n = zero} nC₀)))
    (lem (imG x))
```

为了把单纯的像属于变成选定的原像，可以把命题截断直接消去到纤维类型 Σ[ y ∈ B ] (g y ≡ x) 本身，只要该类型是命题。这正是 g 与 A 上的假设发挥作用之处：g 的单射性利用到 g x 的两条路径 p 与 p′ 证明任意两个原像 y 与 y′ 相等，而 A 的 h-集合结构使 A 中所得的相等成为命题，`Σ≡Prop` 再把这一点扩展到整个序对。注意 h-集合假设恰好只在这里、构造中的其他地方都不需要。

```agda
  fiberG-prop : (x : A) → isProp (Σ[ y ∈ B ] (g y ≡ x))
  fiberG-prop x (y , p) (y' , p') = Σ≡Prop {A = B} {B = λ y → g y ≡ x}
    (λ y → setA (g y) x) (gi y y' (p ∙ sym p'))
```

有了纤维的命题性，`fiberG` 就是把命题截断的像陈述消去到纤维类型：由于目标是命题，`PT.rec` 以纤维上的恒等映射为作用即可应用。这是论证中第一个选定原像作为数据而非仅仅存在的位置，而打开它的正是排中律加 h-集合结构，不是命题截断自身的任何性质。

```agda
  fiberG : (x : A) → ⟨ imG x ⟩ → Σ[ y ∈ B ] (g y ≡ x)
  fiberG x = PT.rec (fiberG-prop x) (λ w → w)
```

对好元素 x，选定的原像现在可以命名为 `ginv x`：它是 `fiberG` 由 `notC→imG` 产出的纤维的第一个分量。其规格 `ginv-spec` 记录 g (ginv x) ≡ x，取自同一纤维的第二个分量。于是在好的一侧，h 将把 x 送回 B 中一个 g-像恰为 x 的点，这正是作为 g 的逆片段应有的行为。

```agda
  ginv : {x : A} → (⟨ C x ⟩ → Empty.⊥) → B
  ginv {x} nC = fiberG x (notC→imG nC) .fst

  ginv-spec : {x : A} (nC : ⟨ C x ⟩ → Empty.⊥) → g (ginv nC) ≡ x
  ginv-spec {x} nC = fiberG x (notC→imG nC) .snd
```

候选双射 h 现在定义在假想的裁决上，而非直接定义在 A 上：给定 x 与坏性命题 `C x` 的判定 d，坏情形送 x 到 f x，好情形送到 `ginv x`。把裁决作为显式参数处理使情形分析保持诚实；随后两条引理，即相对于裁决的单射性与满射性，将在本节末与 `lem` 提供的实际判定相结合。

```agda
  h : (x : A) → ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) → B
  h x (inl _) = f x
  h x (inr nC) = ginv nC
```

h 的单射性按裁决对作四种情形证明。两侧都坏时，h 两侧都是 f，由 f 的单射性立即完成。当 x 坏而 x′ 好时，假设 h x dx ≡ h x′ dx′ 说 g (f x) ≡ ginv x′，施加 g 并用 ginv 的规格得 g (g (f x)) ≡ x′。由于坏性沿 g ∘ f 传播，x 坏使 g (f x) 坏；用 `subst` 把 g (f x) 的坏性沿该路径搬运即得 x′ 坏，与 x′ 好的裁决矛盾。

```agda
  h-inj : (x x' : A) (dx : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) (dx' : ⟨ C x' ⟩ ⊎ (⟨ C x' ⟩ → Empty.⊥))
        → h x dx ≡ h x' dx' → x ≡ x'
  h-inj x x' (inl cx) (inl cx') e = fi x x' e
  h-inj x x' (inl cx) (inr nCx') e =
    Empty.rec (nCx' (subst (λ w → ⟨ C w ⟩) (cong g e ∙ ginv-spec nCx') (gf-closed {x = x} cx)))
```

镜像情形，x 好 x′ 坏，是对称的：搬运沿反向路径进行，被消灭的是 x。最后一种情形两侧都好，h 两侧都是 ginv，等式读作 ginv x ≡ ginv x′。施加 g 把它变成 g (ginv x) ≡ g (ginv x′)，两侧串上 ginv 的两条规格便直接得 x ≡ x′。这条引理处处未用 h-集合假设；单射性纯粹是对裁决的情形分析。

```agda
  h-inj x x' (inr nCx) (inl cx') e =
    Empty.rec (nCx (subst (λ w → ⟨ C w ⟩) (sym (cong g e) ∙ ginv-spec nCx) (gf-closed {x = x'} cx')))
  h-inj x x' (inr nCx) (inr nCx') e = sym (ginv-spec nCx) ∙ cong g e ∙ ginv-spec nCx'
```

相对于裁决的满射性对每个 y ∈ B 陈述，裁决取在 A 的元素 g y 上，而非 B 的元素上。好情形下原像就是 g y 自身：按假设它是好的，h 把它送到 `ginv (g y)`，再用 ginv 的规格与 g 的单射性把该值等同于 y。见证被打包成命题截断序对，因为最终定理只宣称仅仅存在的满射性。

```agda
  h-surj : (y : B) (d : ⟨ C (g y) ⟩ ⊎ (⟨ C (g y) ⟩ → Empty.⊥))
         → ∥ Σ[ x ∈ A ] Σ[ dx ∈ ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥) ] (h x dx ≡ y) ∥₁
  h-surj y (inr nCgy) = ∣ g y , inr nCgy , gi (ginv nCgy) y (ginv-spec nCgy) ∣₁
```

g y 是坏的情形下，`C-view` 把坏性证明分解为两个选项。第一个说 g y 在 g 的像之外，但 y 自己用自反路径见证了它的像属于关系，这矛盾可推出任何东西，特别是所需的命题截断陈述。第二个给出 z ∈ A 使 g (f z) ≡ g y 且 z 是坏的；此时 z 是原像，因为 h z = f z 且 g (f z) 等于 g y，再由 g 的单射性把 f z 等同于 y。两个分支都在单个命题截断内展示其见证，因此除已假设的裁决外不消耗其他裁决。

```agda
  h-surj y (inl cgy) = PT.rec squash₁
    (λ { (inl c0) → Empty.rec (c0 ∣ y , refl ∣₁) ; (inr (z , gfy , cz)) → ∣ z , inl cz , gi (f z) y gfy ∣₁ })
    (C-view {x = g y} cgy)
```

最后一条引理回应针对整个设计的一个异议：h 是相对于裁决定义的，而定理需要 A 上的单个函数。`h-cons` 说裁决的选择无关紧要：对固定的 x，两个输出相等。都坏时是自反性；混合情形是矛盾的，因为一个裁决反驳另一个的见证；都好时归结为选定原像的唯一性：`fiberG` 产出的两个纤维因纤维类型是命题而相等，取第一分量经合质性保持该相等。正是这种一致性使依赖裁决的构造成为映射的真正定义。

```agda
  h-cons : (x : A) (dx dx' : ⟨ C x ⟩ ⊎ (⟨ C x ⟩ → Empty.⊥)) → h x dx ≡ h x dx'
  h-cons x (inl cx) (inl cx') = refl
  h-cons x (inl cx) (inr nCx') = Empty.rec (nCx' cx)
  h-cons x (inr nCx) (inl cx) = Empty.rec (nCx cx)
  h-cons x (inr nCx) (inr nCx') = cong fst (fiberG-prop x (fiberG x (notC→imG nCx)) (fiberG x (notC→imG nCx')))
```

一致性建立之后，裁决可以一次性给定。接下来三行组装出定理。

```agda
  ĥ : A → B
```

映射 `ĥ` 是 h 施加于典范裁决 `lem (C x)`：排中律判定每个 x 的坏性，而 h-cons 保证任何其他判定都会产出相同的值。这里正是模块假设 `lem` 被定义本身消耗之处。

```agda
  ĥ x = h x (lem (C x))
```

单射性从相对版本逐字转移，因为典范裁决正是裁决参数的特殊选取：`ĥ-inj x x' e` 恰是这些裁决处的 `h-inj`。

```agda
  ĥ-inj : (x x' : A) → ĥ x ≡ ĥ x' → x ≡ x'
  ĥ-inj x x' e = h-inj x x' (lem (C x)) (lem (C x')) e
```

满射性需要额外一步。相对引理 `h-surj` 施加于 g y 的典范裁决，给出命题截断的三元组 x、dx 及路径 h x dx ≡ y，但其前两个分量谈的是假想的 h x dx 而非 `ĥ x`。沿 `h-cons x dx (lem (C x))` 改写，它识别这两个值，再前置对称路径，就把三元组转成 `ĥ x ≡ y` 的见证。整个陈述仍是命题截断的：定理断言原像仅仅存在。

```agda
  ĥ-surj : (y : B) → ∥ Σ[ x ∈ A ] (ĥ x ≡ y) ∥₁
  ĥ-surj y = PT.map (λ { (x , dx , e) → x , sym (h-cons x dx (lem (C x))) ∙ e })
    (h-surj y (lem (C (g y))))
```

抽象构造现在应用于累积层级本身。V 的每个元素 a 都带有成员类型 ⟪ a ⟫，即其成员的类型。Bernstein 构造要求第一个类型具有 h-集合结构，所以第一步是证明 ⟪ a ⟫ 是 h-集合。嵌入 ⟪ a ⟫↪ 把每个成员指标送到它在 V 内所指标的成员；由于 V 是 h-集合且该映射是嵌入，其定义域继承了 h-集合性。有了这一条事实，⟪ a ⟫ 与 ⟪ b ⟫ 之间的两条互逆单射便产生一个打包成依赖三元组的双射。

h-集合性证书由两条已导入的事实复合而成。映射 ⟪ a ⟫↪ 是到 V 的嵌入，即其所有纤维都是命题；而层级 V 经其构造子 setIsSet 是 h-集合。嵌入到 h-集合中的类型自身是 h-集合，因为定义域中的相等可以在施加该映射之后比较。随后的签名以与抽象定理相同的形状陈述集合论推论：从 ⟪ a ⟫ 到 ⟪ b ⟫ 的单射 f 与返回的单射 g，连同各自的单射性证明，作为显式假设。

```agda
small-set : (a : V ℓ) → isSet (⟪ a ⟫)
small-set a = Embedding-into-isSet→isSet (⟪ a ⟫↪ , isEmb⟪ a ⟫↪) setIsSet

cantor-bernstein : (a b : V ℓ) (f : ⟪ a ⟫ → ⟪ b ⟫)
    → ((x y : ⟪ a ⟫) → f x ≡ f y → x ≡ y)
    → (g : ⟪ b ⟫ → ⟪ a ⟫) → ((x y : ⟪ b ⟫) → g x ≡ g y → x ≡ y)
```

结果类型是显式的依赖三元组而非记录：从 ⟪ a ⟫ 到 ⟪ b ⟫ 的函数 h，其单射性作为命题值分量，以及仅仅存在的满射性，即对 ⟪ b ⟫ 的每个 y 断言一个命题截断的原像。两侧条件之间的不对称是刻意的，与抽象定理一致：单射性作为真正的数据陈述，满射性只作为单纯存在陈述。陈述中没有任何对层级的层或属于关系的量化；一切都发生在两个成员类型内部。

```agda
    → Σ[ h ∈ (⟪ a ⟫ → ⟪ b ⟫) ]
        (((x y : ⟪ a ⟫) → h x ≡ h y → x ≡ y)
      × ((y : ⟪ b ⟫) → ∥ Σ[ x ∈ ⟪ a ⟫ ] (h x ≡ y) ∥₁))
cantor-bernstein a b f fi g gi = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )
  where
```

证明是一次单独的实例化。把模块 `Bernstein` 在 A = ⟪ a ⟫、B = ⟪ b ⟫ 处实例化，为 A 提供 h-集合性证书，两条单射原样传入，即暴露出分量 ĥ、ĥ-inj 与 ĥ-surj；定义把它们组装成三元组。上一节的全部工作未经修改地被复用。

```agda
  module M = Bernstein {A = ⟪ a ⟫} {B = ⟪ b ⟫} (small-set a) f fi g gi
```

上面的推论把 V 的成员类型写死了。更可复用的形式使设置保持抽象：一个码的载体 `C`、给每个码指派一个小类型的 `P`，以及表达「a 编码了从 P a 到 P b 的单射」的关系 `R a b`。把这一抽象与上一节联系起来的是读回 `read`：从 R a b 的一个元提取出真实的函数及其单射性证明。给定两个方向各一条这样的读回，Bernstein 构造便可逐字应用。这里提供两个入口：一个把这对编码单射作为数据，一个单纯地接受它，此时双射也单纯地存在。

参数恰好列出所需的强度。载体 C 住在自己的层级 ℓ₁，关系 R 在 ℓ₂，因此码及其关系不必是小的；必须小的是每个 P a，它住在排中律可用的固定层级 ℓ。对每个 a，假设 P a 是 h-集合，对应 Bernstein 模块的 h-集合性假设。关系 R 本身作为类型完全任意：除读回外对它不作任何假设，读回从 R a b 的元返回一个序对，第一分量是函数 P a → P b，第二分量是该函数的单射性证明。特别地，提取出的单射是真正的数据，不是命题截断的存在。

```agda
module MutualInj {ℓ₁ ℓ₂ : Level} (C : Type ℓ₁) (P : C → Type ℓ)
    (R : (a b : C) → Type ℓ₂)
    (setP : (a : C) → isSet (P a))
    (read : (a b : C) → R a b
          → Σ[ f ∈ (P a → P b) ] ((x y : P a) → f x ≡ f y → x ≡ y)) where
```

第一个入口以两条编码单射为显式参数陈述转移：从 R a b 中的前向码与 R b a 中的后向码，它以与上一节完全相同的形状返回 P a 与 P b 之间的双射三元组。陈述量化的是关系的元而非其命题截断，因此码全程作为数据可用。

```agda
  mutual→bijection : (a b : C) → R a b → R b a
    → Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁))
  mutual→bijection a b fwd bwd = M.ĥ , ( M.ĥ-inj , M.ĥ-surj )
```

定义在 A = P a、B = P b 处实例化 Bernstein 模块，读回正是在此被消耗。前向码 fwd 经 `read a b` 拆解为函数与单射性分量，后向码同理，只是 R 与 read 的参数对调；每个分量由第一、第二分量的投影选取。h-集合性字段接受 `setP a`。于是到达 Bernstein 模块的是真正的单射，那里证明的一切原样适用。

```agda
    where
    module M = Bernstein {A = P a} {B = P b} (setP a)
      (read a b fwd .fst) (read a b fwd .snd)
      (read b a bwd .fst) (read b a bwd .snd)
```

第二个入口把输入弱化为单纯存在：收到的不是码，而是「这样的码单纯存在」的命题截断陈述。其结论相应地被弱化两次。双射陈述本身被命题截断，而满射性本来就在内部是命题截断的；因此最终类型断言的是双射仅仅存在，而非任何特定的一个可被点名。这种弱化不可逆：输入上的命题截断无法消去到双射的数据中，只能消去到命题值的目标，而整个陈述恰是这样的目标。

```agda
  ∃bijection : (a b : C) → ∥ R a b ∥₁ → ∥ R b a ∥₁
    → ∥ Σ[ h ∈ (P a → P b) ]
        (((x y : P a) → h x ≡ h y → x ≡ y)
      × ((y : P b) → ∥ Σ[ x ∈ P a ] (h x ≡ y) ∥₁)) ∥₁
  ∃bijection a b fwd bwd = PT.rec squash₁
```

证明嵌套两次命题截断消去。消去 fwd 得到某个码 w；消去 bwd 得到 w′；内层消去的目标是整个双射陈述的命题截断，由 squash₁ 是命题，因此从 `mutual→bijection` 产出显式三元组并用 ∣ ⋯ ∣₁ 注入是合法的。两次消去的顺序无关紧要，因为两个目标都是命题。

```agda
    (λ w → PT.rec squash₁ (λ w' → ∣ mutual→bijection a b w w' ∣₁) bwd)
    fwd
```