Add Functors to CatDat

[ScriptRaccoon]

Add Functors to CatDat

As suggested in #4, this PR adds functors, their properties, and implications of functor properties to CatDat. Several new tables and pages have been added. This PR also prepares for adding other categorical structures (such as monoidal categories or 2-categories) in the future.

URLs

In preparation for this PR, most of the old URLs for categories have been changed: /search has become /category-search and /property/[id] has become /category-property/[id], etc. This has already been done in the main branch. This makes them consistent with the new URLs /functor-search, /functor-property/[id], etc.

Structure Selector

The header has been redesigned. It now also includes a structure selector which allows to switch between categories and functors. It is also visible on mobile. The selected structure is defined by the URL. Switching to "functors" brings the user to the page with the list of functors and changes the navigation component (both on desktop and mobile appropriately: it now shows links to the functor pages.

I have only added a few functors so far, more can be added later. For this reason there is also no search by name yet.

Functor Detail Pages

The functor detail page shows the definition of the functor, which includes source and target category, its satisfied and non-satisfied properties. As with categories, the application deduces further satisfied and non-satisfied properties by using implications (see below).

Property List Page

For now, I have added 27 properties of functors. We can add more later.

Since there aren't so many, there is no search by name yet.

Property Detail Page

The property detail page shows the definition of a property of functors, its dual property (if available), relevant implications, functors that have this property, and functors that do not have this property.

Deduction System

As with categories and their properties, there is a script that automatically deduces properties of functors (satisfied or not) based on a list of implications. I have added the well-known implications between the existing properties. Implications are automatically dualized, e.g. comonadic => left adjoint is dualized from monadic => right adjoint.

Again: since there aren't too many implications for now, there is no search yet. Also, there is no toggle to show/hide dualized implications (like on the page for category implications), the page just always shows all implications.

As mentioned, the application deduces further satisfied and non-satisfied properties of functors by using these implications.

Implication Detail Page

As with implications between properties of categories, the implication detail page here shows the required assumptions of the functor and the conclusion(s), together with a proof or a reference to it. Here is the Special Adjoint Functor Theorem for example.

There is a big difference to implications between properties of categories, though: As the example already shows, some results need assumptions also for the source or the target category. These need to be recorded as well. The deduction system uses these as well by checking the properties of the source and target categories that have been derived before.

For example: when a functor with domain $\mathbf{FinSet}$ preserves products and equalizers, it is not deduced that it is continuous, since the result "product-preserving + equalizer-preserving => continuous" requires the domain to have products, and $\mathbf{FinSet}$ does not have products. However, it has finite products, so we can deduce at least that the functor is left exact.

Search

It is possible to search for functors that satisfy some properties while not satisfying others. This is basically the same as for categories. For example, one can search for functors that are cocontinuous but not continuous.

Missing Data

For the 6 examples of functors I have tried to decide all properties. There are some open cases. They are listed on the page with missing data (route /missing).

Code duplication

Many features for functors are very similar to the ones for categories. For now, we have a lot of copy pasted code, but this can be unified in the future. In some rare cases this has been done already (for example, the function get_property_url now accepts a type which can be functor or category).

There will be a big obstacle, though: as mentioned, functor implications are more complex than category implications, since they also involve source and target assumptions. And this is actually a pattern: in the same way that a functor has two "underlying" categories, a monoidal category has one underlying category. When we add monoidal categories in the future, some implications will reference the underlying category as well.

New Database Diagram

This is the updated database diagram. All the tables on the right are new. There are many similarities, but also differences to the existing tables on the left (for categories). At some point we should also rename the old tables (properties -> category-properties, etc.).

Documentation

Of course, the documentation has been updated as well.

Commit History

The original commits have been rebased and edited a lot. Now you can check the individual changes by going through the commits.