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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11923 invoked from network); 3 Aug 2023 08:51:42 -0000 Received: from mail-oa1-x3b.google.com (2001:4860:4864:20::3b) by inbox.vuxu.org with ESMTPUTF8; 3 Aug 2023 08:51:42 -0000 Received: by mail-oa1-x3b.google.com with SMTP id 586e51a60fabf-1bb6519da1dsf885397fac.3 for ; Thu, 03 Aug 2023 01:51:42 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1691052700; x=1691657500; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:sender:from :to:cc:subject:date:message-id:reply-to; bh=GRI9qB53IFf2pSNlzo6an6ZNdAIqpZoBC9tzRSv8EhU=; b=mLpMW520h9iU8bHt2g6Bkq5zjqBhDkZyKMgOxjfu32J7eSf1X1K8H3lzyb4/YoAvj0 WTMLToLyOhBXCIwwm5cC23s/bKAWk3wKvKxqRYIpDXZtn1MmlwhitrwAhsvtMV9Q1oWf J1JRXi171+Mt3BBkuwliKNF7B+vU0Br9LOgEXtZkoWQgPKXJ4+HsBGP8kpl+LNhff2xI aVlz+QnAdwnmeAiKsKvQyx6w+B5bg458zZj1U0M2g1sOnktIClo1ysVEw09DYSWpSKP8 6M/KG6L/zwFPwlAscFq6MORkGC9j2O7ByGAXv3DPmAcqZ+ohKutgdBIcBg37txhaIOA5 6ulw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1691052700; x=1691657500; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:references:in-reply-to:message-id:to:from:date:from:to:cc :subject:date:message-id:reply-to; bh=GRI9qB53IFf2pSNlzo6an6ZNdAIqpZoBC9tzRSv8EhU=; b=BLNLlcAzrNYVMyrDl8WhoFz7iCbXUPyh+U/ZAhoZ2Z0vacumBniENvT6f3W6tUJqz4 ltAGFlIHlc4EpT18mdYhxICkwBUDspMvkOdwCOh0RWvxEQe7mPqNywlGzTitnoAL9QR9 fea7YZqswkyAqfsT1BCr90WY3rtONRn1xdTdU/GMzHvSNPuYpONIyGZU072LlgU4rGDF lt0npr3crc9uuDHPJJVhoywsIDj7HJoGBT19+lai+X+Av8S+dFO8uqJT8VRzl4h/c6g/ F8X+la+oQ8Tp+wjCFfMDmhwT2lM2Iwzq1LKTp7Q/ICSB71n3o0CNbYNMHdgRdz46AUNY 5aiA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1691052700; x=1691657500; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-sender:mime-version:subject:references:in-reply-to :message-id:to:from:date:x-beenthere:x-gm-message-state:sender:from :to:cc:subject:date:message-id:reply-to; bh=GRI9qB53IFf2pSNlzo6an6ZNdAIqpZoBC9tzRSv8EhU=; b=XrKo7mwv3gQqXwT5AfeqQcj70TRnyEpoGPNjU5rHV998rCUFjA4B7yhDsGRVwfSqX+ klM5zmhvLmtSVkWQJWQ8Dz09U5wipH0vfeXU8O/TeYkKuVolkhW5Nvto/E6wMWMkm3S9 C8J4kb+tIEZ2YqGgCqVO30w0LXi2lXni04olvK5belDXGMZy6S8PHB866oJ+z8EzwTOM liUKjXR5cQh9NFkJ/jqyqLaCtjru0OfP0Ldnbev/TOtngpu2QDuOdb0MPzvySh2oSoVa PYXX2hftE/4s1bJ/K1tBbBydOZQLMpQ8uYuOa8YfcS4bCDXgV3Wr5PzV9oT+ZBJeHbnB 66Ig== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLYnS6PXygC0CvKZo9o80N27o3GnnqvHf8Cr0oBf5ZZNoNyK7D7X Fi+EDotzwBKQd+JMe4hbJjs= X-Google-Smtp-Source: APBJJlFwUuDYfTYd5TZeNSAPsIaMc83jtdVYtDniUU+NnaJe9ZsQm6x4ujpdCpgcZNtA4FOPoLsGsQ== X-Received: by 2002:a05:6870:e24b:b0:1b0:897d:1817 with SMTP id d11-20020a056870e24b00b001b0897d1817mr20113102oac.14.1691052699374; Thu, 03 Aug 2023 01:51:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:b520:b0:1b3:a2b3:6b5d with SMTP id v32-20020a056870b52000b001b3a2b36b5dls76776oap.1.-pod-prod-08-us; Thu, 03 Aug 2023 01:51:38 -0700 (PDT) X-Received: by 2002:a9d:750f:0:b0:6b9:cf90:87a6 with SMTP id r15-20020a9d750f000000b006b9cf9087a6mr16865543otk.1.1691052698290; Thu, 03 Aug 2023 01:51:38 -0700 (PDT) Date: Thu, 3 Aug 2023 01:51:37 -0700 (PDT) From: amp To: Homotopy Type Theory Message-Id: In-Reply-To: <40E71FEB-72B6-4FDC-BA7B-C206FDE54717@andrej.com> References: <1670F781-BEB6-45D0-9466-DA546711E329@manchester.ac.uk> <40E71FEB-72B6-4FDC-BA7B-C206FDE54717@andrej.com> Subject: Re: [HoTT] Peter Aczel MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2564_1363974384.1691052697693" X-Original-Sender: andrew.m.pitts@gmail.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: , ------=_Part_2564_1363974384.1691052697693 Content-Type: multipart/alternative; boundary="----=_Part_2565_1036246821.1691052697694" ------=_Part_2565_1036246821.1691052697694 Content-Type: text/plain; charset="UTF-8" I was very saddened to read the news of Peter Aczel's death. I greatly admired his work, not only for its content but also for its clarity. His promotion of informal rigorous reasoning in type theory that Andrej Bauer mentioned in another post is an example. He also had very nice handwriting! -- I found this out when he very generously shared some of his unpublished work with me when I was a graduate student in the late 70s and early 80s. (He later examined my PhD thesis.) RIP, Peter. Andrew M. Pitts Professor of Theoretical Computer Science Department of Computer Science and Technology University of Cambridge William Gates Building 15 JJ Thomson Ave Cambridge CB3 0FD, UK -- 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/a1e5f28a-165d-4558-826a-6ccec5c2ecefn%40googlegroups.com. ------=_Part_2565_1036246821.1691052697694 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I was very saddened to read the news of Peter Aczel's death.

I = greatly admired his work, not only for its content but also for its clarity= . His promotion of informal rigorous reasoning in type theory that Andrej B= auer mentioned in another post is an example. He also had very nice handwri= ting! -- I found this out
when he very generously shared some of his u= npublished work with me when I was a graduate student in the late 70s and e= arly 80s. (He later examined my PhD thesis.)

RIP, Peter.
Andrew M. Pitts
Professor of Theoretical Computer Science
Dep= artment of Computer Science and Technology
University of Cambridge William Gates Building
15 JJ Thomson Ave
Cambridge CB3 0FD, U= K

--
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://groups.google.c= om/d/msgid/HomotopyTypeTheory/a1e5f28a-165d-4558-826a-6ccec5c2ecefn%40googl= egroups.com.
------=_Part_2565_1036246821.1691052697694-- ------=_Part_2564_1363974384.1691052697693--