Re: [UniMath] Vladimir Voevodsky

Re: [UniMath] Vladimir Voevodsky

[N. Raghavendra]

At 2017-09-30T21:24:44-07:00, Daniel R. Grayson wrote:

> The following message from the director of the Institute for Advanced
> Study in Princeton announces sad news: ...

I hesitate to write here, because I did not know Vladimir Voevodsky, and
I know very little of his work, although I have been trying to learn
about univalent foundations and UniMath.  Yet, even with the limited
nature of my interaction with him, I grew to admire him, just as did
many others.

I first saw Voevodsky when he lectured at the 1998 ICM in Berlin.  I
first met him on 15 February 2011, when he came and spent a couple of
days at the place where I work, in Allahabad, India.  He gave a lecture
the next day, on `Mathematics and computers'.  He spoke about the
univalent foundations of mathematics, and showed some code in the CoqIDE
on his MacBook.

Voevodsky was then on his way to an annual student gathering at the
Indian Institute of Technology in the nearby city of Kanpur, organised
by the mostly engineering undergraduates there.  I asked him if he was
visiting any other places in India, and was surprised when he said that
he had come all the way just for that event.  Voevodsky was accompanied
by his friend Roman Mikhailov, who had spent a few years in Allahabad.

I found Veovodsky's lecture here fascinating.  However, it took me some
years before I became more seriously interested in UniMath.  I then had
a few small interactions with Voevodsky at the GitHub site of the
project, and twice on email.  I admired the fact that he did not dismiss
any of my utterly stupid queries, but answered them to the point.  I was
looking forward to learning more about UniMath, and about his ideas on a
description of type theory for mathematicians.

In July, 2015, when there was a discussion in a thread titled `Voevodsky
on formalizing type theory' in the HoTT Google group, he wrote the
following brief note to me:

----------------------------------------------------------------------
From: Vladimir Voevodsky <vlad...@ias.edu>
Subject: Re: [HoTT] Voevodsky on formalizing type theory
To: "N. Raghavendra" <ra...@hri.res.in>
Cc: "Prof. Vladimir Voevodsky" <vlad...@ias.edu>
Date: Mon, 13 Jul 2015 16:07:02 -0400 (2 years, 12 weeks, 1 day ago)
X-Mailer: Apple Mail (2.2098)

Maybe I should visit the Harish-Chandra Research Institute again :)

Vladimir.
----------------------------------------------------------------------

It was written jokingly, but I wrote back to him, saying that he would,
of course, be truly welcome here.  And, perhaps irrationally, I hoped
that he would return here and speak again, as inspiringly as before,
about foundations and formalisation.  I was utterly saddened by his
passing, and will cherish my brief interactions with a great man.

Raghu.

--
N. Raghavendra <ra...@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/