Add support for other categorical structures

[varkor]

In addition to categories, it would be useful to be able to add entries and properties for structures such as functors, natural transformations, 2-categories, double categories, (infinity, 1)-categories, and so on. While it would presumably require a few changes to the structure of the current data format, the system seems flexible enough to support this without too much additional effort.

[ScriptRaccoon]

Thank you for the suggestion.

Long ago I already tried to incorporate information about special types of morphisms: regular monomorphisms, split monomorphisms, effective monomorphisms, etc. There are also implications between these properties of morphisms, and counterexamples. This should still be findable in the commit history. However, I removed it again because it didn't really fit with the rest of the application. In the end, this would just become a collection of examples and counterexamples for properties of monomorphisms (and epimorphisms), the database probably would not save any specific morphisms, which is a huge difference to what CatDat currently is.

Following your suggestion, I would start with the simplest case: functors. But I am afraid it would turn into the same situation. I don't think it makes much sense to store specific functors in a database. Again, it would amount to a collection of examples and counterexamples, e.g. a fully faithful functor that is not essentially surjective, or a functor that preserves finite limits but not all limits. Somehow, it doesn't feel right to include this in CatDat.

You suggested higher categories, and my objections do not apply to them. However, I am concerned that it would be quite difficult to add, say, 2-categories to the application and (a) include a sufficiently large number of examples of 2-categories (so that it is worthwhile), (b) include a sufficiently large number of properties of 2-categories, and (c) keep the UI clear and easy to use.

[varkor]

Again, it would amount to a collection of examples and counterexamples

I don't think I quite follow. Isn't this precisely the focus of CatDat at the moment? E.g. the search feature specifically allows you to search for categories satisfying property X but not property Y. I suppose it's not clear to me what argument applies to functors that does not apply to categories.

However, I am concerned that it would be quite difficult to add, say, 2-categories to the application and (a) include a sufficiently large number of examples of 2-categories (so that it is worthwhile), (b) include a sufficiently large number of properties of 2-categories, and (c) keep the UI clear and easy to use.

Regarding (a), there are "more" examples of 2-categories than of 1-categories (trivially, since every 1-category is a 2-category, and also because essentially every concept in 1-category theory can be extended, typically in several ways, to 2-category theory). So certainly a sufficient number of examples exist. There is a question of whether people will be motivated to contribute enough of them, but this applies in general to CatDat. I would be keen at least to add plenty of examples of double categories.

Regarding (b), I think the same comment applies. Pretty much every property of 1-categories has several analogues for 2-categories.

I understand the concern in (c), but I think it should not add much overhead. For instance, the "Categories" tab could become a "structures" tab, with an input field at the top to filter by kind of structure (and similarly for properties, which would be relative to the kind of structure). Then each individual page would be no more complicated (apart from some annotation somewhere saying what kind of structure it is).

[ScriptRaccoon]

I see. Maybe I can give it a try.

I still think there is a crucial difference between categories and, say, functors as for the database. A functor usually only acts as a device to "communicate" between categories, they are usually not interesting in their own right. (From a practical standpoint, of course every category $\mathcal{C}$ can also be seen as a functor $1 \to \mathcal{C}$.) Because of this, I think that the community does not need a "list of functors" in the same way as a "list of categories".

But indeed: it would be nice to have a functor property combo search.

So here is a suggestion what to do next:

• Rename existing table properties to properties-for-categories. Rename table category-properties to category-property-pairs. Same for non-properties. Rename table implications to category-implications. This is to avoid confusion with what comes next and to make it scalable.
• Add new tables: functors, properties-for-functors, functor-property-pairs, functor-non-property-pairs, functor-implications.
• Fill the tables properties-for-functors (see below) and functor-implications.
• Fill the table functors: not as an attempt to list all interesting functors, but to provide witnesses for functors which have property P but not property Q (if that is consistent).

Some ideas for properties-for-functors:

• preserves limits
• preserves products
• ... same with all other types of limits and colimits
• is a right adjoint
• is an isomorphism (evil!)
• is an equivalence
• is fully faithful
• is faithful
• is full
• is essentially surjective
• is conservative
• creates limits
• reflects limits
• is monadic
• is comonadic
• is accessible
• is dense

Some implications:

• isomorphism => equivalence <=> fully faithful + essentially surjective
• is a right adjoint => preserves limits => preserves products + preserves terminal object + ...
• monadic => is a right adjoint

Let me know what you think.

[ScriptRaccoon]

I have created this PR to add functors.

#12