This is part three in a series of posts on avoiding the axiom of choice (part one, part two).

In my previous post, I explained one place where the axiom of choice often shows up in category theory, namely, when defining certain functors whose action on objects is specified only up to unique isomorphism. In this post, I’ll explain another place AC shows up, when talking about equivalence of categories. (Actually, as we’ll see, it’s really the same underlying issue, of defining a functor defined only up to unique isomorphism; this is just a particularly important instantiation of that issue.)

When are two categories “the same”? In traditional category theory, founded on set theory, there are quite a few different definitions of “sameness” for categories. Ultimately, this comes down to the fact that set theory does not make a very good foundation for category theory! There are lots of different ideas of equivalence, and they often do not correspond to the underlying equality on sets, so one must carefully pick and choose which notions of equality to use in which situations (and some choices might be better than others!). Every concept, it seems, comes with “strict” and “weak” variants, and often many others besides. Maintaining the principle of equivalence requires hard work and vigilence.

As an example, consider the following definition, our first candidate for the definition of “sameness” of categories:

Two categories \(\mathbb{C}\) and \(\mathbb{D}\) are isomorphic if there are functors \(F : \mathbb{C} \to \mathbb{D}\) and \(G : \mathbb{D} \to \mathbb{C}\) such that \(GF = 1_\mathbb{C}\) and \(FG = 1_\mathbb{D}\).

Seems pretty straightforward, right? Well, this is the right idea in general, but it is subtly flawed. In fact, it is somewhat “evil”, in that it talks about equality of functors (\(GF\) and \(FG\) must be equal to the identity). However, two functors \(H\) and \(J\) can be isomorphic without being equal, if there is a natural isomorphism between them—that is, a pair of natural transformations \(\phi : H \to J\) and \(\psi : J \to H\) such that \(\phi \circ \psi\) and \(\psi \circ \phi\) are both equal to the identity natural transformation.¹ For example, consider the Haskell functors given by

data Rose a = Node a [Rose a]
data Fork a = Leaf a | Fork (Fork a) (Fork a)

These are obviously not equal, but they are isomorphic, in the sense that there are natural transformations (i.e. polymorphic functions) rose2fork :: forall a. Rose a -> Fork a and fork2rose :: forall a. Fork a -> Rose a such that rose2fork . fork2rose === id and fork2rose . rose2fork === id (showing this is left as an exercise for the interested reader).

Here, then, is a better definition:

Categories \(\mathbb{C}\) and \(\mathbb{D}\) are equivalent if there are functors \(F : \mathbb{C} \to \mathbb{D}\) and \(G : \mathbb{D} \to \mathbb{C}\) which are inverse up to natural isomorphism, that is, there are natural isomorphisms \(GF \cong 1_\mathbb{C}\) and \(FG \cong 1_\mathbb{D}\).

So the compositions of the functors \(F\) and \(G\) do not literally have to be the identity functor, but only (naturally) isomorphic to it. This does turn out to be a well-behaved notion of sameness for categories (although you’ll have to take my word for it).

The story doesn’t end here, however. In set theory, a function is a bijection—that is, an isomorphism of sets—if and only if it is both injective and surjective. By analogy, one might wonder what properties a functor \(F : \mathbb{C} \to \mathbb{D}\) must have in order to be one half of an equivalence. This leads to the following definition:

\(\mathbb{C}\) is proto-equivalent² to \(\mathbb{D}\) if there is a functor \(F : \mathbb{C} \to \mathbb{D}\) which is full and faithful (i.e., a bijection on each hom-set) as well as essentially surjective, that is, for every object \(D \in \mathbb{D}\) there exists some object \(C \in \mathbb{C}\) such that \(F\ C \cong D\).

Intuitively, this says that \(F\) “embeds” an entire copy of \(\mathbb{C}\) into \(\mathbb{D}\) (that’s the “full and faithful” part), and that every object of \(D\) which is not directly in the image of \(F\) is isomorphic to one that is. So every object of \(\mathbb{D}\) is “included” in the image of \(\mathbb{C}\), at least up to isomorphism (which, remember, is supposed to be all that matters).

So, are equivalence and protoequivalence the same thing? In one direction, it is not too hard to show that every equivalence is a protoequivalence: if \(F\) and \(G\) are inverse-up-to-natural-isomorphism, then they must be fully faithful and essentially surjective. It would be nice if the converse were also true: in that case, in order to prove two categories equivalent, it would suffice to construct a single functor \(F\) from one to the other, and show that \(F\) has the requisite properties. This often ends up being more convenient than explicitly constructing two functors and showing they are inverse. However, it turns out that the converse is provable only if one accepts the axiom of choice!

To get an intuitive sense for why this is, suppose \(F : \mathbb{C} \to \mathbb{D}\) is fully faithful and essentially surjective. To construct an equivalence between \(\mathbb{C}\) and \(\mathbb{D}\), we must define a functor \(G : \mathbb{D} \to \mathbb{C}\) and show it is inverse to \(F\) (up to natural isomorphism). However, to define \(G\) we must give its action on each object \(D \in \mathbb{D}\), that is, we must exhibit a function \(\mathrm{Ob}\ \mathbb{D} \to \mathrm{Ob}\ \mathbb{C}\). We know that for each \(D \in \mathbb{D}\) there exists some object \(C \in \mathbb{C}\) such that \(F\ C \cong D\). That is,

is a collection of non-empty sets. However, in a non-constructive logic, knowing these sets are nonempty does not actually give us any objects! Instead, we have to use the axiom of choice, which gives us a choice function \(\mathrm{Ob}\ \mathbb{D} \to \mathrm{Ob}\ \mathbb{C}\), and we can use this function as the object mapping of the functor \(G\).

So AC is required to prove that every protoequivalence is an equivalence. In fact, the association goes deeper yet: it turns out that the statement “every protoequivalence is an equivalence” (let’s call this the Axiom of Protoequivalence, or AP for short) not only requires AC, but is equivalent to it—that is, you can also derive AC given AP as an axiom!

On purely intuitive grounds, however, I would wager that to (almost?) anyone with sufficient category theory experience, it “feels” like AP “ought to be” true. If there is a full, faithful, and essentially surjective functor \(F : \mathbb{C} \to \mathbb{D}\), then \(\mathbb{C}\) and \(\mathbb{D}\) “ought to be” equivalent. The particular choice of functor \(G : \mathbb{D} \to \mathbb{C}\) “doesn’t matter”, since it makes no difference up to isomorphism. On the other hand, we certainly don’t want to accept the axiom of choice. This puts us in the very awkward and inconsistent position of having two logically equivalent statements which we want to respectively affirm and reject. A fine pickle indeed! What to do?

There are four options (that I know of, at least):

1. If one is feeling particularly rational, one can simply say, “Well, since AC and AP are equivalent, and I reject AC, I must therefore reject AP as well; my feelings about it are irrelevant.”

This is a perfectly sensible and workable approach. It’s important to highlight, therefore, that the “problem” is in some sense more a philosophical problem than a technical one. One can perfectly well adopt the above solution and continue to do category theory; it just may not be the “nicest” (a philosophical rather than technical notion!) way to do it.

We can therefore also consider some more creative solutions!

2. In a classical setting, one can avoid AC and affirm (an analogue of) AP by generalizing the notion of functor to that of anafunctor (Makkai 1996). Essentially, an anafunctor is a functor “defined only up to unique isomorphism”. It turns out that the appropriate analogue of AP, where “functor” has been replaced by “anafunctor”, is indeed true—and neither requires nor implies AC. Anafunctors “act like” functors in a sufficiently strong sense that one can simply do category theory using anafunctors in place of functors. However, one also has to replace natural transformations with “ananatural transformations”, etc., and it quickly gets rather fiddly.

3. In a constructive setting, a witness of essential surjectivity is necessarily a function which gives an actual witness \(C \in \mathbb{C}\), along with a proof that \(F\ C \cong D\), for each \(D \in \mathbb{D}\). In other words, a constructive witness of essential surjectivity is already a “choice function”, and an inverse functor \(G\) can be defined directly, with no need to invoke AC and no need for anafunctors. So in constructive logic, AP is simply true. However, this version of “essential surjectivity” is rather strong, in that it forces you to make choices you might prefer not to make: for each \(D \in \mathbb{D}\) there might be many isomorphic \(C \in \mathbb{C}\) to choose from, with no “canonical” choice, and it is annoying (again, a philosophical rather than technical consideration!) to be forced to choose one.

4. Instead of generalizing functors, a more direct solution is to generalize the notion of equality. After all, what really seems to be at the heart of all these problems is differing notions of equality (i.e. equality of sets vs isomorphism vs equivalence…). This is precisely what is done in homotopy type theory (Univalent Foundations Program 2013).³ It turns out that if one builds up suitable notions of category theory on top of HoTT instead of set theory, then (a) AP is true, (b) without the need for AC, (c) even with a weaker version of essential surjectivity that corresponds more closely to essential surjectivity in classical logic.⁴ This is explained in Chapter 9 of the HoTT book.

I plan to continue writing about these things in upcoming posts, particularly items (2) and (4) above. (If you haven’t caught on by now, I’m essentially blogging parts of my dissertation; we’ll see how far I get before graduating!) In the meantime, feedback and discussion are very welcome!