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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 26166 invoked from network); 13 May 2020 11:30:04 -0000 Received: from mail-qt1-x838.google.com (2607:f8b0:4864:20::838) by inbox.vuxu.org with ESMTPUTF8; 13 May 2020 11:30:04 -0000 Received: by mail-qt1-x838.google.com with SMTP id u61sf16083546qtd.4 for ; Wed, 13 May 2020 04:30:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1589369402; cv=pass; d=google.com; s=arc-20160816; b=KvfIIXZrXzf3+XgLbMZ5HHPdEbVapFDAhXe+7GpexfPWrtuyB4RYSHOl6TZKmI9LIv a0T22MUw182dSDWKq2/mk1YcLPZyAIQqU6HRKf2inEqgNBQSqKVbVs9KxHp9sjL1GoVo O0k6Hyd4AUwmWZN0cwYw+ZXRfNf9OadrfVEpowwUq8IxMqtelpxv+9z92Yf9OIGTLmkx EWdTvU4JwgV4d0HaxaN6ikGWR5hoNNBtgSIJSxGsQzuQPilXaQoE+LV5xR5YCO2QIOxt F8lyAfd0h83y1Ai1IwDZxC7zXkriin0WGLUJr7dleBJBOvkYbUlASJk25R7s3Qe8daaA UVGQ== 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 :mime-version:sender:dkim-signature:dkim-signature; bh=H+jagZ4Ve6/2Qtsqt6CorfyDhdGe3cq94P9glCJeZbM=; b=rp+6TeTMm3g7AbwwvKlGsM36GjRG0IStMjbub9GbXYaTGJrpeh0rzNyGW2BmzqG9IX fNGGuLTYDY+HfC5fGki670MIDx/J4ZiXLkCeKsBJoYdP4B8NHBUb0Guazr8r6ffGqfBX bGVCpu1G1hbB4HJQWUscpmIc3XzBe4GMilzFEQxQrNjdBkPDRzgKb3/rbMIsZEy1zdat 6VLuIdl2uEBdy8PlFhdugFH+ArimJIPDr5lh6P3rjw6rDUgi5X95tui6fYs0pFgbC4Gq rjcyb7yT2NpPYdppbi2CV65BX8VL8fVi3GkMmKVHjPJRcPWWvSLjnU2I+NcuSro2SXzy ypmw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ayY52nTQ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a36 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version: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=H+jagZ4Ve6/2Qtsqt6CorfyDhdGe3cq94P9glCJeZbM=; b=KDaUrU1ZmDJOxaZqPsjDjsKWfOSOe3EPfXgQcnB+/yr8SABnYBsgXlbSSo142VgHW8 0hKOM+YL5+bxEg0tqPMTp/AHraaQCzKyhnBgrceMKvES2VpQu8zj+szbigHhqH5k3old IdA1Z/Pk8bLMStr0QYtQkqZ+icHZfQ38is+5E/yPiR+IWCpmbXybVY4XFk5QpRpQImyl TUUVRRbV/7XohMhgYKq7PODgUBBO9d5cElmoZSv1AejPLeMV9iY6Y9FcIz4lIqQKRgmM 8XUral9ZkQSF7y11UaqqeW5Us46ocCL8Yz8w31ciG8PoYaXanWuU3wyujvtALqOXnpzh uvyg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version: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=H+jagZ4Ve6/2Qtsqt6CorfyDhdGe3cq94P9glCJeZbM=; b=PatFJPjEefmHQAzxhmoGJBAWQp6Cbm29MPALcZq4ZI1q7D6JBPfqQguuZcyi8iDo+2 W9M70H7ke7i8EyKkU+ZEmq++XDEk4alA+qR8XJjiPP5qj1Ls3QIVEHea3iz48Kh65NGN YKDFgpSg+T3uW4HjpcVbgHlcG73dIAhKQPbUG8d585OKrsV9vOXcXyLiaUIstz5q1BlK fBW+tVR3TAdOxdMcpESS7ZhxwyfOSVCzidgxFF033BjLhdJJakoHYApkJKeMzsWlC58G 45BMyYJWIEou18BGijY1XwrefKjefY/rIWdIDtTBDQK8hVDJaUI6oS6yQ59d1X6imdVz Yr1A== 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: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=H+jagZ4Ve6/2Qtsqt6CorfyDhdGe3cq94P9glCJeZbM=; b=Hz97MGoWg0kiYom3qh5sFZ6ms5TZ6824IF3Gk4B11haU9c4hh5hCXvM+7+KaYZP6Eb hB+2ieOf8PqjHB0uU0gZB7uouwhi4cMm9bkm269wC+19VWaHulJnjIJlP2wviQphdl8o +KEEomuZ4r3hFTGjAmtSEgP91vVIzMJSxEBIDxsdnWuBsqVt65RXEPpGATU2Xjxb4t1S e93AHgagFQfqR5JS83eh9kDrMXC2a20qeudQfH+Rh8YHS7AAMXfy3RWo/frhad93ljhR 6idrq/GGZrRc17t1bMToBmJ3t/8Sx0/mnJKddUReBqh8PnEZ3+URg1cGu1V1abCZqQD9 u3Vg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533sm+eUesK5VZzdV2LiWkvPuDo4EeFDUHVnHax2au8NzfnseRYs zy3OaYc+sdKEE/LqL66ulPE= X-Google-Smtp-Source: ABdhPJzjkFvZ03hdVAFOUeT1xPqGOxRaITaHH4hCxet6la1tjDbjf+2ke94ngzDrm3JLxbyeg/2HwA== X-Received: by 2002:ad4:580b:: with SMTP id dd11mr7366956qvb.145.1589369402345; Wed, 13 May 2020 04:30:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:620a:2142:: with SMTP id m2ls819131qkm.1.gmail; Wed, 13 May 2020 04:30:02 -0700 (PDT) X-Received: by 2002:a05:620a:15c:: with SMTP id e28mr27075690qkn.100.1589369401944; Wed, 13 May 2020 04:30:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589369401; cv=none; d=google.com; s=arc-20160816; b=ffkpwBlB5haGhitoW7t7ATiT/JSUJc8Ia7PwPlcWLfzmaHInCYypN0mC/bQNrXZGmY jWMSj0+/HA/1HeEJF9sy6nD0h0SDJc1YXDx0QVHTiOKyiKR8GV266ZJAxNmwhmJFd7zZ xGTJdZJcgjLerOoNL558Nh+jl2FconOqZuGb4zZ1Fj5UPd+TTv6JICcI1tvb2Nt6Zbvg UuweCQXskXb+6f/qkW6B9Ke6B0H6jjpTeD2M4OEucFdSK6bsB/He+HVmDWnbYLsVgUqU 6kgY/Ca0veqzBInoCmUO3Zotd8GNYaDgJ+fstXZAk4A0si2/D7Zp92sM0Eip6anAqSj0 59Nw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=Bwkyj0izKLD+4Tp50tBcAt61jwPjZKRSvpaHgzfdVs8=; b=PKlqTP5/cna8/IHzOkIQWNiWRRKIw/sqx2TFJ5KgdtHlFUFgD/Cdq9SZj9hAwkNk3l vcvYotH6EnDTzUatEwHJUbbwrzGgiE1W8W5yOAMvgkVSVJtMhghRkgwwnRV7UXxRBL7S OHR4uYbhHYWa0+dcglFo5cm9uPB+bvubDEaUU24PC75A0xVspc9NzEJQwOy6cBgS5NlS J/bQFLBYGk5+Ykpk+c+RQdfu4TXaTZCYoHOZ+eWOUar6R2ibF0Hd23y8eUBv0C9s22/N 3ypyEK0eOD4Pia1AL8G1L2hLkIKiMc27/KmV4w9j44x9jRdYp7C8r7d1k3iqjHKMYSj0 dSlA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ayY52nTQ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a36 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa36.google.com (mail-vk1-xa36.google.com. [2607:f8b0:4864:20::a36]) by gmr-mx.google.com with ESMTPS id v73si842545qka.5.2020.05.13.04.30.01 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 13 May 2020 04:30:01 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a36 as permitted sender) client-ip=2607:f8b0:4864:20::a36; Received: by mail-vk1-xa36.google.com with SMTP id s85so4161125vks.11 for ; Wed, 13 May 2020 04:30:01 -0700 (PDT) X-Received: by 2002:a1f:5fc5:: with SMTP id t188mr11809091vkb.34.1589369401405; Wed, 13 May 2020 04:30:01 -0700 (PDT) MIME-Version: 1.0 From: Egbert Rijke Date: Wed, 13 May 2020 13:29:50 +0200 Message-ID: Subject: [HoTT] agda chat on zulip To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000096753b05a585e634" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ayY52nTQ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2607:f8b0:4864:20::a36 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --00000000000096753b05a585e634 Content-Type: text/plain; charset="UTF-8" Dear all, I created a zulipchat for agda. Feel free to join! https://agda.zulipchat.com/join/dig82g1cmzd4bqrtp6o3qxaa/ With kind regards, Egbert -- 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/CAGqv1OBOVKUPKaxDb%2Bhkx7n%2BbFMqpEDkRjWTD%2BXds_x7y47CdA%40mail.gmail.com. --00000000000096753b05a585e634 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

I created a = zulipchat for agda. Feel free to join!


With kind regards,
E= gbert

--
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/CAGqv1OBOVKUPKaxDb%2Bhkx7n%= 2BbFMqpEDkRjWTD%2BXds_x7y47CdA%40mail.gmail.com.
--00000000000096753b05a585e634--