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


view this post on Zulip 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).

view this post on Zulip Fernando Chu (Mar 17 2026 at 17:20):

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

view this post on Zulip 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.

view this post on Zulip Fernando Chu (Mar 17 2026 at 20:43):

It is clear, thanks!

view this post on Zulip fosco (Mar 18 2026 at 11:06):

I would love to know what you think about it

This is so cool!

view this post on Zulip 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!)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip fosco (Mar 18 2026 at 11:19):

Maybe I'm looking in the wrong place:

Are all proofs who seem to be missing to be added in the long run? For example, the claim "FinAb\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?

view this post on Zulip fosco (Mar 18 2026 at 11:21):

Take a soon-to-appear page "Ho(Top){\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"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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 "FinAb\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.

view this post on Zulip 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:

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip John Baez (Mar 22 2026 at 18:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ralph Sarkis (Mar 24 2026 at 08:25):

How would you say that CRingop\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)

view this post on Zulip Martin Brandenburg (Mar 24 2026 at 10:49):

Ralph Sarkis said:

How would you say that CRingop\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.

view this post on Zulip 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.

view this post on Zulip 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 C\mathcal{C} and its opposite Cop\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 Grpop\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 Grpop\mathrm{Grp}^{op} is not a category people study in its own right.

view this post on Zulip 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. nNBSn\coprod_{n \in \mathbb N} \mathbf BS_n and FinBij\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.

view this post on Zulip 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 C\mathcal{C} and its opposite Cop\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 CC and CopC^{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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!).

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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 SetopSet^{op} is not finitary algebraic.

view this post on Zulip 米田 豊 (MAITA, Yutaka) (Mar 26 2026 at 14:42):

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

view this post on Zulip 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?

view this post on Zulip Martin Brandenburg (Mar 27 2026 at 09:12):

米田 豊 (MAITA, Yutaka) said:

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

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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Martin Brandenburg (Mar 28 2026 at 01:11):

Functors are coming soon! :magic_wand:

page for contravariant power set functor

right adjoint property page

list of implications of functor properties

special adjoint functor theorem

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Nathanael Arkor (Mar 30 2026 at 08:08):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Nathanael Arkor (Mar 30 2026 at 11:09):

(It seems to be working now for me.)

view this post on Zulip 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.

view this post on Zulip Morgan Rogers (he/him) (Mar 30 2026 at 11:12):

Okay sounds like my suggestion was irrelevant :grinning_face_with_smiling_eyes:

view this post on Zulip Martin Brandenburg (Apr 02 2026 at 09:45):

Functors are now available in CatDat! You can see the current list at https://catdat.app/functors and browse through the new pages. As with categories, we have pages for individual functors, properties, implications, and a deduction system. All details can be found here.

view this post on Zulip JR Learnstomath (Apr 03 2026 at 11:10):

Wow, this is AMAZING @Martin Brandenburg! Thank you so much, this is hugely helpful to me as a not-in-academia-learning-CT person.

view this post on Zulip JR Learnstomath (Apr 03 2026 at 11:12):

I didn't find locos (list-arithmetic distributive category), is it because it's from a 1990 paper? (I don't presume to be able to add to this database, I'm just learning stuff)

view this post on Zulip Martin Brandenburg (Apr 03 2026 at 17:39):

I haven't heard of this property before. It seems to be very niche, right?

view this post on Zulip Kevin Carlson (Apr 03 2026 at 21:49):

I've never heard of it myself.

view this post on Zulip Valeria de Paiva (Apr 03 2026 at 21:53):

List-arithmetic distributive categories: Locoi

J.R.B. Cockett , https://www.sciencedirect.com/science/article/pii/002240499090121W

but I have never worked with them myself.

view this post on Zulip John Baez (Apr 04 2026 at 20:34):

Are ya livin' la vida locos, @JR Learnstomath?

view this post on Zulip JR Learnstomath (Apr 05 2026 at 05:37):

John Baez said:

Are ya livin' la vida locos, JR Learnstomath?

Indeed -- woke up in Locos City, cartesian cats and parametrized list object dolls (eep, too many syllables!)

Oh, I think that nowadays, it goes by the name arithmetic pretopos: nLab https://ncatlab.org/nlab/show/arithmetic+pretopos

view this post on Zulip Dmitri Pavlov (Apr 08 2026 at 04:25):

Are there any plans to turn this website into a wiki? The current ways of contributing impose rather high barriers.

view this post on Zulip Ryan Schwiebert (Apr 08 2026 at 15:56):

I’m interested in the problem of lowering the contribution bar too. In the past the thing that was used the most was a suggestion form. Second most popular were suggestions submitted by chats (math.se chatroom and blog comments).

I like the idea of opening up some fields to wiki-like access and wonder if this architecture would allow that.

view this post on Zulip Martin Brandenburg (Apr 09 2026 at 02:07):

Dmitri Pavlov said:

Are there any plans to turn this website into a wiki? The current ways of contributing impose rather high barriers.

Hey Dmitri!

First of all, there is the google form that allows contributions for anyone, there is no barrier. (It has also been used already.) Submitting an issue on GitHub also only requires a GitHub account. The only technical "barrier" is when you want to create a pull request, that is true.

But there are many reasons why I do not plan to make it a "Wiki". I assume this means that basically anyone can create an account and edit the data (maybe with some peer review process). Here is why:

A Wiki (usually) only concerns static data. While CatDat generates static data in the end (except for the search and comparison pages), I think it is not really comparable to any other Wiki. Most of the data in CatDat is generated. As of writing this, there are 7800 category property assignments. But only 752 of them have been added manually! The vast majority of properties are deduced via the implications. On top of that, implications are also dualized automatically if applicable. There are even plans to make this whole deduction system more powerful and dynamic (see issue 22 for example).

So, when someone wants to make a "Wiki style" edit, they actually also need to see all the deduced properties. But this means to rebuild the whole database, rerender all pages, maybe more. (Yes, rebuild, since what happens if some wrong property is fixed, for example?) How should we even do this in the browser? It is possible of course, but it requires a lot of effort.

The deduction system also checks if any contradiction is generated. You cannot possibly add an implication that, via some steps in between, concludes that the category of sets is, say, abelian. If we want to allow "Wiki style" edits, for each potential edit a copy of the SQLite database has to be generated on the fly (where to save it?), checked for errors, ... I think this will produce a huge technical overhead.

It is much easier to let CatDat do its thing on your local machine, check if everything is OK, and then push the commit. (Of course, the checks are also made during deployment.) I also like that the current system with PRs on GitHub has a built-in peer review system, that we can discuss in issues, comment on PRs, etc.

But what we can and should do: make the contribution guidelines easier to understand. Also maybe add a section for those who never used GitHub before. By the way, I also added a section with example PRs to make it easier to understand how they look like. I think they demonstrate quite well that additions to the database are mostly "just text" (example). If there is anything else one can improve in this document, please let me know (or create an issue / PR :D).

EDIT. Ah and we can combine these approaches as well. What about adding a textarea on each page where every user can "submit" new data (a new category, a new proof, etc.), but this just generates a GitHub issue? Then I (or anyone with the technical background) can implement it. Maybe this makes the google form superfluous.

view this post on Zulip Martin Brandenburg (Apr 09 2026 at 02:51):

This recently opened PR is also a quite good illustration in which way CatDat differs from a Wiki. It has added the property "cocartesian coclosed" (among other things). CatDat has assigned this property to all the categories automatically! Namely, it automatically dualized all the implications for "cartesian closed" categories and made deductions based on these. Not a single category was spared by these deductions. A Wiki approach (as I know it, at least) is the opposite, it would add the info here and there, but it would never be as systematic.

This nlab page mentions and proves the result that every category that is cartesian closed and cocartesian coclosed is automatically thin. Fun Fact: CatDat deduces this automatically, which is why it does not have to be manually added. The chain is basically: ccc => terminal object, coccc + terminal object => strict terminal object (dualized from: ccc + initial object => strict initial object), ccc + strict terminal object => thin.

view this post on Zulip Martin Brandenburg (Apr 10 2026 at 14:19):

Martin Brandenburg said:

Dmitri Pavlov said:

Are there any plans to turn this website into a wiki? The current ways of contributing impose rather high barriers.

EDIT. Ah and we can combine these approaches as well. What about adding a textarea on each page where every user can "submit" new data (a new category, a new proof, etc.), but this just generates a GitHub issue (via GitHub API, the user does not need an account)? Then I (or anyone with the technical background) can implement it. Maybe this makes the google form superfluous.

I have now added a suggestion form on (almost) every CatDat page. It generates issues on GitHub. I hope this helps to bring down the barrier to contribute. (Details)

view this post on Zulip Dmitri Pavlov (Apr 13 2026 at 05:50):

A suggestion form is closer to what I had in mind. It seems to be working, modulo a bizarre limit of 50 characters. I hope you do not have spam bot problems, as the form appears to be unprotected (?). Concerning your comments: the database does not have to be rebuilt every time an edit is made. The edits can be approved asynchronously. What I had in mind is similar to the suggestion form, but allowing for structured input of information, so that contributions only need to be approved, not created from a free-form information.

view this post on Zulip Martin Brandenburg (Apr 13 2026 at 14:01):

The form is not unprotected, see the linked PR for details. There is a rate limit, that can be elevated to an IP ban, and a profanity filter. Still no auth, so it is not 100% safe, yes. I will add auth when it becomes necessary (but at which point it makes no sense anymore to have this form since one can just write a GitHub issue directly).

The limit of 50 characters is only for the short summary - that will be the title of the GitHub issue. That should indeed be short. The body can be up to 10000 characters (and we can increase this limit if necessary). Since you have already created an issue (thanks!), it seems that this has worked well so far.

What I had in mind is similar to the suggestion form, but allowing for structured input of information, so that contributions only need to be approved, not created from a free-form information.

Yes, I know, but all the mentioned problems remain. But maybe it will work some day. The automated tests that I have added today are a step in that direction.