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,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 26210 invoked from network); 23 May 2023 11:58:15 -0000 Received: from mail-qt1-x83f.google.com (2607:f8b0:4864:20::83f) by inbox.vuxu.org with ESMTPUTF8; 23 May 2023 11:58:15 -0000 Received: by mail-qt1-x83f.google.com with SMTP id d75a77b69052e-3f39abae298sf51468781cf.1 for ; Tue, 23 May 2023 04:58:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1684843093; cv=pass; d=google.com; s=arc-20160816; b=PWLLZ4coa23S8jEhxFit4f7RzJeA042qeA0Ws4S7zvbwswRc3a0CHFxPqvbdf8ydqX 3Jva8ZtcE3L52HcJVoJC2MqScVDacf9Z4o/hp/80SPEblF3UrSJ2ynWZI333JgvCCtDx Mg3oihdtWB30ZW642CRxI1M9guDaxIPJy/ROeWpIKfnDjFsjW+7o3iiK1vgOCZfpd3/b nUypkKTqQQmaeZ1QUihk9L6GYEaX8Kih+8QZpyp9pGHbIPxwCL1xa+Bu7tolwl97VVDh wDpDBR6zXznbx7fNzbDZbVJPdt2d77FtrXkzqkz86s8It01KR/eemrZELm7vHaaZFelE UufQ== 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:message-id:subject:date :mime-version:from:content-transfer-encoding:sender:dkim-signature; bh=+IrynjtvV5SPejWW9w1lt5VS7XblbsX3KGabZutKW+0=; b=tRiZZBZauINwGKOBxIBwQO1cAuRnTCqFZvHB5ej5F/ar9bfPqHEpmz5H6RuyjAOwIC WJxcLGlZUdwflxkmgnNZNTOUZJw2GaI3zPA+cXdQkzZrtCzHGvtNHCe9lwgadvWd5KW7 HctUuXKMlzhzMhVVjD6yWsZaze7cNkKpm7NoXs1XwvuoS0OVSrYoRhgky12zgJmD3hvV Typv3wsV/on603AZ9YO6jU734qivhNvsOtaZl6zaogsXFMLO1glr6J+O4OuZL7E2ncYO cZ1X5uEMcJWKzGBdloAA+zJx9+LfinAVpbwp5BmUrm5/SID0GPi+ybXvBjVrxKvcSI0d s0uQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PLOcnMx4; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1684843093; x=1687435093; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:message-id:subject:date:mime-version:from :content-transfer-encoding:sender:from:to:cc:subject:date:message-id :reply-to; bh=+IrynjtvV5SPejWW9w1lt5VS7XblbsX3KGabZutKW+0=; b=UiMFoUPQVsSEkGsQ6FCUDINz2umZcRw/lH0F+/BhA1sUImmkaxEvHB2+sy3L67ZeJh ZkjvHzARfmrsZb8PMBs5i43lX5lybVzKZBQKyYOnYllowHqr3oTIYbQosMkoVrrir6vS A23icFWEPpJ5LwMF6vw6+NmPpofL74bbe+ded8kVmZmaNWcKRRg4l3H71c6kkeO83e4e eySoBscIfzjLD+eshOIfhNyeI8P1sY+dy1lJ2V1LWxuJdM1Dv/5WsY6oMpjvdiWUVrBW d0zmrXVoZpfw/eH0BhI7bav7b6d1Zz5HhrOfm84aeanDlhYix7Ke05MuVp6eH1jhCrvD XgvQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684843093; x=1687435093; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:message-id :subject:date:mime-version:from:content-transfer-encoding :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=+IrynjtvV5SPejWW9w1lt5VS7XblbsX3KGabZutKW+0=; b=ECLPlErl7GQIL/XRKDYkwPkD5HEj5FpoqGWGcf09/uOxds7R1g8fFoARBHm8VGairf nkebKBXVBNt+qGx6CjKqjwB4pc2lOVZ/D3iu+B5y21PGWPI4AmBZdWLnlpI4bsnbpb6F N3OUIS5r/yaJK4zrKS9387PbrHPOXht3S9EQUOCumZtuGujtzSyU93iMime4uaaS3NKt fJjDRqEI+cWoxHNlF6+Tout9XHy7WK7qAd5kxihMdvpR3w9mIzPA5cpSrNiatbZX+Sqo 0vlDkqs4yqodKRTAY8XlezwYEiwSZOFFm4+C/BbhPqgETwE8pjzzQAahwlWctk55BGbb +lVA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDxwvZOwZTLOFSPkQv7Vzx8JXOGQnb0GTWDvfW7DguBLAaOXIIxu X2Y6W4sfXEANXhGQIuY3BaY= X-Google-Smtp-Source: ACHHUZ5I9Io2IhP+zFuHrBt2muQ9hM8QEY6DEt9Q3swne1HzGMZ5G8tynZVU9S97tpeKXC8kWimUQQ== X-Received: by 2002:ac8:5c05:0:b0:3f6:b1ff:3b9b with SMTP id i5-20020ac85c05000000b003f6b1ff3b9bmr1854784qti.9.1684843093102; Tue, 23 May 2023 04:58:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:48c5:0:b0:3f5:3b17:86f3 with SMTP id l5-20020ac848c5000000b003f53b1786f3ls6541522qtr.1.-pod-prod-01-us; Tue, 23 May 2023 04:58:11 -0700 (PDT) X-Received: by 2002:ac8:5bcc:0:b0:3f4:dc79:1a6e with SMTP id b12-20020ac85bcc000000b003f4dc791a6emr20339618qtb.19.1684843091916; Tue, 23 May 2023 04:58:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684843091; cv=none; d=google.com; s=arc-20160816; b=Zih9fIxZ0obNsD6rBKmEbGvowZr6yxx2/GxXVeWPkcm3qsmvnAAlPHh1bQ20bcE1nV ID0x5YGVM/meYo+W5W8bWLxlYF9voWEj7AEWjzQdpEHSiZYS3ZKBv7n/ouFPwSVhRjnn v/5Pgla9Aw2s3eao7O1lnH9w4pEwYIt6T27EhVTsaXEWKy+RU7IXcMo/13WzZYA+aYw5 lwkV5ufQsQ2NU8eeeUF6HlFAjf30x35kB+XgtAL3a2CynNqs7/0FURhptHCKrLpaCtOY u1qrcATenirfUF6WdTvmaizqFUcf598hFeSNgY+MRRTylDZU499GD9mAN/max+IzHcqY 0z2Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:message-id:subject:date:mime-version:from :content-transfer-encoding:dkim-signature; bh=50e9W5UeH4PnLedW0QWtn8wCChjxldi+hzo/C3OKkiU=; b=N6HouwV8y+nNCbqGsehVGQ+3V3SnzbMVE9z8HkP1m3A5Lmmc0pUMwaoZza/Be2LNpU qA9B6FWJemCnxypbyENTW55y+hD7RWtQ0UyABp71JkQ5WxpMSj9yfqB66Ukda5C/uu0E DQPFx52HOyVuQ/qCJIo1zLV1p+hb4+x8mGNFazOg9dPyChps0ODjs2dfBrQ1sP7qgJQk 7m2zxcpsRYkXiUxlGkAg8Pm1KN6vTPSMA54yuWhSNIvIzysij59tcVwvl70YwfFemhX6 Ug1pc0U8z3fmT1sCiCuOne4bOC0+F0QCpFLTJ3U63nVZzrDSwStTivh3DwElfd0XZYl6 9jMg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PLOcnMx4; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qt1-x82a.google.com (mail-qt1-x82a.google.com. [2607:f8b0:4864:20::82a]) by gmr-mx.google.com with ESMTPS id ge15-20020a05622a5c8f00b003f6ad166f0csi528727qtb.1.2023.05.23.04.58.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 23 May 2023 04:58:11 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::82a as permitted sender) client-ip=2607:f8b0:4864:20::82a; Received: by mail-qt1-x82a.google.com with SMTP id d75a77b69052e-3f6b94062f3so4072971cf.0 for ; Tue, 23 May 2023 04:58:11 -0700 (PDT) X-Received: by 2002:ac8:5f82:0:b0:3f4:e7e4:177b with SMTP id j2-20020ac85f82000000b003f4e7e4177bmr23390247qta.18.1684843091248; Tue, 23 May 2023 04:58:11 -0700 (PDT) Received: from smtpclient.apple (pool-96-235-63-8.pitbpa.east.verizon.net. [96.235.63.8]) by smtp.gmail.com with ESMTPSA id n12-20020ac85a0c000000b003e302c1f498sm884790qta.37.2023.05.23.04.58.09 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 23 May 2023 04:58:10 -0700 (PDT) Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable From: Steve Awodey Mime-Version: 1.0 (1.0) Date: Tue, 23 May 2023 07:58:09 -0400 Subject: [HoTT] The HoTT Book is (almost) done! Message-Id: To: Homotopy Type Theory X-Mailer: iPhone Mail (20E252) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu.edu header.s=google-2021 header.b=PLOcnMx4; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::82a as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.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: , List-Unsubscribe: , Dear HoTT Book Coauthors and Users, After 10 years and thousands of improvements, it=E2=80=99s time to close th= e book on The Book and declare it officially done! That will happen in a no= t-so somber ceremony to be live-streamed online from HoTT 2023 in Pittsburg= h and Mission Control in Ljubljana at midnight CEST on Wednesday 24 May 202= 3 (let=E2=80=99s say 11:59pm to avoid the ambiguity). Please join us to celebrate the occasion! We will use the CMU HoTT Seminar= Zoom: https://cmu.zoom.us/j/622894049 Meeting ID: 622 894 049 Passcode: Brunerie's number And let=E2=80=99s get those last pull requests resolved people! Univalent regards, Steve=20 11:59 CEST=20 ~ 6pm EDT=20 =3D 10pm UTC --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/C51B71F1-2843-4142-ADA5-2B866D1B0EE6%40cmu.edu.