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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 5087 invoked from network); 13 May 2020 13:20:00 -0000 Received: from mail-wr1-x43e.google.com (2a00:1450:4864:20::43e) by inbox.vuxu.org with ESMTPUTF8; 13 May 2020 13:20:00 -0000 Received: by mail-wr1-x43e.google.com with SMTP id 90sf8585409wrg.23 for ; Wed, 13 May 2020 06:20:00 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1589375999; cv=pass; d=google.com; s=arc-20160816; b=gyPwZsdKrnwxl6Hb6mrITZ4wCRbtWcFAXTRArwwHA39r5N2XxbRYztuhIREhz6K19x EPRJmwOcA5sqts2nqsGcexN0RgfGC+5zPTnujJ2fhnOQ2mQVBQmkFY92EWFsxzEh08Un TJ4P9XBKKTPfZ5zQM8JO1pegxT5Y+0e12p7ntNQgFOL4F2eG6zjmvVbEPGRp++Q6Ulb/ iLiHc/lNjvvJ83PhrPEhzxu03GkPNOf0DA9khqaP4x0k3wTx5YRIdg48zegdO4HjpWqO 5X4gkIosjcVefTX6ExoF7Df4jBgLCViWeNWuqkGJwHWZzYbmHPsWkJ42/lfcLRtee40D xoMQ== 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:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature; bh=QVKr4fB6mbYMhgPIgnTR6eicPOMKRFV3mMnGS5TPkD4=; b=gRycfhFuWWinidNW4sCgIGga2mG5vtJ75IhryQUPsyxR8Edpv5hvPIAY3uDpOQone5 enZJK81DN9xLVxd7KqK3YOkX91Lt7rhmaXjbqLTgCh3saAImQtTxQQiDjDbybONvW0xw 6Mz5vpf56yOEje01AWnY9cNvlHinaXhcURN5g/zhP2trueR5pBgOwWRN6fpM4fpB5Zdz Osg4MgyWEpNQV4nLLNHM22dbP0wfU5QtBgmhUw2MZK2vcj6qgqfl/TiFo3ugy6xbj2xU JO9VDWluGCDIo6aZe6aZOV/VnuCkZ/l7IkLSjKk8K28E3JnHKQcr8pZzcCtSptxgSro/ /dJw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=QVKr4fB6mbYMhgPIgnTR6eicPOMKRFV3mMnGS5TPkD4=; b=O2zOwNkm2ndrSgLVKZIYzpP3KBdXtR3d4zHXBgMeUOrXvSqk4/Z86DUHT8GGOAe7QC LduYgqqG/g/32reUGBnUoorfz75I86nNIEsMOnophf9JI83yjVeDBdq5Gbtu2skjxQIb VrRDrGR+K4+gLTU01iMhW8+Yx9CKp1/EYL4eGa32SltLqpoPG4TailkALg35oOlTwAMB D3+Ilq8KreON3EQJZQ4YxTpnbMzuHT1aDpDA4rX/EJbPkzdVChMpAuU5SCbs0sbkYbEL soimLmB+PcPtfs2pXJgG2OXvQC7ytaeWsLxgMGgDGuelC0l5itBipjqz8nVSZ1ksytqO P4aA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=QVKr4fB6mbYMhgPIgnTR6eicPOMKRFV3mMnGS5TPkD4=; b=FVZ3TBMp1S7HSG1xMY2a3ip5NsDjrjAf7xvLBVYbO8/zTJdXCFa5U30Xf9QHqHBjSI sHwtBuJ2ALIWydtUOI7Qs4wDyfdwU0Qc+P7C6r+bLnTAL7pSSdDAaGSmykWfpByl8wmo Rkg931s0+jIggsJzo5VK13K2j3CacG/1+QiefoAWwjxkPe22um0nncUeYqDKbvwDfnbG jP+DvAR/5cMAAcBaTc1wKkW2fhlwHIDuM1XSi4OcUIMd4i9x+LpCmn2A07vpuER01xEG /KnMj79P1s0v6VCVgyAwcU8nZVc9QD7X7trEOhfjQYl92bG7Bh8/t4BIUDEGZxLEpIXl BHRg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGi0Puao6hhZkYbI/WLIXxItfi8XQl5itBngomhONFLgMhAxeDAYqiI9 Ni4Kakvgwuyj6QVpNzAz5Oo= X-Google-Smtp-Source: APiQypIhOhZL2pjFWHy+53Y+QmRZN+og8VhLtXtdx7cjkPnkAAWkIeLBCPKw2mHNO3DBYDTdcxWVGw== X-Received: by 2002:a7b:c24b:: with SMTP id b11mr13559155wmj.101.1589375999483; Wed, 13 May 2020 06:19:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:4103:: with SMTP id l3ls858362wrp.7.gmail; Wed, 13 May 2020 06:19:59 -0700 (PDT) X-Received: by 2002:adf:84e5:: with SMTP id 92mr1283083wrg.341.1589375998914; Wed, 13 May 2020 06:19:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589375998; cv=none; d=google.com; s=arc-20160816; b=m0vTKgwJH0dwnj9pBhZKvbScptiLFsm1R2/sHQ3NcyrBfy8DO4pOo7Sr5LUFn7kse2 AkzWXFHRBi36w87yrvu/gVRwLl3tr1LjKPxXVTPXEZIuLDiSINqIStTaBYhqg5W+ypmI jlk31Yz6kf8L7UaN93/vi4Iar+VO7PzSEMLJ0hG4T0UADs8bxc9oh4Px7XrS9Gc9YngY My8TsbvcCFzP4yiJTiUyLjMTgPUCqTZGB2526LO9TInTAPfhCjGZSQz4hKbhNMgsy6Wz Qak2C6VUZE8s6xSxI8TBuku1xvvQXVNrqfTsLO+2hcY9PVYgF2BDTKLaH2Q3oS2hriXJ cM9Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=hehy0gS5sw129eTWNrzxJw1jTX1thLB+8T8CCjRtZug=; b=vKK6h7cV8Dqdyddnbf25U8R7ZAhCE9v312BjQD+sBM7n8QQ1POSPxn0PQqvPnXuhEv Au5Rz8gNhN+rrs35QQm7/fwiU4Yn22GdwfoTrhp8ldrJWaN9QGMIxtzDm6g/u9vdZrlF wlaeEJrvYF0cBlrtbXL6ywiqDsQfJHCc7nYHhiTr+JUaS3k8q1F7F04Cfid6N1g8gdYK 3fAbwXJMIZVDAkaVwQ5DS+rf6DkZspx8V0U1BitTd7POgY2gnE563+3//TKzkR1JoiU5 Tt1rDJhSAnVKhtVtzk/0xRj+W9tqbX55AwyE82uF+kFel9iGEMmDee7Y0OpeadFRMidy fJ1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id a22si1036879wmd.4.2020.05.13.06.19.58 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 May 2020 06:19:58 -0700 (PDT) Received-SPF: pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) client-ip=129.16.226.131; Received: from [192.168.1.9] (129.16.10.245) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1913.5; Wed, 13 May 2020 15:19:58 +0200 Subject: Re: [HoTT] agda chat on zulip To: References: From: Nils Anders Danielsson Message-ID: Date: Wed, 13 May 2020 15:19:57 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Originating-IP: [129.16.10.245] X-ClientProxiedBy: tyrell.ita.chalmers.se (129.16.226.132) To stark.ita.chalmers.se (129.16.226.131) X-Original-Sender: nad@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se 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: , 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.