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 and 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 is an injection if and only if it is left-cancellable, in the sense that implies . But, for types and that are not sets, this notion is too weak, and, moreover, is not a proposition as the identity type has multiple elements in general. The appropriate notion of embedding for a function of arbitrary types and is given by any of the following two equivalent conditions:
- The map is an equivalence for any .
- The fibers of are all subsingletons.
A map of sets is an embedding if and only if it is left-cancellable. However, for example, any map that picks a point is left-cancellable, but it is an embedding if and only if the point is homotopy isolated, which amounts to saying that the identity type is contractible. This fails, for instance, when the type is the homotopical circle, for any point , or when is a univalent universe and 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 and be embeddings of arbitrary types and .
We say that is a -point if for any and with , the -fiber of is inhabited. Using function extensionality and the assumption that is an embedding, we see that being a -point is property rather than data, because subsingletons are closed under products.
Considering and , we see that if is a -point then the -fiber of is inhabited, and hence we get a function of -points of into . By construction, we have that . In particular if is a -point for a given , we get , and because , being an embedding, is left-cancellable, we get
Now define by if is a -point, and , otherwise.
To conclude the proof, it is enough to show that is left-cancellable and split-surjective, as any such map is an equivalence.
To see that is left-cancellable, it is enough to show that the images of and in the definition of don’t overlap, because and are left-cancellable. For that purpose, let be a non--point and be a -point, and, for the sake of contradiction, assume . Then . Now, because if were a -point then so would be , we conclude that it isn’t, and hence neither is , which contradicts the assumption.
To see that is a split surjection, say that is an -point if there are designated and with and the -fiber of empty. This is data rather than property, and so this notion could not have been used for the construction of . But every non--point is a -point, applying excluded middle to the -fiber of in the definition of -point.
Claim. If is not a -point, then there is a designated point of the -fiber of such that is not a -point either. To prove this, first notice that it is impossible that is not an -point, by the above observation. But this is not enough to conclude that it is an -point, because excluded middle applies to subsingletons only, which the notion of -point isn’t. However, it is readily seen that if is an -point, then there is a designated point in the -fiber of . From this it follows that it impossible that the subtype of the fiber consisting of the elements with not a -point is empty. But the -fiber of is a proposition because 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 is a split surjection. For any , we check whether or not is a -point. If it is, we map to , and if it isn’t we map to the point 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 and are not necessarily sets. We instead apply it to (1) the property of being a -point, defined in terms of the fibers of , (2) a fiber of , and (3) a subtype of a fiber of . These three types are propositions because the functions and are embeddings rather than merely left-cancellable maps.
A version of this argument is available in Agda.
If the type in the proof is connected, then every map of into a set is constant. In particular, the property of being a -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 or , which means that one of the embeddings and is already an equivalence.
Mike Shulman observed that this is true even without excluded middle: If is connected and we have an embedding and any function at all , then is an equivalence. For any , we have since is connected; thus is (non-split) surjective. But a surjective embedding is an equivalence.
>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.
If (or even its set-truncation) is inhabited, the converse holds. The idea is that connectedness in HoTT is defined as the set-truncation being contractible, so this is equivalent to having 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.)
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).
Nice! The point about embeddings vs left-cancellable maps is critical, as there is a simple pair of left-cancellable maps between and (taking going forward and, going backward, mapping to and shifting the indices of the circles by one), but no isomorphism/weak equivalence between those.
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!
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