---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
```

# Cantor–Schröder–Bernstein inside L

```agda
open import Base.Prelude
open import Base.Classical using ( LEM; lowerLEM )
```

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.

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

```agda
open import FOL.ZFStructure using ( module hPropView )
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 )
```

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.

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

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

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

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