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.
Asad Saeeduddin (Mar 29 2021 at 03:58):hello there. does anyone know of a structured library of facts and factoids about various xyz-monoids and xyz-categories, and various things that each one exemplifies? beyond "x is an example of [a, b, c, ...]", there's lots of dimensions along which the data can be structured, e.g. the lattices formed by concepts under the relation of "generalizes", but something basic would also be very ueful.
as someone who doesn't know how to do much category theory, but can find a lot of uses for it, i find it hard to review/recall quickly whether such and so a x-monoid/category/functor has such-and-so a property, or whether all foos are bars. i think a more structured library of facts that is akin to the excellent ncatlab project would be very useful to me (and other people like me).
Asad Saeeduddin (Mar 29 2021 at 04:01):perhaps the exercise of structuring these facts for systematic presentation will involve some non-trivial category theory (structuring mathematics is after all what category theory excels at)
John Baez (Mar 29 2021 at 04:19):I don't know of anything like what you want.
I believe the Topos Institute is planning to do some work on a more structured version of the nLab - better for computers. But this will be just the start of things, not the end.
There's a lot of room for other projects, too.
Javier Prieto (Mar 29 2021 at 09:26):Many facts about category theory and other areas of mathematics have been formalized in different proof assistants over the years. This is at the other end of the spectrum in relation to the nlab: good for computers to parse, terrible for humans. However, good documentation built on top of these standard libraries should make them more human-friendly.