Michael Shulman regular 2-categories and choice

Regularity without choice

The 1-category $Set$ 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 $Set$ is a pretopos.

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

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

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

Of course, there is a sense in which this is not a “real” use of choice, since $f(a_b)$ is determined by $b$ 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 $Cat$ 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 $Cat$ 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, $Cat$ (his $AnaCat$) is cartesian closed in the sense that there is an anaequivalence $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^B$ means in this context. That is, the category of small anafunctors from a small category $B$ to a small category $C$ is not itself small (at least not if $B$ 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 $X\to A$ is isomorphic to one whose set of specifications is of the form

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

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

You only need choice if you want there to be a function assigning to each anafunctor $X\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)$ 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 $F$, the set ${|F|}(x,a)$ of specifications from $x$ to $a$ is, if inhabited, isomorphic to $Iso(a,a)$. However, that isomorphism is non-canonical (to be precise, ${|F|}(x,a)$ is a torsor over $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 $x$ and $a$ such that ${|F|}(x,a)$ is inhabited, an isomorphism ${|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)$, 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, $Cat$ “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