Cantor–Schröder–Bernstein inside L

Suppose two constructible sets admit coded injections in both directions. Their member types then admit a bijection, merely as an existence statement. This is the internal form of the Cantor–Schröder–Bernstein theorem used here: the hypotheses are expressed in the language of L, while the resulting bijection compares the ordinary types presenting the two sets.

The argument passes through two levels. A set of L carries an underlying set in the ambient cumulative hierarchy. Its members form an ordinary type, written ⟪ fst a ⟫; coded injections belong to the object theory, whereas functions between these member types belong to the metatheory.

{-# 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 )

To apply the type-level theorem, each member type must be an h-set. The cumulative hierarchy already supplies this property: paths between two members carry no additional higher information. Thus setPL provides exactly the h-set certificate required for every presentation.

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 )

An injection code consists of a constructible graph together with three satisfaction facts and one value-range condition. They say that the graph is single-valued, has the prescribed domain, is injective, and sends every input into the prescribed codomain. These conditions contain precisely the information needed to recover a metatheoretic injection.

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 ⟫)

The function readL performs this passage. Given a coded graph from a to b, it returns an actual function from the members of a to the members of b, together with a proof that equal outputs have equal inputs. The construction itself is supplied by the preceding analysis of coded injections.

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

The abstract Cantor–Schröder–Bernstein argument can now be instantiated with constructible sets as objects, their member types as presentations, and coded graphs as injections. The h-set certificates and readL verify its two structural requirements. The same instantiation provides both a version for explicit witnesses and a version for merely existing witnesses.

  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

The public theorem uses the second form because InjL records only the propositional truncation of an injection code. From the two truncated hypotheses it therefore derives a truncated bijection. Excluded middle is used inside the underlying type-level proof to separate the Cantor–Schröder–Bernstein construction into its cases; unique preimages are recovered from injectivity and the h-set condition, rather than from any choice principle.

  → ∥ Σ[ 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