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.
Jacques Carette (Aug 21 2021 at 14:25):In set-based category theory, trying to fit all (small) categories into a (large) category doesn't work so well, in that you end up with the wrong equality on functors. It works 'better' to consider this as a 2-category, so that one can use natural isomorphisms as the 'correct' notion of functor equivalence.
But in E-Category theory, this is not needed!. In other words, the (large) E-category of (small) E-categories works, there is no need to go to 2-categories!
There is a different bonus in the above formalization with explicit universe polymorphism: one can see exactly how large the result ends up being. The 'diversity' of universes gets erased, and then only the object universe gets bumped up a size.
It still ends up being Cartesian closed (see Cats-CCC at the bottom of https://agda.github.io/agda-categories/Categories.Category.Instance.Properties.Cats.html) but only when all 3 universes coincide. Nevertheless "extremely large" collections of categories are still CCC.
Nathanael Arkor (Aug 21 2021 at 19:32):What do you mean by "the wrong equality on functors"?
Jacques Carette (Aug 21 2021 at 22:36):Extensional equality. Being 'exactly equal' in both components.
Mike Shulman (Aug 22 2021 at 00:00):I would argue that that's not really an analogue of Cat but rather of Ho(Cat), the category (which is a sensible 1-category even in set-based category theory) whose morphisms are natural isomorphism classes of functors.
Mike Shulman (Aug 22 2021 at 00:01):Note that Ho(Cat) is also CCC even in set-based category theory, but it fails to have other good properties like the existence of limits and colimits. I would expect the same is true for your E-category.
John Baez (Aug 22 2021 at 00:19):Oh, I was wondering what Jacques was talking about... I guessed he meant Ho(Cat).
Jacques Carette (Aug 22 2021 at 16:18):And now I have a name for it, thanks. And I'll have to investigate limits and colimits for it, it hasn't been done yet. Any pointers to the literature as to what the obstruction is likely to be?
Mike Shulman (Aug 22 2021 at 19:46):