Re: [HoTT] Re: Vladimir Voevodsky

[Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>]

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

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

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