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 3460 invoked from network); 27 Apr 2022 11:00:59 -0000 Received: from mail-wr1-x439.google.com (2a00:1450:4864:20::439) by inbox.vuxu.org with ESMTPUTF8; 27 Apr 2022 11:00:59 -0000 Received: by mail-wr1-x439.google.com with SMTP id n17-20020adfc611000000b0020a7e397ccasf593186wrg.23 for ; Wed, 27 Apr 2022 04:00:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1651057259; cv=pass; d=google.com; s=arc-20160816; b=jD8BjAc6K28kCavsPJHo3PhKQSA/k7Kkrsu0/hTvjEBcyWq8tbCAGOCsc91+y0AQDE Hgp1nBZmbMSlbxA0WO7HPlbWgn+cL8LTIkSDkyBiooHc/7MzFeSzFH4YiBrfZhj7ALnx QI7ito3Rr8eGdL/omV4hp0bLtGv29KnUPBySxzngeb27BkoLZQGiHiEefzVX5+cjXnsx uGizCzNzsxu4V+p5uwpg9aAgyLcYjKMguOalNGq9f8QfdYwEXd8xWfmEQNBo5HriAnhm CMLOpwwJ4d3NNFUwNeG7hgTqoS1+Gpg20blSSs/6tXUepO+hjlZx3URg/QvThztzRizN lNAQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe: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=hwFKdS0TaurWUHR+TokqS5jSCuWwO1BIQzQEGRwl9Uo=; b=iIVOFH32oBfzLLmJzKhDCLEX/gi+C/93Jy9ClnAd9EwjcW2LrkyvDqOFSgkVJuglmd 6/hD5LkVicu7yyzzJDWwN92ooc3gzM0aOAjm+JcnoODc05Cg3NwNSM2KpttOHiFQZRIP E5PDHW/m2UaS+Ym2fFZ95bfoFcgxZt6qi5HG7VzROvhbBpMViD+F63BV+4eBcCVqTlDu I6aZzLViKHhxFmuuLoo/g8yWHdwO0mZoayTNs8oaWedz/vNpCo4yI91Z+MfEsPV8LxUZ J7T6hk+d9D2QvvjAzRaS4H+Zw0pmfJN2H9djjGNYphlgoo+fRGUkoYbZ3nOlFTNVJe8x DwyQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20210112.gappssmtp.com header.s=20210112 header.b=69cv8Vm3; spf=neutral (google.com: 2a00:1450:4864:20::12d is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; 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-subscribe:list-unsubscribe; bh=hwFKdS0TaurWUHR+TokqS5jSCuWwO1BIQzQEGRwl9Uo=; b=ExDIV+QPq6W9vmqGlUkKkGp9zVOaa9JDlFdOPQRupITf10+QeLwcdK1jhDUScMYfpa tFETG2GUR47y11lJy9yPm66VwEnuRRVpcHm0qyl8sQdKRB6H4kGYGUYWi0JNj99TLDwH Mqhw5C5ocjF2rtoJ/YXWDyeSsNG6ZBK9IhR5N3S+rzqsjtB+L18RRYT2+jdGZNaM2T2v G45D3lGtqmJEEvrxxwS/qILQkKWR+Z1CzOnsRywARXRSvp68NBW1IQMyZGj2Imk76opw XlNZd7utNBLALF8KE2SckbDdD+Lf84TT1OzV6SXxaS7ngjfgUydLlheIVNM76Pr3HGoJ HkrQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; 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-subscribe:list-unsubscribe; bh=hwFKdS0TaurWUHR+TokqS5jSCuWwO1BIQzQEGRwl9Uo=; b=HPQ7N6EGxLJxeTCNgOdu4BRBV/M2x2Q01yrZc9cWSL/e+1lCdWscfXhhEv10k6fBe9 e+vlEDayg3FGafYKDoS88J5NdArf+VychI6vUZPdWtz9kl91NXy+wSrU9LHhlnsrScJl EPfycwmwjhdqWUG/sSHLYdaMVnjUKdv5lzgh6OYgK9+XtK3s68iX52JjiPjCqeV7WyCH UrJxhyMfABN1n37Pl1AukpNXXcio/WJX+1qZ/gzfyAPKJ6j360gZJtQ7bz5LMxAg8qZu PepvWmjDrakOTTkCn44kb2u0N4/G6qC1IpcwFm1DG813YNrPgb4bGyNnb5A38IfgYO9U zwvw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530Lxaqp0A/3xBmqDa3cNGiFBSPT8YFpX9wp8272/49YjdM5HNuU jTb3OP/y2zzAlbNtX0C12xU= X-Google-Smtp-Source: ABdhPJxkSt49qltXUi4Wiyz2JEqH44N6jnCdrlsZUkhC7FOsLOpfJb0FLgXIJd1hdjXiGwwVYSrCjQ== X-Received: by 2002:a5d:6486:0:b0:20a:93fe:dd09 with SMTP id o6-20020a5d6486000000b0020a93fedd09mr21948624wri.436.1651057258921; Wed, 27 Apr 2022 04:00:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:4f42:b0:393:edbd:e7a5 with SMTP id m2-20020a05600c4f4200b00393edbde7a5ls872323wmq.3.gmail; Wed, 27 Apr 2022 04:00:57 -0700 (PDT) X-Received: by 2002:a1c:7408:0:b0:38e:b7af:c503 with SMTP id p8-20020a1c7408000000b0038eb7afc503mr34951749wmc.58.1651057257201; Wed, 27 Apr 2022 04:00:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1651057257; cv=none; d=google.com; s=arc-20160816; b=DgS4P/rnBsD0uuMxTNYOdpWxbAOs1SqFze0BWkB3IgEEs3YFv7z1QP3n5UHAK+JY1V gWKgCtorQcP88vRxtATXYyO/uDZW8A/6+0aVOnsebrBpAwsmQvCsMKhoLAVbh1nnnV7e FXOtUrt8YzTJYe8nX70ZpNw1sIaGwWqDQFCMjZ+oNr+XCR9JU6Ot8HsP5UZXlEDkWddn HX+kfhshbw5YmjbhF1lCoKExDOCLcpdQfaeRMgab+gAhhXiafHeS+WKMST8hoWrU050L MSpR0/orQA4g92AzZGFMlDhKUkXSZBW4P72AGfggkQwLZk3/PEfxrcU3/B9R7EtSPZmc 0mHQ== 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 :dkim-signature; bh=waamImDgGaAKwu2wrmpivGNg42jfeAVooH6gcaFkLMI=; b=znNonxzFRN1IjRuUBmzAGnmsJDjrM5Pld6CAuZG/xkm98elXPKY/PmwwUjiTGB5ywg FZt8rwQmDrQzQ/8ujdt+ZRX7ahFmoBL3WW/zK4g0Sr9bg0c2wdFPE/ghWCoDgOv6nxrU tF8PYTB0r6OJFAX+HilMbi4jqbq5VqxVW8NuvONpa8eNLSeJjfcoIYhuLfHM7mMF6sIB Px2ptxW+Eki540pBUlj5Zg6VYvH4jqF/WwnMQWT/ozVPCsIy4VIGG8tiyZdTw5W2fK8p gvLhPYBP+PBBjIPw3cyrJ4t87kBa4YEX8MCwBIYWzp5MjXvDDVhhYWWcRURtDmXu9GXY LBsA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej-com.20210112.gappssmtp.com header.s=20210112 header.b=69cv8Vm3; spf=neutral (google.com: 2a00:1450:4864:20::12d is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.com Received: from mail-lf1-x12d.google.com (mail-lf1-x12d.google.com. [2a00:1450:4864:20::12d]) by gmr-mx.google.com with ESMTPS id d23-20020a1c7317000000b0038ebc691b17si347192wmb.2.2022.04.27.04.00.57 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 27 Apr 2022 04:00:57 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4864:20::12d is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) client-ip=2a00:1450:4864:20::12d; Received: by mail-lf1-x12d.google.com with SMTP id j4so2446837lfh.8 for ; Wed, 27 Apr 2022 04:00:57 -0700 (PDT) X-Received: by 2002:a05:6512:11ef:b0:464:f033:5a96 with SMTP id p15-20020a05651211ef00b00464f0335a96mr20138057lfs.82.1651057256213; Wed, 27 Apr 2022 04:00:56 -0700 (PDT) MIME-Version: 1.0 References: <876f6e58-211c-4824-e938-4b915e18d859@fromzerotoinfinity.xyz> <6A66F50E-FAF2-4C31-ABA9-835ED4FDE345@gmail.com> <776cef63-67d8-4413-9cf6-c005e548c386n@googlegroups.com> <065d081e-b470-7f00-8090-a8cd15ed4592@gmail.com> <8d56b68f-2473-4f50-9d00-28cc58fbd8e7n@googlegroups.com> <5595508f-15bd-42a2-a350-103647bfac1an@googlegroups.com> In-Reply-To: From: Andrej Bauer Date: Wed, 27 Apr 2022 13:00:39 +0200 Message-ID: Subject: Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000042c31905dda0b993" X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej-com.20210112.gappssmtp.com header.s=20210112 header.b=69cv8Vm3; spf=neutral (google.com: 2a00:1450:4864:20::12d is neither permitted nor denied by best guess record for domain of andrej.bauer@andrej.com) smtp.mailfrom=andrej.bauer@andrej.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: , List-Unsubscribe: , --00000000000042c31905dda0b993 Content-Type: text/plain; charset="UTF-8" This mailing list is a community service. The present discussion has run its course and is not contributing anything to the community anymore. At present its only purpose is bickering and reiterating of opinions that have already been stated multiple times. I am therefore locking it. The mailing list owner, Andrej Bauer -- 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/CAB0nkh088mBUrQ3eQyLPFD1xRkoHgF9G9oHiMgELTaxw3h18bA%40mail.gmail.com. --00000000000042c31905dda0b993 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This mailing list is a community service. The present disc= ussion has run its course and is not contributing anything to the community= anymore. At present its only purpose is bickering and reiterating of opini= ons that have already been stated multiple times. I am therefore locking it= .

The mailing list owner,

Andre= j Bauer

--
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/CAB0nkh088mBUrQ3eQyLPFD1xRkoHgF9G= 9oHiMgELTaxw3h18bA%40mail.gmail.com.
--00000000000042c31905dda0b993--