From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.103.194 with SMTP id b185mr1103174ywc.11.1506957753990; Mon, 02 Oct 2017 08:22:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.129.156.130 with SMTP id t124ls141211ywg.5.gmail; Mon, 02 Oct 2017 08:22:33 -0700 (PDT) X-Received: by 10.129.75.194 with SMTP id y185mr4928766ywa.70.1506957753169; Mon, 02 Oct 2017 08:22:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1506957753; cv=none; d=google.com; s=arc-20160816; b=CJFrVZ5147nCEHFciOyRgaFBW3UjJV2VPeCAiEWrQ9xmsFtg0PfUqwBxc9fCAwY2vV NMtX+GXL3w4kn9OsC2G1m8avkzU6lp3ehjLXLYKqSn/e2E5cIXyKHhfFz4ruNlz5xppx 44NVwM2tsdCdN9ic/4ZyvrmvV5SR9nqIB+4w8ASZyZf94f0McPKFrVyaUGK3DsBbHyWX 2zZfbu26u31EcpB4VpP821O3ERar5lIEmD7Yyol2eFoCscupXQjuM3ljN/Rbstl17ESf bUBJXWRFJJMuPi9Y34UTlERr3x7c8xHAKQ8fJ/MXqhFhpXRN8IWIzeJa8GGZXtnRiURi nfqg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=Oatr9KvJ/4/0cp08ZclcBPfKXreQIiNjjEEim/0oS7U=; b=NLEqQU156U3FR2abB7jcJFVaxCbu2iiVopKkk4k6+QKgXes66CTXi76EykTFFmPNfq mgD313/N/f5Oi55HxwH6mS1+THMGI0V1B4qp8uiKgaMcZIj7gI3tYIlBoQ2ndiZUwdHR ba9ZwHeXc9L4g3xJROlmyrEPWQLpzjbiMF1xfHIpDX/PhjVQqdyUMsSNEEYT8JTvJ+mv YmJikNdeeCP1X84MowWPgfeeiv/TAelm29hFI1NKa4yzoDyUqyMgsUc/j60BbhJGJnPV S8blmwlLOsnYKM8aLhWkPZiyKcq8M/JLMcicSA1WKdhJdJPgsm2Ew8kDvo+1IAVCCoii a+dQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=DYrK8Yp9; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Return-Path: Received: from mail-yw0-x22e.google.com (mail-yw0-x22e.google.com. [2607:f8b0:4002:c05::22e]) by gmr-mx.google.com with ESMTPS id p66si602131ywh.1.2017.10.02.08.22.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 02 Oct 2017 08:22:32 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4002:c05::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=DYrK8Yp9; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-yw0-x22e.google.com with SMTP id p10so3898745ywh.8 for ; Mon, 02 Oct 2017 08:22:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrej-com.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=Oatr9KvJ/4/0cp08ZclcBPfKXreQIiNjjEEim/0oS7U=; b=DYrK8Yp9TrOzZXfwzLRf6E4O1JU4UIkKLBcW+PSbcMkSU4U5AIXaCTk3KqWkNH4XmC kc8ghUa4Rg4GdQsqSuSGFUYSiGgw39ZlEUXrYifBIZXB7rLQsalk/p5XbKdD5I7Fym1T 3YDWSykR6eaiFFJoJZMtAck+xi/y9PmK+15qoSnl1U9Qx97cXQQRRjF+j/oqBUcAnMgU CWTMqKktVfJjz/f6nBC9bVsH3IUSWpY0Bk6E6Uabbz1IndCBgBpddVaF2z8Fl9pKHSJK by8jWQzUoN1+C57jZTBgHfTSwDu3WsKn4Hloqhsyu583l4NQckugFKZ+tuTK586VNFFM uIVg== X-Gm-Message-State: AHPjjUj2ABt3N/PcNtwc99Bg4TPVALA3R0YhH1sj1pmwIkqfqulfKw35 S94vOXiTrKaO+psYuF89VZwa14jD0v2mPzhCdvwg2fsq X-Received: by 10.129.136.67 with SMTP id y64mr12772076ywf.55.1506957751638; Mon, 02 Oct 2017 08:22:31 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.162.134 with HTTP; Mon, 2 Oct 2017 08:22:31 -0700 (PDT) X-Originating-IP: [2001:1470:fff0:830:7d15:26ed:2dcb:6d76] In-Reply-To: References: From: Andrej Bauer Date: Mon, 2 Oct 2017 17:22:31 +0200 Message-ID: Subject: Re: [HoTT] Vladimir Voevodsky To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" This summer in Cambridge, Vladimir and I planned a dinner but then had to cancel it due to other obligations. The last message I got from Vladimir said: "Someplace else and hopefully not in too distant a future, Ok?" I will miss Vladimir. Andrej