Cantor–Schröder–Bernstein inside L

Fix a universe level ℓ and assume lem : LEM (ℓ-suc ℓ). This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

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 ⟪ a .fst ⟫; coded injections belong to the object theory, whereas functions between these member types belong to the metatheory.

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.

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 ( ⟪_⟫ )

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

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 (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

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 → ⟪ a .fst ⟫)
  (λ 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 ∶ (⟪ 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