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.
Daniel Geisler (Apr 20 2020 at 15:57):What symbolic software packages do people use in their research? Julia, Pari GP, Mathematica, Maple, home brew? Does anyone use the Comstruct package? Thanks.
James Wood (Apr 21 2020 at 10:07):Probably the biggest one here, if you count it, would be proof assistants. I've been using Agda a lot, and recently it's helped me check some proof refactorings.
Thibaut Benjamin (Apr 21 2020 at 11:54):A bit linked: which formalism have you used to handle categories in Agda? Do you have a github or something where I could look it up? I tried developing some categories in Agda, but never reached the point where I could really benefit from having a proof assistant. I use Agda a lot for working on type theory, and the benefit is much more immediate there
James Wood (Apr 21 2020 at 12:05):Okay, I'm using it more like you, for type theory. If I were to do more category theory, I'd probably start from agda-categories.
Thibaut Benjamin (Apr 21 2020 at 14:53):Thanks, it looks there is quite a lot in this already! I might have a go with it when I have some free time
Fabrizio Genovese (Apr 21 2020 at 15:04):A similar thing in idris is idris-ct
Thibaut Benjamin (Apr 22 2020 at 08:38):Thanks for pointing it out, I have never used idris, so there is probably a bigger learning curve for me. I have worked with UniMath formalization of categories, but unfortunately Coq does not support natively inductive-recursive types, that I need to work with type theory. I have moved out of this a bit at the moment, but I will go back to it and check this out as well