From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.217.68 with SMTP id q65mr12127805oig.53.1520501185285; Thu, 08 Mar 2018 01:26:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.202.198.6 with SMTP id w6ls555302oif.22.gmail; Thu, 08 Mar 2018 01:26:24 -0800 (PST) X-Received: by 10.202.236.139 with SMTP id k133mr12141219oih.6.1520501184089; Thu, 08 Mar 2018 01:26:24 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520501184; cv=none; d=google.com; s=arc-20160816; b=hjdIbYsECMpB8qzDkoNBJE86qVN0VTmZ27U1QmEjQgGl4hpwajdpDAx+RkXolHaNZJ YqKQ1+yj1M8FDrVN3Wo9mufCpr8cqSz6Vq8tXxjRhH325dT6gt7/txDT6RHN702hPAyN Gm0VyA86QBOc+3B5f3ljfWSr0tqwdIG5ZjBwbGqkUB0ilXdEce07DraxIL1lmfsc6WrU Z6Z8v5UdjAvJtP9iFLJyHfW8ALcHeDYVXifCLiT+9vLW11YfsJZkgEVNYkk4Mk87yRZI F/Zn3guZJ7C5EXraM+47WFnNQb/oiztLv/11oC5pnsCWgHcXidIAdgPHwy+84xyYCuXn 9f2A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=e1ySTG4Rg1Xv+rrmX3V0JR4kBCvHwmQ/+cXOpDs1AXg=; b=TwHhnoOEwva2XU0xtcS09/gTynqteaCrlJphQHm1K1CmfiKI38ibeUOY4N3jNAZb61 gA9GhlVvL7fn/vGhZJekNwLErVUa7J9QnNCcaK2iNvDICS++crPtrLuOaL5+cMU7k4Fr Ndz0Vdqy6ATvm/UsOg9KTPuSsuXx8M2OZ16PzGsfPHldI4VQQL8bAPZHnRkGA1/deN1X REYuDz7t6czGYQ+D73/HFU0SYzyR7+CvmXiEEHQumHQaI4Pj7bq9I2Jn1GCKqB3fSyPR YzTiInQiJVaYPUvveZhhJGUge3MId1JQAujVIt5Cuvfv3xattzGNi3aQnK52YCy1iugn P5nQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=cwjg7sBa; spf=neutral (google.com: 2607:f8b0:4001:c0b::22c 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-it0-x22c.google.com (mail-it0-x22c.google.com. [2607:f8b0:4001:c0b::22c]) by gmr-mx.google.com with ESMTPS id f45si1415785oth.0.2018.03.08.01.26.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Mar 2018 01:26:23 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4001:c0b::22c is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) client-ip=2607:f8b0:4001:c0b::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrej-com.20150623.gappssmtp.com header.s=20150623 header.b=cwjg7sBa; spf=neutral (google.com: 2607:f8b0:4001:c0b::22c is neither permitted nor denied by best guess record for domain of andrej...@andrej.com) smtp.mailfrom=andrej...@andrej.com Received: by mail-it0-x22c.google.com with SMTP id u5so7122922itc.1 for ; Thu, 08 Mar 2018 01:26:23 -0800 (PST) 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 :content-transfer-encoding; bh=e1ySTG4Rg1Xv+rrmX3V0JR4kBCvHwmQ/+cXOpDs1AXg=; b=cwjg7sBa0hhEGX1tA3HTxFuItOwHEholxse+Q3tz2RVfApteZGeDAoacl+LOZU7fcu y4BSxpa0t+4aFTt0erEtEx4VrlrhsSGqdNLd3VWwellLhRFQGDuODkwcBvk8zYfPT0R8 HQdhczoW3mzZ+ZD9URaauVTO0ApprunREOws8nkcJ45THESZBTEOyq7ik7bGJ38OtjhX kjZwqWHSKX/kCSoVI5DHD+BJClxLmI3JGR3MPEC/qE3VOa3GYoaZqrbdPsZDa4vgseXq qZWnIXPq2T9VXTS1UXOkdOZ5Amls7wbAHGzy2Ay1qcEY2Nhf9jjqsDoNNb+vclBSilAW 21ig== X-Gm-Message-State: AElRT7EmAIUNEFKryohZkOvamoiXSQPvBQ085FkFIM8Dxxqj0uKnQJTs p0d89jwpXvbyaKQRQg4iu7NkyXkgYf05uZTHRV8bTplg X-Received: by 10.36.104.1 with SMTP id v1mr27010939itb.70.1520501183497; Thu, 08 Mar 2018 01:26:23 -0800 (PST) MIME-Version: 1.0 Received: by 10.192.171.138 with HTTP; Thu, 8 Mar 2018 01:26:22 -0800 (PST) X-Originating-IP: [2001:1470:fff0:830:bc42:b944:e3d3:1767] In-Reply-To: References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com> From: Andrej Bauer Date: Thu, 8 Mar 2018 10:26:22 +0100 Message-ID: Subject: Re: [HoTT] Re: Univalence from scratch To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > Martin-L=C3=B6f's paper "25 years of constructive type theory" Sorry, that should have been: Martin-L=C3=B6f's contribution in the book "25 years of constructive type theory"