In basic category theory we learn that size distinctions play a crucial role. In particular, if a “category” must have a set of objects and a set of morphisms, where “set” is interpreted relative to some membership-based set theoretic foundation (such as ZFC), then there cannot be a category of all sets, since by Cantor’s paradox there is no set of all sets. But we want to have a category called Set, so we generally either allow “large categories” that have only a “class” of objects, or introduce some bound on the size of the sets allowed as objects of . In either case there are now some very set-like objects (whether we call them “classes” or “large sets”) that are not objects of , which causes some headaches.
However, many people would find it natural to say that while there is not a set of all sets, there is a category of all sets. For example, from a categorical perspective it doesn’t make sense to talk about equality of sets, only isomorphism, whereas the elements of a set by definition come with a notion of equality. However, it is not immediately clear how to make this precise. Clearly we will have to give up the definition of a category as having a set of objects and a set of morphisms. One natural idea suggested by the theory of 2-toposes is to assume, as our basic theory, that:
This is to be regarded as a logical theory akin to ZFC or the theory of an elementary topos, as a proposed foundation for mathematics. In particular, we take the notion of “category” (and “functor” and “natural transformation”) as basic, rather than the notion of “set” (and “function”), and choose an appropriate list of axioms providing for various different ways to construct categories and functors. We can then define “set” to mean “discrete category,” just as in ordinary set theory we can define “truth value” to mean “subsingleton set.”
With this meaning of “set”, the existence of a discrete opfibration classifier means that there is a category of all sets. More precisely, we have an object of , which we will denote “”, equipped with a discrete opfibration such that for any object of , pullback of determines an equivalence
We will write “” for the full sub-2-category of spanned by the discrete objects. Of course, it is equivalent to an ordinary category, but in the “meta” sense, not the sense of the theory in which “category” means “object of ”. (The relationship between “meta” categories and objects of is a bit analogous to the relationship between “classes” and sets in classical set theory—which, of course, begs the question of repeating the process one level up!) Thus, to avoid confusion, we carefully distinguish from ; the relationship is that , since .
Clearly no 2-category constructed from the usual models of set theory will have this property, but from one perspective perhaps one should not expect to be able to construct 2-toposes from 1-toposes. Certainly we can’t construct 1-toposes from 0-toposes (Heyting algebras) without some prior notion of “set” for our sheaves to take values in.
The most important question, then, is is this consistent? It is certainly quite possible that the answer is no; we haven’t been looking for a contradiction for very long. But if it is consistent, the next question is what else can we consistently assume about ? Some potential additional hypotheses include:
Let me pose this as a challenge to readers of this page:
Currently, combinations that are known to be contradictory (see below) include:
Note that having enough groupoids implies that is a topos, as do exponentials together with Booleanness, as do exponentials together with duality.
It thus appears that the strongest “live” combination is
To a mathematician trained in a foundation of set theory, having a category of all sets may seem fraught with paradoxes. It is worth giving an example to show that the barbarians may not be quite so close to the gate as all that. In the book Accessible Categories by Makkai-Pare, it is shown (using a traditional set-theoretic foundation) that if is an accessible category, then accessible fibrations over can be identified with accessible pseudofunctors . Thus, accessible discrete fibrations over can be identified with accessible functors . So, with a suitable “niceness” restriction on both the categories allowed and the functors allowed, it is already possible in set theory for to function as a “category of all sets” in some sense.
It is also worth remarking on the intuitive similarity of our definition “a set is a discrete category,” or equivalently “all discrete categories are sets,” to one version of the set-theoretic hypothesis Vopenka’s principle which states that “any discrete full subcategory of a locally presentable category is a set.”
Of course, the 2-category of accessible categories is not a 2-pretopos, does not have opposites (so that calling a contravariant functor “accessible” is not strictly kosher), and the variance of this example is different from our proposed axiom above. So this is certainly not a consistency proof. But it suggests at least a vague hope that there might be a consistency proof relative to some large cardinal axiom.
If is an object of (i.e. a “category”), then if is a discrete object of (i.e. a “set”) and is an eso, then it makes sense to say that is the (or “a”) set of objects of , since can be presented as the quotient of a 2-congruence on . So saying that every category has a set of objects would be essentially the same as saying that has enough discretes.
Now if itself had a set of objects, that set would function as a “set of all sets,” which would certainly lead to contradictions in the usual way. But in our framework, at least a priori all we can conclude from that is that does not have a set of objects, i.e. does not admit any eso from a discrete object, and therefore in particular does not have enough discretes. (We will see below that actually, it almost certainly cannot have enough groupoids either.)
However, many categories do have a set of objects. In particular, any category that is “small” relative to the the usual set-theoretic foundations will be constructible in our theory as the quotient of some 2-congruence on a set, and therefore will have a set of objects. And by properties of regular 2-categories, any category with a set of objects will be the quotient of some 2-congruence on a set, and so categories having a set of objects can be identified with internal categories in .
Thus, we have not done away with “size distinctions” entirely, but our point of view is different. Rather than thinking of categories with a set of objects as somehow “smaller” than those without, we think of them as equipped with a notion of equality on their objects, which other categories (such as ) may lack. We will see below that size distinctions do not play nearly as important a role as they do with the usual foundations, due to the existence of a category of all sets.
Since is a Heyting 2-pretopos with a discrete opfibration classifier, it automatically inherits a cosieve classifier, i.e. a subobject object which classifies cosieves. Since if is discrete, any subobject is a cosieve, in particular we have . Thus, is almost a topos, but of course will not itself be a set. But it is posetal, so its core, if it has one, will be discrete. Since a core of would be its coreflection into the groupoidal objects, we would have
Cat(A,J\Omega) \simeq Cat_g(A,\Omega)\simeq J(Sub(A))
so that would be a subobject classifier in . Since is cartesian closed if has exponentials, we have shown:
If has exponentials and enough groupoids, then is a topos.
Actually, however, exponentials are unnecessary. Observe that since classifies discrete opfibrations, classifies maps between discrete opfibrations. We can then use the internal first-order logic to cut out a subobject that classifies monomorphisms between discrete opfibrations. Finally, if is discrete, we pull back the second projection along the classifying map of , to get , the object of monomorphisms into . The universal property of is that morphisms correspond to subobjects of in . Since if is discrete, subobjects of in are the same as subobjects of , is almost like a power object of in . Of course, it is also not discrete, but the same argument for its core shows that:
If has enough groupoids, then is a topos.
Recall also that any cartesian closed Boolean category is a topos, since then is a subobject classifier. Thus we also have:
If is Boolean, then is a topos.
Finally, we observe that exponentials and a duality involution also suffice. Let be the cosieve classifier; then is a sieve opclassifier, i.e. is equivalent to the opposite of the poset of sieves on . On we thus have both a sieve and a cosieve , pulled back from and ; let be the subobject of defined as in the Heyting algebra structure. Now maps into classify sieves and cosieves that are equal as subobjects, which is to say, subobjects that are both sieves and cosieves. And transformations between maps correspond to both inclusions of cosieves and coinclusions of sieves, which is to say, identities; thus is discrete, and hence a subobject classifier in .
If has exponentials and a duality involution, then is a topos.
Now, it is not immediately clear what being a topos implies about the properties of in the internal logic of . A full treatment will have to await developing the internal logic better, and especially the behavior of Kripke-Joyal semantics? and functor comprehension?. However, there are some things we can say right away.
Suppose that has exponentials and a duality involution. Then the exponential of an opfibration to a fibration is an opfibration. Applying this to the universal discrete opfibration and the universal discrete fibration , both pulled back to , we obtain a discrete opfibration over . Of course, it has a classifying map ; thus exponentials in are represented by a morphism in . It’s not obvious whether this implies that “ is cartesian closed” is true in the internal logic of , but it is true that if and are sets (discrete objects of ), with classifying maps and , then is classified by .
Now if in addition is a topos, then taking to be its subobject classifier, we obtain a contravariant powerset functor . The existence of a covariant powerset functor is less obvious, but I believe that functor comprehension? will let us prove that if has enough groupoids, then it exists.
The category of all sets, if it exists, has all limits and colimits (not just small ones). The colimits (in fact, all left Kan extensions) are easiest to construct using the comprehensive factorization. Since for any , the functor
(-\circ k):Cat(B,set)\to Cat(A,set)
is equivalent to
the left adjoint to the latter gives a left adjoint to the former; but this just says that all left extensions along into exist. And the Beck-Chevalley property for says precisely that these left extensions are pointwise, in the usual 2-categorical sense that they remain extensions when pasting on comma squares.
We assumed countable-coherency in constructing the comprehensive factorization, which is not an elementary condition, but I think that similar “internalized” arguments should work as long as has an exponentiable NNO (in the same way that an ordinary -pretopos with an NNO can be shown to be finitely cocomplete).
Similarly, if has exponentials, then each pullback functor has a right adjoint , and so we obtain all right extensions into . The dual Beck-Chevalley condition also implies pointwiseness of these extensions.
It is true in any 2-category that if is a morphism such that if the left extension exists and is preserved by , then it is a right adjoint to . Since admits all left extensions, it follows that any morphism that preserves all left extensions (that is, all colimits) has a right adjoint, and dually any morphism preserving all right extensions (all limits) has a left adjoint. Thus we have a “dream adjoint functor theorem” requiring no “small-generator” hypotheses. Presumably any category constructed from in a reasonable way should inherit all limits and colimits, so that the adjoint functor theorem will apply to such categories as well.
In particular, if is an object (such as ) having all limits and is a subobject of closed under such limits, then the inclusion has a left adjoint, i.e. is reflective in . Note again the similarity with one of the classical consequences of Vopenka’s principle, namely “any full subcategory of a locally presentable category which is closed under limits is reflective.”
The classical argument of Freyd that a category with limits the size of its set of objects is a preorder depends on having a discrete category that is as big as the collection of objects of the category. (It also requires classical logic.) Since we have discarded the assumption of enough discretes, we don’t have to worry about becoming a poset in this way. However, we do have another potential problem, stemming from an otherwise lovely fact.
If has an NNO, then for any endomorphism and any object , the induced endofunctor has a terminal coalgebra, and these are preserved by pullback. Therefore, “ has a terminal coalgebra” is true in the internal logic of .
This follows the classical proof of the Knaster-Tarski theorem for posets, see e.g. Lambek, “A fixpoint theorem for complete categories.” Let be the inserter of , with inserted 2-cell , and let with be the left extension of along . We have a 2-cell obtained from the universal property of the Kan extension (by definition ). Thus is an -coalgebra, so is an -coalgebra, and is an -coalgebra for any , clearly preserved by pullback.
Now if is any -coalgebra, we have where , so induces a map with . The 2-cell then induces a map , and the equality
f\phi c'.\gamma = f\phi c' . \alpha c' = (f\phi.\alpha)c'= (\tau!.\phi)c' = \tau!c'.\phi c' = \tau.\phi c'
implies that is a coalgebra map. Moreover, coalgebra maps in correspond to 2-cells , and the interchange law for the composite implies that
\phi d' . i\theta = t!\theta . \phi c' = \phi c'
and thus .
Now the equality means that induces a 2-cell (using the 2-dimensional universal property of ). Then the interchange law for the composite implies that . But since exhibits as a left extension, this implies , and therefore . It follows that for any coalgebra map , we have ; thus is a terminal coalgebra.
Dually, using limits, we have:
If has exponentials, then for every , each has an initial algebra, and these are preserved by pullback.
In general, having initial algebras and final coalgebras for endofunctors is quite useful. An NNO is itself an initial algebra for the endofunctor . More generally, initial algebras for polynomial endofunctors (“-types”) capture various types of well-founded recursion. However, since by Lambek’s lemma, an initial algebra or final coalgebra is a fixed point of the functor, this can be a problem.
In addition to our standing hypotheses ( is a Heyting 2-pretopos with a discrete opfibration classifier), it is inconsistent to assume that
By the Knaster-Tarski theorem and Lambek’s lemma, either of the first two hypotheses ensures that any covariant endofunctor of has a fixed point. In particular, we have a set which is isomorphic to its power object in . But this is impossible, since Cantor’s diagonal argument is valid in any topos.
Now suppose, instead of enough groupoids, that has exponentials and a duality involution. Then fixing any , the “exponentials” map gives us a functor , and therefore an iterated covariant functor , which once again must have a fixed point. Combining this with Theorem 4, we have:
In addition to our standing hypotheses, it is inconsistent to assume that
Theorem 4 implies that is a topos, hence has a subobject classifier . Now by the above arguments and the Knaster-Tarski theorem, the endofunctor of has a fixed point, say . Therefore, we have a monomorphism (the first morphism being “singletons”). Applying contravariant again, which turns monics into epics, we have an epimorphism . Now Cantor’s diagonal argument applies again.
There can be particular objects in a locally cartesian closed category (or even a topos) such that has a fixed point. For instance, this is certainly the case if is a model of the untyped lambda calculus with , and these are known to exist in some toposes. Moreover, there are cartesian closed categories of domains in which the equation has a solution for any . This doesn’t answer the question of whether it is consistent for to have a fixed point for every in a locally cartesian closed pretopos, but it suggests that any such contradiction will have to result from a more clever argument.
Now suppose that , and hence , is Boolean, and that is a topos (as is the case if we also have exponentials). Let denote the category of sets equipped with a binary relation , and let denote the full subcategory of determined by those such that for all . Booleanness tells us that is, in fact, the category of “sets and injective functions.” Now, if we have a comprehensive factorization, then the forgetful functor has a colimit; call it . The usual arguments show that since is a filtered diagram of injections, each object in the diagram injects into the colimit . Therefore, every set injects into , including . Applying the contravariant power set functor of to the injection , we obtain a surjection , contradicting Cantor’s theorem.
In fact, however, Booleanness is unnecessary. If we perform the above construction in the non-Boolean case, then the category we obtain is the category of sets and ”-injective functions,” i.e. functions such that if then . If is again the colimit of , then every object in the colimit -injects into , and in particular so does . Now just as an injection gives us a surjection , a -injection gives us a surjection , where is the object of -closed subsets of . But the Cantor diagonal set is defined by a negative property , hence is -closed, so again we have a contradiction.
In addition to our standing hypotheses, it is inconsistent to assume that
We constructed the comprehensive factorization using countable coherency, but an exponentiable NNO should allow the “internalization” of this argument. Thus the above contradiction goes through in either case.
All the above contradictions have come from Cantor’s paradox. Russell’s paradox seems unlikely to have any effect on a categorical theory, where membership is a purely local notion. The other classical paradox of set theory, attributed to Burali-Forti among others, is that the set of all ordinal numbers would itself be an ordinal number. I have not yet figured out the best way to construct the collection of ordinal numbers in a Heyting 2-pretopos with a discrete opfibration classifier, but it seems likely that however we do it, it will be a posetal object rather than a discrete one, and hence not a candidate to be an element of itself.
However, as pointed out by Toby below, if we were in a (2,3)-pretopos containing a “(1,2)-category of all posets” then we could construct the poset of all ordinal numbers and show that it is an element of itself, recovering the Burali-Forti paradox. We don’t have a precise definition yet of a (2,3)-pretopos, and there are certain obstacles? that you might not expect. But let’s suppose for the sake of argument that we’ve got a “Heyting (2,3)-pretopos,” with an exponentiable NNO, and an object that classifies all “posetal opfibrations.”
Define a wellfounded poset to be a poset equipped with an additional binary relation such that
This isn’t the “correct” constructive definition of “wellfounded,” but it’ll be enough to get a contradiction.
Let be the “(1,2)-category of all wellfounded posets,” which we can construct, using the internal logic of our Heyting (2,3)-pretopos, as a full subobject of . (We need an exponentiable NNO to be able to quantify over infinite sequences.) Then a morphism in between two wellfounded posets and is a map of posets which preserves , i.e. if then . Let be the posetal reflection of ; thus we have in iff there exists an preserving both and .
Now define a relation on by setting if there exists an in such that there is a with for all . We claim that with this relation is wellfounded. Clearly if , then . And if we have
\dots\prec A_3 \prec A_2\prec A_1
then we have functions and elements such that for all . Thus, we have
\dots \prec f_2(f_3(a_3)) \prec f_2(a_2)\prec a_1
contradicting wellfoundedness of . Therefore, with is itself a wellfounded poset.
Now, for any wellfounded poset and any , we have a wellfounded poset . If , then of course and so in . And if , then and is a bound for the inclusion , so that in this case in . Therefore, is a function in , so in . (We are tacitly identifying wellfounded posets with their classifying maps .) Moreover, the inclusion is bounded by , so we have in . Thus is a bound for the function from to , so we have in . Finally, taking we obtain , contradicting the wellfoundedness of .
It is inconsistent to assume the existence of a Heyting (2,3)-pretopos with an exponentiable NNO and a posetal-opfibration classifier.
By using a better definition of wellfoundedness, we can replace the NNO with a duality involution. Let’s redefine a poset with an extra binary relation to be wellfounded if
Recall that a sieve is a ff which is also a fibration, or equivalently a down-closed sub-poset. As in the 2-category case above, a posetal-opfibration classifier gives us a cosieve classifier, so we can quantify over cosieves in the internal logic; thus with a duality involution, we can classify over sieves as well. Hence we can construct the “(1,2)-category of all wellfounded posets” as a full subobject of , using the internal logic of our Heyting (2,3)-pretopos.
The usual constructive definition of wellfoundedness refers to any subset, rather than just sieves, but we can actually recover that. If is any subobject, define ; then is a sieve. It is easy to check that if is “inductive” in the above sense, then so is (using the assumption that implies ); hence , and since , we have . In particular, we can now use the classical argument to show that is irreflexive: for all .
We now repeat the same argument; the only point of difference is the proof that the posetal reflection of is wellfounded in our new sense. So let be a sieve of wellfounded posets with the property that if for all , then . For any wellfounded , define . Since is a sieve, is a sieve. Suppose that and for all . Then for all such . Then for any wellfounded such that , there is a function bounded by some . But then by assumption, and so since is a sieve. Thus, by the assumption on , we have and thus . Thus, since is wellfounded, we have . But now, if is any wellfounded poset such that , we have bounded by some , whence (since ) and so since is a sieve. Thus, again by assumption on , we have . Therefore, every wellfounded poset is in , so ; hence is wellfounded.
Thus we have:
It is inconsistent to assume the existence of a Heyting (2,3)-pretopos with exponentials, a duality involution, and a posetal-opfibration classifier.
Mike, you've thought about these matters more deeply than I have, so just a few global comments:
If there are enough groupoids, then you can construct the set of equivalence classes of objects of a category as the discrete reflection of its core. I don’t know any other 2-categorical way to construct it, or even to define what it would mean.
Your third suggestion seems like a reasonable thing to try, although it would require working in (at least) a (2,3)-category containing a (1,2)-category of all posets, rather than a 2-category containing a category of all sets. Also, I don’t know how, constructively, to define what it means for a reflexive relation to be well-founded, only an irreflexive one. Do you? —Mike
OK, that's what I expected you to say about (2), so I'm glad that I understand that. I'm not sure that I like a foundation of the theory of categories that doesn't allow this, but of course the point is that one has options, and that's interesting.
To construct a well-ordered poset, you equip a poset with a well-founded (hence irreflexive) and transitive relation , then impose the extensionality condition that
\forall t: t \prec x \Rightarrow t \prec y
implies that , rather than that
\forall t: t \prec x \Leftrightarrow t \prec y
implies that as you would to construct a well-ordered set. In other words, a well order on a poset is a structure rather than a property, just as a well order on a set is, except that (classically at least) you can prove that any well order on a poset is unique. Also note that a well order on a poset respects the partial order in that implies that , which is sesquivariant, so contravariance needs to be in the language to make it work.
Even so, I see how you still get out of it, however; as you say, you have a category of all sets rather than a category of all posets, and without enough groupoids you can’t define the faithful functor from posets to sets that would allow you to realise the subcategory of all well-ordered posets and give it the structure of a well-ordered poset. That's pretty clever!
Mike: It does suggest, though, that having an -topos containing an -category of all -categories is likely to become impossible at , although I need to think about it for a bit and convince myself that there isn’t any other “out.” Since we know that it is possible at ( itself is such), this leaves the case as an intriguing no-mans-land.
Regarding sets of isomorphism classes of objects, of course any category having a set of objects, or even a groupoid of objects, will necessarily have a set of isomorphism classes of objects. I don’t think I’ve ever felt any need to talk about the class of isomorphism classes of objects of a large category; what reasons do you have to want it?
Mike: Okay, I convinced myself that Burali-Forti goes through in a (2,3)-category; see above.
This also makes me a bit sad because I don’t know how to define the category of topological spaces in a 2-pretopos where is not a topos, and I’d sort of hoped to be able to solve this problem in a (2,3)-pretopos.
Toby: ‘Regarding sets of isomorphism classes of objects … what reasons do you have to want it?’: To complete the identification of small categories with categories that have a notion of equality of objects. Since I can define equality of isomorphism classes of objects (or more simply, since I can define equality of objects as isomorphism), there should be a small category that has this class of objects, even though it's not equivalent to the category that we started with (which is just as well since that was not small). And if you say that a locally small category with a small set of (isomorphism classes of) objects must itself be (equivalent to a category which is) small, then I accuse you of using the axiom of choice!
And people do use classes of isomorphism classes of large categories. Certainly people talk about the class of cardinal numbers, even if they're set theorists who won't admit that their motivation is to talk about the class of isomorphism classes of . And people form things like the free group on the monoid of isomorphism classes of a monoidal category, even if maybe they should be decategorifying less when they do that. So these do come up in mathematics in practice.
Besides, I want to take homotopy groups of -categories.
Mike: Just because you have a notion of equality between s doesn’t necessarily mean that you have a set of s, or a small category whose objects are s. A small category is a category that additionally has a notion of equality of objects, but if I just give you some notion of equality between s, all you can say is that if there is a category of s, then it is small.
I don’t think I’ve ever seen anyone take the free group on a monoid of isomorphism classes of a large monoidal category. The monoidal categories from which people construct -theory and so on are all (essentially) small. And it’s not clear to me that set theorists really need a (discrete) class of cardinalities; mightn’t the category of sets itself suffice?
(I’m doing my best to play devil’s advocate here, although other things being equal, I also would certainly prefer to have cores. But they seem to be contradictory with a category of all sets, so I’m trying my best to imagine a world without them.)
Toby: ‘if I just give you some notion of equality between s, all you can say is that if there is a category of s, then it is small’: But this notion of equality exists for any category ; the notion is isomorphism, defining a set . It actually does not follow that the category is small, because one needs the axiom of choice to define the eso from to (even as an anafunctor), so it's not like is a set of objects of . But it is the set of isomorphism classes of objects of or (which is how I prefer to think of it) the set of objects of up to isomorphism.
I know, you can't actually form in the language available here, so there's no contradiction, but I still feel that ought to be as legitimate as .
I don't know enough about -theory to know if they only do this stuff to essentially small categories. I know that often they limit themselves to, say, finite-dimensional spaces, but does it change anything to drop such restrictions? I don't know. I think that we can agree that all of this stuff probably works better if one simply declines to decategorify. But it still seems wrong that one may not be able to decategorify.
Actually, IIUC we can decategorify if we end up with a poset rather than a set, so let's do that, getting a poset of cardinal numbers, posetal groups and rings in -theory, and an -tuply monoidal poset (rather than an -tuply groupal set) as at a given object of an -category (and in particular a pointed poset rather than a pointed set as ). Then you're saying that a poset need not have an underlying set! Just calling it ‘-category’ instead of ‘poset’ does not change the fact that this is crazy.
I understand that we're being devil's advocates to one another. I like getting rid of size conditions on theorems as much as you like having cores.
Mike: Of course, a “notion of equality” is a very vague term; for instance a priori nothing prevents us from saying that every is equal to every other . But I think that maybe your problem is that you’re still thinking of a category as a collection of objects together with a collection of morphisms, rather than as an atomic object in its own right. From the latter point of view, you can’t just take the objects of a category, slap a notion of equality on them, and call the result a set. More generally, you can’t just take the objects of a category, slap on a new collection of morphisms, and call the result a category. I like to think of this as analogous to how in classical set theory you can’t just take any arbitrary collection of things and call it a set, despite whatever our intuition may say; you have to adhere to a specific list of rules for forming sets out of other sets.
Amusingly, -theory actually becomes trivial if you allow infinite-dimensional spaces, because of the Eilenberg swindle. For any projective there is an infinite-dimensional such that ; thus when we take the monoid of isomorphism classes and add inverses to make it a group, everything gets identified with zero. I’m never quite sure whether I’ve made my peace with that.
Regarding decategorification, I would just argue that decategorification is something that only works when your category has a set of objects. If you look at instances of decategorification, I think they nearly always operate on small categories. Large categories just don’t tend to get decategorified very much. In the classical picture this is probably partly because they would decategorify to proper classes rather than sets; here it’s because they don’t decategorify at all.
You can “decategorify to a poset” if by that you mean take the posetal reflection. But the posetal reflection of is not likely to be very interesting; for instance any set admitting a global element will be identified with . So I’m not sure if this is quite what you’re envisioning?
Anyway, I don’t see why it’s any crazier to have posets without an underlying set of objects than to have categories without an underlying groupoid of objects. Probably you’re saying that they’re both crazy, but I don’t see how pointing to one of them makes the other one seem more crazy.
Mike: One other thought, which I’ve mentioned elsewhere but which might bear repeating here: there are lots of Grothendieck 2-toposes that do not have enough groupoids, and in which many or most objects, including posetal objects, do not have cores. It suffices to consider 2-sheaves on pretty much any 2-site that is not a (2,1)-site, just like you can get non-localic 1-toposes by looking at sheaves on a site that is not a posite. The simplest example is the 2-presheaf 2-topos where is the “walking 2-cell.” An example pointed out by Street, which deserves further study, is where is the algebraic simplex category, so that an object of is a category equipped with a monad. Along the same lines there is the 2-category of adjunctions, or the 2-category of categories equipped with a reflective subcategory. I haven’t spent much time looking for interesting non-presheaf 2-toposes, but they must be out there; one obvious place to look is classifying 2-toposes of 2-geometric theories.
On the other hand, I don’t know any 2-toposes that lack cores but still have a duality involution. So that combination would be harder to justify this way.
Toby: I understand that categories from this perspective are atomic objects, and that's why you're able to dictate what can and can't be done with them. But I also would like them to match my intuitive understanding of what a category is, and that is (in part) a collection of objects and several collections of morphisms (one for each pair of objects, not a single collection of all morphisms although one can be constructed from the data at hand).
When I say that something is crazy, I don't mean that it's nonsense but that it violates my intuition of what a thing should be. And I think that you agree that lack of cores is crazy in this sense, since you said that you'd like to have them. If we disagree, it's on the relative value of cores vs a category of all sets (since size distinctions have also offended intuition at least since Frege and Russell), but I don't really intend to make a final judgement even on that.
I focused attention on posets just to make things simpler, once I realised that the issue already appeared there. I mean, if a theory of categories that needn’t have cores seems crazy, how much crazier (and how much more accessible the craziness to non-category-theorists) must be a theory of posets that needn't have underlying sets! (Of course, when taking the set of objects up to isomorphism of a category, you have to take the core before you take the posetal reflection, since the other order gives the wrong answer, as you point out with the example of . Still it's worth noticing that the posetal reflection alone is still possible in your scheme, and it does give a sort of poset of connected components.)
I don't think that I have anything new to say; I'm just explaining why I said what I said before. But thanks to this conversation, I think that I now understand what you're doing here. (And thanks for the Eilenberg swindle.)
Mike: I view intuition as potentially changeable. A lack of cores does violate my intuition of categories, but I’m entertaining the possibility that my intuition is flawed and should be changed. And since, as I said above, there are plenty of Grothendieck 2-toposes that lack cores, one doesn’t have to want a category of all sets to think it might be worthwhile trying to do without cores.
Even with a classical set-theoretic foundation, there are plenty of posets that don’t have underlying sets, as long as you don’t let the occurrence of “set” in “poset” prejudice you and remember that “poset” means “(0,1)-category.” For instance, the poset of ordinal numbers. Classically, they have underlying classes, but not underlying sets. In ZFC, at least, a proper class is not a “real” object, and thus neither are these posets. Our desire to make them real may lead us to introduce classes (or large sets) as a new sort of object; the point here is (to beat a dead horse once again) that we can introduce such posets as real objects without needing to introduce the proper classes that “underlie” them.
I’m glad this conversation was helpful; it’s been helpful to me as well. But I still want to know whether this is consistent!
Toby: Would you argue that none of the large categories that we really want in mathematical practice are groupoids? So for example, we really want the large poset of ordinal numbers (which is the same as the category of ordinal numbers if you require morphisms to preserve the inductive structure in a natural way) but not the large symmetric poset (that is, large set) of cardinal numbers (since we should just stick to the category of sets). Of course, the (essentially small) groupoid of finite sets is used, for example in the theory of structure/stuff types, but not so much the large groupoid of all sets (which has the large set of cardinal numbers as its posetal reflection).
If I knew whether a Heyting 2-pretopos with a discrete opfibration classifier can exist, I'd tell you. If you just want a duality involution without cores, I expect you can get that by starting with one of your examples above and using forcing (or 2-forcing). But I doubt that forcing can get the discrete opfibration classifier. (I actually don't know very much about forcing. I should learn.)
Mike: I would say, more conservatively, that it’s not clear to me at present that any of the large categories we really want in mathematical practice are obtained from some “more naturally occurring” large category by discarding noninvertible morphisms. There may be particular large categories that happen to be groupoids already. In fact, exactness and some infinitary structure (I think probably an exponentiable NNO is good enough, and still first-order) lets you construct the groupoid reflection of any category, even a large one. So there are large groupoids, and we might be interested in some of them (although none comes immediately to mind).
Of course, I wasn’t expecting you to tell me the answer! Forcing is certainly a possibility, although both cores and duality are “global” statements about all objects, so it’d require some thought to make it work, at least.
Toby: Perhaps we should try to find a contradiction by assuming such a -pretopos and using forcing to make one with cores. But I don't know how to do that.
Just to keep me straight: The ‘groupoid reflection’ of a category is the free groupoid on a category, formed by throwing in formal inverses to all morphisms (and generating formal products and identifying as required). While the ‘core’ of a category is the fascist (co-free) groupoid on a category, formed by keeping only the invertible morphisms. Right?
Mike: Yes. I call it the groupoid reflection because it is, of course, the left adjoint to the inclusion of groupoids in categories. The core is dually the right adjoint to that inclusion, although only at the level of 1-categories or (2,1)-categories, not 2-categories.