The Cantor-Schröder-Bernstein Theorem for ∞-groupoids

The classical Cantor-Schröder-Bernstein Theorem (CSB) of set theory, formulated by Cantor and first proved by Bernstein, states that for any pair of sets, if there is an injection of each one into the other, then the two sets are in bijection.

There are proofs that use excluded middle but not choice. That excluded middle is absolutely necessary was recently established by Pierre Pradic and Chad E. Brown.

The appropriate principle of excluded middle for HoTT/UF says that every subsingleton (or proposition, or truth value) is either empty or pointed. The statement that every type is either empty or pointed is much stronger, and amounts to global choice, which is incompatible with univalence (Theorem 3.2.2 of the HoTT book). In fact, in the presence of global choice, every type is a set by Hedberg’s Theorem, but univalence gives types that are not sets. Excluded middle middle, however, is known to be compatible with univalence, and is validated in Voevodsky’s model of simplicial sets. And so is (non-global) choice, but we don’t need it here.

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:

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

In set theory, a map $f : X \to Y$ is an injection if and only if it is left-cancellable, in the sense that $f(x)=f(x')$ implies $x=x'$ . But, for types $X$ and $Y$ that are not sets, this notion is too weak, and, 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:

The map $\mathrel{ap}(f,x,x') : x = x' \to f(x) = f(x')$ is an equivalence for any $x,x':X$ .
The fibers of $f$ are all subsingletons.

A map of sets is an embedding if and only if it is left-cancellable. However, for example, any map $1 \to 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, which amounts to saying that the identity type $y = y$ is contractible. This fails, for instance, when the type $Y$ is the homotopical circle, 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.

It is the second characterization of embedding given above that we exploit here.

The Cantor-Schröder-Bernstein Theorem for homotopy types, or ∞-groupoids. For any two types, if each one is embedded into the other, then they are equivalent, in the presence of excluded middle.

We adapt Halmos’ proof in his book Naive Set Theory to our more general situation. We don’t need to invoke univalence, the existence of propositional truncations or any other higher inductive type for our construction. But we do rely on function extensionality.

Let $f : X \to Y$ and $g : Y \to X$ be embeddings of arbitrary types $X$ and $Y$ .

We say that $x:X$ is a $g$ -point if for any $x_0 : X$ and $n : \mathbb{N}$ with $(g \circ f)^n (x_0)=x$ , the $g$ -fiber of $x_0$ is inhabited. Using function extensionality and the assumption that $g$ is an embedding, we see that being a $g$ -point is property rather than data, because subsingletons are closed under products.

Considering $x_0=x$ and $n=0$ , we see that if $x$ is a $g$ -point then the $g$ -fiber of $x$ is inhabited, and hence we get a function $g^{-1}$ of $g$ -points of $X$ into $Y$ . By construction, we have that $g(g^{-1}(x))=x$ . In particular if $g(y)$ is a $g$ -point for a given $y:Y$ , we get $g(g^{-1}(g(y)))=g(y)$ , and because $g$ , being an embedding, is left-cancellable, we get
$g^{-1}(g(y))=y$ .

Now define $h:X \to Y$ by $h(x) = g^{-1}(x)$ if $x$ is a $g$ -point, and $h(x)=f(x)$ , otherwise.

To conclude the proof, it is enough to show that $h$ is left-cancellable and split-surjective, as any such map is an equivalence.

To see that $h$ is left-cancellable, it is enough to show that the images of $f$ and $g^{-1}$ in the definition of $h$ don’t overlap, because $f$ and $g^{-1}$ are left-cancellable. For that purpose, let $x$ be a non- $g$ -point and $x'$ be a $g$ -point, and, for the sake of contradiction, assume $f(x) = g^{-1}(x')$ . Then $g(f(x))=g(g^{-1}(x'))=x'$ . Now, because if $g(f(x))$ were a $g$ -point then so would be $x$ , we conclude that it isn’t, and hence neither is $x'$ , which contradicts the assumption.

To see that $h$ is a split surjection, say that $x : X$ is an $f$ -point if there are designated $x_0 : X$ and $n : \mathbb{N}$ with $(g \circ f)^n (x_0)=x$ and the $g$ -fiber of $x_0$ empty. This is data rather than property, and so this notion could not have been used for the construction of $h$ . But every non- $f$ -point is a $g$ -point, applying excluded middle to the $g$ -fiber of $x_0$ in the definition of $g$ -point.

Claim. If $g(y)$ is not a $g$ -point, then there is a designated point $(x : X , p : f(x)=y)$ of the $f$ -fiber of $y$ such that $x$ is not a $g$ -point either. To prove this, first notice that it is impossible that $g(y)$ is not an $f$ -point, by the above observation. But this is not enough to conclude that it is an $f$ -point, because excluded middle applies to subsingletons only, which the notion of $f$ -point isn’t. However, it is readily seen that if $g(y)$ is an $f$ -point, then there is a designated point $(x,p)$ in the $f$ -fiber of $y$ . From this it follows that it impossible that the subtype of the fiber consisting of the elements $(x,p)$ with $x$ not a $g$ -point is empty. But the $f$ -fiber of $y$ is a proposition because $f$ is an embedding, and hence so is the subtype, and therefore the claim follows by double-negation elimination.

We can now resume the proof that $h$ is a split surjection. For any $y:Y$ , we check whether or not $g(y)$ is a $g$ -point. If it is, we map $y$ to $g(y)$ , and if it isn’t we map $y$ to the point $x : X$ given by the claim.

This concludes the proof.

So, in this argument we don’t apply excluded middle to equality directly, which we wouldn’t be able to as the types $X$ and $Y$ are not necessarily sets. We instead apply it to (1) the property of being a $g$ -point, defined in terms of the fibers of $g$ , (2) a fiber of $g$ , and (3) a subtype of a fiber of $f$ . These three types are propositions because the functions $f$ and $g$ are embeddings rather than merely left-cancellable maps.

A version of this argument is available in Agda.

9 Responses to The Cantor-Schröder-Bernstein Theorem for ∞-groupoids

Martin Escardo says:

28 January 2020 at 09:11

Addendum.

If the type $X$ in the proof is connected, then every map of $X$ into a set is constant. In particular, the property of being a $g$ -point is constant, because the type of truth values is a set (assuming univalence for subsingletons). Hence, by excluded middle, it is constantly true or constantly false, and so $h=g^{-1}$ or $h = f$ , which means that one of the embeddings $f$ and $g$ is already an equivalence.

Mike Shulman observed that this is true even without excluded middle: If $X$ is connected and we have an embedding $g : Y \to X$ and any function at all $f : X \to Y$ , then $g$ is an equivalence. For any $x:X$ , we have $\left\lVert g(f(x)) = x \right\rVert$ since $X$ is connected; thus $g$ is (non-split) surjective. But a surjective embedding is an equivalence.

- David Roberts says:
  
  1 February 2020 at 23:44
  
  >If the type X in the proof is connected, then every map of X into a set is constant.
  
  How much does this hold in the other direction? Classically, a topological space is connected if and only if every map from it to a discrete space is constant.
  
  - Pierre Pradic says:
    
    2 February 2020 at 10:54
    
    If $X$ (or even its set-truncation) is inhabited, the converse holds. The idea is that connectedness in HoTT is defined as the set-truncation $\| X \|$ being contractible, so this is equivalent to having $X \to \| X\|$ constant and a basepoint.
    
    (This works with the weak version of constancy in https://homotopytypetheory.org/2015/06/11/not-every-weakly-constant-function-is-conditionally-constant/. This does not reverse in general, because the definition of connectedness rules out the empty type.)
    
    - David Roberts says:
      
      2 February 2020 at 16:49
      
      This makes sense. In my algebraic topology class I defined a space to be connected when every continuous function to a discrete space *has range a single point* (which is what I implicitly meant by “constant” above, thought I’m familiar with the issue of defining constant in HoTT).
      
Pierre Pradic says:

28 January 2020 at 13:55

Nice! The point about embeddings vs left-cancellable maps is critical, as there is a simple pair of left-cancellable maps between $\mathbb{N} \times S^1$ and $1 + \mathbb{N} \times S^1$ (taking $\mathsf{inl}$ going forward and, going backward, mapping $\mathsf{inl}(*)$ to $(0, \mathsf{base})$ and shifting the indices of the circles by one), but no isomorphism/weak equivalence between those.

- Martin Escardo says:
  
  28 January 2020 at 13:58
  
  This is a very nice and simple example showing that we need to consider the stronger notion of embedding for the result to be true!
  
Martin Escardo says:

31 January 2020 at 17:42

I have rewritten the Agda proof, to try to make it more readable, in two ways: (1) I added the above meta-mathematical comments as Agda comments. (2) I defined Agda idioms corresponding to natural-language idioms for expressing proofs and used them in the Agda proofs. Does the Agda proof get more readable in this way, for people acquainted with type theory but not Agda?
Here it is.

Pingback: Resumen de lecturas compartidas del 25 al 31 de enero de 2020 | Vestigium
Pingback: Resumen de lecturas compartidas durante enero de 2020 | Vestigium