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