## Stream: maths

### Topic: Category of categories?

#### Daniel Donnelly (Aug 28 2019 at 17:01):

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 (Aug 28 2019 at 17:04):

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

#### Kevin Buzzard (Aug 28 2019 at 17:08):

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 (Aug 28 2019 at 17:21):

@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 (Aug 28 2019 at 17:22):

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

#### Daniel Donnelly (Aug 28 2019 at 17:23):

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

#### Daniel Donnelly (Aug 28 2019 at 17:24):

Another is for viewing what categories are defined

#### Daniel Donnelly (Aug 28 2019 at 17:25):

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

#### Daniel Donnelly (Aug 28 2019 at 17:27):

I'll call it "Categories & Functors"

#### Daniel Donnelly (Aug 28 2019 at 17:27):

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

#### Scott Morrison (Aug 28 2019 at 23:39):

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 (Aug 28 2019 at 23:40):

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 (Aug 28 2019 at 23:41):

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.

Last updated: May 10 2021 at 07:15 UTC