Michael Shulman regular 2-categories and choice

Regularity without choice

The 1-category SetSet is a 1-topos, and in particular regular, without any need for the axiom of choice, or indeed even any need for classical logic. Even predicativists generally agree that SetSet is a pretopos.

However, at first glance, the axiom of choice seems to be necessary in order for CatCat to be a regular 2-category. Specifically, given a commutative square of functors

A f C e m B g D\array{A & \overset{f}{\to} & C\\ e \downarrow && \downarrow m\\ B& \underset{g}{\to} & D}

in which mm is full and faithful and ee is essentially surjective, in order to define a lift h:BCh:B\to C we have to first choose, for each bBb\in B, an object a bAa_b\in A and an isomorphism e(a b)be(a_b)\cong b, then defining h(b)=f(a b)h(b)=f(a_b) with its action on morphisms determined by gg (since mm is ff).

Of course, there is a sense in which this is not a “real” use of choice, since f(a b)f(a_b) is determined by bb 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 CatCat 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.

Discussion on cartesian closure

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 CatCat 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, CatCat (his AnaCatAnaCat) is cartesian closed in the sense that there is an anaequivalence Cat(A×B,C)Cat(A,C B)Cat(A\times B,C) \simeq Cat(A, C^B), and this is all one ought to need or want. Am I wrong?

Toby: But without that SCSA thing, I don't know what C BC^B means in this context. That is, the category of small anafunctors from a small category BB to a small category CC is not itself small (at least not if BB 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 XAX\to A is isomorphic to one whose set of specifications is of the form

(x,a)SIso(a,a)\coprod_{(x,a)\in S} Iso(a,a)

for some SOb(X)×Ob(A)S\subset Ob(X)\times Ob(A). And there is clearly a set of these, so the full subcategory of Cat(X,A)Cat(X,A) on them should be an exponential A XA^X in CatCat.

You only need choice if you want there to be a function assigning to each anafunctor XAX\to A an isomorphism to one of the above form. And you can avoid using the full strength of choice by allowing yourself to replace Iso(a,a)Iso(a,a) 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 FF, the set |F|(x,a){|F|}(x,a) of specifications from xx to aa is, if inhabited, isomorphic to Iso(a,a)Iso(a,a). However, that isomorphism is non-canonical (to be precise, |F|(x,a){|F|}(x,a) is a torsor over Iso(a,a)Iso(a,a)). 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 xx and aa such that |F|(x,a){|F|}(x,a) is inhabited, an isomorphism |F|(x,a)Iso(a,a){|F|}(x,a)\overset{\cong}{\to} Iso(a,a), and that requires some choice. Where SCSA is weaker than AC is that you don’t need to be able to choose isomorphisms to Iso(a,a)Iso(a,a), 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, CatCat “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

Last revised on February 19, 2010 at 06:21:58. See the history of this page for a list of all contributions to it.