RE: [HoTT] Re: Vladimir Voevodsky

["Joyal, André" <"joyal..."@uqam.ca>]

[-- Attachment #1: Type: text/plain, Size: 2981 bytes --]

Dear homotopy type theorists,

A very sad news.

My first contact with Vladimir and his ideas was at a meeting in Oberwolfach 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 inconsistent!
He later came to distrust the applications of his ideas to homotopy theory!

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

-André J

________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf 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, with his own direct contributions and early insights into working in type theory without UIP; also through his influence within the field, with a strong 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 interest.

He was always stimulating and insightful, if not always easy to work with — extremely mathematically exacting.  His views and goals were often idiosyncratic and surprising, but always came from extremely well-thought-out mathematical grounds, that one might disagree with but could never dismiss.

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

–Peter.


On Sun, Oct 1, 2017 at 6:54 AM, Daniel R. Grayson <danielrich...@gmail.com<mailto:danielrich...@gmail.com>> 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 email to HomotopyTypeThe...@googlegroups.com<mailto: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 email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 8306 bytes --]