From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.130.196 with SMTP id m65mr6100907ioi.39.1506870416178; Sun, 01 Oct 2017 08:06:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.83.17 with SMTP id h17ls2844014iob.19.gmail; Sun, 01 Oct 2017 08:06:55 -0700 (PDT) X-Received: by 10.36.105.82 with SMTP id e79mr5995187itc.44.1506870415431; Sun, 01 Oct 2017 08:06:55 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1506870415; cv=none; d=google.com; s=arc-20160816; b=VPxqyRBvaMmePsZoEpM338nlEBEfIU94PQ8ZL68mbFUEdo5D10mnqF50BzQE7dOQ5P NTv/OBVXUnhcABoOREKs1AwINw0/IngkIIaYF0uVJg2Wy5NFOc0v2zTCcVIhUEkllWyA Cuf1TMCtQH5xrV+PYcrSvS/ahyXrrllGMuRijycjZJtpBXngjg5KL8jZblcEx8c2jWjp ezYQTwsMdsKMBvzqDZceaiO4iVJzFjGtzuVK7HfUS+OxyyHUVINw1TdArUlJv3ZRo74F zaw1VwHvv4t9g6V77Q/X0qxWkzsgdU9Mj5iuqiur/4FDHOlwHGaLYXoPlmhZnjFS2Brs MvqA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from:arc-authentication-results; bh=qu7idM3zwP5y6du+iwNwRF1iPPY6NXnGF5KijSvk0Nc=; b=p0CkhBQ0Kf2faVhzsfdGkSQmZMLexBCCMaTBrByP8U6v3LQwlTB7DjQddsHpcV64th ZzsfFnBFaTglbvYDVQ3w74mjec1PUZF61C9sLVr4UHMViL3hTON56zAri7YLq0R85g/i 86MwFi3adxKAizh1Ry/9I2Pltfs+Hf1JsLdlyC51G02qbihJY538YAAcK5km13E0LQgl 5wiO9AotZABoh9z3nKjCt8nIy3TJJ3WE0r7XbreLcviyarJc3foBkmCXXS8T2upRio4s fJsENo6kg3X0AO3lyOUPDgDLAkbydVeQT5DXNZxjmW30Aqcd+qepdq5vjnj8TfuA8twp lnOQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=uqam.ca Return-Path: Received: from data.hamecon.telecom.uqam.ca (data.hamecon.telecom.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id c184si90474itg.6.2017.10.01.08.06.55 for ; Sun, 01 Oct 2017 08:06:55 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=uqam.ca Authentication-Results: data2.hamecon.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@Message.gst.uqam.ca Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postm...@Message.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@Message.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DKbpyyVsD_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3DSgJDDHH=5FwjgA=3A10_a=3D02M-m0pO-4AA=3A10_a=3D4RBUngkUAAA?= =?us-ascii?q?A=3A8_a=3DpGLkceISAAAA=3A8?= =?us-ascii?q?_a=3DNcHOd7QWAAAA=3A8_a=3D1XWaLZrsAAAA=3A8_a=3Dqrlz2rzYQw4hcGy?= =?us-ascii?q?VmywA=3A9?= =?us-ascii?q?_a=3DcZsLftHXYMVGdQJL=3A21_a=3DvdSNHKi9LskeWcUp=3A21_a=3DpILNO?= =?us-ascii?q?xqGKmIA=3A10?= =?us-ascii?q?_a=3DqJcnUnNV4j4A=3A10_a=3D8UEV-LYRAAAA=3A8_a=3DVOi4X4onAAAA?= =?us-ascii?q?=3A8?= =?us-ascii?q?_a=3DuBvL=5FTQY6O5VGXXGnlMA=3A9_a=3DDRvyVG-AbrjrePBJ=3A21_a=3D?= =?us-ascii?q?Dhdg8ftG3VmsnoN5=3A21?= =?us-ascii?q?_a=3DoIWQTXz-TBnJJ7v7=3A21_a=3D=5FW=5FS=5F7VecoQA=3A10_a=3Dfrz?= =?us-ascii?q?4AuCg-hUA=3A10_a=3Dc4S9Whzb7AQA=3A10?= =?us-ascii?q?_a=3D=5FsbA2Q-Kp09kWB8D3iXc=3A22_a=3Dyxg6MydoOon7ZmLlweV3=3A22?= =?us-ascii?q?_a=3DVQ2JQ4pOynkHRowHV3RP=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2AdAgAEBNFZ/9H20IRcGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBgm9uZG4nB4Nqm32IQ413gSUDXAoYAQqFGAKEM0MUAQIBAQEBAQEBayi?= =?us-ascii?q?FGAEBAQEDTjsCAQgNBAQBAQsdByEQARQJCAIEAQcHBAEHEgMEiStMAxUQp3Iih?= =?us-ascii?q?w0Ng3IBAQEBAQEBAwEBAQEBAQEBAQEBGAWDLYhlgl6BbgUBEgEhNIMMgjIFh0S?= =?us-ascii?q?RFIgePIdehz9OAZBthxWMcIhkgTk2IU80C4Y3gjx2AQeHFIEkAYEPAQEB?= X-IPAS-Result: =?us-ascii?q?A2AdAgAEBNFZ/9H20IRcGgEBAQECAQEBAQgBAQEBgm9uZG4?= =?us-ascii?q?nB4Nqm32IQ413gSUDXAoYAQqFGAKEM0MUAQIBAQEBAQEBayiFGAEBAQEDTjsCA?= =?us-ascii?q?QgNBAQBAQsdByEQARQJCAIEAQcHBAEHEgMEiStMAxUQp3Iihw0Ng3IBAQEBAQE?= =?us-ascii?q?BAwEBAQEBAQEBAQEBGAWDLYhlgl6BbgUBEgEhNIMMgjIFh0SRFIgePIdehz9OA?= =?us-ascii?q?ZBthxWMcIhkgTk2IU80C4Y3gjx2AQeHFIEkAYEPAQEB?= X-IronPort-AV: E=Sophos;i="5.42,464,1500955200"; d="scan'208,217";a="219273000" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 01 Oct 2017 11:06:22 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.101]) by Message.gst.uqam.ca ([169.254.1.117]) with mapi id 14.02.0387.000; Sun, 1 Oct 2017 11:06:19 -0400 From: =?Windows-1252?Q?Joyal=2C_Andr=E9?= To: Peter LeFanu Lumsdaine , Homotopy Type Theory Subject: RE: [HoTT] Re: Vladimir Voevodsky Thread-Topic: [HoTT] Re: Vladimir Voevodsky Thread-Index: AQHTOnFmdiT6ji/RLE67loujgN3UgaLPPdWA///MrUc= Date: Sun, 1 Oct 2017 15:06:19 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138CB327A@Pli.gst.uqam.ca> References: <099725f2-f96b-4d48-9300-1236cff72224@googlegroups.com>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B138CB327APligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B138CB327APligstuqamca_ Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable Dear homotopy type theorists, A very sad news. My first contact with Vladimir and his ideas was at a meeting in Oberwolfac= h in 2011. He gave a series of talks on constructive mathematics and homotopy theory, = framed as a tutorial with the proof assistant Coq. His notion of a contractible object and of an equivalence were striking. I had a hard time understanding his ideas, because they were described very= formally. He apparently distrusted informal expressions of mathematical ideas. One evening, he expressed the opinion that Peano arithmetic was inconsisten= t! He later came to distrust the applications of his ideas to homotopy theory! The contributions of Voevodsky to mathematics and to type theory will forev= er remain. Thank you Vladimir! -Andr=E9 J ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Peter LeFanu Lumsdaine [p.l.lu...@gmail.com] Sent: Sunday, October 01, 2017 9:18 AM To: Homotopy Type Theory Subject: Re: [HoTT] Re: Vladimir Voevodsky A huge shock, and a massive loss for our field. Vladimir contributed so much to what the field is today. Most obviously, w= ith his own direct contributions and early insights into working in type th= eory without UIP; also through his influence within the field, with a stron= g and well-articulated vision of topics he felt were important to work on (= most concretely, directing and co-ordinating the work of many contributors = in the UniMath library); and of course also through his outreach to a wider= mathematics audience, helping to put type theory and formalisation on the = radar of many people who otherwise might not have given it attention or int= erest. He was always stimulating and insightful, if not always easy to work with = =97 extremely mathematically exacting. His views and goals were often idio= syncratic and surprising, but always came from extremely well-thought-out m= athematical grounds, that one might disagree with but could never dismiss. We=92ve lost a huge contributor and leader in the field, and will all be th= e poorer for it. =96Peter. On Sun, Oct 1, 2017 at 6:54 AM, Daniel R. Grayson > wrote: And there is this: https://www.ias.edu/news/2017/vladimir-voevodsky -- 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 HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. -- 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 HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --_000_8C57894C7413F04A98DDF5629FEC90B138CB327APligstuqamca_ Content-Type: text/html; charset="Windows-1252" Content-Transfer-Encoding: quoted-printable
Dear homotopy type theorists,

A very sad news.

My first contact with Vladimir and his ideas was at a meeting in Oberwolfac= h in 2011.
He gave a series of talks on constructive mathematics and homotopy theory, = framed
as a tutorial with the proof assistant Coq.
His notion of a contractible object and of an equivalence were striking. I had a hard time understanding his ideas, because they were described very= formally.
He apparently distrusted informal expressions of mathematical ideas.
One evening, he expressed the opinion that Peano arithmetic was inconsisten= t!
He later came to distrust the applications of his ideas to homotopy theory!=

The contributions of Voevodsky to mathematics and to type theory will forev= er remain.
Thank you Vladimir!

-Andr=E9 J

From: homotopyt...@googlegroups.com [homo= topyt...@googlegroups.com] on behalf of Peter LeFanu Lumsdaine [p.l.lu...@g= mail.com]
Sent: Sunday, October 01, 2017 9:18 AM
To: Homotopy Type Theory
Subject: Re: [HoTT] Re: Vladimir Voevodsky

A huge shock, and a massive loss for our field.

Vladimir contributed so much to what the field is today.  Most ob= viously, with his own direct contributions and early insights into working = in type theory without UIP; also through his influence within the field, wi= th a strong and well-articulated vision of topics he felt were important to work on (most concretely, directing an= d co-ordinating the work of many contributors in the UniMath library); and = of course also through his outreach to a wider mathematics audience, helpin= g to put type theory and formalisation on the radar of many people who otherwise might not have given it attentio= n or interest.

He was always stimulating and insightful, if not always easy to work w= ith =97 extremely mathematically exacting.  His views and goals were o= ften idiosyncratic and surprising, but always came from extremely well-thou= ght-out mathematical grounds, that one might disagree with but could never dismiss.

We=92ve lost a huge contributor and leader in the field, and will all = be the poorer for it.

=96Peter.


On Sun, Oct 1, 2017 at 6:54 AM, Daniel R. Grayso= n <danielrich= ...@gmail.com> wrote:

--
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+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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+unsu...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--_000_8C57894C7413F04A98DDF5629FEC90B138CB327APligstuqamca_--