L 内部的 Cantor–Schröder–Bernstein 定理

设两个可构造集合之间存在双向的编码单射，那么它们的成员类型之间仅仅存在一个双射。这是本章采用的 Cantor–Schröder–Bernstein 定理的内部形式：假设用 L 的语言表述，所得双射则比较这两个集合对应的普通类型。

论证在两个层面之间进行。L 的集合带有外围累积层级中的底层集合，其成员组成普通类型 ⟪ fst a ⟫。编码单射属于对象理论，而这些成员类型之间的函数属于元理论。

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

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

module L.CantorBernstein {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )

要使用类型层的定理，每个成员类型都必须是h-集合。累积层级已经保证这一性质：两个成员之间的路径不再含有更高层的额外信息。因此，setPL 为每个呈现给出所需的h-集合证书。

open import V.CantorBernstein {ℓ} (lowerLEM lem)
  using ( small-set; module MutualInj )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.Coding.Injection {ℓ} lem using ( module Small )

一个单射码由一个可构造图、三条满足事实和一条值域条件组成。它们分别说明该图是单值的、具有指定定义域、满足单射性，并把每个输入送入指定陪域。这些条件恰好足以恢复一条元理论中的单射。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )
setPL : (a : S) → isSet (⟪ fst a ⟫)

函数 readL 完成这一转换。给定从 a 到 b 的编码图，它返回一个从 a 的成员到 b 的成员的实际函数，并证明输出相等必有输入相等。这一构造来自前面对编码单射的分析。

setPL a = small-set (fst a)
readL : (a b : S) → Σ[ F ∈ S ] InjCode F a b
      → Σ[ f ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
          ((x y : ⟪ fst a ⟫) → f x ≡ f y → x ≡ y)
readL a b (F , sv , dm , ij , ran) = SM.small , SM.small-inj

现在可以把抽象的 Cantor–Schröder–Bernstein 论证应用于这一情形：对象取可构造集合，呈现取其成员类型，单射取编码图。h-集合证书与 readL 验证了所需的两项结构条件。同一次实例化既给出使用显式见证的版本，也给出仅仅假定见证存在的版本。

  where
  module SM = Small F a b sv dm ij ran

module MutualInjL = MutualInj S (λ a → ⟪ fst a ⟫)
  (λ a b → Σ[ F ∈ S ] InjCode F a b) setPL readL
mutual-inj→bijection : (a b : S) → InjL a b → InjL b a

公开的定理采用后一种形式，因为 InjL 只保留单射码的命题截断。因此，两个截断的假设导出一个截断的双射。排中律在底层类型论证明中用来区分 Cantor–Schröder–Bernstein 构造的各种情形；唯一原像由单射性与h-集合条件恢复，并不依赖任何选择原理。

  → ∥ Σ[ h ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
       (((x y : ⟪ fst a ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ fst b ⟫) → ∥ Σ[ x ∈ ⟪ fst a ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection