I think the zulip chats might be slightly friendlier for newcomers than any of the sources you mentioned just because they're more casual. For instance, I asked some very naive questions on the lean zulip chat and wasn't made to feel like a complete idiot. Since zulip seems to be increasingly popular in other communities with an interest in formalized mathematics, this might also serve as a "recruiting opportunity" to get some new folks to start playing around with agda. Emily -- Associate Professor, Dept. of Mathematics Johns Hopkins University www.math.jhu.edu/~eriehl she/her On Wed, May 13, 2020 at 6:20 AM Nils Anders Danielsson wrote: > On 2020-05-13 13:29, Egbert Rijke wrote: > > I created a zulipchat for agda. Feel free to join! > > > > https://agda.zulipchat.com/join/dig82g1cmzd4bqrtp6o3qxaa/ > > Is there a need for yet another channel for communication about Agda? > People are already asking questions on the Agda mailing list, on the > GitHub bug tracker, on the IRC channel, on Gitter, on Reddit, and on > Stack Overflow. What is the purpose of adding yet another channel (which > additionally seems to require you to log in just to see what others have > written)? > > -- > /NAD > > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/a17e988e-1455-3bc5-03c5-d24c5b07747a%40cse.gu.se > . > > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAAjZwAb1mNUDUphDimRxJeUkYJkWq3VpgWYcCxbsgN5Uy2edQg%40mail.gmail.com.