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

In my previous post, we considered the “Axiom of Protoequivalence”—that is, the statement that every fully faithful, essentially surjective functor (i.e. every protoequivalence) is an equivalance—and I claimed that in a traditional setting this is equivalent to the axiom of choice. However, intuitively it feels like AP “ought to” be true, whereas AC must be rejected in constructive logic.

One way around this is by generalizing functors to anafunctors, which were introduced by Makkai (1996). The original paper is difficult going, since it is full of tons of detail, poorly typeset, and can only be downloaded as seven separate postscript files. There is also quite a lot of legitimate depth to the paper, which requires significant categorical sophistication (more than I possess) to fully understand. However, the basic ideas are not too hard to grok, and that’s what I will present here.

It’s important to note at the outset that anafunctors are much more than just a technical device enabling the Axiom of Protoequivalence. More generally, if everything in category theory is supposed to be done “up to isomorphism”, it is a bit suspect that functors have to be defined for objects on the nose. Anafunctors can be seen as a generalization of functors, where each object in the source category is sent not just to a single object, but to an entire isomorphism class of objects, without privileging any particular object in the class. In other words, anafunctors are functors whose “values are specified only up to unique isomorphism”.

Such functors represent a many-to-many relationship between objects of \(\mathbb{C}\) and objects of \(\mathbb{D}\). Normal functors, as with any function, may of course map multiple objects of \(\mathbb{C}\) to the same object in \(\mathbb{D}\). The novel aspect is the ability to have a single object of \(\mathbb{C}\) correspond to multiple objects of \(\mathbb{D}\). The key idea is to add a class of “specifications” which mediate the relationship between objects in the source and target categories, in exactly the same way that a “junction table” must be added to support a many-to-many relationship in a database schema, as illustrated below:

On the left is a many-to-many relation between a set of shapes and a set of numbers. On the right, this relation has been mediated by a “junction table” containing a set of “specifications”—in this case, each specification is simply a pair of a shape and a number—together with two mappings (one-to-many relations) from the specifications to both of the original sets, such that a specification maps to a shape \(s\) and number \(n\) if and only if \(s\) and \(n\) were originally related.

In particular, an anafunctor \(F : \mathbb{C} \to \mathbb{D}\) is defined as follows.

• There is a class \(S\) of specifications.
• There are two functions \(\mathrm{Ob}\ \mathbb{C} \stackrel{\overleftarrow{F}}{\longleftarrow} S \stackrel{\overrightarrow{F}}{\longrightarrow} \mathrm{Ob}\ \mathbb{D}\) mapping specifications to objects of \(\mathbb{C}\) and \(\mathbb{D}\).

\(S\), \(\overleftarrow{F}\), and \(\overrightarrow{F}\) together define a many-to-many relationship between objects of \(\mathbb{C}\) and objects of \(\mathbb{D}\). \(D \in \mathbb{D}\) is called a specified value of \(F\) at \(C\) if there is some specification \(s \in S\) such that \(\overleftarrow{F}(s) = C\) and \(\overrightarrow{F}(s) = D\), in which case we write \(F_s(C) = D\). Moreover, \(D\) is a value of \(F\) at \(C\) (not necessarily a specified one) if there is some \(s\) for which \(D \cong F_s(C)\).

The idea now is to impose additional conditions which ensure that \(F\) “acts like” a regular functor \(\mathbb{C} \to \mathbb{D}\).

• Functors are defined on all objects; so we require each object of \(\mathbb{C}\) to have at least one specification \(s\) which corresponds to it—that is, \(\overleftarrow{F}\) must be surjective.
• Functors transport morphisms as well as objects. For each \(s,t \in S\) (the middle of the below diagram) and each \(f : \overleftarrow{F}(s) \to \overleftarrow{F}(t)\) in \(\mathbb{C}\) (the left-hand side below), there must be a morphism \(F_{s,t}(f) : \overrightarrow{F}(s) \to \overrightarrow{F}(t)\) in \(\mathbb{D}\) (the right-hand side):

• Functors preserve identities: for each \(s \in S\) we should have \(F_{s,s}(\mathit{id}_{\overleftarrow{F}(s)}) = \mathit{id}_{\overrightarrow{F}(s)}\).
• Finally, functors preserve composition: for all \(s,t,u \in S\) (in the middle below), \(f : \overleftarrow{F}(s) \to \overleftarrow{F}(t)\), and \(g : \overleftarrow{F}(t) \to \overleftarrow{F}(u)\) (the left side below), it must be the case that \(F_{s,u}(f ; g) = F_{s,t}(f) ; F_{t,u}(g)\):

Our initial intuition was that an anafunctor should map objects of \(\mathbb{C}\) to isomorphism classes of objects in \(\mathbb{D}\). This may not be immediately apparent from the definition, but is in fact the case. In particular, the identity morphism \(\mathit{id}_C\) maps to isomorphisms between specified values of \(C\); that is, under the action of an anafunctor, an object \(C\) together with its identity morphism “blow up” into an isomorphism class (aka a clique). To see this, let \(s,t \in S\) be two different specifications corresponding to \(C\), that is, \(\overleftarrow{F}(s) = \overleftarrow{F}(t) = C\). Then by preservation of composition and identities, we have \(F_{s,t}(\mathit{id}_C) ; F_{t,s}(\mathit{id}_C) = F_{s,s}(\mathit{id}_C ; \mathit{id}_C) = F_{s,s}(\mathit{id}_C) = \mathit{id}_{\overrightarrow{F}(s)}\), so \(F_{s,t}(\mathit{id}_C)\) and \(F_{t,s}(\mathit{id}_C)\) constitute an isomorphism between \(F_s(C)\) and \(F_t(C)\).

There is an alternative, equivalent definition of anafunctors, which is somewhat less intuitive but usually more convenient to work with: an anafunctor \(F : \mathbb{C} \to \mathbb{D}\) is a category of specifications \(\mathbb{S}\) together with a span of functors \(\mathbb{C} \stackrel{\overleftarrow{F}}{\longleftarrow} \mathbb{S} \stackrel{\overrightarrow{F}}{\longrightarrow} \mathbb{D}\) where \(\overleftarrow{F}\) is fully faithful and (strictly) surjective on objects.

Note that in this definition, \(\overleftarrow{F}\) must be strictly (as opposed to essentially) surjective on objects, that is, for every \(C \in \mathbb{C}\) there is some \(S \in \mathbb{S}\) such that \(\overleftarrow{F}(S) = C\), rather than only requiring \(\overleftarrow{F}(S) \cong C\). Given this strict surjectivity on objects, it is equivalent to require \(\overleftarrow F\) to be full, as in the definition above, or to be (strictly) surjective on the class of all morphisms.

We are punning on notation a bit here: in the original definition of anafunctor, \(S\) is a set and \(\overleftarrow{F}\) and \(\overrightarrow{F}\) are functions on objects, whereas in this more abstract definition \(\mathbb{S}\) is a category and \(\overleftarrow{F}\) and \(\overrightarrow{F}\) are functors. Of course, the two are closely related: given a span of functors \(\mathbb{C} \stackrel{\overleftarrow{F}}{\longleftarrow} \mathbb{S} \stackrel{\overrightarrow{F}}{\longrightarrow} \mathbb{D}\), we may simply take the objects of \(\mathbb{S}\) as the class of specifications \(S\), and the actions of the functors \(\overleftarrow{F}\) and \(\overrightarrow{F}\) on objects as the functions from specifications to objects of \(\mathbb{C}\) and \(\mathbb{D}\). Conversely, given a class of specifications \(S\) and functions \(\overleftarrow{F}\) and \(\overrightarrow{F}\), we may construct the category \(\mathbb{S}\) with \(\mathrm{Ob}\ \mathbb{S} = S\) and with morphisms \(\overleftarrow{F}(s) \to \overleftarrow{F}(t)\) in \(\mathbb{C}\) acting as morphisms \(s \to t\) in \(\mathbb{S}\). From \(\mathbb{S}\) to \(\mathbb{C}\), we construct the functor given by \(\overleftarrow{F}\) on objects and the identity on morphisms, and the other functor maps \(f : s \to t\) in \(\mathbb{S}\) to \(F_{s,t}(f) : \overrightarrow{F}(s) \to \overrightarrow{F}(t)\) in \(\mathbb{D}\).

Every functor \(F : \mathbb{C} \to \mathbb{D}\) can be trivially turned into an anafunctor \(\mathbb{C} \stackrel{\mathit{Id}}{\longleftarrow} \mathbb{C} \stackrel{F}{\longrightarrow} \mathbb{D}\). Anafunctors also compose. Given compatible anafunctors \(F : \mathbb{C} \stackrel{\overleftarrow F}{\longleftarrow} S \stackrel{\overrightarrow F}{\longrightarrow} \mathbb{D}\) and \(G : \mathbb{D} \stackrel{\overleftarrow G}{\longleftarrow} T \stackrel{\overrightarrow G}{\longrightarrow} \mathbb{E}\), consider the action of their composite on objects: each object of \(\mathbb{C}\) may map to multiple objects of \(\mathbb{E}\), via objects of \(\mathbb{D}\). Each such mapping corresponds to a zig-zag path \(C \longleftarrow s \longrightarrow D \longleftarrow t \longrightarrow E\). In order to specify such a path it suffices to give the pair \((s,t)\), which determines \(C\), \(D\), and \(E\). Note, however, that not every pair in \(S \times T\) corresponds to a valid path, but only those which agree on the middle object \(D \in \mathbb{D}\). Thus, we may take \(\{ (s,t) \mid s \in S, t \in T, \overrightarrow{F}(s) = \overleftarrow{G}(t) \}\) as the set of specifications for the composite \(F ; G\), with \(\overleftarrow{F ; G}(s,t) = \overleftarrow{F}(s)\) and \(\overrightarrow{F ; G}(s,t) = \overrightarrow{G}(t)\). On morphisms, \((F ; G)_{(s,t),(u,v)}(f) = G_{t,v}(F_{s,u}(f))\). It is not hard to check that this satisfies the anafunctor laws.

If you know what a pullback is, note that the same thing can also be defined at a higher level in terms of spans. \(\mathbf{Cat}\), the category of all (small) categories, is complete, and in particular has pullbacks, so we may construct a new anafunctor from \(\mathbb{C}\) to \(\mathbb{E}\) by taking a pullback of \(\overrightarrow F\) and \(\overleftarrow G\) and then composing appropriately.

One can go on to define ananatural transformations between anafunctors, and show that together these constitute a \(2\)-category \(\mathbf{AnaCat}\) which is analogous to the usual \(2\)-category of (small) categories, functors, and natural transformations; in particular, there is a fully faithful embedding of \(\mathbf{Cat}\) into \(\mathbf{AnaCat}\), which moreover is an equivalence if AC holds.

To work in category theory based on set theory and classical logic, while avoiding AC, one is therefore justified in “mixing and matching” functors and anafunctors as convenient, but discussing them all as if they were regular functors (except when defining a particular anafunctor). Such usage can be formalized by turning everything into an anafunctor, and translating functor operations and properties into corresponding operations and properties of anafunctors.

However, as I will argue in some future posts, there is a better solution, which is to throw out set theory as a foundation of category theory and start over with homotopy type theory. In that case, thanks to a generalized notion of equality, regular functors act like anafunctors, and in particular AP holds.