The Cantor–Schröder–Bernstein theorem for decidable embeddings

Content created by Fredrik Bakke.

Created on 2025-10-29.
Last modified on 2025-10-29.

module foundation.cantor-schroder-bernstein-decidable-embeddings where

open import foundation.action-on-identifications-functions
open import foundation.decidable-embeddings
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.double-negation-dense-equality-maps
open import foundation.double-negation-images
open import foundation.function-types
open import foundation.injective-maps
open import foundation.perfect-images
open import foundation.retracts-of-types
open import foundation.sections
open import foundation.universe-levels
open import foundation.weak-limited-principle-of-omniscience

open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.negation

open import logic.double-negation-eliminating-maps
open import logic.double-negation-stable-embeddings

Idea

The Cantor–Schröder–Bernstein theorem^¶ for decidable embeddings states that, assuming the weak limited principle of omniscience (WLPO), then if two types A and B mutually embed via embeddings whose fibers are decidable, then A and B are equivalent types.

Classically, i.e., under the assumption of the law of excluded middle, the Cantor–Schröder–Bernstein theorem asserts that from any pair of injective maps between sets f : A → B and g : B → A we can construct a bijection between A and B. In a recent generalization, Martín Escardó proved that the Cantor–Schröder–Bernstein theorem also holds for ∞-groupoids [Esc21]. His generalization asserts that given two types that embed into each other, then the types are equivalent.

In this file we give a fine-grained deconstruction of the construction used in the proof of this Cantor–Schröder–Bernstein-Escardó theorem, originally due to König [Kon06], and use this to give the generalization of the theorem for decidable embeddings under the assumption of the weak limited principle of omniscience.

Construction

Given a pair of mutually converse maps f : A → B and g : B → A such that

1. the maps f and g satisfy double negation elimination on their fibers
2. f has double negation dense equality
3. g is injective
4. the perfect image of g relative to f is decidable

then B is a retract of A. If f moreover is injective, then this retract is an equivalence.

This can be understood as an entirely constructive formulation of the Cantor–Schröder–Bernstein theorem.

The reader may also note that under the additional assumption of function extensionality, double negation eliminating injections are double negation stable embeddings.

The underlying map A → B of the construction.

module _
  {l1 l2 : Level}
  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  where

  map-construction-Cantor-Schröder-Bernstein' :
    (x : A) → is-decidable (is-perfect-image f g x) → B
  map-construction-Cantor-Schröder-Bernstein' x (inl γ) =
    inverse-of-perfect-image x γ
  map-construction-Cantor-Schröder-Bernstein' x (inr nγ) =
    f x

  map-construction-Cantor-Schröder-Bernstein :
    (D : (x : A) → is-decidable (is-perfect-image f g x)) → A → B
  map-construction-Cantor-Schröder-Bernstein D x =
    map-construction-Cantor-Schröder-Bernstein' x (D x)

Computing the underlying map A → B of the construction.

  compute-map-construction-Cantor-Schröder-Bernstein' :
    (G' : is-injective g) →
    (y : B) →
    (γ : is-perfect-image f g (g y)) →
    (d : is-decidable (is-perfect-image f g (g y))) →
    map-construction-Cantor-Schröder-Bernstein'
      ( g y) d ＝
    y
  compute-map-construction-Cantor-Schröder-Bernstein' G' y γ (inl v') =
    is-retraction-inverse-of-perfect-image G' y v'
  compute-map-construction-Cantor-Schröder-Bernstein' G' y γ (inr v) =
    ex-falso (v γ)

  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein :
    (G : is-double-negation-eliminating-map g)
    (G' : is-injective g)
    (F : is-double-negation-eliminating-map f)
    (F' : has-double-negation-dense-equality-map f) →
    (y : B) →
    (nγ : ¬ (is-perfect-image f g (g y))) →
    (d :
      is-decidable
        ( is-perfect-image f g
          ( element-has-not-perfect-fiber-is-not-perfect-image
              G G' F F' y nγ))) →
    map-construction-Cantor-Schröder-Bernstein'
      ( element-has-not-perfect-fiber-is-not-perfect-image G G' F F' y nγ)
      ( d) ＝
    y
  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
    G G' F F' y nγ (inl v) =
    ex-falso
      ( is-not-perfect-image-has-not-perfect-fiber-is-not-perfect-image
          G G' F F' y nγ v)
  compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
    G G' F F' y nγ (inr _) =
    is-in-fiber-element-has-not-perfect-fiber-is-not-perfect-image
      G G' F F' y nγ

The underlying section B → A of the construction.

module _
  {l1 l2 : Level}
  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  (G : is-double-negation-eliminating-map g)
  (G' : is-injective g)
  (F : is-double-negation-eliminating-map f)
  (F' : has-double-negation-dense-equality-map f)
  where

  map-section-construction-Cantor-Schröder-Bernstein' :
    (y : B) → is-decidable (is-perfect-image f g (g y)) → A
  map-section-construction-Cantor-Schröder-Bernstein' y (inl _) =
    g y
  map-section-construction-Cantor-Schröder-Bernstein' y (inr nγ) =
    element-has-not-perfect-fiber-is-not-perfect-image G G' F F' y nγ

  map-section-construction-Cantor-Schröder-Bernstein :
    (D : (y : B) → is-decidable (is-perfect-image f g (g y))) →
    B → A
  map-section-construction-Cantor-Schröder-Bernstein D y =
    map-section-construction-Cantor-Schröder-Bernstein' y (D y)

  is-section-map-section-construction-Cantor-Schröder-Bernstein' :
    (y : B)
    (d : is-decidable (is-perfect-image f g (g y))) →
    (d' :
      is-decidable
        ( is-perfect-image f g
          ( map-section-construction-Cantor-Schröder-Bernstein' y d))) →
    map-construction-Cantor-Schröder-Bernstein'
      ( map-section-construction-Cantor-Schröder-Bernstein' y d)
      ( d') ＝
    y
  is-section-map-section-construction-Cantor-Schröder-Bernstein' y (inl γ) =
    compute-map-construction-Cantor-Schröder-Bernstein' G' y γ
  is-section-map-section-construction-Cantor-Schröder-Bernstein' y (inr nγ) =
    compute-map-construction-on-not-perfect-image-Cantor-Schröder-Bernstein
      G G' F F' y nγ

  is-section-map-section-construction-Cantor-Schröder-Bernstein :
    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
    is-section
      ( map-construction-Cantor-Schröder-Bernstein D)
      ( map-section-construction-Cantor-Schröder-Bernstein (D ∘ g))
  is-section-map-section-construction-Cantor-Schröder-Bernstein D y =
    is-section-map-section-construction-Cantor-Schröder-Bernstein' y
      ( D (g y))
      ( D (map-section-construction-Cantor-Schröder-Bernstein (D ∘ g) y))

  section-construction-Cantor-Schröder-Bernstein :
    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
    section (map-construction-Cantor-Schröder-Bernstein D)
  section-construction-Cantor-Schröder-Bernstein D =
    ( map-section-construction-Cantor-Schröder-Bernstein (D ∘ g) ,
      is-section-map-section-construction-Cantor-Schröder-Bernstein D)

  retract-construction-Cantor-Schröder-Bernstein :
    (D : (x : A) → is-decidable (is-perfect-image f g x)) →
    B retract-of A
  retract-construction-Cantor-Schröder-Bernstein D =
    retract-section
      ( map-construction-Cantor-Schröder-Bernstein D)
      ( section-construction-Cantor-Schröder-Bernstein D)

Injectivity of the constructed map.

module _
  {l1 l2 : Level}
  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  (F' : is-injective f)
  where

  is-injective-map-construction-Cantor-Schröder-Bernstein' :
    {x x' : A}
    (d : is-decidable (is-perfect-image f g x))
    (d' : is-decidable (is-perfect-image f g x')) →
    map-construction-Cantor-Schröder-Bernstein' x d ＝
    map-construction-Cantor-Schröder-Bernstein' x' d' →
    x ＝ x'
  is-injective-map-construction-Cantor-Schröder-Bernstein'
    {x} {x'} (inl ρ) (inl ρ') p =
    ( inv (is-section-inverse-of-perfect-image x ρ)) ∙
    ( ap g p) ∙
    ( is-section-inverse-of-perfect-image x' ρ')
  is-injective-map-construction-Cantor-Schröder-Bernstein'
    {x} {x'} (inl ρ) (inr nρ') p =
    ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p))
  is-injective-map-construction-Cantor-Schröder-Bernstein'
    {x} {x'} (inr nρ) (inl ρ') p =
    ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p)
  is-injective-map-construction-Cantor-Schröder-Bernstein'
    {x} {x'} (inr nρ) (inr nρ') p =
    F' p

Piecing it all together.

module _
  {l1 l2 : Level}
  {A : UU l1} {B : UU l2} {f : A → B} {g : B → A}
  (G : is-double-negation-eliminating-map g)
  (G' : is-injective g)
  (F : is-double-negation-eliminating-map f)
  (F'' : is-injective f)
  (D : (x : A) → is-decidable (is-perfect-image f g x))
  where

  is-equiv-map-construction-Cantor-Schröder-Bernstein :
    is-equiv (map-construction-Cantor-Schröder-Bernstein D)
  is-equiv-map-construction-Cantor-Schröder-Bernstein =
    is-equiv-is-injective
      ( section-construction-Cantor-Schröder-Bernstein G G' F
        ( has-double-negation-dense-equality-map-is-emb
          ( is-emb-is-injective-is-double-negation-eliminating-map F F''))
        ( D))
      ( λ {x} {x'} →
        is-injective-map-construction-Cantor-Schröder-Bernstein' F''
          ( D x)
          ( D x'))

  equiv-construction-Cantor-Schröder-Bernstein : A ≃ B
  equiv-construction-Cantor-Schröder-Bernstein =
    ( map-construction-Cantor-Schröder-Bernstein D ,
      is-equiv-map-construction-Cantor-Schröder-Bernstein)

Theorem

It follows from the weak limited principle of omniscience that, for every pair of mutual decidable embeddings f : A ↪ B and g : B ↪ A, it is decidable for every element x : A whether x is a perfect image of g relative to f. Applying this fact to the Cantor-Schröder-Bernstein construction, we conclude with the main result.

module _
  {l1 l2 : Level} (wlpo : level-WLPO (l1 ⊔ l2))
  {A : UU l1} {B : UU l2}
  where

  abstract
    Cantor-Schröder-Bernstein-WLPO' :
      {f : A → B} {g : B → A} →
      is-decidable-emb g →
      is-decidable-emb f →
      A ≃ B
    Cantor-Schröder-Bernstein-WLPO' G F =
      equiv-construction-Cantor-Schröder-Bernstein
        ( is-double-negation-eliminating-map-is-decidable-emb G)
        ( is-injective-is-decidable-emb G)
        ( is-double-negation-eliminating-map-is-decidable-emb F)
        ( is-injective-is-decidable-emb F)
        ( is-decidable-is-perfect-image-WLPO wlpo
          ( G)
          ( is-decidable-map-is-decidable-emb F)
          ( has-double-negation-dense-equality-map-is-emb
            ( is-emb-is-decidable-emb F)))

    Cantor-Schröder-Bernstein-WLPO : (A ↪ᵈ B) → (B ↪ᵈ A) → A ≃ B
    Cantor-Schröder-Bernstein-WLPO (f , F) (g , G) =
      Cantor-Schröder-Bernstein-WLPO' G F

References

• Escardó’s formalizations of this theorem can be found at https://www.cs.bham.ac.uk/~mhe/TypeTopology/CantorSchroederBernstein.index.html. [Esc]

[Esc21]

Martín Hötzel Escardó. The Cantor–Schröder–Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3):363–366, 09 2021. arXiv:2002.07079, doi:10.1007/s40062-021-00284-6.

[Esc]

Martín Hötzel Escardó and contributors. TypeTopology. GitHub repository. Agda development. URL: https://github.com/martinescardo/TypeTopology.

[Kon06]

J. König. Sur la théorie des ensembles. Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, 143:110–112, 1906. URL: https://gallica.bnf.fr/ark:/12148/bpt6k30977.image.f110.langEN.

[Wie]

Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

See also

The Cantor–Schröder–Bernstein theorem holds constructively for many notions of finite type, including

• Dedekind finite types
• Finite types (unformalized)
• Finitely enumerable types
• Kuratowski finite sets
• Subfinite types
• Subfinitely enumerable types

External links

• See also the twin formalization in TypeTopology at CantorSchroederBernstein.CSB-WLPO. There it is verified that the construction does not depend on any other axioms than WLPO, and the assumption that f has double negation dense equality on fibers is somewhat further weakened.

• The Cantor–Schröder–Bernstein theorem is the 25th theorem on Freek Wiedijk’s list of 100 theorems [Wie].

Recent changes

• 2025-10-29. Fredrik Bakke. A constructive Cantor–Schröder–Bernstein theorem (#1206).