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.
Alex Kreitzberg (Sep 23 2025 at 06:48):After the foundations conversation I'm thinking I should actually dig my heels in and read the HoTT book. I'd like to ask questions as I go through it, but this online community seems just off topic.
Is there some other online forum where "progress updates & questions" as I read through the HoTT book would be very on topic and welcome?
Nathanael Arkor (Sep 23 2025 at 07:14):There's a Homotopy Type Theory Zulip that could be appropriate.
Ulrik Buchholtz (Sep 23 2025 at 07:19):The Univalent Agda Discord – invite link – is also quite active, and has a general (not Agda-specific) HoTT channel.
Chris Grossack (she/they) (Sep 23 2025 at 15:28):You might also be interested in the recordings from the HoTTEST Summer School that happened a few years ago (available here). Iirc we mainly worked in book HoTT for all the non-agda lectures, and the agda lectures pivoted to cubical halfway through, but I might be misremembering
Chris Grossack (she/they) (Sep 23 2025 at 15:29):There's a discord for the summer school (invite link), but it's become less active over time. Nowadays it's basically been subsumed by the univalent agda discord that Ulrik linked. There's tons of people there would would be happy to help out with any questions you have ^_^