The Cantor–Schröder–Bernstein–Escardó theorem

module foundation.cantor-schroder-bernstein-escardo where
Imports 
open import foundation.decidable-types
open import foundation.law-of-excluded-middle
open import foundation.perfect-images
open import foundation.split-surjective-maps

open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.injective-maps
open import foundation-core.negation
open import foundation-core.universe-levels

Idea

The classical Cantor–Schröder–Bernstein theorem asserts that from any pair of injective maps f : A → B and g : B → A we can construct a bijection between A and B. In a recent generalization, Escardó proved that a Cantor–Schröder–Bernstein theorem also holds for ∞-groupoids. His generalization asserts that given two types that embed into each other, then the types are equivalent.

Statement

type-Cantor-Schröder-Bernstein-Escardó : (l1 l2 : Level) → UU (lsuc (l1 ⊔ l2))
type-Cantor-Schröder-Bernstein-Escardó l1 l2 =
  {X : UU l1} {Y : UU l2} → (X ↪ Y) → (Y ↪ X) → X ≃ Y

Proof

The law of excluded middle implies Cantor-Schröder-Bernstein-Escardó

module _
  {l1 l2 : Level} (lem : LEM (l1 ⊔ l2))
  where

  module _
    {X : UU l1} {Y : UU l2} (f : X ↪ Y) (g : Y ↪ X)
    where

    map-Cantor-Schröder-Bernstein-Escardó' :
      (x : X) → is-decidable (is-perfect-image (map-emb f) (map-emb g) x) → Y
    map-Cantor-Schröder-Bernstein-Escardó' x (inl y) =
      inverse-of-perfect-image x y
    map-Cantor-Schröder-Bernstein-Escardó' x (inr y) =
      map-emb f x

    map-Cantor-Schröder-Bernstein-Escardó :
      X → Y
    map-Cantor-Schröder-Bernstein-Escardó x =
      map-Cantor-Schröder-Bernstein-Escardó' x
        ( is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)

    is-injective-map-Cantor-Schröder-Bernstein-Escardó :
      is-injective map-Cantor-Schröder-Bernstein-Escardó
    is-injective-map-Cantor-Schröder-Bernstein-Escardó {x} {x'} =
      l (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)
      (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x')
      where
      l :
        (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x))
        (d' : is-decidable (is-perfect-image (map-emb f) (map-emb g) x')) →
        ( map-Cantor-Schröder-Bernstein-Escardó' x d) ＝
        ( map-Cantor-Schröder-Bernstein-Escardó' x' d') →
        x ＝ x'
      l (inl ρ) (inl ρ') p =
        inv (is-sec-inverse-of-perfect-image x ρ) ∙
          (ap (map-emb g) p ∙ is-sec-inverse-of-perfect-image x' ρ')
      l (inl ρ) (inr nρ') p =
        ex-falso (perfect-image-has-distinct-image x' x nρ' ρ (inv p))
      l (inr nρ) (inl ρ') p =
        ex-falso (perfect-image-has-distinct-image x x' nρ ρ' p)
      l (inr nρ) (inr nρ') p =
        is-injective-is-emb (is-emb-map-emb f) p

    is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó :
      is-split-surjective map-Cantor-Schröder-Bernstein-Escardó
    is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó y = pair x p
      where
      a :
        is-decidable
          ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y)) →
        Σ ( X)
          ( λ x →
            ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
              map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y))
      a (inl γ) = pair (map-emb g y) ψ
        where
        ψ :
          ( d :
            is-decidable
              ( is-perfect-image (map-emb f) (map-emb g) (map-emb g y))) →
          map-Cantor-Schröder-Bernstein-Escardó' (map-emb g y) d ＝ y
        ψ (inl v') =
          is-retr-inverse-of-perfect-image {is-emb-g = is-emb-map-emb g} y v'
        ψ (inr v) = ex-falso (v γ)
      a (inr γ) = pair x ψ
        where
          w :
            Σ ( fib (map-emb f) y)
              ( λ s → ¬ (is-perfect-image (map-emb f) (map-emb g) (pr1 s)))
          w =
            not-perfect-image-has-not-perfect-fiber
              ( is-emb-map-emb f)
              ( is-emb-map-emb g)
              ( lem)
              ( y)
              ( γ)
          x : X
          x = pr1 (pr1 w)
          p : map-emb f x ＝ y
          p = pr2 (pr1 w)
          ψ :
            ( d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
            map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y
          ψ (inl v) = ex-falso ((pr2 w) v)
          ψ (inr v) = p
      b :
        Σ ( X)
          ( λ x →
            ( (d : is-decidable (is-perfect-image (map-emb f) (map-emb g) x)) →
              map-Cantor-Schröder-Bernstein-Escardó' x d ＝ y))
      b =
        a ( is-decidable-is-perfect-image-is-emb
            ( is-emb-map-emb g)
            ( lem)
            ( map-emb g y))
      x : X
      x = pr1 b
      p : map-Cantor-Schröder-Bernstein-Escardó x ＝ y
      p = pr2 b (is-decidable-is-perfect-image-is-emb (is-emb-map-emb g) lem x)

    is-equiv-map-Cantor-Schröder-Bernstein-Escardó :
      is-equiv map-Cantor-Schröder-Bernstein-Escardó
    is-equiv-map-Cantor-Schröder-Bernstein-Escardó =
      is-equiv-is-split-surjective-is-injective
        map-Cantor-Schröder-Bernstein-Escardó
        is-injective-map-Cantor-Schröder-Bernstein-Escardó
        is-split-surjective-map-Cantor-Schröder-Bernstein-Escardó

  Cantor-Schröder-Bernstein-Escardó :
    type-Cantor-Schröder-Bernstein-Escardó l1 l2
  pr1 (Cantor-Schröder-Bernstein-Escardó f g) =
    map-Cantor-Schröder-Bernstein-Escardó f g
  pr2 (Cantor-Schröder-Bernstein-Escardó f g) =
    is-equiv-map-Cantor-Schröder-Bernstein-Escardó f g

References