---
title: "Cantor–Schröder–Bernstein inside L"
module: L.CantorBernstein
lang: en
site: "Bedrock"
description: "Cantor–Schröder–Bernstein inside L"
stage: "Ordinals, injections and cardinals"
reading_order: 94
canonical: https://bedrock.institute/en/L.CantorBernstein.html
html: L.CantorBernstein.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/CantorBernstein.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.CantorBernstein, L.Constructible, L.Cardinal, L.Coding.Injection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.CantorBernstein.md, https://bedrock.institute/ja/L.CantorBernstein.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
  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.

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