Thanks to Jeremy Avigad, I learnt in February 2010 about Vladimir’s IAS presentation 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 clearly concerned, 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ó > 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.