The Cantor-Schröder-Bernstein Theorem for ∞-groupoids
-----------------------------------------------------
Martín Hötzel Escardó
6th February 2020
School of Computer Science
Birmingham Theory Group
Lab Lunch Talk
This talk has embedded Agda code.
In the end I gave the talk in a whiteboard (without showing any
Agda code). But it followed the script outlined in these "slides".
I have also written a blog post that gives the proof in
mathematical vernacular:
https://homotopytypetheory.org/2020/01/26/the-cantor-schroder-bernstein-theorem-for-∞-groupoids/
Abstract
--------
(1) CSB in constructive set theory implies excluded middle
(Pradic & Brown 2019, https://arxiv.org/abs/1904.09193).
If for all sets X and Y, the existence of injections X → Y and
Y → X implies X ≃ Y,
then P ∨ ¬ P for any proposition P.
(2) In homotopy type theory / univalent foundations (HoTT/UF),
excluded middle implies CSB, not only for sets, but also for
arbitrary homotopy types, or ∞-groupoids.
Assuming excluded middle, for all homotopy types X and Y, if
there are embeddings X → Y and Y → X, then X ≃ Y.
This seems to be a new result.
HoTT/UF
-------
An intensional Martin-Löf type theory (MLTT) in which types are
understood as homotopy types, or ∞-groupoids, rather than as sets as
in the original Martin-Löf conception.
We work with a Spartan MLTT:
1. Empty type 𝟘.
2. One-point type 𝟙.
3. A type ℕ of natural numbers.
4. Type formers
Π (product),
+ (binary sum),
Σ (sum),
Id (identity type).
5. Universes (types of types), ranged over by 𝓤,𝓥,𝓦.
(Here are lecture notes for HoTT/UF in Agda:
https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes)
Possible axioms for HoTT/UF
---------------------------
1. Function extensionality. \ Given constructive content
2. Propositional extensionality. | by cubical type theory.
3. Univalence. |
4. Existence of propositional truncations. | (Implemented in Cubical Agda).
5. Existence of (some) higher inductive types. /
6. Propositional resizing and impredicativity. ⟩ Constructive status open.
7. Excluded middle. \ Non constructive.
8. Choice. /
* We will not postulate them. Instead we will use them as explicit
assumptions in theorems and constructions, when needed.
* For this talk we need only function extensionality and excluded
middle.
* Univalence implies function extensionality and propositional
extensionality.
* Unique choice just holds.
* Choice implies excluded middle, as usual.
* Excluded middle implies propositional resizing and
impredicativity.
* Function extensionality and propositional resizing imply the
existence of propositional truncations, and hence so do function
extensionality and excluded middle.
* Univalence and propositional truncations imply the existence of
some higher inductive types, such as the homotopical circle and
set quotients.
* HoTT/UF has a model in Kan simplicial sets after Voevodsky.
* It validates the above axioms, assuming classical logic and
Grothendieck universes in the meta-theory.
* Types are interpreted as homotopy types.
Main differences between HoTT/UF and MLTT
-----------------------------------------
1. The treatment of identity types.
* For a type X and points x , y : X, the identity type
Id X x y,
also written
x ＝ y
here, collects all the ways in which x and y are identified.
* The type x ＝ y has (provably) multiple elements in general.
* In the homotopical understanding, the identifications are paths.
* Example. In the type of groups, one can prove that the
identifications are in bijection with group isomorphisms,
assuming univalence.
Similarly for the types of rings, metric spaces, topological
spaces, graphs, posets, categories, functor algebras etc.
(https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/)
2. The treatment of propositions.
* There isn't a a built-in type of propositions as in the
Calculus of Constructions (CoC).
* The constructed type of propositions, in a type universe 𝓤, is
Ω 𝓤 := Σ P ꞉ 𝓤 ̇ , is-prop P.
* A proposition, or truth value, is defined to be a type with at
most one element, or a subsingleton.
This e.g. makes unique choice automatic, while in CoC unique
choice fails.
Part 1
------
The Pradic-Brown argument rendered in HoTT/UF
---------------------------------------------
\begin{code}
{-# OPTIONS --safe --without-K #-}
module CantorSchroederBernstein.CSB-TheoryLabLunch where
open import CoNaturals.Type
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import TypeTopology.CompactTypes
open import TypeTopology.GenericConvergentSequenceCompactness
open import UF.Embeddings
open import UF.Equiv
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
\end{code}
Our formulation of Cantor-Schröder-Bernstein:
\begin{code}
CSB : 𝓤 ̇ → 𝓥 ̇ → 𝓤 ⊔ 𝓥 ̇
CSB X Y = (X ↪ Y) → (Y ↪ X) → X ≃ Y
CantorSchröderBernstein : (𝓤 𝓥 : Universe) → (𝓤 ⊔ 𝓥)⁺ ̇
CantorSchröderBernstein 𝓤 𝓥 = (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) → CSB X Y
\end{code}
We begin by recalling some definitions.
\begin{code}
recall-decidable : {A : 𝓤 ̇ } → is-decidable A ＝ (A + ¬ A)
recall-decidable = by-definition
recall-Compact : {X : 𝓤 ̇ }
→ is-Compact X {𝓥} ＝ ((A : X → 𝓥 ̇ )
→ ((x : X) → is-decidable (A x))
→ is-decidable (Σ x ꞉ X , A x))
recall-Compact = by-definition
recall-ℕ∞ : ℕ∞ ＝ (Σ α ꞉ (ℕ → 𝟚) , is-decreasing α)
recall-ℕ∞ = by-definition
recall-ℕ∞-Compact : funext 𝓤₀ 𝓤₀ → is-Compact ℕ∞ {𝓤}
recall-ℕ∞-Compact fe = ℕ∞-Compact fe
\end{code}
The following is Lemma 7 of the above reference, using retractions
rather than surjections, for simplicity:
\begin{code}
Pradic-Brown-lemma : {X : 𝓤 ̇ } {A : 𝓥 ̇ }
→ retract (A + X) of X
→ is-Compact X
→ is-decidable A
Pradic-Brown-lemma {𝓤} {𝓥} {X} {A} (r , s , η) c = γ e
where
P : X → 𝓤 ⊔ 𝓥 ̇
P x = Σ a ꞉ A , r x ＝ inl a
d : (x : X) → is-decidable (P x)
d x = equality-cases (r x)
(λ (a : A) (u : r x ＝ inl a) → inl (a , u))
(λ (y : X) (v : r x ＝ inr y) → inr (λ (a , u) → +disjoint (inl a ＝⟨ u ⁻¹ ⟩
r x ＝⟨ v ⟩
inr y ∎)))
e : is-decidable (Σ x ꞉ X , P x)
e = c P d
f : A → Σ x ꞉ X , P x
f a = s (inl a) , a , η (inl a)
γ : is-decidable (Σ x ꞉ X , P x) → is-decidable A
γ (inl (x , a , u)) = inl a
γ (inr φ) = inr (contrapositive f φ)
\end{code}
Function extensionality is used twice in the following, once to know
that ℕ∞ is a set, and once to know that it is compact.
\begin{code}
recall-EM : EM 𝓤 ＝ ((P : 𝓤 ̇ ) → is-prop P → P + ¬ P)
recall-EM = by-definition
\end{code}
Function extensionality says that any two pointwise equal functions
are equal.
\begin{code}
CSB-gives-EM : funext 𝓤₀ 𝓤₀
→ (P : 𝓤 ̇ )
→ is-prop P
→ CSB ℕ∞ (P + ℕ∞)
→ P + ¬ P
CSB-gives-EM fe P i csb = γ
where
f : ℕ∞ → P + ℕ∞
f = inr
j : is-embedding f
j = inr-is-embedding P ℕ∞
z : P → ℕ∞
z _ = Zero
g : P + ℕ∞ → ℕ∞
g = cases z Succ
a : is-embedding z
a = maps-of-props-into-sets-are-embeddings z i (ℕ∞-is-set fe)
b : is-embedding Succ
b = lc-maps-into-sets-are-embeddings Succ Succ-lc (ℕ∞-is-set fe)
c : disjoint-images z Succ
c = λ (p : P) (x : ℕ∞) (q : Zero ＝ Succ x) → Zero-not-Succ q
k : is-embedding g
k = disjoint-cases-embedding z Succ a b c
e : ℕ∞ ≃ P + ℕ∞
e = csb (f , j) (g , k)
ρ : retract (P + ℕ∞) of ℕ∞
ρ = ≃-gives-▷ e
γ : P + ¬ P
γ = Pradic-Brown-lemma ρ (ℕ∞-Compact fe)
\end{code}
Hence if we assume Cantor-Schröder-Bernstein for the first universe 𝓤₀
and an arbitrary universe 𝓥, as formulated above, then we get excluded
middle for propositions in the universe 𝓥:
\begin{code}
CantorSchröderBernstein-gives-EM : funext 𝓤₀ 𝓤₀
→ CantorSchröderBernstein 𝓤₀ 𝓥
→ EM 𝓥
CantorSchröderBernstein-gives-EM fe csb P i = CSB-gives-EM fe P i (csb ℕ∞ (P + ℕ∞))
\end{code}
Part 2
------
Can the Cantor-Schröder-Bernstein Theorem be generalized from sets to
arbitrary homotopy types, or ∞-groupoids, in the presence of excluded
middle?
This seems rather unlikely at first sight:
1. CSB fails for 1-categories.
In fact, it already fails for posets.
For example, the intervals (0,1) and [0,1] are order-embedded
into each other, but they are not order isomorphic.
2. The known proofs of CSB for sets rely on deciding equality of
elements of sets.
But, in the presence of excluded middle, the types that have
decidable equality are precisely the sets, by Hedberg’s Theorem.
Now:
* In set theory, a map f : X → Y is an injection if and only if it
is left-cancellable:
f x = f x' implies x = x'.
* But, for (homotopy) types X and Y that are not sets, this notion
is too weak.
* Moreover, is not a proposition as the identity type x ＝ x' has
multiple elements in general.
The appropriate notion of embedding for a function f of arbitrary
types X and Y is given by any of the following two equivalent
conditions:
1. The map ap f x x' : x ＝ x' → f x ＝ f x' is an equivalence for any x , x' : X.
2. The fibers of f are all subsingletons.
We have:
* A map of sets is an embedding if and only if it is left-cancellable.
* However, for example, any map 𝟙 → Y that picks a point y : Y is
left-cancellable.
But it is an embedding if and only if the point y is homotopy isolated.
This amounts to saying that the identity type y = y is a singleton.
This fails, for instance, when the type Y is the homotopical
circle S¹, for any point y, or when Y is a univalent universe
and y : Y is the two-point type, or any type with more than one
automorphism.
* Example (Pradic). There are injections both ways between the
types ℕ × S¹ and 𝟙 + ℕ × S¹, but they aren't equivalent as one
of them has an isolated point but the other doesn't.
No injection 𝟙 + ℕ × S¹ → ℕ × S¹ is an embedding.
* It is the second characterization of embedding given above that
we exploit here.
Theorem
-------
The Cantor-Schröder-Bernstein Theorem holds for all homotopy types, or
∞-gropoids, in the presence of excluded middle.
Our proof adapts Halmos' proof in his book Naive Set Theory to our
more general situation.
The fiber of a point y : Y over a map f : X → Y collects all the
points x : X that are mapped by f to a point identified with y,
together with the identification datum:
\begin{code}
recall-fiber : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) (y : Y)
→ fiber f y ＝ (Σ x ꞉ X , f x ＝ y)
recall-fiber f x = by-definition
recall-is-embedding : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
→ is-embedding f ＝ ((y : Y) → is-prop (fiber f y))
recall-is-embedding f = by-definition
\end{code}
The type (X ↪ Y) collects all embeddings of the type X into the type Y:
\begin{code}
recall-type-of-embeddings : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (X ↪ Y) ＝ (Σ f ꞉ (X → Y) , is-embedding f)
recall-type-of-embeddings = by-definition
\end{code}
We are now ready to formulate and prove the theorem.
\begin{code}
EM-gives-CantorSchröderBernstein : Fun-Ext
→ EM (𝓤 ⊔ 𝓥)
→ CantorSchröderBernstein 𝓤 𝓥
EM-gives-CantorSchröderBernstein {𝓤} {𝓥} fe excluded-middle
X Y (f , f-is-emb) (g , g-is-emb) =
need X ≃ Y which-is-given-by 𝒽
where
remark-f : type-of (f , f-is-emb) ＝ (X ↪ Y)
remark-f = by-assumption
remark-g : type-of (g , g-is-emb) ＝ (Y ↪ X)
remark-g = by-assumption
\end{code}
In order to define 𝒽 : X ≃ Y, we use a notion of g-point.
\begin{code}
is-g-point : (x : X) → 𝓤 ⊔ 𝓥 ̇
is-g-point x = (x₀ : X) (n : ℕ) → ((g ∘ f) ^ n) x₀ ＝ x → fiber g x₀
\end{code}
What is important for our purposes is that this is property rather
than data, using the fact that g is an embedding.
We use the fact that propositions are closed under products, which
requires function extensionality:
\begin{code}
being-g-point-is-prop : (x : X) → is-prop (is-g-point x)
being-g-point-is-prop x =
Π-is-prop fe (λ (x₀ : X ) →
Π-is-prop fe (λ (n : ℕ ) →
Π-is-prop fe (λ (p : ((g ∘ f) ^ n) x₀ ＝ x) → need is-prop (fiber g x₀)
which-is-given-by (g-is-emb x₀))))
\end{code}
By construction, considering x₀ = x and n = 0, we have that g is
invertible at g-points, because, by definition, we have that
((g ∘ f) ^ 0) x ＝ x).
\begin{code}
g-is-invertible-at-g-points : (x : X) → is-g-point x → fiber g x
g-is-invertible-at-g-points x γ = γ x 0 (by-definition ∶ ((g ∘ f) ^ 0) x ＝ x)
\end{code}
The fiber point is given by the first projection of the fiber:
\begin{code}
g⁻¹ : (x : X) → is-g-point x → Y
g⁻¹ x γ = fiber-point (g-is-invertible-at-g-points x γ)
\end{code}
Because being a g-point is property, we can apply excluded middle to
it:
\begin{code}
δ : (x : X) → is-decidable (is-g-point x)
δ x = excluded-middle (is-g-point x) (being-g-point-is-prop x)
\end{code}
The rest of the proof shows that the following function is an
equivalence:
\begin{code}
h : X → Y
h x = Cases (δ x)
(γ ꞉ is-g-point x ↦ g⁻¹ x γ)
(ν ꞉ ¬ is-g-point x ↦ f x)
\end{code}
For that purpose, it is enough to show that it is left-cancellable and
split-surjective.
To show that it is left-cancellable, we first show that g⁻¹ is a
two-sided inverse in its domain of definition.
That it is a right inverse follows from the definition of fiber, by
taking the fiber path, which is given by the second projection:
\begin{code}
g⁻¹-is-rinv : (x : X) (γ : is-g-point x) → g (g⁻¹ x γ) ＝ x
g⁻¹-is-rinv x γ = fiber-identification (g-is-invertible-at-g-points x γ)
\end{code}
That it is a left inverse follows from the above and the fact that g,
being an embedding, is left-cancellable:
\begin{code}
g⁻¹-is-linv : (y : Y) (γ : is-g-point (g y)) → g⁻¹ (g y) γ ＝ y
g⁻¹-is-linv y γ = have (g (g⁻¹ (g y) γ) ＝⟨ g⁻¹-is-rinv (g y) γ ⟩
g y ∎)
so-apply embeddings-are-lc g g-is-emb
\end{code}
We also need the following two facts to establish the
left-cancellability of h:
\begin{code}
α : (x : X) → is-g-point (g (f x)) → is-g-point x
α x γ = need is-g-point x
which-is-given-by
assume x₀ ∶ X and
assume n ∶ ℕ and
assume p ∶ ((g ∘ f) ^ n) x₀ ＝ x then
(need fiber g x₀
which-is-given-by
have ap (g ∘ f) p ∶ ((g ∘ f) ^ (succ n)) x₀ ＝ g (f x)
so-apply γ x₀ (succ n))
f-g⁻¹-disjoint-images : (x x' : X)
→ ¬ is-g-point x
→ (γ : is-g-point x')
→ f x ≠ g⁻¹ x' γ
f-g⁻¹-disjoint-images x x' ν γ p = have p ∶ f x ＝ g⁻¹ x' γ
so need contradiction
which-is-given-by
have γ ∶ is-g-point x'
which-is-impossible-by (v ∶ ¬ is-g-point x')
where
q : g (f x) ＝ x'
q = have p ∶ f x ＝ g⁻¹ x' γ
so-use (g (f x) ＝⟨ ap g p ⟩
g (g⁻¹ x' γ) ＝⟨ g⁻¹-is-rinv x' γ ⟩
x' ∎)
u : ¬ is-g-point (g (f x))
u = have ν ∶ ¬ is-g-point x
so-apply contrapositive (α x)
v : ¬ is-g-point x'
v = transport (- ↦ ¬ is-g-point -) q u
\end{code}
It is convenient to work with the following auxiliary function H and
prove properties of H and then specialize them to h:
\begin{code}
H : (x : X) → is-decidable (is-g-point x) → Y
H x d = Cases d
(γ ꞉ is-g-point x ↦ g⁻¹ x γ)
(ν ꞉ ¬ is-g-point x ↦ f x)
notice-that : h ＝ x ↦ H x (δ x)
notice-that = by-definition
h-lc : left-cancellable h
h-lc {x} {x'} = l (δ x) (δ x')
where
l : (d : is-decidable (is-g-point x)) (d' : is-decidable (is-g-point x'))
→ H x d ＝ H x' d'
→ x ＝ x'
l (inl γ) (inl γ') p = have p ∶ g⁻¹ x γ ＝ g⁻¹ x' γ'
so (x ＝⟨ (g⁻¹-is-rinv x γ)⁻¹ ⟩
g (g⁻¹ x γ ) ＝⟨ ap g p ⟩
g (g⁻¹ x' γ') ＝⟨ g⁻¹-is-rinv x' γ' ⟩
x' ∎)
l (inl γ) (inr ν') p = have p ∶ g⁻¹ x γ ＝ f x'
which-is-impossible-by (- ↦ f-g⁻¹-disjoint-images x' x ν' γ (- ⁻¹))
l (inr ν) (inl γ') p = have p ∶ f x ＝ g⁻¹ x' γ'
which-is-impossible-by f-g⁻¹-disjoint-images x x' ν γ'
l (inr ν) (inr ν') p = have p ∶ f x ＝ f x'
so-apply embeddings-are-lc f f-is-emb
\end{code}
Next we want to show that h is split surjective. For that purpose, we
define the notion of f-point, which is data rather than property (as
several x₀ and n are possible answers in general).
(In particular, excluded middle can't be applied to the type
f-point x, because excluded middle applies only to truth values.)
\begin{code}
f-point : (x : X) → 𝓤 ⊔ 𝓥 ̇
f-point x = Σ x₀ ꞉ X , (Σ n ꞉ ℕ , ((g ∘ f) ^ n) x₀ ＝ x) × ¬ fiber g x₀
\end{code}
What is important for our argument is that non-f-points are g-points:
\begin{code}
non-f-point-is-g-point : (x : X) → ¬ f-point x → is-g-point x
non-f-point-is-g-point x ν x₀ n p = need fiber g x₀ which-is-given-by
(Cases (excluded-middle (fiber g x₀) (g-is-emb x₀))
(σ ꞉ fiber g x₀ ↦ σ)
(u ꞉ ¬ fiber g x₀ ↦ have (x₀ , (n , p) , u) ∶ f-point x
which-is-impossible-by (ν ∶ ¬ f-point x)))
\end{code}
We use the notion of f-point to prove the following, whose statement
doesn't refer to the notion of f-point.
\begin{code}
claim : (y : Y) → ¬ is-g-point (g y) → Σ (x , p) ꞉ fiber f y , ¬ is-g-point x
claim y ν = v
where
i : ¬¬ f-point (g y)
i = have ν ∶ ¬ is-g-point (g y)
so-apply contrapositive (non-f-point-is-g-point (g y))
ii : f-point (g y) → Σ (x , p) ꞉ fiber f y , ¬ is-g-point x
ii (x₀ , (0 , p) , u) = have p ∶ x₀ ＝ g y
so have (y , (p ⁻¹)) ∶ fiber g x₀
which-is-impossible-by (u ∶ ¬ fiber g x₀)
ii (x₀ , (succ n , p) , u) = a , b
where
q : f (((g ∘ f) ^ n) x₀) ＝ y
q = have p ∶ ((g ∘ f) ^ (succ n)) x₀ ＝ g y
∶ g (f (((g ∘ f) ^ n) x₀)) ＝ g y
so-apply embeddings-are-lc g g-is-emb
a : fiber f y
a = ((g ∘ f) ^ n) x₀ , q
b : ¬ is-g-point (((g ∘ f) ^ n) x₀)
b = assume γ ∶ is-g-point (((g ∘ f) ^ n) x₀)
then (have γ x₀ n refl ∶ fiber g x₀
which-is-impossible-by (u ∶ ¬ fiber g x₀))
iii : ¬¬ (Σ (x , p) ꞉ fiber f y , ¬ is-g-point x)
iii = double-contrapositive ii i
iv : is-prop (Σ (x , p) ꞉ fiber f y , ¬ is-g-point x)
iv = have f-is-emb y ∶ is-prop (fiber f y)
so-apply subtypes-of-props-are-props' pr₁ (pr₁-lc (λ {σ} → negations-are-props fe))
v : Σ (x , p) ꞉ fiber f y , ¬ is-g-point x
v = double-negation-elim excluded-middle _ iv iii
\end{code}
With this we are ready to show that h is a split surjection. The idea
is that, given y : Y, we check whether g y is a g-point or not, and if
it is we map it to g y, and otherwise we map y to the point x : X
given by the above claim. But then, of course, we also need to argue
that this works. As above, we use the auxiliary function H for that
purpose.
\begin{code}
h-split-surjection : (y : Y) → Σ x ꞉ X , h x ＝ y
h-split-surjection y = x , p
where
a : is-decidable (is-g-point (g y))
→ Σ x ꞉ X , ((d : is-decidable (is-g-point x)) → H x d ＝ y)
a (inl γ) = g y , ψ
where
ψ : (d : is-decidable (is-g-point (g y))) → H (g y) d ＝ y
ψ (inl γ') = H (g y) (inl γ') ＝⟨ by-definition ⟩
g⁻¹ (g y) γ' ＝⟨ g⁻¹-is-linv y γ' ⟩
y ∎
ψ (inr ν) = have ν ∶ ¬ is-g-point (g y)
which-contradicts (γ ∶ is-g-point (g y))
a (inr ν) = x , ψ
where
w : Σ (x , p) ꞉ fiber f y , ¬ is-g-point x
w = have ν ∶ ¬ is-g-point (g y)
so-apply claim y
x : X
x = fiber-point (pr₁ w)
p : f x ＝ y
p = fiber-identification (pr₁ w)
ψ : (d : is-decidable (is-g-point x)) → H x d ＝ y
ψ (inl γ) = have γ ∶ is-g-point x
which-is-impossible-by (pr₂ w ∶ ¬ is-g-point x)
ψ (inr ν) = H x (inr ν) ＝⟨ by-definition ⟩
f x ＝⟨ p ⟩
y ∎
b : Σ x ꞉ X ,((d : is-decidable (is-g-point x)) → H x d ＝ y)
b = a (δ (g y))
x : X
x = pr₁ b
p : h x ＝ y
p = h x ＝⟨ by-construction ⟩
H x (δ x) ＝⟨ pr₂ b (δ x) ⟩
y ∎
\end{code}
And because left-cancellable split surjections are equivalences, we
are done:
\begin{code}
𝒽 : X ≃ Y
𝒽 = h , lc-split-surjections-are-equivs h h-lc h-split-surjection
\end{code}
Q.E.D.