Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: this category "is an object of itself"!

Tim Campion (Jul 20 2022 at 20:46):

I just noticed something which is really messing with my head. Let $\infty = (\infty,1) =$.

Let $\kappa \geq \omega$ be a regular cardinal. Let $Pr^L_\kappa$ denote the $\infty$-category of locally $\kappa$-presentable $\infty$-categories and left adjoint functors which preserve $\kappa$-presentable objects. Note that there is an adjoint equivalence $Ind_\kappa : Rex^{idem}_\kappa {}^\to_\leftarrow Pr^L_\kappa : (-)_\kappa$, where $Rex^{idem}_\kappa$ is the $\infty$-category of small $\infty$-categories with $\kappa$-small colimits and split idempotents (this last proviso is automatic when $\kappa > \omega$). Here $Ind_\kappa$ is what you think, and $(-)_\kappa$ takes the full subcategory of $\kappa$-presentable objects.

¡¡Observation!!: $Pr^L_\kappa$ is itself locally $\kappa$-presentable.

That is, we have $Pr^L_\kappa \in Pr^L_\kappa$ -- "a category that eats itself"!

Proof: It's equivalent to show that $Rex_\kappa^{idem}$ is locally $\kappa$-presentable. For this, observe that the forgetful functor $Rex_\kappa^{idem} \to Cat$ is monadic (with left adjoint $(Psh(-))_\kappa$), and preserves $\kappa$-filtered colimits (you can deduce this from the observation that the walking idempotent $Idem$, along with every $\kappa$-small $\infty$-category, is $\kappa$-presentable in $Cat$). Since $Cat$ is locally $\kappa$-presentable and $Rex_\kappa^{idem}$ is the algebras for a $\kappa$-accessible monad thereon, the latter is also locally $\kappa$-presentable.

Tim Campion (Jul 20 2022 at 20:47):

It's so unusual for me to think about a "category which appears as an object of itself" that I'm still pondering whether the simple argument above is mistaken...

Tim Campion (Jul 20 2022 at 20:52):

I think it's correct, though. Assuming this, the next thing to ponder is whether there is a category-theoretic sense in which "$Pr^L_\kappa$ is an object of itself". Something more "intrinsic" than saying "$Pr^L_\kappa$ lies in the image of the forgetful functor $Pr^L_\kappa \to CAT$".

Tim Campion (Jul 20 2022 at 20:53):

And most of all -- how does the relation $Pr^L_\kappa \in Pr^L_\kappa$ avoid leading to Russell-type paradoxes?

Tim Campion (Jul 20 2022 at 21:06):

This would all work just as well with locally presentable $(1,1)$-categories, except for the fact that the collection thereof really needs to be a $(2,1)$-category.

Tim Campion (Jul 20 2022 at 21:15):

Tim Campion said:

... Since $Cat$ is locally $\kappa$-presentable and $Rex_\kappa^{idem}$ is the algebras for a $\kappa$-accessible monad thereon, the latter is also locally $\kappa$-presentable....

I'm a bit paranoid now -- although the nlab page indicates that taking EM categories preserves accessibility ranks, the citation is to 2.78 of Adamek-Rosicky, which only says that the EM category of an accessible monad is accessible, without commenting on the preservation of accessibility ranks. But I think the nlab is correct under the stated assumption of local presentability -- if $T$ is a $\kappa$-accessible monad on a $\kappa$ - accessible category $C$, then I believe that $Alg T$ is densely generated by the free algebras on $\kappa$-presentable objects of $C$, and these objects are definitely $\kappa$-presentable. This doesn't immediately imply that $Alg T$ is $\kappa$-accessible, but if we assume that $C$ is locally $\kappa$-presentable and not just $\kappa$-accessible, then $Alg T$ is also cocomplete, so we can deduce that it's locally $\kappa$-presentable by the criterion of Gabriel and Ulmer (Thm 1.20 in Adamek-Rosicky), i.e. we see that $Alg T$ is cocomplete with a strong generator of $\kappa$-presentable objects.

Tim Campion (Jul 20 2022 at 21:17):

(Strictly speaking this might not all be in the literature in the $\infty$-setting, but it should at least be expected there.)

Naso (Jul 21 2022 at 02:28):

The technical details of this are way beyond me, but instinctively the idea that things can be parts of themselves is pretty natural: fractals are everywhere in nature. So this seems like someething which should be possible and useful. is this construction related to non-wellfounded sets?

Tobias Schmude (Jul 21 2022 at 06:24):

I'll have to trust you on the accessibility part, but how does this avoid running into the same size issues as the usual $\mathrm{Cat} \in \mathrm{Cat}$?

Tobias Schmude (Jul 21 2022 at 06:26):

naso evangelou-oost said:

The technical details of this are way beyond me, but instinctively the idea that things can be parts of themselves is pretty natural: fractals are everywhere in nature.

Isn't that more about containing isomorphic copies of itself? That's of course completely unproblematic, but as far as I understand that's not what's happening here.

Zhen Lin Low (Jul 21 2022 at 09:36):

The relationship between the accessibility rank of a monad and the accessibility rank of the category of algebras is a little bit fiddly. You might want to look at theorem 2.18 in my model categories paper: http://www.tac.mta.ca/tac/volumes/31/2/31-02abs.html

Zhen Lin Low (Jul 21 2022 at 09:43):

As you have observed, the key to this phenomenon is Gabriel–Ulmer duality. I don't think there's anything surprising or paradoxical if you stick to the small categories picture. But I do object somewhat to the notion that the correct notion of morphism of locally $\kappa$-presentable categories is a left adjoint functor that preserves $\kappa$-presentable objects – this seems unnatural, though it does amount to taking the opposite of the category where the morphisms are $\kappa$-accessible right adjoint functors...

Steve Awodey (Jul 21 2022 at 13:49):

Not every condition of the form ``let $C$ be the category of all ...'' determines a well-defined category. In this case, the condition:
Tim Campion said:

Let $\kappa \geq \omega$ be a regular cardinal. Let $Pr^L_\kappa$ denote the $\infty$-category of locally $\kappa$-presentable $\infty$-categories...

needs a qualifier - like ``small'' - else you run into the problem that you have observed. The elaborate structure in this example is a red herring though, the category of categories with finite products has finite products, etc. :smile:

Tim Campion (Jul 21 2022 at 15:57):

Steve Awodey said:

Not every condition of the form ``let $C$ be the category of all ...'' determines a well-defined category. In this case, the condition:
Tim Campion said:

Let $\kappa \geq \omega$ be a regular cardinal. Let $Pr^L_\kappa$ denote the $\infty$-category of locally $\kappa$-presentable $\infty$-categories...

needs a qualifier - like ``small'' - else you run into the problem that you have observed. The elaborate structure in this example is a red herring though, the category of categories with finite products has finite products, etc. :smile:

I'm not sure I understand the point about size. The category of small categories with finite products _does_ have finite products, but it is not a small category, so it is not an object of itself. The category of locally small categories with finite products has finite products, but it is not locally small, so it is not an object of itself.

But in the case I'm discussing, the "smallness" condition is precisely the local $\kappa$-presentability condition. So the striking thing is that $Pr^L_\kappa$ is a category of _all_ categories-with-smallness-condition, but $Pr^L_\kappa$ itself satisfies the _same_ smallness condition as its objects!

So it seems to me that from the perspective of smallness, there is something genuinely surprising going on here which doesn't show up in things like "categories with finite products".

Tim Campion (Jul 21 2022 at 16:07):

Zhen Lin Low said:

As you have observed, the key to this phenomenon is Gabriel–Ulmer duality. I don't think there's anything surprising or paradoxical if you stick to the small categories picture. But I do object somewhat to the notion that the correct notion of morphism of locally $\kappa$-presentable categories is a left adjoint functor that preserves $\kappa$-presentable objects – this seems unnatural, though it does amount to taking the opposite of the category where the morphisms are $\kappa$-accessible right adjoint functors...

In the past I have in some sense agreed with this -- I have generally assumed that $Pr^L_\kappa$ is never really the category I want to understand or think about, but only something which is introduced as a technical tool to understand more "intrinsically interesting" categories like $Pr^L$ (the category of all locally presentable categories and all left adjoint functors).

Of course, the notion of the "right" morphisms to consider is only truly justified by what you can do with them.

But maybe I'll push back from a purely conceptual perspective -- I think there's a case to be made that when considering the collection of locally $\kappa$-presentable categories as such, it _is_ very natural to restrict the morphisms to be left adjoints which preserve $\kappa$-compact objects. I can think of several reasons (perhaps not wholly independent from one another):

1. At a very basic level, when restricting the objects of $Pr^L$ to be the objects of $Pr^L_\kappa$, it seems very natural to also restrict the morphisms. One indication of this is that the full subcategory of $Pr^L$ on the objects of $Pr^L_\kappa$ has an essentially small set of objects, but is not even locally essentially small! When was the last time you thought about a non-locally-small category with a small set of objects?

2. As you say, this condition is equivalent to requiring the right adjoints to be $\kappa$-accessible. So to the extent that it's natural to consider the category $Acc_\kappa$ of $\kappa$-accessible categories and $\kappa$-accessible functors, it's also natural to consider $Pr^L_\kappa$. For instance, the morphisms of $Pr^L_\kappa$ are precisely the morphisms in the ambient 2-category $Acc_\kappa$ which have right adjoints in $Acc_\kappa$.

3. $Pr^L_\kappa$ is a very nice category -- as I've mentioned, it's complete and cocomplete, monadic over $Cat$, even locally $\kappa$-presentable. The full subcategory of $Pr^L$ on the same objects has none of these properties.

Tim Campion (Jul 21 2022 at 16:08):

Tobias Schmude said:

I'll have to trust you on the accessibility part, but how does this avoid running into the same size issues as the usual $\mathrm{Cat} \in \mathrm{Cat}$?

That's what I'd like to know!

Taichi Uemura (Jul 21 2022 at 19:02):

Tim Campion said:

I think it's correct, though. Assuming this, the next thing to ponder is whether there is a category-theoretic sense in which "$Pr^L_\kappa$ is an object of itself". Something more "intrinsic" than saying "$Pr^L_\kappa$ lies in the image of the forgetful functor $Pr^L_\kappa \to CAT$".

Maybe one could say that $Pr^L_\kappa$ is a model of some type theory satisfying type-in-type.

Morgan Rogers (he/him) (Jul 21 2022 at 19:32):

The analogue of Russell's paradox would only arise if the "subcategory of $\kappa$-presentable categories which do not contain themselves" is also $\kappa$-presentable, and I would bet that it isn't.

Leopold Schlicht (Jul 21 2022 at 19:37):

I think the problem disappears if you specify precisely from which universe the objects of $Pr^L_\kappa$ are drawn. $Pr^L_\kappa$ itself should live in a higher universe, so it can't be an element of itself, although it is equivalent, as a category, to an object of itself.

Tim Campion (Jul 21 2022 at 20:18):

Leopold Schlicht said:

I think the problem disappears if you specify precisely from which universe the objects of $Pr^L_\kappa$ are drawn. $Pr^L_\kappa$ itself should live in a higher universe, so it can't be an element of itself, although it is equivalent, as a category, to an object of itself.

I suppose you could do that if you view this as a problem. But to me, what's interesting is that it's something which looks like it should be a problem but... apparently it is not a problem! (i.e. there is no contradiction here)

Tim Campion (Jul 21 2022 at 20:28):

Leopold Schlicht Oh, I think I see what you mean now -- you're saying that this story actually would be a problem if the object - set of $Pr^L_\kappa$ were literally an element of (a tuple packaging it with its morphisms and composition to form a category, which is an element of) the object set of $Pr^L_\kappa$. You're pointing out that this is not literally the case... which is an important point!

Tim Campion (Jul 21 2022 at 20:58):

The precise reason why will be sensitive to how things are formalized. But if we work in ZFC with one universe $V_\lambda$, and if we define the object-set of $Pr^L_\kappa$ to comprise certain categories whose object sets are subsets of $V_\lambda$, and if we encode categories as certain 4-tuples of sets (objects, morphisms, composition, identities), and if we just assume that 4-tuples are part of our basic language rather than worrying about how Kuratowski ordered pairs work, then the elements of $Pr^L_\kappa$ are certain elements of $$V_{\lambda+1}$, and $Pr^L_\kappa$ is an element of $V_{\lambda+2}$. And some (in fact most) of its elements are too big to live in $V_\lambda$, so they are properly in $V_{\lambda+1}$, so $Pr^L_\kappa$ is properly in $V_{\lambda+2}$. So it's not an element of itself.

We might alternatively think about whether $(Rex^{idem}_\kappa)_\kappa$ is an element of $(Rex^{idem}_\kappa)_\kappa$, where the objects of $Rex^{idem}_\kappa$ are certain elements of $V_\lambda$. The answer is no for size reasons -- $(Rex^{idem}_\kappa)_\kappa$ is essentially small, but not literally small, so it doesn't live in $V_\lambda$.

But what if we impose some skeletality condition? For instance, define $\widetilde{Rex}_\kappa^{idem}$ to comprise those objects of $Rex_\kappa^{idem}$ whose von Neumann rank is minimal in their equivalence class. Then... well, $(\widetilde{Rex}_\kappa^{idem})_\kappa$ is again large even though it's essentially small, so again it is trivially not an element of itself.

Tim Campion (Jul 21 2022 at 21:08):

It should be that $Pr^L_\kappa$, although an object of itself, is not a $\kappa$-presentable object of itself. So the left adjoint functor $\langle Pr^L_\kappa \rangle : Spaces \to Pr^L_\kappa$, which carries $\ast \in Spaces$ to $Pr^L_\kappa \in Pr^L_\kappa$, is not a morphism in $Pr^L_\kappa$. I think this fact ought to be relevant to various paradox-evasion maneuvers.

Mike Shulman (Jul 22 2022 at 06:15):

I would describe the situation as: there is a large category $P$ and a functor $I : P\to \rm CAT$ (where $\rm CAT$ is the very-large category of large categories) that contains $P$ in its essential image. As has been pointed out, the objects of $P = \rm Rex^{idem}_\kappa$ are not actually themselves large categories, they are "presentations" of large categories by the functor $I = \rm Ind_\kappa$. So there's nothing paradoxical about the fact that $P$ itself might be presented by one of the presentations that it contains.

Here's a simpler version of the same phenomenon, requiring nothing so fancy or higher-categorical: let $P=\rm Set$ and let $I(X) = {\rm Set}^X$. Then $I(1) \simeq {\rm Set} = P$, so in this sense $\rm Set$ also "contains itself" if we "identify" a set $X$ with the corresponding power ${\rm Set}^X$.

More generally, any category $P$ with a terminal object "contains itself" via the functor $I:P\to \rm CAT$ defined by $I(x) = P/x$, since $P\simeq P/1$.

Morgan Rogers (he/him) (Jul 22 2022 at 13:29):

Mike Shulman said:

As has been pointed out, the objects of $P = \rm Rex^{idem}_\kappa$ are not actually themselves large categories, they are "presentations" of large categories by the functor $I = \rm Ind_\kappa$. So there's nothing paradoxical about the fact that $P$ itself might be presented by one of the presentations that it contains.

I feel this is dismissing the curiousness of the set-up. If we had a general way to build Ind-functors on $\kappa$-presentable categories (so to view the objects of a generic such category as themselves being $\kappa$-presentable categories) we could nail down Russell's paradox and get a genuinely interesting result for free. Your last example might provide some insight into what that might look like: the category of small categories without a terminal object cannot be a small category, or else we could ask whether the slice pseudo-functor contains that category in its essential image. (This is easy to argue by other means, by constructing a class of them, but hopefully it illustrates the point.)

Nathanael Arkor (Jul 22 2022 at 13:44):

From a categorical logic perspective, a locally finitely presentable category is precisely the category of models of an essentially algebraic theory. That the category of locally finitely presentable categories is locally finitely presentable means that locally finitely presentable categories are essentially algebraic, which is really just an observation about the expressivity of essentially algebraic theories, and in that sense should be expected for any sufficiently expressive notion of logic, since with enough expressivity, you ought to be able to describe any kind of structure: in particular, the one that axiomatises the structure of categories of models of that kind of theory.

Mike Shulman (Jul 22 2022 at 14:22):

Yes, I am dismissing the curiousness of the setup, becuase I don't feel it is curious. I think those who think it is curious are being misled by the apparent "canonicalness" of the equivalence $\rm Rex^{idem}_\kappa \simeq Pr^L_\kappa$, when in fact nothing very strange is going on.

John Baez (Jul 22 2022 at 14:57):

A less fancy example of that phenomenon is that there's a multisorted Lawvere theory whose algebras are multisorted Lawvere theories.

John Baez (Jul 22 2022 at 14:59):

We need "multisorted" here because there's not an ordinary ("1-sorted") Lawvere theory for ordinary Lawvere theories. But there's a multisorted Lawvere theory for ordinary Lawvere theories. So if we're looking for a kind of fixed point - a kind of theory that can describe itself - that's powerful enough to describe Lawvere theories, it's natural to go up to multisorted Lawvere theories.

John Baez (Jul 22 2022 at 15:02):

An even more stripped-down example is that there's a colored operad for colored operads.

Nathanael Arkor (Jul 22 2022 at 15:55):

John Baez said:

A less fancy example of that phenomenon is that there's a multisorted Lawvere theory whose algebras are multisorted Lawvere theories.

This isn't quite an example (though the principle is similar). For every set $S$, there is a set $S' \not\cong S$ and an $S'$-sorted algebraic theory whose algebras are $S$-sorted algebraic theories. However, the category of all multisorted algebraic theories (where $S$ is not fixed) is not the category of models for an algebraic theory (multisorted or otherwise), nor is the category of locally strongly finitely presentable categories. So the situation is not quite the same as the essentially algebraic setting, where we really do recover the entire category, without fixing the sorts.

John Baez (Jul 22 2022 at 16:01):

Okay, it's different. Yes, in my both my examples there's an $S'$-sorted theory whose algebras are $S$-sorted theories, where $S'$ is obtained by applying some functor to the set $S$.

Morgan Rogers (he/him) (Jul 22 2022 at 17:16):

Nathanael Arkor said:

From a categorical logic perspective, a locally finitely presentable category is precisely the category of models of an essentially algebraic theory. That the category of locally finitely presentable categories is locally finitely presentable means that locally finitely presentable categories are essentially algebraic, which is really just an observation about the expressivity of essentially algebraic theories, and in that sense should be expected for any sufficiently expressive notion of logic, since with enough expressivity, you ought to be able to describe any kind of structure: in particular, the one that axiomatises the structure of categories of models of that kind of theory.

Isn't this exactly the kind of loop that Gödel exploited to get his incompleteness theorem? You and @Mike Shulman might have enough intuition about the area that this seems unsurprising, but that doesn't preclude the possibility of exploiting this perspective.

Evan Patterson (Jul 22 2022 at 18:51):

I've wondered about that before myself. It's a neat fact that "essentially algebraic theories are essentially algebraic" (for example, a category with chosen finite limits can be axiomatized as a generally algebraic theory or a essentially algebraic theory). But does that have any proof-theoretical implications?

Tim Campion (Jul 22 2022 at 19:04):

Taichi Uemura said:

Tim Campion said:

I think it's correct, though. Assuming this, the next thing to ponder is whether there is a category-theoretic sense in which "$Pr^L_\kappa$ is an object of itself". Something more "intrinsic" than saying "$Pr^L_\kappa$ lies in the image of the forgetful functor $Pr^L_\kappa \to CAT$".

Maybe one could say that $Pr^L_\kappa$ is a model of some type theory satisfying type-in-type.

I like this idea!

If you could interpret type theory in $Pr^L_\kappa$, so that an object of $Pr^L_\kappa$ is a type in your type theory, and if you moreover interpret a term of type $\mathcal K$ to mean an object of $\mathcal K$, then it seems plausible that you could arrange to have the judgment $\vdash U : U$ be valid in your type theory, where $U$ is the type corresponding to $Pr^L_\kappa$ itself. So I wonder:

1. How much type theory can be interpreted in $Pr^L_\kappa$?

It will probably have to be some kind of linear type theory.

2. Same as (1), but additionally requiring that a term correspond to an object.

3. Can such a type theory be set up with $\vdash U : U$ being valid?

4. In general, what kinds of limitations on a type theory validating $\vdash U : U$ are there?

Ulrik Buchholtz (Jul 29 2022 at 14:28):

Tim Campion said:

3. Can such a type theory be set up with $\vdash U : U$ being valid?

I don't know about $\mathrm{Pr}^L_\kappa$, but here's a different example of such a type theory: Consider MLTT without universes and with the induction scheme for $\mathbb{N}$ (the only recursive inductive type) restricted to first-order motives. It's known that all functions $f: \mathbb{N} \to \mathbb{N}$ in this system are primitive recursive. Now add a universe $(U,T)$, where $U$ is interpreted as the natural numbers, and $T(e):=W_e := \mathrm{dom}(\phi_e)$, the $e$-th recursively enumerable set. This universe is closed under all the type formers of the theory except $\Pi$-types, indeed with codes given by primitive recursive operations, and we obviously have a code for $U$ in $U$ as well, e.g., by picking the same code as for $\mathbb{N}$.

4. In general, what kinds of limitations on a type theory validating $\vdash U : U$ are there?

From Girard's paradox, you can't have this if $U$ is closed under $\Pi$-types and you have contraction, i.e., you allow non-linear uses of variables. So there are two options: Disallow $\Pi$-types as above, or move to a linear or affine logic.

Sam Speight (Jul 29 2022 at 15:29):

Maybe goes without saying, but you could retain dependent functions and non-linear logic and accept that all types are inhabited (Girard's paradox). Which is a certain kind of inconsistency ("logical inconsistency"), but does not imply that all terms collapse (are judgementally equal, "equational inconsistency"). Right?

Ulrik Buchholtz (Jul 29 2022 at 15:41):

I think that's right, and that's a good point.

Mike Shulman (Jul 29 2022 at 21:47):

I think you can say even a bit more than that. It's true that all types will be inhabited, but not all types will be inhabited by a normal form. So you can recover a sort of logical consistency if you insist that only normal (or normalizing) terms count as proofs. Now the price you pay is giving up cut / modus ponens: you can have normal terms $a : A$ and $f : A\to B$ for which $f a : B$ doesn't normalize. (In fact I think you get a sort of "paraconsistent logic", with "dialetheias" $D$ such that $D$ and $\neg D$ are both provable, but can't be combined into a normal proof of $\bot$.)

One of these days I want to explore this idea more deeply. I think there are some philosophers who've thought about a similar approach to sequent calculus under the heading of "proof-theoretic semantics", but I don't think I've seen it considered in type theory (has anyone?).

Steve Awodey (Jul 30 2022 at 11:25):

Mike Shulman said:

One of these days I want to explore this idea more deeply. I think there are some philosophers who've thought about a similar approach to sequent calculus under the heading of "proof-theoretic semantics", but I don't think I've seen it considered in type theory (has anyone?).

Thierry once told me that he had looked into this as a way of using the original system with type:type. He said it was Per's idea. So, yes.

Mike Shulman (Jul 30 2022 at 16:12):

Cool! Thanks, I'll ask him about it sometime.

Tim Campion (Aug 08 2022 at 22:46):

Ulrik Buchholtz said:

Tim Campion said:

3. Can such a type theory be set up with $\vdash U : U$ being valid?

I don't know about $\mathrm{Pr}^L_\kappa$, but here's a different example of such a type theory: Consider MLTT without universes and with the induction scheme for $\mathbb{N}$ (the only recursive inductive type) restricted to first-order motives. It's known that all functions $f: \mathbb{N} \to \mathbb{N}$ in this system are primitive recursive. Now add a universe $(U,T)$, where $U$ is interpreted as the natural numbers, and $T(e):=W_e := \mathrm{dom}(\phi_e)$, the $e$-th recursively enumerable set. This universe is closed under all the type formers of the theory except $\Pi$-types, indeed with codes given by primitive recursive operations, and we obviously have a code for $U$ in $U$ as well, e.g., by picking the same code as for $\mathbb{N}$.

4. In general, what kinds of limitations on a type theory validating $\vdash U : U$ are there?

From Girard's paradox, you can't have this if $U$ is closed under $\Pi$-types and you have contraction, i.e., you allow non-linear uses of variables. So there are two options: Disallow $\Pi$-types as above, or move to a linear or affine logic.

Ah, that's promising! I would expect any type theory modeled by $Pr^L_\kappa$ to be "linear" in nature anyway. So maybe Girard's paradox can be avoided.