From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6830:3150:: with SMTP id c16mr15757497ots.251.1585746624072; Wed, 01 Apr 2020 06:10:24 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:467:: with SMTP id 94ls1642918otc.11.gmail; Wed, 01 Apr 2020 06:10:22 -0700 (PDT) X-Received: by 2002:a05:6830:1e10:: with SMTP id s16mr16619274otr.222.1585746622681; Wed, 01 Apr 2020 06:10:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1585746622; cv=none; d=google.com; s=arc-20160816; b=dM9vNQdwRV4jyiA/6VKGxEI/vATm/5pzucbo8nFwO2E9npHsiCTD5gBvbWGvzQqrdg Yq5l6SULq951jbE+yn2KLmvEXDPlDYUmcWKInmrUqxt9lPg1JAxmRODXetfexTZmXiF9 sUqOxlVsmiSglSVNhgxvAvbWlQ/Q/+C1BKTcCOsHaupm/eHQaQwTFarPmxyx641zn/5w GkO8n9UdkqvNSIakidEALmP68jlgipyeWGe4Z8PYX9tv3f88/ZdPlRuyP2TQFanWmjMy uVF1Rt6q99r1sIAAvGQU3BSq4R9Zv2qlxxF/WqpSUDZ+RfEENzRtIYsevwicj9K86l1l qDyA== 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=UO7fc3zblcLwdJItaZkxMN2vLOZpfFuRd6Ba4hRtxwQ=; b=YQJydAXVTbEtqf+lRuNBxDYDMQxp7Mnciw0c35EJjYyBSnCEqaeNsigA/3IhuEJwk6 R+QxUrut2rEuwxzz3zViB0kWECjwzUQLx9gSAoreqvxpG1COpRT3D4h1MU0a7+QEpTVF F2n36kJSCI6yZHULozafAee7YXRrFqew31A5kgV7KC5CWzuKIQc+Z5LPwYKNZDfRsIJd CUapMQ9S1CYV3SHKcdKi5DeBnSc1+aYHu6vTO5KC5XT1rizmqGEOIanxnl+xrupOM7ir YNaudJ86BhyP5vFUWPFYD39kO3215q59rN3DgJarn282H1MPU/yT9c2X36ddsXF2Zeq1 /VJA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=t++eyjIQ; spf=pass (google.com: domain of b.a.w...@gmail.com designates 2607:f8b0:4864:20::b2e as permitted sender) smtp.mailfrom=b.a.w...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb1-xb2e.google.com (mail-yb1-xb2e.google.com. [2607:f8b0:4864:20::b2e]) by gmr-mx.google.com with ESMTPS id d11si133124otk.5.2020.04.01.06.10.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 01 Apr 2020 06:10:22 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w...@gmail.com designates 2607:f8b0:4864:20::b2e as permitted sender) client-ip=2607:f8b0:4864:20::b2e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=t++eyjIQ; spf=pass (google.com: domain of b.a.w...@gmail.com designates 2607:f8b0:4864:20::b2e as permitted sender) smtp.mailfrom=b.a.w...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yb1-xb2e.google.com with SMTP id 204so13189141ybw.5 for ; Wed, 01 Apr 2020 06:10:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=UO7fc3zblcLwdJItaZkxMN2vLOZpfFuRd6Ba4hRtxwQ=; b=t++eyjIQ5EL1VHstznKCbuausTxEOC/qr6bJD/eKRvb90Hx3NZKK6sXm53MzKbjKGK ozWGh3+vlTyUa/rAzb22yCkfBj3YEKUfTYwqxr4XTYjdyy5+x3weKn7Z/gisrf7NF9Pv hMT9Tiqh71qgBQO/bwRKCYnjKrvCXOwbVin0C559KVVm+cQJ/RW0ao/MUiLjLquiKlTy b0wA4CAc03kXjsjMgNWuGcgv37/J8mnBYhAzMVqUMnUK0uPTJ6gD6PXV53YhBHpdFpV7 KBjC1JrRi/BEA/acUZ6oQuWZUCb56TXJ3wl7JT25sMcrTTtzFQ8/pUm1xxUaKh2jiuYq avDg== X-Gm-Message-State: ANhLgQ0Tm4e3arcGS7aqcUMv41j+vEboGZTgpkJkiqLjriC2feuQWtyo LTiLWDkJHh+IshXraAHRtKB+etXQxGK+xSLPw9SIe+BpF3Y= X-Received: by 2002:a25:d9c1:: with SMTP id q184mr39655260ybg.349.1585746621573; Wed, 01 Apr 2020 06:10:21 -0700 (PDT) MIME-Version: 1.0 From: Bas Spitters Date: Wed, 1 Apr 2020 15:10:10 +0200 Message-ID: Subject: HoTT Zullip To: homotopytypetheory Content-Type: text/plain; charset="UTF-8" With Johan Commelin we started a HoTT bulletin board. The interaction is a bit faster than using a mailing-list. People seem to be enjoying it: https://hott.zulipchat.com/