nForum - Catabase: a database of categories

Hi! Corbin here with yet another ridiculous idea.

Quoting from the infamous database of categories discussion:

I remember someone at nLab could write the database in Ruby, is this offer still on?

I want to propose something quite different.

I’ve prototyped what I’m thinking of as a catabase. This is a plain SQL database which encodes some relations between categories, considering them as first-order objects. For example, there is a table called categories with a column for category names, and two human-readable columns describing objects and arrows. There’s a table called subcategories with a column for subcategory names, and a column for parent category names. Indeed, for all properties and structures listed by Baez as “the basic properties one instantly wants to know about any category one meets,” there is a table or view. For example, in the case of finite limits, there is a table categorical_structure which pairs categories with universal objects (and a table universal_objects) and a view has_finite_limits which queries that table to enumerate categories which have sufficient universal objects to have all finite limits.

Further, I have prototyped the basics of user-friendly display using Datasette. For each category, and some categorical structures, a nice blurb is generated. This is similar to the Abstract Wikipedia proposal. For example, the table karoubi_envelopes has formatting so that Datasette prints the following upon viewing a row:

The category Man is the Karoubi envelope of Op(FinCartSp). Put another way, Op(FinCartSp) is a wide subcategory of Man and every idempotent in Man is split.

While terse (and probably wrong, as I’m not actually good at maths!) this is well-formatted and can be arbitrarily extended with basic SQL and HTML knowledge.

It’s not at all perfect. A short summary of issues:

• Properly-factored tables require many associated queries to look up linked data. This is the N+1 antipattern in Web application design. The template for the categories table has 25 queries, of which four fit the N+1 antipattern.
• I don’t think that the tables are properly factored. groupoids is effectively a view on categories, but topoi is its own table, because topoi have some associated properties (whether it has an NNO, is Boolean, etc.) while groupoids are merely categories which satisfy a property. This leads to…

• Strange monomorphism. Should Cat get a row in categories, or should there be a table 2-categories? Or more pointedly, every core is an essentially wide subcategory, but some cores are only known as special cases; how should the tables cores and essentially_wide_subcategories be factored?

  • For bonus points, SQLite doesn’t permit taking foreign keys of views, so it’s not possible to preserve our custom SQL types; we also can’t take tables from views, so we can’t compute facts in a way which propagates through the SQL structure.
• A lot of data is redundant. There’s a table categorical_structure for all universal properties, and a table enrichments for al enriched categories; they could be finer-grained.

How could this be productionized? The main concern is multiple writers to a single source of truth, and so I imagine that SQLite would be replaced with Pg. Otherwise, though, I’m not sure that it’d be different from any other Datasette deployment; there’s a Docker image, a database that has to be backed up, and a list of contributor keys to authenticate writers.

What would be better? Wagn (now Decko) is pretty nifty, although it used to be a headache to administer and I’m not sure whether it’s gotten easier.

Thanks for reading! I am extremely interested in folks’ feelings about this.