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

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

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

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

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

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

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )

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

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

setPL a = small-set (a .fst)
readL : (a b : S) → Σ[ F ∶ S ] InjCode F a b
      → Σ[ f ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
          ((x y : ⟪ a .fst ⟫) → 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 → ⟪ a .fst ⟫)
  (λ 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 ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
       (((x y : ⟪ a .fst ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ b .fst ⟫) → ∥ Σ[ x ∶ ⟪ a .fst ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection