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.

References

Makkai, Michael. 1996. “Avoiding the Axiom of Choice in General Category Theory.” Journal of Pure and Applied Algebra 108 (2). Elsevier: 109–73.

5 Responses to Anafunctors

David Roberts says:

August 13, 2014 at 2:37 am

Maybe I’ll just mention this:

http://www.tac.mta.ca/tac/volumes/26/29/26-29abs.html

;-) Hope you find it useful… I have a sequel in the works that works in any 2-category with appropriate (very weak) structure.

- Brent says:
  
  August 20, 2014 at 12:23 pm
  
  Thanks!
  
Thomas Benjamin says:

May 24, 2015 at 11:03 am

If one can use anafunctors to avoid the axiom of choice, is it possible to define an ‘endo-anafunctor’ from the category Set into Set such that the ‘endo-anafunctor’ in question is also an elementary embedding that is not the identity? Can one define the notion of elementary embedding in terms of functors and anafunctors?

- Brent says:
  
  May 24, 2015 at 4:27 pm
  
  I don’t really know anything about elementary embeddings so I couldn’t say.
  
- David Roberts says:
  
  May 25, 2015 at 1:49 am
  
  Hi Thomas, no doubt you’re thinking of trying to define a Reinhardt cardinal in structural, choiceless, set theory. Note that an elementary embedding will induce a conservative logical functor with extra properties. Even studying elementary embeddings from a structural viewpoint is hardly started.
  
  Note that one might want to do this, instead of using the category of sets, with some form of algebraic set theory (AST), which axiomatises the category of classes. This is a structural analogue of class-set theory. There is no guarantee this will make things easier, but since elementary embeddings preserve all of first-order logic, and topos theory deals mainly with bounded quantifiers, it seems something is necessary beyond just the category of sets. Work of Mike Shulman on stack semantics is also relevant here, as it is a means to capture unbounded quantifiers in structural set theory without looking at AST.
  
  Hope this helps, and I’ve love to hear from you if you have any good ideas (see my website for email).

Anafunctors

References

About Brent

5 Responses to Anafunctors

Leave a Reply Cancel reply

Pages

Categories

Archives

Top Posts

Blogroll

Fun

Personal

Meta

Anafunctors

References

Share this:

Like this:

Related

About Brent

5 Responses to Anafunctors

Leave a Reply Cancel reply

Pages

Categories

Archives

Top Posts

Blogroll

Fun

Personal

Meta