From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 8908 invoked from network); 13 May 2020 13:54:31 -0000 Received: from mail-qk1-x73f.google.com (2607:f8b0:4864:20::73f) by inbox.vuxu.org with ESMTPUTF8; 13 May 2020 13:54:31 -0000 Received: by mail-qk1-x73f.google.com with SMTP id v6sf17158689qkd.9 for ; Wed, 13 May 2020 06:54:31 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1589378070; cv=pass; d=google.com; s=arc-20160816; b=H1yVXWdIAKy4KkCaMYn7I4YDwum2yxz4TFWjxdhl15g6taHO1uE2x+DrNhBzignPuH IXQ3Uv1oA+UCmJDSIq9rsxuo7tZRzLh/u+yogehddeNcKPUxyjbBxms6KQqYMno0nwN8 kCHClZ42HFvvqMhBTUsAgAsl/A7q1JR/+1Phm0zoCrSdhL7+XFLCudX/pqqoYiuEslVx VOdo2WxtzIIOG9G2a3pw3JRAdNhiY17VM0fH6zArkfBWzrEzqep85VeOXSfuOrzuKYEF KkmORVRImiJerhCO6xr/FiNYk8A6+Ssqkbv7XJk/yZKEF9HEKzHaNvm/y0QCYQBzVF7W DO+w== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=BnfOtShByKM6xOZqjo4HXxqI2XiqsHjoFlBMcnmlC4k=; b=PAPIt2KPejQBW0kerJCUBwwqSqVAB6/wIw3J9hhfn3USEEIQB9f+stpDV/WKxygphF NKbN0P4uPgWqZpOFzX0ENuerQi/EnxFHr3YNQk72nwm5YmMe6NB2Sl3fHb4AMZ+Uu6tP c7TavJfKliIjExxXubYhBvqCKaDkHsjbteKCX8LHNCwpH/pRq9Vep3wVhI0HSnH6481k QrQDJYI6kCBw4o+r65gXCwv4W99oU5BtovQQSpazkbdBaq7i40gn2jp6lPf82Jl8MJFe 55r/mcHmTj3sV7ckevPSPRfF8ndZUwZyeE/ZkZIQTQDO+jLM59RNbcA9wqu647hmdegO B6cw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of eriehl@gmail.com designates 209.85.222.177 as permitted sender) smtp.mailfrom=eriehl@gmail.com; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=BnfOtShByKM6xOZqjo4HXxqI2XiqsHjoFlBMcnmlC4k=; b=WHARCsQHgU7zbP7tCvzr9KiLfwpCn7Aorlc5oKt51Hu1v8kxRxYdRiVn0B+Az+lM6s +JEclzJntUe17d0llNcasnsEouI7yIypC1DPYlOpOy6GEJv4lxTML4izOKEIZ5PuRJiJ w4zo/Cq1yzhv46OEnw1y2CO0FjYttP/c3Mh3W5JOow1hOqbsQOVoci3h9VrWh3ZVy1Mt 1BLHEnQIL/yYfN9giWSQfDsIKt13X1/DM+P2Qr9kOlsvLZADEZJX41SdeLFi07iDeWN6 DwMpthUt2vOjJFIpNARs99JC55MUGu8ct6C+bKMJN1c6AbAyiIfvaPqxrggSyb6sfqSE VGCg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=BnfOtShByKM6xOZqjo4HXxqI2XiqsHjoFlBMcnmlC4k=; b=tiKn0xsb1T+cZuEeoUGm8P8UoKyU1TFMxzkG/9kzwPiHPmF71FMnR7bIa0uiifG71Z 9huHVZaZZb+auKXla7zODSLZ3xQI0EOWJIvtMXe2NU8mnopMg4o59Nvt6/Cdj3O9lbJE Yz/1XJEbG7IrcXSLa6RWvs3N8iMcwg87MF6v0cvLmX5PQ9GKjbxOWdzQUa44NL9QDgxN +yN1QGniT42FWOaTuJNSHFZhJ5m5+04FgJWVFXwkNVY9nc0Usv6+eEkF8QRc+1wum+ci RJ6zydZlrlJAWilq/7reF0+37GWCeRupPNj5aSY+DxtgAblMwvPs6fFncos/DtD01VU/ jxvg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530crS4cg3V3PVhy7n0ggPMD85VIaetvwQG6+1gz6Z794EsBVrVb 7+BCVI+mQTCW4SDMBZOr00A= X-Google-Smtp-Source: ABdhPJx+R8ZD6zK0aYJMhsQP/sbkjDmrim5rG9O7oMiPERLvEclwUamlqzSOAybY/I4x5270qYoWzw== X-Received: by 2002:ae9:f50f:: with SMTP id o15mr12824069qkg.177.1589378068434; Wed, 13 May 2020 06:54:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aed:2d62:: with SMTP id h89ls837326qtd.0.gmail; Wed, 13 May 2020 06:54:28 -0700 (PDT) X-Received: by 2002:ac8:19ca:: with SMTP id s10mr1148357qtk.11.1589378068047; Wed, 13 May 2020 06:54:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589378068; cv=none; d=google.com; s=arc-20160816; b=Xa6iGEgGC6AMqDay+b5CGxGHYk9PRDPS06sS6A0ZXo5zpupy5/q9WX1NsIQrh/4y3S WemNGZAR+uG3mzFCtIIzpco+TCyVAiAj1bnXm1Z4G/Fe646obGpJbiczgAsIr0s8vHv9 m0G/I+tt1vMMz3+HaWdHFtv1zwXp+roLHB5mJUd1JbklAw3JG9fnhuHKe+Ew6z9TSCU3 x45u0C77xANWlSM1TUgozoFLI+OUM4Rm8CYiPBf00SxZni+/47V3aRfXoDtczzBGSWDX c1/ZLLqlYb+AUzn8/+NVdoJ+6/6aDU0DnXswL1LXl8wd3FBr+7ogyupxOONpHdpBD8GK 8nyw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version; bh=rJ84bHpgg7xaUIR3WM8juXkeTO2u/ftjDOLGgqjAjIY=; b=BgqU4xrBZ6Fcq9O00HYHjiytKmyClDx671xSiK0C1y3vnjtFLdk1zf1kX4MFqbhxuI zh20nL12mbL/DHJazTnBOCFGYtjECBEYnvTAWBBiaEpxBynw6qyEl6M4Rvp2OcrQBWTc V715Eg/xLNyugY06Bd72jAkEhOPjuIbAZOlbtDADql2+GMO/x2cxxfLYaPovFCf4I0LV 92FdELxVmRG3vnYPalV/xr9VZIvbcXek08QPX0GIyEqlD0uA1sIkwJEfLifKt3xPjKFj 4SsmGMW1Qe+rNVoEQAG9ofu26hEZVg3ABxd1wsDBLIoxMn6Fl3S79M1lnykwR9Aa3E3B uETA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of eriehl@gmail.com designates 209.85.222.177 as permitted sender) smtp.mailfrom=eriehl@gmail.com; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu Received: from mail-qk1-f177.google.com (mail-qk1-f177.google.com. [209.85.222.177]) by gmr-mx.google.com with ESMTPS id v73si875303qka.5.2020.05.13.06.54.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 13 May 2020 06:54:28 -0700 (PDT) Received-SPF: pass (google.com: domain of eriehl@gmail.com designates 209.85.222.177 as permitted sender) client-ip=209.85.222.177; Received: by mail-qk1-f177.google.com with SMTP id s186so15515312qkd.4 for ; Wed, 13 May 2020 06:54:28 -0700 (PDT) X-Received: by 2002:a05:620a:227:: with SMTP id u7mr25718234qkm.182.1589378063223; Wed, 13 May 2020 06:54:23 -0700 (PDT) Received: from mail-yb1-f174.google.com (mail-yb1-f174.google.com. [209.85.219.174]) by smtp.gmail.com with ESMTPSA id f68sm14086967qke.74.2020.05.13.06.54.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 13 May 2020 06:54:23 -0700 (PDT) Received: by mail-yb1-f174.google.com with SMTP id o134so3192628ybg.2 for ; Wed, 13 May 2020 06:54:22 -0700 (PDT) X-Received: by 2002:a25:4289:: with SMTP id p131mr42739879yba.311.1589378062669; Wed, 13 May 2020 06:54:22 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Emily Riehl Date: Wed, 13 May 2020 06:53:46 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] agda chat on zulip To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000d6dd8505a587eaf7" X-Original-Sender: eriehl@math.jhu.edu X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of eriehl@gmail.com designates 209.85.222.177 as permitted sender) smtp.mailfrom=eriehl@gmail.com; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=math.jhu.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000d6dd8505a587eaf7 Content-Type: text/plain; charset="UTF-8" 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. --000000000000d6dd8505a587eaf7 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I think the zulip chats might be slightly friendlier = for newcomers than any of the sources you mentioned just because they'r= e 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 communiti= es with an interest in formalized mathematics, this might also serve as a &= quot;recruiting opportunity" to get some new folks to start playing ar= ound with agda.

Emily
--
Associate Professor, Dept. = of=C2=A0Mathematics
Johns Hopk= ins 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/dig82g= 1cmzd4bqrtp6o3qxaa/

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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAAjZwAb1mNUDUphDimRxJeUkYJkWq3Vp= gWYcCxbsgN5Uy2edQg%40mail.gmail.com.
--000000000000d6dd8505a587eaf7--