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 11683 invoked from network); 3 Aug 2023 08:42:34 -0000 Received: from mail-ot1-x33c.google.com (2607:f8b0:4864:20::33c) by inbox.vuxu.org with ESMTPUTF8; 3 Aug 2023 08:42:34 -0000 Received: by mail-ot1-x33c.google.com with SMTP id 46e09a7af769-6bb0bb5c5f3sf1124983a34.2 for ; Thu, 03 Aug 2023 01:42:34 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1691052153; cv=pass; d=google.com; s=arc-20160816; b=jfe8w3MUjr6b/0vNURAMJEl21hnC3lAfxqZu209IGoxaYsNIcFrkpydmgDdwBctJpl AfM63+0sJiu85LoThDxHJcU4CnAvZ3RDYMm2KqEp1D2gVI8O4IYVwA3QigOkAaY9zrY9 7A3Zuu9pQcyxOWLEZuLLsVaV867O6wZ51h3IhoJ6WOrQL5GKgemSRSgX1xu7SSg4zWiU PnE1YYejrfuM05e7GRmaYI8aQyGAdFfQ9eDyFlSyGTqOz9cXSjnfg/7UroTj7u6QYp6o F7jOUMQ20uMG1s4Bn9cAyIq5cpF4+1aX0idURQOBEqF99Cm7kcWT3cSuS3EchxUX/2Ck BAeg== 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:message-id:in-reply-to:to :references:date:subject:mime-version:content-transfer-encoding:from :sender:dkim-signature; bh=SBA0hz/JcvNeiFIVh2BIfkC+Ue+z+BoCcr8eP4P30W8=; fh=u/Fr9cZM1XutKZ24S1OBSxvC69zq2L3zM8PfkZfME8w=; b=jxHz6GCUPytTOqSe7St1WmLYlXB2Ms9PzQTOxV0e3JNAkMxj3YB2BjfurOP8FwNeBE W8PQ6+HZMC1Gv/yx1vgGOYlYgsv+hR39UGwH7fjA1WAsdq0ulqdqJg+TyF8+hu1QcxQf OnT2sryq/zXBxCRV6cWjirCPTC8I2OsaObcS2sahtv0ykfkTubzsZq5Vq37ybYQb0mzP mRsnXIlMSM3IWKMzdUbFkaXrG/d58+S9Ec+dOEml2xb0b+PHr5A0932BdHZPGJ3EuOTg NHE5Ry18z1kZoOeT1njgx55jX0i2BBTzMoBJ4tOXAsIsZsJDOjLcSi9cgvxLK701ZKfT Locw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=kGE6b4i1; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.23 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1691052153; x=1691656953; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:message-id:in-reply-to:to:references:date:subject :mime-version:content-transfer-encoding:from:sender:from:to:cc :subject:date:message-id:reply-to; bh=SBA0hz/JcvNeiFIVh2BIfkC+Ue+z+BoCcr8eP4P30W8=; b=XiN1umQIomDF8XRbxL8OjZIBSywQ2nw54eLuTBuT+SiaA9WY+6qj2rpbGQl20H76rA p3mPjmm5QULTES2JaV98auuXKt6GGqmMoDxlAARmzKm7mz21L3YYzzxdxO/jPwDkYp9E 7S4c1cyf1Hn9xe9p9GEhasVpTpDc5AunAtaM57eHRB9OF9a6dHWidcc2uqZwYGssElr4 OVsxWPtyFIBmvp4kNAJkdCnR2p2pbE7sdb+av/18or4XbYFeaBECH9eBSOHIBEttUbLW BeK+6Cbi6hy/ARdPZC3IRSoDHbjPCZnikpg/kn6hrXqAnvnRJaqttduRArfQeVuIInpF C7EA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1691052153; x=1691656953; 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:message-id :in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=SBA0hz/JcvNeiFIVh2BIfkC+Ue+z+BoCcr8eP4P30W8=; b=VPwbHVD7uKy447z/IQvWwH4G2QEnpB/NtoNt15R4Tvhm/ClJwwusXAX7RubNShG6ds gE3+/5I+QWHb+BQ7UPpqRP8JsZ83M6+QP5H4aBtesyqvbHIAuL9vdhYYKFYCG/ReUABJ 455dbMnVzoXrNxj2EdPKL/6W6EOVcXZnF/k3bsMxu5dGD1JLijDJcu9szhXVk3aYAKzC QXzmfhjx6SATjsXqeL39xqWMIk16pivi778e4bVZZLUJq1ctB5+3RiDVtUPGDAPr0cao dM46E8Zwk7s187eM52LLf0jLgT4PGpTCROhQhrVws9rocEUfF1kasU1KFaBG2lwg/v61 NYAA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLY9qI+7NOwj6IogODcYcLlc4WG0YyvnRVrzPsTSqqvScs8N7kV2 FuKbNRLtyqyPIcvNnKibKiE= X-Google-Smtp-Source: APBJJlF057ndfUim0lssZujBXFN2ca4M4Q3W4cRuX6ZkEfqyV9UHz0JsKRLoyJKafaGj1WTVozVuLg== X-Received: by 2002:a05:6870:4394:b0:1b0:222f:9cda with SMTP id r20-20020a056870439400b001b0222f9cdamr20956889oah.0.1691052152457; Thu, 03 Aug 2023 01:42:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:ac10:b0:1bb:a4bd:43e5 with SMTP id kw16-20020a056870ac1000b001bba4bd43e5ls1721034oab.1.-pod-prod-07-us; Thu, 03 Aug 2023 01:42:31 -0700 (PDT) X-Received: by 2002:a54:4714:0:b0:3a7:4f8:eb76 with SMTP id k20-20020a544714000000b003a704f8eb76mr15844146oik.24.1691052151089; Thu, 03 Aug 2023 01:42:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1691052151; cv=none; d=google.com; s=arc-20160816; b=C3ssnx9vRCQ5n/T2xJqI2dB3jq+O4ArEyc16fcl+WKvF/mUNULRPSrDG06TTEr73vJ jBmbCQ6F/jGJgpIZO0DC8CDZWPsPL2nBlJVssB4+SraJsZwTgjxrz0tdVVPIvp0T9zvF h3MNN1XHIBJQhgPjEddeSSwPEp9vd3WUCLf7c7D7auJU555cbhES3onc8IklSjE22saJ v5U0NqcWrfWgflr5E9YPfd5LPMKOBj0GiGMk2i9qlt5OHpVuJz4vJ8T1LjmlnfKUHtXm ygrWAeGhLfLhnXyJShOImI41I6Spg8j+I0CXU2d7OpoA2NON9b7VrbTZ49dzWh0BBk4L kCDA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version :content-transfer-encoding:from:dkim-signature; bh=ItmGs0IohO66K61dIv8Q1rE5p0cHwulCQaXFZ1RP9IU=; fh=u/Fr9cZM1XutKZ24S1OBSxvC69zq2L3zM8PfkZfME8w=; b=e1FB9NzBlrY5qS91Hppq/hhBXyfvEsXBVD08KgoTAKXKl7NKvwEVPc9KuJweyL5+jh ZXdCTD9mLu/a0DbfHpSJneaj8p0lIgEq5UFjai/V0OgG9GjQdtt9/LN4DEACti14kXBj FMc7uoK2vtloBmox/GQSB2bbDQFEoXQcJBNv5ZMCcjWmYwXTbfqjo4ne5qLOY/kEJIPw ewQaMOibQlsTHFNgA2c3qagGwpZ+fG2lgZcEEHjYGT6OS7+z34UJr+cOZ8EOMUElLYle PF8pjmqdAJF4jQtYqJgS9efYaDojTnZ7bAMFvZbV7fWioQC3VeyDhqisR9dTKjQD/k58 cuhw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=kGE6b4i1; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.23 as permitted sender) smtp.mailfrom=andrej.bauer@andrej.com Received: from qs51p00im-qukt01080502.me.com (qs51p00im-qukt01080502.me.com. [17.57.155.23]) by gmr-mx.google.com with ESMTPS id pm2-20020a17090b3c4200b00268b0001dc6si163340pjb.3.2023.08.03.01.42.30 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 03 Aug 2023 01:42:30 -0700 (PDT) Received-SPF: pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.23 as permitted sender) client-ip=17.57.155.23; Received: from smtpclient.apple (qs51p00im-dlb-asmtp-mailmevip.me.com [17.57.155.28]) by qs51p00im-qukt01080502.me.com (Postfix) with ESMTPSA id 728714E40121 for ; Thu, 3 Aug 2023 08:42:28 +0000 (UTC) From: andrej.bauer@andrej.com Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3731.500.231\)) Subject: Re: [HoTT] Peter Aczel Date: Thu, 3 Aug 2023 10:42:16 +0200 References: <1670F781-BEB6-45D0-9466-DA546711E329@manchester.ac.uk> To: "HomotopyTypeTheory@googlegroups.com" In-Reply-To: <1670F781-BEB6-45D0-9466-DA546711E329@manchester.ac.uk> Message-Id: <40E71FEB-72B6-4FDC-BA7B-C206FDE54717@andrej.com> X-Mailer: Apple Mail (2.3731.500.231) X-Proofpoint-ORIG-GUID: o3jHpOjnt6L4B-on0uh4BZVw2QsHThzy X-Proofpoint-GUID: o3jHpOjnt6L4B-on0uh4BZVw2QsHThzy X-Proofpoint-Virus-Version: =?UTF-8?Q?vendor=3Dfsecure_engine=3D1.1.170-22c6f66c430a71ce266a39bfe25bc?= =?UTF-8?Q?2903e8d5c8f:6.0.425,18.0.572,17.11.62.513.0000000_definitions?= =?UTF-8?Q?=3D2022-01-11=5F01:2022-01-11=5F01,2020-02-14=5F11,2021-12-02?= =?UTF-8?Q?=5F01_signatures=3D0?= X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 mlxscore=0 phishscore=0 clxscore=1030 suspectscore=0 bulkscore=0 spamscore=0 malwarescore=0 adultscore=0 mlxlogscore=664 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.12.0-2212070000 definitions=main-2308030076 X-Original-Sender: andrej.bauer@andrej.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@andrej.com header.s=sig1 header.b=kGE6b4i1; spf=pass (google.com: domain of andrej.bauer@andrej.com designates 17.57.155.23 as permitted sender) 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: , >=20 > I write to let you know of the sad news that Peter Aczel passed away on A= ugust 1st. >=20 This is sad news indeed. My condolences go to his family. Let Peter Aczel=E2=80=99s contribution to homotopy type theory be remembere= d. In 2012 at IAS he initiated a working group on informal rigorous reasoni= ng in type theory, whose activities expanded into the writing of the HoTT b= ook. Without Peter=E2=80=99s initiative there would be no book, nor the ens= uing success of homotopy type theory. With kind regards, Andrej --=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/40E71FEB-72B6-4FDC-BA7B-C206FDE54717%40andrej.com.