From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, MALFORMED_FREEMAIL,MISSING_HEADERS,RCVD_IN_DNSWL_NONE autolearn=no autolearn_force=no version=3.4.2 Received: from mail-pf1-x440.google.com (mail-pf1-x440.google.com [IPv6:2607:f8b0:4864:20::440]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4f18025b for ; Mon, 18 Nov 2019 13:26:48 +0000 (UTC) Received: by mail-pf1-x440.google.com with SMTP id w16sf14103664pfq.14 for ; Mon, 18 Nov 2019 05:26:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574083606; cv=pass; d=google.com; s=arc-20160816; b=KlWQN8w2XbE8XBlPLA380iLFCQ4uNpc0pFcQmlHqO8ddlIorDhf81aDA8l6DqYOafg /TMiew9b9pII8BUtpZyWdZ/Gu3wthgIRb76eGffvLP9+9+MPgxbmx4aUyBkdUVj5DAUI R2sqM2Tb7K+WVBjKX5czmwAeO76PglUZqg7a88MrmL1b+luqmLWuJa+AJIf3K2jh4SEa QSqpcTUlWVHS+rqRLRvacAr3UTJ2nAw2pgPzV95HgEhwGJ0XzLxJP3VG5TCeIBb6Mcrw nGgm23WPslYDJATr0K5OFlwd7w1P21rVn4cuEVZiVz2mhN6vzfaAV79VgRNin90ez4dc 1fxA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=pGKLO+vSOkFP3ZK/2H6wqakx0CWUzIMTiilsobpVEQg=; b=SPW6JYjtc6aLuUSP4snoXko9LQuYPKhtcfz2sGrALYsPqGHdArcKNV8TmWOJF0JI62 mCLKmK9OSxa1jW7RbwUrbMYp9W4AKxTAQubqwyDqMdNnGW8bRuhsc9YfOqD9ktcciC1B IFJEfBHdj9/WE2aUJRu++HFaKr8hZPHgVL3fb1ti9XDyNgernSfRDP7FyQnWZl8VUsuF HkLjrNzPMJubO1ckjlUMnztohYKYVvGGZPmCJxP2Ow8UB3qaI2rfDFJ9edlek8upjiFH oEhcXtzabesPfZm/mHRJwN4QYS4nX6APbWsXphFEpkAZKdkjH46epibGgUCN5m1DNWlb MgUg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hT9LEu3p; spf=pass (google.com: domain of i.chaitanya.ls@gmail.com designates 2607:f8b0:4864:20::d44 as permitted sender) smtp.mailfrom=i.chaitanya.ls@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=pGKLO+vSOkFP3ZK/2H6wqakx0CWUzIMTiilsobpVEQg=; b=ogjuDfHoSqpNbEumrufFdgWZm0wwmGm+hxfB58c7IAFINbzyIWscEzlrLAQD5OPtbL KllLCcrthBrOe2wE+VVkusELDF0kfMZsTS8eDWU2ZWNbf5/JzY5EL1i4/Df75XhkuXqy YiSNYnQIFbqSI/KCYdblgUOpDwf74d6opUS/r/wV3itbhDCsMPMFtOmfIdnXnsycOnZf A5kb9/TnKMMszs0cbZz4k5tqoJqUzHSRUdugu7C6FSclAcU+xELuqjyascFyn8mog13L vHyz1eaAmnmvq1bd1B+YZlQUJ8UXsLRp+Tt4VzPbuLd4z/KruIFbvsnckrU8yhkUNZaz ydPA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:cc :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=pGKLO+vSOkFP3ZK/2H6wqakx0CWUzIMTiilsobpVEQg=; b=GzjTJ6vc1lAC3mQ2Cf2mA2MOxUJcozKbDpUWrr+cV1/CSuBjSZNTGJdZ7vz/FoyMmj YPpSZVQxo5ZP6trhoWfIqAvu/dj1j+fZiFKn3Z/Gu+75wAtIdm8rJauXr3DKEbV0VSiA CpVWjBkpLXBGIJ1gGd9AyIrsDaXXukn9In1Y6Ikz2lr12lLFIih97xFNOh+GDmI92MOs Lw6hsjoe20VJsi7q0zMCP73UuFGDk3B7DRDYoZ8E5WQdANu09iErS8DpTWSnbUODVIpX ouaqzmEgGqrQNpGcH5FRi9z9JWXFcHjrbzlNZZ/sADqxAUdYvuO60eUqKYLbTkfLOA5y 7Haw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=pGKLO+vSOkFP3ZK/2H6wqakx0CWUzIMTiilsobpVEQg=; b=gx9ZIpV9ibEwdXYE25YOwBxZt8u9oon4HZuhIyy6tm/vSC6nV7O2Qeplwl/wSqiM+E as0vTPK8k7PqLsYsTJn1F9u7DSsdIXW6fLLDwJkOvT2pPkXv/YBMWFFQuFQjmjbswwrB i9Ff+b2GYI8UxvWQJ4cmgIrjXXKFq5qjsBQwfx8BkSzdq0+KM7WgN2aRwrC2bfWy4sNS pjRsiUU4ztfVjgdE37PoeBw59zMd5c+nYCl22d/2fuPHDDRP+KN1Us1LNG8AALr6RHe1 Wk1LCsoRDL3fsSk9P4c5vumqT8K1CHB8QLFlMq9iYEnEVSKuqdrmiNKZuck2UtoOhVlh huqA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWLj3rUagHg3cNhAeMaAHGpQ4WZI5iqfHhBlu7l5MxskzzmpF9i B+gsVMvGZ91MrBVLhQVhxfY= X-Google-Smtp-Source: APXvYqye40n7CKWV3KVObAlR8y8US9sqMIKWrean/WoItxVLTczcF71EUlYsdyHCfAsLM8zHHFaKXQ== X-Received: by 2002:a62:1e42:: with SMTP id e63mr21279526pfe.25.1574083606466; Mon, 18 Nov 2019 05:26:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:3d86:: with SMTP id k128ls604199pga.11.gmail; Mon, 18 Nov 2019 05:26:46 -0800 (PST) X-Received: by 2002:a63:d011:: with SMTP id z17mr11558141pgf.119.1574083605910; Mon, 18 Nov 2019 05:26:45 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574083605; cv=none; d=google.com; s=arc-20160816; b=m/1ExJ2HbRF7wZcT7w+dI7SUjoZYqHz8fnXPsAHzwODilxqJlyroVICJ3i+1YNvIth xcQKM0haHhlUjtfo/+RWVv/xaj96DJIUZy2JN7xV/2vm8cFFT4xK0mO6uuZzeURgy5Pa W7lDcol1Qg0qlnnfaOIptZeeCoBBOnH3Z3XCAxxJWiwvBiAS4s/0kjpvOvMTUMzF2eUR SoIz4ZFkmpQvU9UfaI10RkeIVrNHn88iHQ5OPJ8Bz+DLjk535KMj1QE2D251IYEAzYHl PHAPjaITeznX57Y3rAJK/BkxSEzw7TQX/+QNkYtjsi7cnhlVJeO2PB8PyYnumHk/aG7R P/+g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=0Cga2fHVp7COmslqupB4byYrQ3/9PUqekDdeGX1Sp9E=; b=YndXYUiqAEvq41QlF+Jk16bNxkPbCdaBx9TU0hzLpH5SSZCSI9J0bSaTRbWfPcFW1J yN9DO5Zbm+LasH/d+JWBIcHZib/BIYmq8uWQrlONewdSTsbu8HGcZPddk7P9r8j8Clof /BEAqFzYJikovEB/3FxYqduEOwctmfnKr12dmUT2n33oFnJEigoORk+J5r88x1UN7xYe mZPyUOwQw83kzpXLovQXrhPPgw+94GrSI9bHLXGVRT18yT23Jq0c4lKtys2mAElrOcBb 1G14irw3GWZBODyBMHAxAclpsWz9DSpznW6hB80vVMcAPJjr0Ik62CAQUZOGh6NFP1pj JZ+Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hT9LEu3p; spf=pass (google.com: domain of i.chaitanya.ls@gmail.com designates 2607:f8b0:4864:20::d44 as permitted sender) smtp.mailfrom=i.chaitanya.ls@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd44.google.com (mail-io1-xd44.google.com. [2607:f8b0:4864:20::d44]) by gmr-mx.google.com with ESMTPS id t71si792761pjb.2.2019.11.18.05.26.45 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 18 Nov 2019 05:26:45 -0800 (PST) Received-SPF: pass (google.com: domain of i.chaitanya.ls@gmail.com designates 2607:f8b0:4864:20::d44 as permitted sender) client-ip=2607:f8b0:4864:20::d44; Received: by mail-io1-xd44.google.com with SMTP id r144so18675703iod.8 for ; Mon, 18 Nov 2019 05:26:45 -0800 (PST) X-Received: by 2002:a02:9144:: with SMTP id b4mt11095612jag.118.1574083604862; Mon, 18 Nov 2019 05:26:44 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Chaitanya LS Date: Mon, 18 Nov 2019 14:21:27 +0100 Message-ID: Subject: =?UTF-8?Q?Re=3A_=5BHoTT=5D_Sad_news_=E2=80=94_Erik_Palmgren?= Cc: "HomotopyTypeTheory@googlegroups.com" , constructivenews@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000001e5d4505979ee66a" X-Original-Sender: i.chaitanya.ls@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hT9LEu3p; spf=pass (google.com: domain of i.chaitanya.ls@gmail.com designates 2607:f8b0:4864:20::d44 as permitted sender) smtp.mailfrom=i.chaitanya.ls@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --0000000000001e5d4505979ee66a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear all, This is very sad news indeed. My memory of Erik is as a quiet but thoughtful and warm person, candid and principled, and vastly knowledgeable. Erik was my entry-point into the world of type theory, when, in 2016, he let me, then an impressionable masters student, into his cavernous setoid libraries, where I spent six happy months messing with E-categories---'"Erik"-categories'---and ECwAs, lost in the heady lure of checking coherences in a proof assistant. -Chaitanya. On Fri, Nov 15, 2019 at 11:15 PM Peter LeFanu Lumsdaine < p.l.lumsdaine@gmail.com> wrote: > Dear colleagues, > > Some very sad news =E2=80=94 Erik Palmgren passed away unexpectedly this = week at > his home in Stockholm, after a short period of bad health. > > Besides being insightful and influential in his own work, mostly on > constructive mathematics and related topics in logic, Erik was also a > generous and sensitive mentor to many students and younger colleagues, > first in Uppsala and then in Stockholm. He will be deeply missed. > > Personal website: http://staff.math.su.se/palmgren/ > > For any academic business regarding Erik, please contact either me < > p.l.lumsdaine@math.su.se> or Jonas Bergstr=C3=B6m (he= ad of > the Stockholm University mathematics division). > > Sadly, > =E2=80=93Peter. > > -- > 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/CAAkwb-k00GTNS4jm3vg= vJoAK5mUuJU6RDZH_6cKs5hD1M4wOKA%40mail.gmail.com > > . > --=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/CALwTfBf%3D80-ak%2Bgn%2BdDV3rsEoaSTMQPG9jH8_9EqQvYZpV%2B= 85Q%40mail.gmail.com. --0000000000001e5d4505979ee66a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Dear all,

This is very sad news indeed.

My memory of Erik is as a quiet but thoughtful and warm person, candid and principled, and vastly knowledgeable.

Erik was my entry-point into the world of type theory, when, in 2016, he let me, then an impressionable masters student, into his cavernous setoid libraries, where I spent six happy months messing with E-categories---'"Erik"-categories'---and ECwAs= , lost in the heady lure of checking coherences in a proof assistant.

-Chaitanya.


--
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 htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/CALwTfBf%3D80-ak%2Bgn%2Bd= DV3rsEoaSTMQPG9jH8_9EqQvYZpV%2B85Q%40mail.gmail.com.
--0000000000001e5d4505979ee66a--