Michael Shulman category of all sets

This page is quite speculative and especially welcomes contributions from readers. (A lot of its current content, especially the Knaster-Tarski theorem, is from discussions with Mathieu Dupont, who arrived at the same speculation independently.) The details require the theory developed at 2-categorical logic, but the basic idea is straightforward and poses a challenge: can you derive a contradiction from the assumption that there is a category of all sets? -Mike

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 SetSet. In either case there are now some very set-like objects (whether we call them “classes” or “large sets”) that are not objects of SetSet, 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 CatCat, which we will denote “setset“, equipped with a discrete opfibration elsetel\to set such that for any object XX of CatCat, pullback of elsetel\to set determines an equivalence

DOpf(X)Cat(X,set).DOpf(X)\simeq Cat(X,set).

We will write “SetSet“ for the full sub-2-category disc(Cat)disc(Cat) of CatCat 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 CatCat“. (The relationship between ”meta“ categories and objects of CatCat 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 SetSet from setset; the relationship is that SetCat(1,set)Set\simeq Cat(1,set), since SetDOpf(1)Set\simeq DOpf(1).

Clearly no 2-category CatCat 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 CatCat? Some potential additional hypotheses include:

  1. CatCat has exponentials.
  2. CatCat has a natural numbers object.
  3. CatCat has enough groupoids or enough discretes.
  4. CatCat has a duality involution (which may fix groupoids).
  5. CatCat is countably or infinitarily coherent (not an elementary hypothesis).
  6. CatCat is well-pointed?.
  7. CatCat is Boolean.
  8. SetSet is a topos.
  9. setset is a topos” is true in the internal logic of CatCat.

Let me pose this as a challenge to readers of this page:

  • Challenge: Find as many contradictions as you can between various combinations of these hypotheses.

Currently, combinations that are known to be contradictory (see below) include:

  • exponentials + enough groupoids
  • exponentials + duality
  • exponentials + NNO + SetSet is a topos
  • countably-coherent + SetSet is a topos

Note that having enough groupoids implies that SetSet is a topos, as do exponentials together with Booleanness, as do exponentials together with duality.

It thus appears that the strongest “live” combination is

  • exponentials + NNO + well-pointed

A plausibility argument: accessible categories

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 CC is an accessible category, then accessible fibrations over CC can be identified with accessible pseudofunctors C opCatC^{op}\to Cat. Thus, accessible discrete fibrations over CC can be identified with accessible functors C opSetC^{op}\to Set. So, with a suitable “niceness” restriction on both the categories allowed and the functors allowed, it is already possible in set theory for SetSet 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 AccAcc 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.

Categories with a set of objects

If AA is an object of CatCat (i.e. a “category”), then if XX is a discrete object of CatCat (i.e. a “set”) and XAX\to A is an eso, then it makes sense to say that XX is the (or “a”) set of objects of AA, since AA can be presented as the quotient of a 2-congruence on XX. So saying that every category has a set of objects would be essentially the same as saying that CatCat has enough discretes.

Now if setset 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 setset does not have a set of objects, i.e. does not admit any eso from a discrete object, and therefore in particular CatCat 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 SetSet.

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 setset) 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.

Making SetSet a topos

Since CatCat is a Heyting 2-pretopos with a discrete opfibration classifier, it automatically inherits a cosieve classifier, i.e. a subobject object Ωset\Omega\hookrightarrow set which classifies cosieves. Since if AA is discrete, any subobject is a cosieve, in particular we have Sub(A)Cat(A,Ω)Sub(A)\simeq Cat(A,\Omega). Thus, SetSet is almost a topos, but of course Ω\Omega will not itself be a set. But it is posetal, so its core, if it has one, will be discrete. Since a core of Ω\Omega would be its coreflection into the groupoidal objects, we would have

Cat(A,JΩ)Cat g(A,Ω)J(Sub(A))Cat(A,J\Omega) \simeq Cat_g(A,\Omega)\simeq J(Sub(A))

so that JΩJ\Omega would be a subobject classifier in SetSet. Since SetSet is cartesian closed if CatCat has exponentials, we have shown:

Theorem

If CatCat has exponentials and enough groupoids, then SetSet is a topos.

Actually, however, exponentials are unnecessary. Observe that since setset classifies discrete opfibrations, set 2set ^{\mathbf{2}} classifies maps between discrete opfibrations. We can then use the internal first-order logic to cut out a subobject monoset 2mono \hookrightarrow set ^{\mathbf{2}} that classifies monomorphisms between discrete opfibrations. Finally, if AA is discrete, we pull back the second projection monosetmono \to set along the classifying map a:1seta:1\to set of AA, to get PAP A, the object of monomorphisms into AA. The universal property of PAP A is that morphisms XPAX\to P A correspond to subobjects of X *AX^*A in DOpf(X)DOpf(X). Since if XX is discrete, subobjects of X *AX^*A in DOpf(X)DOpf(X) are the same as subobjects of X×AX\times A, PAP A is almost like a power object of AA in SetSet. Of course, it is also not discrete, but the same argument for its core shows that:

Theorem

If CatCat has enough groupoids, then SetSet is a topos.

Recall also that any cartesian closed Boolean category is a topos, since then 2=1+12=1+1 is a subobject classifier. Thus we also have:

Theorem

If CatCat is Boolean, then SetSet is a topos.

Finally, we observe that exponentials and a duality involution also suffice. Let Ω\Omega be the cosieve classifier; then Ω o\Omega^o is a sieve opclassifier, i.e. Cat(X,Ω o)Cat(X,\Omega^o) is equivalent to the opposite of the poset of sieves on XX. On Ω×Ω o\Omega\times\Omega^o we thus have both a sieve RR and a cosieve SS, pulled back from Ω\Omega and Ω o\Omega^o; let Ω d\Omega_d be the subobject of Ω×Ω o\Omega\times\Omega^o defined as RSR\Leftrightarrow S in the Heyting algebra structure. Now maps into Ω d\Omega_d classify sieves and cosieves that are equal as subobjects, which is to say, subobjects that are both sieves and cosieves. And transformations between maps XΩ dX\to \Omega_d correspond to both inclusions of cosieves and coinclusions of sieves, which is to say, identities; thus Ω d\Omega_d is discrete, and hence a subobject classifier in SetSet.

Theorem

If CatCat has exponentials and a duality involution, then SetSet is a topos.

Making setset a topos

Now, it is not immediately clear what SetSet being a topos implies about the properties of setset in the internal logic of CatCat. 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 CatCat 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 elsetel\to set and the universal discrete fibration V set(el)set oV_{set}(el)\to set^{o}, both pulled back to set o×setset^{o}\times set, we obtain a discrete opfibration over set o×setset^{o}\times set. Of course, it has a classifying map exp:set o×setsetexp:set^{o}\times set \to set; thus exponentials in SetSet are represented by a morphism in CatCat. It’s not obvious whether this implies that “setset is cartesian closed“ is true in the internal logic of CatCat, but it is true that if AA and BB are sets (discrete objects of CatCat), with classifying maps a:1set* oa:1\to set*^o and b:1setb:1\to set, then B AB^A is classified by exp(a,b):1setexp(a,b):1\to set.

Now if in addition SetSet is a topos, then taking B=JΩB=J\Omega to be its subobject classifier, we obtain a contravariant powerset functor p:set osetp:set^o\to set. The existence of a covariant powerset functor p:setsetp:set\to set is less obvious, but I believe that functor comprehension? will let us prove that if CatCat has enough groupoids, then it exists.

Limits and colimits

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 k:ABk:A\to B, the functor

(k):Cat(B,set)Cat(A,set)(-\circ k):Cat(B,set)\to Cat(A,set)

is equivalent to

k *:DOpf(B)DOpf(A),k^*:DOpf(B)\to DOpf(A),

the left adjoint Lan kLan_k to the latter gives a left adjoint to the former; but this just says that all left extensions along kk into setset exist. And the Beck-Chevalley property for Lan kLan_k 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 CatCat has an exponentiable NNO (in the same way that an ordinary Π\Pi-pretopos with an NNO can be shown to be finitely cocomplete).

Similarly, if CatCat has exponentials, then each pullback functor k *:DOpf(B)DOpf(A)k^*:DOpf(B)\to DOpf(A) has a right adjoint Ran kRan_k, and so we obtain all right extensions into setset. The dual Beck-Chevalley condition also implies pointwiseness of these extensions.

Adjoint functor theorem

It is true in any 2-category that if f:ABf:A\to B is a morphism such that if the left extension lan f1 A:BAlan_f 1_A:B\to A exists and is preserved by ff, then it is a right adjoint to ff. Since setset admits all left extensions, it follows that any morphism f:setBf:set\to B that preserves all left extensions (that is, all colimits) has a right adjoint, and dually any morphism f:setBf:set\to B 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 setset 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 AA is an object (such as setset) having all limits and BB is a subobject of AA closed under such limits, then the inclusion BAB\hookrightarrow A has a left adjoint, i.e. BB is reflective in AA. 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.”

Fixed points

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 SetSet becoming a poset in this way. However, we do have another potential problem, stemming from an otherwise lovely fact.

Theorem

If CatCat has an NNO, then for any endomorphism f:setsetf:set\to set and any object XX, the induced endofunctor F X:DOpf(X)DOpf(X)F_X:DOpf(X)\to DOpf(X) has a terminal coalgebra, and these are preserved by pullback. Therefore, “ff has a terminal coalgebra“ is true in the internal logic of CatCat.

Proof

This follows the classical proof of the Knaster-Tarski theorem for posets, see e.g. Lambek, “A fixpoint theorem for complete categories.” Let i:Iseti:I\to set be the inserter of 1,f:setset1,f:set \;\rightrightarrows\; set, with inserted 2-cell α:fii\alpha:f i \to i, and let t:1sett:1\to set with ϕ:it!\phi:i \to t ! be the left extension of IsetI\to set along !:I1!:I\to 1. We have a 2-cell τ:tft\tau:t \to f t obtained from the universal property of the Kan extension (by definition τ!.ϕ=α.fϕ\tau ! . \phi = \alpha . f\phi). Thus tt is an ff-coalgebra, so T=t *(El)T = t^*(El) is an F 1F_1-coalgebra, and ! *T=T X!^*T = T_X is an F XF_X-coalgebra for any XX, clearly preserved by pullback.

Now if CFCC\to F C is any F XF_X-coalgebra, we have γ:cfc\gamma:c \to f c where Cc *(El)C\cong c^*(El), so cc induces a map c:XIc':X \to I with αc=γ\alpha c' = \gamma. The 2-cell ϕc:ic=ct!\phi c':i c' = c \to t! then induces a map Φ C:CT X\Phi_C:C\to T_X, and the equality

fϕc.γ=fϕc.αc=(fϕ.α)c=(τ!.ϕ)c=τ!c.ϕc=τ.ϕcf\phi c'.\gamma = f\phi c' . \alpha c' = (f\phi.\alpha)c'= (\tau!.\phi)c' = \tau!c'.\phi c' = \tau.\phi c'

implies that Φ C\Phi_C is a coalgebra map. Moreover, coalgebra maps h:CDh:C\to D in DOpf(X)DOpf(X) correspond to 2-cells θ:cd\theta:c'\to d', and the interchange law for the composite ϕθ\phi \theta implies that

ϕd.iθ=t!θ.ϕc=ϕc\phi d' . i\theta = t!\theta . \phi c' = \phi c'

and thus Φ Dh=Φ C\Phi_D h = \Phi_C.

Now the equality τ!.ϕ=α.fϕ\tau ! . \phi = \alpha . f\phi means that ϕ\phi induces a 2-cell ϕ:1 It!\phi':1_I \to t'! (using the 2-dimensional universal property of II). Then the interchange law for the composite ϕϕ\phi \phi' implies that 1.ϕ=ϕt!.ϕ1.\phi = \phi t'! . \phi. But since ϕ\phi exhibits tt as a left extension, this implies ϕt=1 t\phi t' = 1_t, and therefore Φ T X=1 T X\Phi_{T_X} = 1_{T_X}. It follows that for any coalgebra map h:CT Xh:C\to T_X, we have Φ C=Φ T Xh=h\Phi_C = \Phi_{T_X} h = h; thus T XT_X is a terminal coalgebra.

Dually, using limits, we have:

Corollary

If CatCat has exponentials, then for every f:setsetf:set\to set, each F X:DOpf(X)DOpf(X)F_X:DOpf(X)\to DOpf(X) has an initial algebra, and these are preserved by pullback.

Contradictions

In general, having initial algebras and final coalgebras for endofunctors is quite useful. An NNO is itself an initial algebra for the endofunctor XX+1X\mapsto X+1. More generally, initial algebras for polynomial endofunctors (“WW-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.

Corollary

In addition to our standing hypotheses (CatCat is a Heyting 2-pretopos with a discrete opfibration classifier), it is inconsistent to assume that 1. CatCat has exponentials or is countably-coherent, and 1. There is a covariant powerset functor p:setsetp:set\to set (such as, I believe, when CatCat has enough groupoids).

Proof

By the Knaster-Tarski theorem and Lambek’s lemma, either of the first two hypotheses ensures that any covariant endofunctor of setset has a fixed point. In particular, we have a set XX which is isomorphic to its power object in SetSet. But this is impossible, since Cantor’s diagonal argument is valid in any topos.

Now suppose, instead of enough groupoids, that CatCat has exponentials and a duality involution. Then fixing any v:1Setv:1\to Set, the “exponentials” map set o×setsetset^o\times set\to set gives us a functor v ():set osetv^{(-)}:set^{o}\to set, and therefore an iterated covariant functor v v ():setsetv^{v^{(-)}}:set\to set, which once again must have a fixed point. Combining this with Theorem , we have:

Theorem

In addition to our standing hypotheses, it is inconsistent to assume that 1. CatCat has a duality involution, and 1. CatCat has exponentials.

Proof

Theorem implies that SetSet is a topos, hence has a subobject classifier Ω\Omega. Now by the above arguments and the Knaster-Tarski theorem, the endofunctor Ω Ω ()\Omega^{\Omega^{(-)}} of SetSet has a fixed point, say XX. Therefore, we have a monomorphism Ω XΩ Ω XX\Omega^X \to \Omega^{\Omega^X} \cong X (the first morphism being “singletons”). Applying contravariant Ω ()\Omega^{(-)} again, which turns monics into epics, we have an epimorphism Ω XΩ Ω X\Omega^X \to \Omega^{\Omega^X}. Now Cantor’s diagonal argument applies again.

There can be particular objects VV in a locally cartesian closed category (or even a topos) such that V V ()V^{V^{(-)}} has a fixed point. For instance, this is certainly the case if VV is a model of the untyped lambda calculus with VV VV\cong V^V, and these are known to exist in some toposes. Moreover, there are cartesian closed categories of domains in which the equation XV V XX\cong V^{V^{X}} has a solution for any VV. This doesn’t answer the question of whether it is consistent for V V ()V^{V^{(-)}} to have a fixed point for every VV 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 CatCat, and hence SetSet, is Boolean, and that SetSet is a topos (as is the case if we also have exponentials). Let gragra denote the category of sets equipped with a binary relation \neq, and let set injset_{inj} denote the full subcategory of gragra determined by those (A,)(A,\neq) such that ab¬(a=b)a\neq b \Leftrightarrow \neg(a=b) for all a,bAa,b\in A. Booleanness tells us that set injset_{inj} is, in fact, the category of “sets and injective functions.” Now, if we have a comprehensive factorization, then the forgetful functor set injsetset_{inj}\to set has a colimit; call it XX. The usual arguments show that since set injset_{inj} is a filtered diagram of injections, each object in the diagram injects into the colimit XX. Therefore, every set injects into XX, including PXP X. Applying the contravariant power set functor of SetSet to the injection PXXP X \to X, we obtain a surjection PXPPXP X \to P P X, contradicting Cantor’s theorem.

In fact, however, Booleanness is unnecessary. If we perform the above construction in the non-Boolean case, then the category set ¬¬injset_{\neg\neg inj} we obtain is the category of sets and “¬¬\neg\neg-injective functions,” i.e. functions f:ABf:A\to B such that if f(a)=f(a)f(a)=f(a') then ¬¬(a=a)\neg\neg(a=a'). If XX is again the colimit of set ¬¬injsetset_{\neg\neg inj}\to set, then every object in the colimit ¬¬\neg\neg-injects into XX, and in particular so does PXP X. Now just as an injection PXXP X\to X gives us a surjection PXPPXP X \to P P X, a ¬¬\neg\neg-injection PXXP X \to X gives us a surjection PXP ¬¬PXP X \to P_{\neg\neg} P X, where P ¬¬AP_{\neg\neg} A is the object of ¬¬\neg\neg-closed subsets of AA. But the Cantor diagonal set is defined by a negative property ¬(xf(x))\neg(x\in f(x)), hence is ¬¬\neg\neg-closed, so again we have a contradiction.

Theorem

In addition to our standing hypotheses, it is inconsistent to assume that 1. CatCat has an exponentiable NNO or is countably-coherent, and 1. SetSet is a topos.

Proof

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.

The Burali-Forti Paradox

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 pospos that classifies all “posetal opfibrations.”

Define a wellfounded poset to be a poset AA equipped with an additional binary relation \prec such that

  1. If xyzwx\le y \prec z \le w then xwx\prec w, and
  2. there does not exist an infinite descending chain x 3x 2x 1\dots \prec x_3\prec x_2\prec x_1.

This isn’t the “correct” constructive definition of “wellfounded,” but it’ll be enough to get a contradiction.

Let WFWF 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 pos pos^{\rightrightarrows}. (We need an exponentiable NNO to be able to quantify over infinite sequences.) Then a morphism in WFWF between two wellfounded posets AA and BB is a map f:ABf:A\to B of posets which preserves \prec, i.e. if a 1a 2a_1\prec a_2 then f(a 1)f(a 2)f(a_1)\prec f(a_2). Let WW be the posetal reflection of WFWF; thus we have ABA\le B in WW iff there exists an f:ABf:A\to B preserving both \le and \prec.

Now define a relation \prec on WW by setting ABA\prec B if there exists an f:ABf:A\to B in WFWF such that there is a bBb\in B with f(a)bf(a)\prec b for all aAa\in A. We claim that WW with this relation is wellfounded. Clearly if ABCDA\le B\prec C\le D, then ADA\prec D. And if we have

A 3A 2A 1\dots\prec A_3 \prec A_2\prec A_1

then we have functions f n:A nA n1f_n:A_n\to A_{n-1} and elements a nA na_n\in A_n such that f n(x)a n1f_n(x)\prec a_{n-1} for all nn. Thus, we have

f 2(f 3(a 3))f 2(a 2)a 1\dots \prec f_2(f_3(a_3)) \prec f_2(a_2)\prec a_1

contradicting wellfoundedness of A 1A_1. Therefore, WW with \prec is itself a wellfounded poset.

Now, for any wellfounded poset AA and any aAa\in A, we have a wellfounded poset (Aa)={xA|xa}(A\downarrow a) = \{x\in A | x\prec a\}. If a 1a 2a_1\le a_2, then of course (Aa 1)(Aa 2)(A\downarrow a_1)\subseteq (A\downarrow a_2) and so (Aa 1)(Aa 2)(A\downarrow a_1)\le (A\downarrow a_2) in WW. And if a 1a 2a_1\prec a_2, then a 1(Aa 2)a_1\in (A\downarrow a_2) and is a bound for the inclusion (Aa 1)(Aa 2)(A\downarrow a_1)\hookrightarrow (A\downarrow a_2), so that in this case (Aa 1)(Aa 2)(A\downarrow a_1)\prec (A\downarrow a_2) in WW. Therefore, a(Aa)a\mapsto (A\downarrow a) is a function AWA\to W in WFWF, so AWA\le W in WW. (We are tacitly identifying wellfounded posets with their classifying maps 1W1\to W.) Moreover, the inclusion (Aa)A(A\downarrow a)\hookrightarrow A is bounded by aAa\in A, so we have (Aa)A(A\downarrow a)\prec A in WW. Thus AWA\in W is a bound for the function a(Aa)a\mapsto (A\downarrow a) from AA to WW, so we have AWA\prec W in WW. Finally, taking A=WA=W we obtain WWW\prec W, contradicting the wellfoundedness of WW.

Theorem

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 \prec to be wellfounded if

  1. If xyzwx\le y \prec z \le w then xwx\prec w, and
  2. For any sieve RAR\subset A, if xRx\in R for all xax\prec a implies aRa\in R, then R=AR=A.

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” WFWF as a full subobject of pos pos^{\rightrightarrows}, 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 RAR\subset A is any subobject, define R={aA|xaxR}R'=\{a\in A | x\le a \Rightarrow x\in R\}; then RR' is a sieve. It is easy to check that if RR is “inductive” in the above sense, then so is RR' (using the assumption that yzwy\prec z\le w implies ywy\prec w); hence R=AR'=A, and since RRR'\subset R, we have R=AR=A. In particular, we can now use the classical argument to show that \prec is irreflexive: xxx\nprec x for all xAx\in A.

We now repeat the same argument; the only point of difference is the proof that the posetal reflection WW of WFWF is wellfounded in our new sense. So let RWR\subset W be a sieve of wellfounded posets with the property that if BRB\in R for all BAB\prec A, then ARA\in R. For any wellfounded AA, define R A={aA|(Aa)R}R_A = \{a\in A | (A\downarrow a)\in R\}. Since RR is a sieve, R AR_A is a sieve. Suppose that aAa\in A and xR Ax\in R_A for all xax\prec a. Then (Ax)R(A\downarrow x)\in R for all such xx. Then for any wellfounded BB such that B(Aa)B\prec (A\downarrow a), there is a function f:B(Aa)f:B\to (A\downarrow a) bounded by some x(Aa)x\in (A\downarrow a). But then (Ax)R(A\downarrow x)\in R by assumption, and so BRB\in R since RR is a sieve. Thus, by the assumption on RR, we have (Aa)R(A\downarrow a)\in R and thus aR Aa\in R_A. Thus, since AA is wellfounded, we have R A=AR_A=A. But now, if BB is any wellfounded poset such that BAB\prec A, we have f:BAf:B\to A bounded by some aAa\in A, whence (Aa)R(A\downarrow a)\in R (since aR Aa\in R_A) and so BRB\in R since RR is a sieve. Thus, again by assumption on RR, we have ARA\in R. Therefore, every wellfounded poset is in RR, so R=WR=W; hence WW is wellfounded.

Thus we have:

Theorem

It is inconsistent to assume the existence of a Heyting (2,3)-pretopos with exponentials, a duality involution, and a posetal-opfibration classifier.

Discussion

Mike, you've thought about these matters more deeply than I have, so just a few global comments: 1. I agree that we don't really want a category to have an underlying set of actual objects, and I agree that small categories can have a notion of equality of objects that categories in general lack. 2. But I would like a category to have an underlying set of equivalence classes of objects, produced by keeping only invertible morphisms and identifying parallel such. Does this have to do with having enough groupoids? 3. Perhaps we should try to define directly the poset of well-founded posets (rather than of sets equipped with a well-founded order relation) to produce the Burali-Forti paradox.

—Toby

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 \prec, then impose the extensionality condition that

t:txty\forall t: t \prec x \Rightarrow t \prec y

implies that xyx \leq y, rather than that

t:txty\forall t: t \prec x \Leftrightarrow t \prec y

implies that x=yx = y 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 abcda \leq b \prec c \leq d implies that ada \prec d, 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 nn-topos containing an (n1)(n-1)-category of all (n2)(n-2)-categories is likely to become impossible at n=(2,3)n=(2,3), 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 n=(1,2)n=(1,2) (PosPos itself is such), this leaves the case n=2n=2 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 SetSet 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 SetSet. 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 \infty-categories.

Mike: Just because you have a notion of equality between XXs doesn’t necessarily mean that you have a set of XXs, or a small category whose objects are XXs. 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 XXs, all you can say is that if there is a category of XXs, 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 KK-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 XXs, all you can say is that if there is a category of XXs, then it is small’: But this notion of equality exists for any category XX; the notion is isomorphism, defining a set |X||X|. It actually does not follow that the category XX is small, because one needs the axiom of choice to define the eso from |X||X| to XX (even as an anafunctor), so it's not like |X||X| is a set of objects of XX. But it is the set of isomorphism classes of objects of XX or (which is how I prefer to think of it) the set of objects of XX up to isomorphism.

I know, you can't actually form |X||X| in the language available here, so there's no contradiction, but I still feel that |X||X| ought to be as legitimate as XX.

I don't know enough about KK-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 KK-theory, and an nn-tuply monoidal poset (rather than an nn-tuply groupal set) as π n\pi_n at a given object of an \infty-category (and in particular a pointed poset rather than a pointed set as π 0\pi_0). Then you're saying that a poset need not have an underlying set! Just calling it ‘(0,1)(0,1)-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 XX is equal to every other XX. 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, KK-theory actually becomes trivial if you allow infinite-dimensional spaces, because of the Eilenberg swindle. For any projective MM there is an infinite-dimensional FF such that MFFM\oplus F \cong F; 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 setset is not likely to be very interesting; for instance any set admitting a global element will be identified with 11. 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 [C,Cat][C,Cat] where CC is the “walking 2-cell.” An example pointed out by Street, which deserves further study, is [BΔ,Cat][B\Delta,Cat] where Δ\Delta is the algebraic simplex category, so that an object of [BΔ,Cat][B\Delta,Cat] 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 set\set. 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 22-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.

Last revised on June 12, 2012 at 11:10:00. See the history of this page for a list of all contributions to it.