From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.159.61.27 with SMTP id l27mr2129318uai.9.1507846906732; Thu, 12 Oct 2017 15:21:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.176.28.76 with SMTP id o12ls1390509uaj.13.gmail; Thu, 12 Oct 2017 15:21:45 -0700 (PDT) X-Received: by 10.31.76.67 with SMTP id z64mr7032182vka.50.1507846905745; Thu, 12 Oct 2017 15:21:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1507846905; cv=none; d=google.com; s=arc-20160816; b=xalHWHJYqy2zKvdmuPDn9WtflvxFkOrAR+m0JpBuwR/g3VoELbaYAPWb0BufjdgPzI o6GJfWpenw6xBC/byWeb1ziWbcDNCF2ezGVnD+nwe16TZRiYZMdFQPO01A7fb0CCi48N mbCKswp88ZvFVT6YRl3XxRWOXtDfnQPJ4yRLMG2a5D0YadHId9QS2T6CJDNez/QZvTgO o9i+lR1BBS/v1YpNGasqDd9nfrj1TpswtDg2bdAhqpMK/Q1amczBjqlr5aUieMzPtNIt 5ZG5io8ZBcjijUwwRcmg1R7M1i632hCRyBLdhKseUVw0jmVgGrOUleq2XczZnQnAXfrg yFHg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=2tgG7cQGaeNqlhKDA3+MPjf9li7RS7C7/wsLpvBmuoE=; b=aZ1QKfvzD0FINWpOOyPXXKaFV10Vd2nztuJi1NXP6RRosBFpnD2gyP2924xdGSccPc kUPKtp1lxLLcSn+Gj2X/bH8W2dONog0HluFYD8PidSfIYo81aT2wt47VQdmzrAdiVDNY oQrHoLxOn43DL1yJBFHQK5BTr+LmtKRvJnKFvRZp22EGs//CyHJRKb3EgrFS/FeXIwQE GKWj6Kwhd48xiYCMAHW3EL2Hmcn6bcNmFHxRKo0HOZhzkNJHFQDi8GowJeQntTE33dbt 2qR0c2qUZDw2kDwWFyAQ6cl1f9bdD9RPfPvHoUpJHoCUv7v8vZeuYQcvhRG6ZiKFMYKA Kj4A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xGb5W/0D; spf=neutral (google.com: 2607:f8b0:400d:c0d::244 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-qt0-x244.google.com (mail-qt0-x244.google.com. [2607:f8b0:400d:c0d::244]) by gmr-mx.google.com with ESMTPS id d33si135064uai.0.2017.10.12.15.21.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 15:21:45 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::244 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:400d:c0d::244; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=xGb5W/0D; spf=neutral (google.com: 2607:f8b0:400d:c0d::244 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-qt0-x244.google.com with SMTP id o52so16376392qtc.9 for ; Thu, 12 Oct 2017 15:21:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=2tgG7cQGaeNqlhKDA3+MPjf9li7RS7C7/wsLpvBmuoE=; b=xGb5W/0DoM1scTBsCCzvUgkDZOL8RXdmNQQPhbT8X3w0cK/0/VcVMYsgPoCt1H/Mz0 DShLC2vzWXaUa7ha9AX9DYVGowJN+SacsNcg8edLlpBA4NfpiOXsby33LQB6oF9j4SH4 5Pcpw48fW2F/53sY5Hr7cVGia918sfko1xIV+4jKuSAWEeeHtCMiTnccXcLR1LqlpR7Q /7PhDTLgz07FS3q+mmSMtv0CalvW2rc+6cfSFnmy1Y+vv32zSZW98047TosI2NrtQS3y +5HLGS/CPJQa561m5AJuHpiK4VEDE/EQwArwnavYNGlahOOxvxK183uFNnxhr+JsZP0K exFA== X-Gm-Message-State: AMCzsaV/F1dC5uXFWDwuYMkxzKR/BZmkqOHCs7sxRA+EOupYw9fQaAnU I3dkVhcKuUFAS66pSwOVWq7yp2P/ X-Received: by 10.37.30.8 with SMTP id e8mr2685343ybe.123.1507846905303; Thu, 12 Oct 2017 15:21:45 -0700 (PDT) Return-Path: Received: from mail-oi0-f51.google.com (mail-oi0-f51.google.com. [209.85.218.51]) by smtp.gmail.com with ESMTPSA id w199sm8783312yww.10.2017.10.12.15.21.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 12 Oct 2017 15:21:44 -0700 (PDT) Received: by mail-oi0-f51.google.com with SMTP id j126so10743495oib.8 for ; Thu, 12 Oct 2017 15:21:44 -0700 (PDT) X-Received: by 10.202.183.8 with SMTP id h8mr2136626oif.281.1507846904252; Thu, 12 Oct 2017 15:21:44 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.7.199 with HTTP; Thu, 12 Oct 2017 15:21:23 -0700 (PDT) In-Reply-To: <164e6589-5d92-4642-add6-fdbe7439d164@googlegroups.com> References: <69c716dc-7fbf-4c07-a128-21c75fc996da@googlegroups.com> <82f74559-e82f-4773-bd7d-2886bd9b38fb@googlegroups.com> <164e6589-5d92-4642-add6-fdbe7439d164@googlegroups.com> From: Michael Shulman Date: Thu, 12 Oct 2017 15:21:23 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Vladimir Voevodsky To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Regarding (0), I'm fairly certain that h-levels were pretty solidly established in the Coq code that he showed us at CMU in February 2010. So if he did formulate them in "early 2010" it was very early in the year. On Thu, Oct 12, 2017 at 2:55 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote: >> >> PS: it is the oldest email I have from him with the word "univalent" or >> "univalence" in it. > > > In the vein of bringing to public record things that Vladimir said, her= e > is a short interview. > > -------- Forwarded Message -------- > Subject: Re: historical question > Date: Thu, 22 Oct 2015 16:08:14 -0400 > From: Vladimir Voevodsky > To: Martin Escardo > CC: Prof. Vladimir Voevodsky > > >> On Oct 22, 2015, at 3:32 PM, Martin Escardo >> wrote: >> >> Hi Vladimir, >> >> (0) When did you formulate hlevels in type theory? > > Probably in early 2010 > >> (1) When did you formulate the univalence axiom? > > Originally in 2005 as a property of morphisms (fibrations). In late 2009 = as > a formula in type theory. > >> >> (And when did you give your model for it?) > > In a sense in 2006, only I did not know how to model the Martin-Lof ident= ity > types and thought that different identity types will need to be introduce= d > that will satisfy univalence but what other properties to require from th= em > I did not know. > >> >> (2) When did you prove that univalence implies function extensionality? > > July 2010. > >> >> I am giving a talk next week trying to rigorously explain the univalence >> axiom to classical mathematicians. This will involve, of course, trying >> to first explain Martin-Loef type theory, particularly the identity type= . >> >> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid >> model, in which they have a proto-form of univalence. Were you inspired >> by that, or were your thoughts independent of that? > > I was not inspired by it. In fact I tried several times to understand wha= t > they are saying and never could. > >> >> (Also: what was your first reaction when you saw the identity type for >> the first time? Did you immediately connect it with path spaces?) > > Not at all. I did not make this connection until late 2009. All the time > before it I was hypnotized by the mantra that the only inhabitant of the = Id > type is reflexivity which made then useless from my point of view. > > Vladimir. > > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.