Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: CatDat – the comprehensive database of categories

Martin Brandenburg (Mar 17 2026 at 17:09):

I am happy to announce CatDat – the comprehensive database of categories and their properties.

https://catdat.app

I explain this app in detail in this video, but you can also click around to get a feel for it. Basically, you can find categories and their (non-)properties, search for combinations of properties, and compare categories with each other.

I would love to know what you think about it, and would be even happier about any contributions! In fact, the application is open-source, and I believe that we, as a community, can complete and expand this database, thereby making it really useful.

What makes this project special (in my opinion) is the integrated deduction system. From a small amount of properties and non-properties many other properties and non-properties can be deduced automatically. The deductions are displayed in a human-readable form on each category detail page.

In the repo's README I also mention related projects, for example the Catabase, but it is different and seems to be abandoned. Let me also mention that CatDat does not want to replace nLab; it tries to add to it.

Personally, I also really enjoyed combining two of my biggest interests (category theory + software development).

Fernando Chu (Mar 17 2026 at 17:20):

Cool project! How does the deduction system work? Is it bruteforcing every possibility?

Martin Brandenburg (Mar 17 2026 at 17:40):

Yeah more or less, but that is OK since (currently) there are "only" about 100 implications. The logic is basically: For a given set of properties, find an implication whose assumptions are known properties, but the conclusion is not. Add the conclusion to the list of properties. Continue until no implication is found.
For non-properties, we also work with the properties. Find an implication whose assumptions are known properties except for one (p), and such that the conclusion is a known non-property. Then p gets added to the non-properties (by proof of contradiction). Continue until no implication is found.
It's so simple but very effective. In particular, every proof is literally a one-liner (based on the known implications).
I hope it's clear. If not, the deduction code tells the whole story.

Fernando Chu (Mar 17 2026 at 20:43):

It is clear, thanks!

fosco (Mar 18 2026 at 11:06):

I would love to know what you think about it

This is so cool!

fosco (Mar 18 2026 at 11:10):

the property of being "concrete" seems missing, and the homotopy category of spaces

(of course it's the first thing I tried!)

Nathanael Arkor (Mar 18 2026 at 11:11):

This is really cool! I can see this being very useful, assuming it receives enough contributions to capture a wide range of properties and examples covering different combinations of properties.

Nathanael Arkor (Mar 18 2026 at 11:14):

One idea that could be nice to try is enumerating finite categories, up to equivalence, up to, say, 10 objects, and automatically deducing their properties. (This topic has been discussed previously on this Zulip, e.g. #learning: questions > Enumerating finite categories.) The reason this would be nice is that I imagine this could discharge many of the combinations of properties that are currently missing, and would furthermore give minimal examples/counterexamples.

fosco (Mar 18 2026 at 11:19):

Maybe I'm looking in the wrong place:

• Proofs for Claims: Provide proofs for all new claims (properties, implications, morphism descriptions). (We are currently working on filling in the existing ones.)

Are all proofs who seem to be missing to be added in the long run? For example, the claim "$\bf FinAb$ doesn't have a generator", is awaiting to be proved by someone, and if yes, is there a guideline for how to prove it?

fosco (Mar 18 2026 at 11:21):

Take a soon-to-appear page "${\bf Ho}({\bf Top})$": non-properties: it is not concrete, but good luck proving it in a one-liner! Is the mere link sufficient to count as "proof"?

Nathanael Arkor (Mar 18 2026 at 11:40):

Yes, you can see examples in which the proof is simply a reference to a textbook, nLab page, etc.

Nathanael Arkor (Mar 18 2026 at 11:41):

I notice there is a similar project SmallCategories, which I'd never come across before. In particular, they have implemented the "generate finite categories" idea I mentioned above. It could be worth getting in contact with Ben Spitz and asking him whether he would consider merging his database with yours.

Theofilos Tsantilas (Mar 18 2026 at 13:46):

That seems a really neat project. I'm leaving this message here to remind myself to come back and see whether I can contribute when I find the time. Hope it grows!

Martin Brandenburg (Mar 18 2026 at 13:59):

fosco said:

the property of being "concrete" seems missing, and the homotopy category of spaces

Thanks for the feedback!

Adding "concretizable" (I don't think "concrete" is a property of a category) is on my todo list, but for me personally it has low priority. There is not much one can do with this property, and either it is trivial to check that something is concretizable, or it is very hard to disprove (hTop).

Yeah hTop should be added, it is also on my todo list. It will be difficult to check all the properties here, though. Many constructions for hTop are weird in a 1-categorical setup. Related.

Martin Brandenburg (Mar 18 2026 at 14:05):

fosco said:

Are all proofs who seem to be missing to be added in the long run? For example, the claim "$\bf FinAb$ doesn't have a generator", is awaiting to be proved by someone, and if yes, is there a guideline for how to prove it?

Yes, currently the reason for a property (or non-property) can be NULL, but I plan to change that. For this, first one has to write down the missing reasons. In many cases I already did that (and sometimes this was not easy), in some cases it is just a matter of writing down the obvious, but in some cases it is not clear at all, and I may even be wrong in some cases (which is why I would like to make the reason mandatory in the future).

As Nathanael already explained, there are three types of proofs in CatDat: 1) Writing "This is trivial" :laughing: 2) Writing down the proof. 3) Referencing a book or article of website. Have a look at the existing examples, this makes it even more clear, I think.

Martin Brandenburg (Mar 18 2026 at 14:07):

Nathanael Arkor said:

This is really cool! I can see this being very useful, [...]

Thanks a lot for your feedback! Also thank you very much for the further references, your pull requests and the issues via the repo. I will now have a look at them. :working_on_it: See you on GitHub then! :folded_hands:

Ryan Schwiebert (Mar 21 2026 at 02:54):

This was my #1 desired database analogous to pi-base/DaRT that I wanted to see. Glad it's finally here! Looking forward to learning how we can all mutually improve these sites.

Sometimes each type of site seems to require its own peculiarities, but as category theory teaches us sometimes there are ways to melt those differences away...

James E Hanson (Mar 22 2026 at 18:19):

I don't know if this would be a good idea but do you have any plans for systematically tracking dual properties?

John Baez (Mar 22 2026 at 18:36):

Maybe simpler to link each category to its dual iff it's in the database....

Martin Brandenburg (Mar 24 2026 at 08:07):

James E Hanson said:

I don't know if this would be a good idea but do you have any plans for systematically tracking dual properties?

I am already doing that? Maybe I misunderstood you. But on every property page, you can see the dual property (if available; sometimes it is not, e.g. nobody talks about co(cartesian closed) categories, or co(locally presentable) categories).

The deduction system also heavily uses dual properties.

Martin Brandenburg (Mar 24 2026 at 08:08):

John Baez said:

Maybe simpler to link each category to its dual iff it's in the database....

The idea is to never add a category which is dual to one of the categories already in the database. If something needs to be said about the dual category, it can also be said about the original - just by dualizing the statement. This is to avoid the clutter and to avoid duplicate information.

For example, I have just added the information that CRing is not coregular - instead of saying that CRing^op is not regular.

In the search page, there is also a link that dualizes the search.

Ralph Sarkis (Mar 24 2026 at 08:25):

How would you say that $\mathbf{CRing}^{\mathrm{op}}$ is isomorphic to the category of affine schemes? (and then transport all properties of one to the other, and similarly for equivalences)

Martin Brandenburg (Mar 24 2026 at 10:49):

Ralph Sarkis said:

How would you say that $\mathbf{CRing}^{\mathrm{op}}$ is isomorphic to the category of affine schemes? (and then transport all properties of one to the other, and similarly for equivalences)

Nitpick: these categories are equivalent, not isomorphic.

To answer your question: The proof that two categories are isomorphic or equivalent does not belong to CatDat (currently). It can be mentioned in the category description, though.

Here is a quote from CONTRUBITING.md:

No dual categories: As a rule of thumb, do not add categories that are dual to categories already in the database. Properties of the dual category should instead be added as properties of the original category (use the corresponding dual property). For example, do not add the dual of the category of sets.

No equivalent categories: Do not add categories that are equivalent or even isomorphic to categories already in the database. If the equivalence is non-trivial, mention it in the description of the original category. Some exceptions are allowed, since certain properties (such as being skeletal) are not invariant under equivalence.

Martin Brandenburg (Mar 24 2026 at 10:52):

But I am currently revising this guideline in the PR on functors. I definitely want to be able to add, say, the contravariant power set functor.

Zoltan A. Kocsis (Z.A.K.) (Mar 24 2026 at 12:57):

Have you considered some sort of notability guideline instead of a strict "no dual categories / no equivalent categories" rule?

It seems to me that CatDat will provide maximal benefit to its audience if it mainly includes categories that we actually study and use. In some cases, it might happen that both a category $\mathcal{C}$ and its opposite $\mathcal{C}^{op}$ are studied in the literature, possibly even under distinct names. For example, one has the category of complete Heyting algebras, and the category of locales. Which one should get priority over the other?

The issue with dual categories like $\mathrm{Grp}^{op}$ does not seem to be that it is the opposite of a category already in the database, but rather that nobody cares, in that $\mathrm{Grp}^{op}$ is not a category people study in its own right.

Joe Moeller (Mar 24 2026 at 15:23):

Having no equivalent category duplicates but also equivalence non-invariant properties are at odds with each other. $\coprod_{n \in \mathbb N} \mathbf BS_n$ and $\mathsf{FinBij}$ are equivalent, but one is skeletal and the other is not. I won't argue against no dual categories, but it does mean you'll have to list stuff about affine varieties in the commutative rings page, same for any Stone-type dualities.

Martin Brandenburg (Mar 24 2026 at 18:40):

Zoltan A. Kocsis (Z.A.K.) said:

In some cases, it might happen that both a category $\mathcal{C}$ and its opposite $\mathcal{C}^{op}$ are studied in the literature, possibly even under distinct names.

That's a good point. I had the (wrong) impression that there is always one "main" category among $C$ and $C^{op}$, and this one should be in CatDat then. But you are right, sometimes both are equally "natural". Affine group schemes and commutative Hopf algebras is another example.

Valeria de Paiva (Mar 24 2026 at 19:25):

Hi @Martin Brandenburg . Thanks for the resource, I find it very exciting. But I was a bit disappointed that it doesn't have things like "monoidal categories" or "smccs" or even "cccs", the kinds of category I'm most interested in. Is this outside of your plans, because of granularity, or have you not gotten to them?

Ryan Schwiebert (Mar 24 2026 at 21:00):

@Valeria de Paiva I could be misunderstanding, but when I read that I think "a monoidal category isn't a category with an intrinsic property, it's a category with additional structure." I think websites like CatDat most often focus on a fixed target (like "category" or "group" or "ring" or "topological space") and focus on properties they can have, and their interrelationships, all scoped by that original choice of "category/group" etc.

In comparison, one might ask why DaRT "doesn't have algebras/Hopf-algebras" and so on.

Now, possibly a website could do multiple flavors of a thing like that, but having said that I can't imagine how i'd adapt what I've written to that scope.

One can easily imagine a parallel site all suited for monoidal categories and their properties.

But I could be hallucinating all this. Maybe "with extra structure" is as valid a property as other more "internal" properties a category could have. Maybe it's not the issue I imagine. I certainly do track things which are algebras and bialgebras in DaRT but it doesn't play a role, really.

Ryan Schwiebert (Mar 24 2026 at 21:23):

Now that you mention it, it sounds more like a hierarchy of structures rather than of properties. People often try to muddle them together in charts https://math.stackexchange.com/q/5123210/29335

Matteo Capucci (he/him) (Mar 25 2026 at 10:57):

Ryan Schwiebert said:

In comparison, one might ask why DaRT "doesn't have algebras/Hopf-algebras" and so on.

One could make the case that [[property-like]] structure (e.g. being cartesian or cartesian closed) deserves to be included, but not proper structure. On the other hand monoidal structures are basically everywhere! So it would be great to have (but of course, it's great as it is already!).

Martin Brandenburg (Mar 25 2026 at 15:59):

Valeria de Paiva said:

[...] I was a bit disappointed that it doesn't have things like "monoidal categories" or "smccs" or even "cccs"

Indeed, Nathanael has suggested the same in issue #4, and we can continue the discussion there. It is definitely doable. As a first step, I want to add functors (PR for functors). After this, I plan to find similarities between the entity systems "category" and "functor" and refactor the codebase. And then (I hope) monoidal categories etc. should not be a big issue anymore.

Valeria de Paiva (Mar 25 2026 at 16:00):

hi @Ryan Schwiebert I am interested in classes of categories that correspond (via curry-howard) to specific logics. So I'm not worried about intrinsic properties vs property-like structure of categories. I thought CatDat would be useful for me, but I guess it isn't. I want a different kind of granularity.

(Sorry, had written before seeing @Martin Brandenburg 's message. Thanks for that and for the stackexchange thread.)

Martin Brandenburg (Mar 26 2026 at 13:04):

Since it has been requested (and will be necessary for introducing functors), dual categories can now also be added. All properties of a category (satisfied or not) that have a dual are automatically added to its dual category, if that dual category is available (code). It is made sure that there is no endless loop. As an example, I have added the dual of the category of sets. Here, 77 properties (satisfied or not) have been automatically deduced from the category of sets. For example, when you click on the reason for "has coequalizers", it shows "Its dual category has equalizers".
You can also add properties that are not dualized, in particular if they have not (yet) a dual in the database. For example, I have added the information that $Set^{op}$ is not finitary algebraic.

米田 豊 (MAITA, Yutaka) (Mar 26 2026 at 14:42):

What metatheory does CatDat rely on? Some categorical properties (e.g., $\mathbf{Set}$ being a complete elementary topos) are sensitive to the choice of foundations.

James E Hanson (Mar 27 2026 at 00:50):

Martin Brandenburg said:

I am already doing that?

Oh so is it just that you don't display a property in the list of properties unless there's actually an example of it in the database?

Martin Brandenburg (Mar 27 2026 at 09:12):

米田 豊 (MAITA, Yutaka) said:

What metatheory does CatDat rely on? Some categorical properties (e.g., $\mathbf{Set}$ being a complete elementary topos) are sensitive to the choice of foundations.

I work with ZFC and two universes $U \in U^+$. A category is, unless otherwise stated, defined as a category which is internal to $U^+$. That is, the set of morphisms and the set of objects belong to $U^+$. It is small when both sets belong to $U$. It is called locally small if the hom-sets belong to $U$. Generally, "small" refers to elements of $U$, and "essentially small" refers to sets (maybe I want them in $U^+$) that are isomorphic to sets in $U$. The category of sets $\mathbf{Set}$ has the object set $U$. The category of large sets $\mathbf{Set}^+$ has the object set $U^+$, it is of course not $U^+$-small, but $U^{++}$-small if you like. Categories are not assumed to be locally small. Hence, the hom-functors $hom(X,-) : \mathcal{C} \to \mathbf{Set}^+$ take values in $\mathbf{Set}^+$.

This is the framework I have been working with in the last 1-2 years, and it solves a lot of set-theoretic issues - at least when it comes to basic category theory (still in the process of updating my book with it...). Perhaps you were alluding to things like Vopenka's principle? We can think about these delicate questions as soon as categories and properties are added where this plays a role.

That being said, I should probably write these conventions somewhere in CatDat.

Martin Brandenburg (Mar 27 2026 at 09:13):

James E Hanson said:

Oh so is it just that you don't display a property in the list of properties unless there's actually an example of it in the database?

No. But apparently then I didn't yet understand your concern / suggestion. Can you perhaps phrase it in a different way? :slight_smile:

Martin Brandenburg (Mar 27 2026 at 09:44):

Meta comment. If you have a GitHub account, then you can also submit your ideas (or questions) in form of a GitHub issue. This option has better visibility and allows me to organize these ideas in a better way. I am also much more active on GitHub than on Zulip (especially in the long run, it may happen that I am not online on Zulip for months). If you don't have a GitHub account, this Google Form provides another option.

Martin Brandenburg (Mar 28 2026 at 01:11):

Functors are coming soon! :magic_wand:

James E Hanson (Mar 28 2026 at 01:32):

Martin Brandenburg said:

James E Hanson said:

Oh so is it just that you don't display a property in the list of properties unless there's actually an example of it in the database?

No. But apparently then I didn't yet understand your concern / suggestion. Can you perhaps phrase it in a different way? :slight_smile:

Let me put it this way. Is the reason why properties like 'co-abelian' aren't listed just that these aren't properties people usually consider?

Martin Brandenburg (Mar 28 2026 at 01:37):

James E Hanson said:

Let me put it this way. Is the reason why properties like 'co-abelian' aren't listed just that these aren't properties people usually consider?

Ah, this is a good question. Yes, that is basically it. (But notice that "abelian" is self-dual, so this is not a good example.) For this reason I also have not (yet) added "coalgebraic" (which actually has two meanings...) or "locally copresentable". But: I have noticed many times that it is useful to add dualized properties to decide other properties. This is because (among other things) "disjoint products", "coregular", "coextensive" and "co-Malcev" made it into CatDat, even though neither of these are common. I noticed that adding these gives a more complete picture. I also still need to add the dual of "exact filtered colimits". Maybe it is even good to enforce that every property has a dual property. :thinking:

Nathanael Arkor (Mar 28 2026 at 08:32):

In theory, you only need to either add opposite categories, or add duals of every property (as long as it is possible to derive a statement about a category from properties both of it and of its dual). However, in practice, it is probably more convenient for users to have both opposite categories and the dual of every property.

Joe Moeller (Mar 29 2026 at 15:58):

You'll need to add properties to the database as well so you can look up which ones are self-dual.

Martin Brandenburg (Mar 30 2026 at 07:55):

Yuto Kawase opened an issue on CatDat which I find quite important. Maybe you want to join the discussion? It is about if "locally small" should be redefined as "locally essentially small".
https://github.com/ScriptRaccoon/CatDat/issues/25
cc. @Nathanael Arkor

Nathanael Arkor (Mar 30 2026 at 08:08):

I'm currently getting a "504 Gateway Time-out" when I try to visit catdat.app.

Martin Brandenburg (Mar 30 2026 at 10:28):

Nathanael Arkor said:

I'm currently getting a "504 Gateway Time-out" when I try to visit catdat.app.

I have checked this and could not reproduce it. To be alerted about this in the future I also created https://catdat.openstatus.dev/ (which shows no problems either - so far). Is the issue still happening?

Morgan Rogers (he/him) (Mar 30 2026 at 11:03):

Where are you based, @Martin Brandenburg ? I was having DNS server errors for some sites hosted in North America this morning.

Martin Brandenburg (Mar 30 2026 at 11:08):

I am based in Berlin, but the website is hosted on Netlify, which has servers all around the world and a globally distributed CDN. So I cannot specify any location.

Nathanael Arkor (Mar 30 2026 at 11:09):

(It seems to be working now for me.)

Ryan Schwiebert (Mar 30 2026 at 11:11):

As I write this, https://www.netlifystatus.com/ has orange "partial outage" notices for the categories "Netlify functions" and "edge functions" which I think is possibly relevant. Site's worked fine for me too when I tested.

Morgan Rogers (he/him) (Mar 30 2026 at 11:12):

Okay sounds like my suggestion was irrelevant :grinning_face_with_smiling_eyes: