Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Emily Riehl <eriehl@math.jhu.edu>
To: HomotopyTypeTheory@googlegroups.com
Subject: Re: [HoTT] agda chat on zulip
Date: Wed, 13 May 2020 06:53:46 -0700	[thread overview]
Message-ID: <CAAjZwAb1mNUDUphDimRxJeUkYJkWq3VpgWYcCxbsgN5Uy2edQg@mail.gmail.com> (raw)
In-Reply-To: <a17e988e-1455-3bc5-03c5-d24c5b07747a@cse.gu.se>

[-- Attachment #1: Type: text/plain, Size: 2035 bytes --]

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 <nad@cse.gu.se>
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.

[-- Attachment #2: Type: text/html, Size: 3558 bytes --]

      reply	other threads:[~2020-05-13 13:54 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-05-13 11:29 Egbert Rijke
2020-05-13 13:19 ` Nils Anders Danielsson
2020-05-13 13:53   ` Emily Riehl [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAAjZwAb1mNUDUphDimRxJeUkYJkWq3VpgWYcCxbsgN5Uy2edQg@mail.gmail.com \
    --to=eriehl@math.jhu.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).