Category of categories?

Stream: maths

[Daniel Donnelly]

For a given, finite set of categories (those declared in an instance of BananaCats), does there exist a category containing all of them, and what is its name? I'm going to have a tab where each of the categories are nodes, and you can functor between them, then check-to-include any diagrams you want to take the image of. The result is a bunch of new diagrams opened in tabs, the functorial images of the earlier diagrams.

[Kevin Buzzard]

What does it mean for a category to contain another category?

[Kevin Buzzard]

Oh -- maybe I can guess what you mean. You cannot really talk about the category of all categories, for the same reason you cannot talk about the set of all sets. You can talk about the category of all sets; similarly, you can talk about the 2-category of all categories. It is not in some sense sensible to talk about a category of categories because categories have structure (natural transformations between functors) which cannot be modelled just using the language of categories -- it's similar to taking a finite collection of sets, considering the set containing all of them, and then realising that you've just lost the ability to talk about morphisms between the sets.

[Daniel Donnelly]

@Kevin Buzzard it's more of a non-important but still useful feature to be able to view the categories and functors and nat transformations between them (drawn as an arrow between arrows in that categories tab). Should I just call it "Categories"?

It's okay that the natural transformations don't show up as categorical morphisms there, since what they'll do is when there's two functors mapping to the same place and a natural map between teh functors, then it will automatically form the commuting squares in the diagrams in the destination category, not to mention also (optionally) reflect positions of source diagrams, for ease-of-use.

[Daniel Donnelly]

It will be an artificial tab, in that it doesn't correspond to Lean statements

[Daniel Donnelly]

One use is for navigating, another use is for connecting functors (though you can do that from each diagram's context menu)

[Daniel Donnelly]

Another is for viewing what categories are defined

[Daniel Donnelly]

If C := Set, then you can optionally view it as "Set" or as "C" in that tab, you can toggle between them.

[Daniel Donnelly]

I'll call it "Categories & Functors"

[Daniel Donnelly]

which hints at it's categorical nature of objects and morphisms

[Scott Morrison]

We have src/category_theory/Cat.lean, which describes the category of (bundled) categories, with the morphisms as functors (and not mentioning natural transformations).

[Scott Morrison]

We also have src/category_theory/functor_category.lean, which, for a fixed C and D, describes the category of functors C ⥤ D and the natural transformations between them.

[Scott Morrison]

It would be perfectly reasonable to set up 2-categories in Lean; these could be closely modelled on the existing construction of monoidal categories, and then define the 2-category of categories/functors/natural transformations, but this hasn't been done yet.