However, at first glance, the axiom of choice seems to be necessary in order for to be a regular 2-category. Specifically, given a commutative square of functors
in which is full and faithful and is essentially surjective, in order to define a lift we have to first choose, for each , an object and an isomorphism , then defining with its action on morphisms determined by (since is ff).
Of course, there is a sense in which this is not a “real” use of choice, since is determined by up to unique isomorphism. It is well-established that in the absence of choice, the usual notion of functor is too strict, and one should instead use anafunctors which determine their values only up to unique isomorphism. And it is not hard to check that if we define to be the (no longer strict) 2-category of categories, anafunctors, and natural transformations, then it is regular, and in fact a 2-pretopos, without any need for choice.
Toby: Something to consider: In Makkai's paper on anafunctors, he needs a (fairly weak) form of the axiom of choice to conclude that the bicategory of categories, and anafunctors, and ananatural transformations is cartesian closed. Maybe the right notions of exponentials don’t require even this.
Mike: Interesting point! Of course, in the absence of choice, one has to use anafunctors in order for to even be a regular 2-category, so this is an important question. However, it seems to me that his proof actually shows that without any choice at all, (his ) is cartesian closed in the sense that there is an anaequivalence , and this is all one ought to need or want. Am I wrong?
Toby: But without that SCSA thing, I don't know what means in this context. That is, the category of small anafunctors from a small category to a small category is not itself small (at least not if is inhabited), and Makkai uses SCSA to prove the existence of an equivalent small category.
Now that I look at this stuff closely again, it seems unlikely to shed much light on the matter here. But there it is.
Mike: If you trace through his proof, it seems to me that what he really shows is that (without any choice) any anafunctor is isomorphic to one whose set of specifications is of the form
for some . And there is clearly a set of these, so the full subcategory of on them should be an exponential in .
You only need choice if you want there to be a function assigning to each anafunctor an isomorphism to one of the above form. And you can avoid using the full strength of choice by allowing yourself to replace by anything in some specified set of sets that are isomorphic to it.
Mike: No, what I said in the previous comment is wrong! What’s true is that for any saturated anafunctor , the set of specifications from to is, if inhabited, isomorphic to . However, that isomorphism is non-canonical (to be precise, is a torsor over ). Thus, in order to to replace your anafunctor by one whose set of specifications is of the above form, you need to choose simultaneously, for every and such that is inhabited, an isomorphism , and that requires some choice. Where SCSA is weaker than AC is that you don’t need to be able to choose isomorphisms to , you just need to be able to choose isomorphisms to something such that there is at most a set of targets of the somethings, and that’s enough to make the category of anafunctors essentially small.
Right now I feel as though even in the absence of choice, “ought” to have all these good properties, including cartesian closure. If anafunctors aren’t good enough to recover all of that without some form of choice, then maybe that just means that even with anafunctors, set-theoretic foundations just aren’t fully capable of mimicking truly categorial foundations.
David Roberts: Clearly WISC has some bearing here (and probably the kernel of the idea originated from this discussion). Is there a 2-categorical form of WISC? Is it useful? I suppose this depends on the analogue of what is considered 'small' in the 2-logic