Re: [HoTT] Vladimir Voevodsky

[Thierry Coquand <Thierry...@cse.gu.se>]

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

 Thanks to Jeremy Avigad, I learnt in February 2010 about Vladimir’s IAS presentation<https://www.youtube.com/watch?v=84vW1hQLFu8>
about foundations of mathematics and homotopy theory. I found it absolutely
fascinating, since it suggested a systematic way to attack one of the main problem of type
theory: how to represent equality, and in particular, what should be the equality type
for the universe. The first conversation we had, Chiemsee June 2010, was about
the fact that, in his model, universes are “homogeneous”, contrary to a stratified
picture where the first universe is the collection of sets, the second the collection
of groupoids and so on.
 Vladimir had a unique sensibility for foundational issues. Just to give an example, he
was <https://www.youtube.com/watch?v=GGyKR4BhUGw> clearly concerned<https://www.youtube.com/watch?v=GGyKR4BhUGw>,  as one should be, by the fact that  the axiom of choice is needed
to prove that  a fully faithful and essentially surjective functor is an equivalence. His
formalism gives a way to address this question.
 He was also unique in his ability to formalise mathematics. It seemed that he was
thinking directly in dependent type theory. His definitions of contractibility and
equivalence are truly beautiful, as his formal proofs in his UniMath library.
 He was humble and really kind in discussions, always trying to explain things as clearly
as possible
 As Edward Frenkel  wrote  “there was a lot of light” and this light will be greatly missed.

 Thierry







On 5 Oct 2017, at 00:52, Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> wrote:

During the Types 2011 meeting in Bergen, I went outside to have
fresh air in a coffee break. Then there was this guy, and we said
hello to each other without asking for names or formal
introductions. He apologized that he was trying to concentrate on
his talk to be given after the break. I nevertheless, perhaps
impolitely, asked what his talk was going to be about. It was
going to be about a homotopical model of type theory (this is
what he said, but in the talk the topic was size). Then I said I
was looking at topological models of type theory myself. He asked
me to explain, which I did. Then he gave his talk. And after that
we met again and had a long conversation, we went together in a
boat trip with the conference crowd, and then we had dinner in
the same table, with many discussions.

I never suspected, at that time, I was talking to a Fields
Medalist. He was just somebody giving an interesting talk in a
conference. After the meeting, when I was back home, he asked me,
by email, what the topology of the universe is, in the models I
was considering.

M.


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