Vladimir Voevodsky

Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 917 bytes --]

Dear Colleagues,

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

---------- Forwarded message ----------
Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
From: Robbert Dijkgraaf
Subject: Sad news

Dear Colleagues,

It is with a heavy heart that I write to share some very sad news. Our dear 
colleague and friend, Vladimir Voevodsky, Professor in the School of 
Mathematics, passed away unexpectedly this morning.

Vladimir was a truly extraordinary mathematician and integral part of our 
community. His death is a tremendous loss for the Institute and for the 
world. We will all miss him dearly and extend our deepest condolences to 
Vladimir’s family and his many colleagues and collaborators around the 
world.

We will soon be sharing more information about a gathering to celebrate 
Vladimir’s life and legacy.

Robbert

[-- Attachment #1.2: Type: text/html, Size: 2706 bytes --]

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 69 bytes --]

And there is this:  https://www.ias.edu/news/2017/vladimir-voevodsky

[-- Attachment #1.2: Type: text/html, Size: 90 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Thomas Streicher]

That is very sad! Didn't know him too well as a person but besides
being a genius in maths I remember him as a very kind person who,
however, seemed to be plagued by various psychological problems.

I had the impression that the last years most of his energy was
consumed by fighting what he himself would have called "his demons".
Nevertheless, he published a lot his last 2 or 3 years.
But whenever I met him I had the impression he was under a very strong
pressure. Apparently too strong to bear for long!

What a genius! What a hard life!

Good bye Valdimir!

Thomas

Re: [HoTT] Re: Vladimir Voevodsky

[Peter LeFanu Lumsdaine]

[-- 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 --]

RE: [HoTT] Re: Vladimir Voevodsky

[Joyal, André]

[-- 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 --]

Re: [HoTT] Vladimir Voevodsky

[Steve Awodey]

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

A tragic loss of a great mathematician and a profound intellect. 
Vladimir was the founder and leader of Univalent Foundations, and his loss is a terrible blow. 
He suffered for his gifts and he gave us much to be grateful for.
I personally enjoyed his friendship and suffered his scorn, and the former was worth the latter. 

Steve
 


> On Oct 1, 2017, at 12:25 AM, Daniel R. Grayson <danielrich...@gmail.com> wrote:
> 
> Dear Colleagues,
> 
> The following message from the director of the Institute for Advanced Study in Princeton announces
> sad news:
> 
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
> 
> Dear Colleagues,
> 
> It is with a heavy heart that I write to share some very sad news. Our dear colleague and friend, Vladimir Voevodsky, Professor in the School of Mathematics, passed away unexpectedly this morning.
> 
> Vladimir was a truly extraordinary mathematician and integral part of our community. His death is a tremendous loss for the Institute and for the world. We will all miss him dearly and extend our deepest condolences to Vladimir’s family and his many colleagues and collaborators around the world.
> 
> We will soon be sharing more information about a gathering to celebrate Vladimir’s life and legacy.
> 
> Robbert
> 
> -- 
> 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 <https://groups.google.com/d/optout>.


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

Re: Vladimir Voevodsky

[Andrei Rodin]

[-- Attachment #1.1: Type: text/plain, Size: 1994 bytes --]

This is a horrible news. In addition to being a mathematician of genius 
Vladimir had a genuine interest to the history and philosophy of his 
discipline; I owe Vladimir hours of extremely tensed discussions on Euclid 
(Vladimir read both the Elements and the Proclus' Commentary very 
carefully), Grassmann (whose writings he studied perhaps more than any 
other historical source). Our last short exchange in LQ in Stockholm was on 
Aristotle: Vladimir told me that he had big plans of studying the history 
of logic. Vladimir had a fantastic capacity of understanding another 
person's ideas immediately following only some hints - or at least this is 
my personal experience with Vladimir. 

We were not close friends but all our meetings and talks were always very 
friendly; in 2015 he was my extremely attentive  host in IAS. I lost an 
important person in my life with Vladimir's unexpected death. Good buy 
Vladimir. 
Andrei

  
On Sunday, 1 October 2017 08:25:36 UTC+4, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced 
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our 
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of 
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our 
> community. His death is a tremendous loss for the Institute and for the 
> world. We will all miss him dearly and extend our deepest condolences to 
> Vladimir’s family and his many colleagues and collaborators around the 
> world.
>
> We will soon be sharing more information about a gathering to celebrate 
> Vladimir’s life and legacy.
>
> Robbert
>

[-- Attachment #1.2: Type: text/html, Size: 3751 bytes --]

Re: [HoTT] Vladimir Voevodsky

[Nicolai Kraus]

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

Truly sad news. I did not know Vladimir well, but I had the privilege to 
talk with him and get his advice at several occasions. Much of what I 
have been doing during the last couple of years was either directly or 
indirectly based on some of Vladimir's many ideas, most importantly 
maybe his observation that homotopy/truncation levels can be defined 
internally in type theory.
May he rest in peace.
Nicolai


On 01/10/17 05:25, Daniel R. Grayson wrote:
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced 
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our 
> dear colleague and friend, Vladimir Voevodsky, Professor in the School 
> of Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of 
> our community. His death is a tremendous loss for the Institute and 
> for the world. We will all miss him dearly and extend our deepest 
> condolences to Vladimir’s family and his many colleagues and 
> collaborators around the world.
>
> We will soon be sharing more information about a gathering to 
> celebrate Vladimir’s life and legacy.
>
> Robbert
> -- 
> 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: 4653 bytes --]

Re: [HoTT] Vladimir Voevodsky

[Chris Kapulkin]

Dear all,

This is very sad news indeed.

For the past three decades, Vladimir has been a leading figure in
mathematics, making landmark contributions to several areas: algebraic
geometry, homotopy theory, and number theory, among others. In his
work he settled multiple open problems, including the conjectures of
Milnor and Bloch-Kato, and his insights led to the creation of whole
new areas of mathematics such as motivic homotopy theory and homotopy
type theory.

Vladimir's style of doing mathematics can be compared only to
Grothendieck's. Those of us who had an honor of working with him know
that, faced with a problem, he would always rethink its basic
definitions and assumptions, to find an elegant and clean solution. He
saw structure where the rest of us were only able to see chaos.

In all aspects of his work, Vladimir was a visionary. He put forward
ideas that seemed unrealistic at first, and then systematically
completed them. He had a clear set of principles that he followed, but
he was not stubborn. On the contrary, even as a beginning graduate
student, I consistently felt that Vladimir treated me, and everyone
else, with an incredible amount of respect and would come to every
conversation ready to change his opinion.

Vladimir has shaped the way I think about mathematics and how I
perceive the beauty of it. Every single conversation that we had made
me a better mathematician, and I still have to come to terms with the
fact that there are so many questions I will not get to ask him.

Our community has lost its creator and the greatest of its members. I
have lost a mentor, a collaborator, and a friend.

Chris Kapulkin

On Sun, Oct 1, 2017 at 12:25 AM, Daniel R. Grayson
<danielrich...@gmail.com> wrote:
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced Study
> in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our dear
> colleague and friend, Vladimir Voevodsky, Professor in the School of
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our
> community. His death is a tremendous loss for the Institute and for the
> world. We will all miss him dearly and extend our deepest condolences to
> Vladimir’s family and his many colleagues and collaborators around the
> world.
>
> We will soon be sharing more information about a gathering to celebrate
> Vladimir’s life and legacy.
>
> Robbert
>
> --
> 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.

Re: [HoTT] Vladimir Voevodsky

[Marcelo Fiore]

[-- Attachment #1.1: Type: text/plain, Size: 4075 bytes --]

Dear All, 

This is shocking news indeed.  

I only got to know Vladimir quite recently, while he kindly came to visit 
me 
at the end of April, before the Big Proof INI programme.  He arrived at the 
Computer Lab and immediately wanted to discuss mathematics, specifically 
that of type systems, which we did on the first day and regularly 
thereafter.  
It took us a bit of time to understand how to interact mathematically with 
each other, but we got there.  In the process, we did some work together 
and I got fond of him.  It is a real shame that he won't be around; 
personally 
because we had plans but, most importantly, for the loss that it represents 
to the field.

Marcelo Fiore.


On Sunday, 1 October 2017 21:09:19 UTC+1, Krzysztof Kapulkin wrote:
>
> Dear all, 
>
> This is very sad news indeed. 
>
> For the past three decades, Vladimir has been a leading figure in 
> mathematics, making landmark contributions to several areas: algebraic 
> geometry, homotopy theory, and number theory, among others. In his 
> work he settled multiple open problems, including the conjectures of 
> Milnor and Bloch-Kato, and his insights led to the creation of whole 
> new areas of mathematics such as motivic homotopy theory and homotopy 
> type theory. 
>
> Vladimir's style of doing mathematics can be compared only to 
> Grothendieck's. Those of us who had an honor of working with him know 
> that, faced with a problem, he would always rethink its basic 
> definitions and assumptions, to find an elegant and clean solution. He 
> saw structure where the rest of us were only able to see chaos. 
>
> In all aspects of his work, Vladimir was a visionary. He put forward 
> ideas that seemed unrealistic at first, and then systematically 
> completed them. He had a clear set of principles that he followed, but 
> he was not stubborn. On the contrary, even as a beginning graduate 
> student, I consistently felt that Vladimir treated me, and everyone 
> else, with an incredible amount of respect and would come to every 
> conversation ready to change his opinion. 
>
> Vladimir has shaped the way I think about mathematics and how I 
> perceive the beauty of it. Every single conversation that we had made 
> me a better mathematician, and I still have to come to terms with the 
> fact that there are so many questions I will not get to ask him. 
>
> Our community has lost its creator and the greatest of its members. I 
> have lost a mentor, a collaborator, and a friend. 
>
> Chris Kapulkin 
>
> On Sun, Oct 1, 2017 at 12:25 AM, Daniel R. Grayson 
> <daniel...@gmail.com <javascript:>> wrote: 
> > Dear Colleagues, 
> > 
> > The following message from the director of the Institute for Advanced 
> Study 
> > in Princeton announces 
> > sad news: 
> > 
> > ---------- Forwarded message ---------- 
> > Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT) 
> > From: Robbert Dijkgraaf 
> > Subject: Sad news 
> > 
> > Dear Colleagues, 
> > 
> > It is with a heavy heart that I write to share some very sad news. Our 
> dear 
> > colleague and friend, Vladimir Voevodsky, Professor in the School of 
> > Mathematics, passed away unexpectedly this morning. 
> > 
> > Vladimir was a truly extraordinary mathematician and integral part of 
> our 
> > community. His death is a tremendous loss for the Institute and for the 
> > world. We will all miss him dearly and extend our deepest condolences to 
> > Vladimir’s family and his many colleagues and collaborators around the 
> > world. 
> > 
> > We will soon be sharing more information about a gathering to celebrate 
> > Vladimir’s life and legacy. 
> > 
> > Robbert 
> > 
> > -- 
> > 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 <javascript:>. 
> > For more options, visit https://groups.google.com/d/optout. 
>

[-- Attachment #1.2: Type: text/html, Size: 5105 bytes --]

Re: Vladimir Voevodsky

[Andrew Polonsky]

[-- Attachment #1.1: Type: text/plain, Size: 1248 bytes --]

An incredible life, full of incredible service to the science and the 
mathematical community.

May he finally find peace -- and then harmony -- that was grudged him by 
the human world.

Andrew

On Sunday, October 1, 2017 at 6:25:36 AM UTC+2, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced 
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our 
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of 
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our 
> community. His death is a tremendous loss for the Institute and for the 
> world. We will all miss him dearly and extend our deepest condolences to 
> Vladimir’s family and his many colleagues and collaborators around the 
> world.
>
> We will soon be sharing more information about a gathering to celebrate 
> Vladimir’s life and legacy.
>
> Robbert
>

[-- Attachment #1.2: Type: text/html, Size: 3075 bytes --]

Re: [HoTT] Vladimir Voevodsky

[Andrej Bauer]

This summer in Cambridge, Vladimir and I planned a dinner but then had
to cancel it due to other obligations. The last message I got from
Vladimir said:

"Someplace else and hopefully not in too distant a future, Ok?"

I will miss Vladimir.

Andrej

Re: Vladimir Voevodsky

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 2137 bytes --]

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.

On Sunday, 1 October 2017 05:25:36 UTC+1, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced 
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our 
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of 
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our 
> community. His death is a tremendous loss for the Institute and for the 
> world. We will all miss him dearly and extend our deepest condolences to 
> Vladimir’s family and his many colleagues and collaborators around the 
> world.
>
> We will soon be sharing more information about a gathering to celebrate 
> Vladimir’s life and legacy.
>
> Robbert
>


[-- Attachment #1.2: Type: text/html, Size: 418124 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Gershom B]

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

The NY Category Theory Seminar devoted tonight's session to the
commemoration of Vladimir. We had prior conducted a multi-year group
read of the HoTT book. We had a little discussion of motivic homotopy
theory and the Bloch–Kato conjecture, though none of us are terribly
familiar with the topic. We also read aloud some of the tributes to
him written by others, and concluded with a mathematical discussion of
the initiality conjecture and B- and C-systems.

We took the photo attached (which is rather blurry, due to being taken
by a camera with a timer) at the end. Behind us on the right is the
definition of a C-system, and on the left is the univalence axiom.

HIs contributions were immense, his vision was far-reaching, and the
impact of his work will continue to unfold in years to come.

—Gershom

[-- Attachment #2: Ny Category Seminar Oct 4.jpg --]
[-- Type: image/jpeg, Size: 197578 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Timothy Carstens]

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

A few years ago, one of the mailing lists advertised a foundations talk he
was to give at the Harvard math department. I flew out to Boston and snuck
in, figuring the Harvard people would assume I was MIT and conversely. I
was found-out, though, as people were filing out after his talk; of course
everyone knows everyone else.

I knew his work from my days as a geometer. It was the sort of thing you
see in grad school and it impresses its beauty upon you forever. I came out
because I'd heard this and that about HoTT and it seemed like a good
opportunity to peek into that world. He seemed surprised that someone not
in-the-know would make the trip. We talked for a bit. He was generous with
his time in a way that struck me as incredibly humble. To the extent that
mathematicians have fans, he was good to his.


On Wed, Oct 4, 2017 at 9:52 PM, Gershom B <gers...@gmail.com> wrote:

> The NY Category Theory Seminar devoted tonight's session to the
> commemoration of Vladimir. We had prior conducted a multi-year group
> read of the HoTT book. We had a little discussion of motivic homotopy
> theory and the Bloch–Kato conjecture, though none of us are terribly
> familiar with the topic. We also read aloud some of the tributes to
> him written by others, and concluded with a mathematical discussion of
> the initiality conjecture and B- and C-systems.
>
> We took the photo attached (which is rather blurry, due to being taken
> by a camera with a timer) at the end. Behind us on the right is the
> definition of a C-system, and on the left is the univalence axiom.
>
> HIs contributions were immense, his vision was far-reaching, and the
> impact of his work will continue to unfold in years to come.
>
> —Gershom
>
> --
> 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: 2704 bytes --]

Re: [HoTT] Vladimir Voevodsky

[Thierry Coquand]

[-- 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 --]

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 8699 bytes --]

Here is the relevant part of the oldest email I have from Vladimir about 
computer proof:

-----------------------------------------------------------------------------
    Date: Tue, 10 Sep 2002 09:15:21 -0400 (EDT)
    From: Vladimir Voevodsky <vlad...@ias.edu>
    To: d...@math.uiuc.edu
    Subject: Re: Fields Medal

    ...

    Vladimir.

    PS I am thinking again about the applications of computers to pure
    math. Do you know of anyone working in this area? I mean mostly some
    kind of a computer language to describe mathematical structures, their
    properties and proofs in such a way that ultimately one may have
    mathematical knowledge archived and logically verified in a fixed
    format.
-----------------------------------------------------------------------------

And here is a brainstorm of his about a computer oracle based on "homotopy
lambda-calculus".  Notice that the concepts of h-level and univalence are
already present, at least in some prescient form.  (Vladimir recently told 
me
that he thought his concept of h-level is much more important than the
univalence axiom.)  You may also notice the early appearance of Brazil.

-----------------------------------------------------------------------------
    From: Vladimir Voevodsky <vlad...@ias.edu>
    Subject: Re: computers and math and education
    Date: Fri, 29 Sep 2006 15:51:36 -0400
    To: d...@math.uiuc.edu

    Dear Dan,

    what you write about the conference is very interesting. Before I get  
    into more detailed comments, a request -- if you learn about some  
    interesting meetings related to this stuff please let me know.

    > The main lesson for me (from all the sessions, not that one tale)  
    > is that these
    > systems are mainly usable by the creator, because the creator can  
    > more or less
    > remember the names of 200 trivial theorems.  It won't scale up  
    > unless searching
    > is improved.  I think you have mentioned to me that searching is  
    > what you are
    > thinking about.

    My whole concept of what one should aim at while developing  
    "productivity software" for pure math has been evolving lately in the  
    following direction.

    Let us start with what would be a perfect system of such sort (such a  
    system is impossible but let's ignore it for a moment).

    Ideally one wants a math oracle. A user inputs a type expression and  
    the system either returns a term of this type or says that it has no  
    terms. The type expression may be "of level 0" i.e. it can correspond  
    to a statement in which case a term is a proof and the absence of  
    terms means that the statement is not provable. It may be "of level  
    1" e.g. it might be the type of solutions of an equation. In that  
    case the system produces a solution or says that there are non. It  
    may be "of level 2" e.g. It might be the type of all solvable groups  
    of order 35555. In that case the system produces an example of such a  
    group etc.

    A realistic approximation of such an oracle may look as follows.  
    Imagine a web-based system with a lot of users (both "creators" and  
    "consumers") and a very large "database". Originally the database is  
    empty (or, rather, contains only the primitive "knowledge" a-la  
    axioms). User A (say in Princeton) inputs a type expression and  
    builds up a term of this type either in one step (just types it in)  
    or in many steps  using the standard proof-assistant capabilities of  
    the system. Both the original and all the intermediate type  
    expressions which occur in the process are filed (in the real time)  
    in the database.  Enter user B (somewhere in Brazil), who inputs  
    another type expression and begins the process of constructing a term  
    of his type. All the intermediate type expressions which show up as  
    well as their negations are filed and also compared in real time with  
    the ones already in the database. If a match occurs the user is  
    informed that this and that type has been considered before and the  
    following terms of this type are known (or it negation has been and  
    terms are known in which case one assumes that the original type has  
    no terms).  Eventually, the database is large enough such that in  
    many cases the system will work like an oracle i.e. will provide  
    information on terms of the type which user B is interested in.

    Clearly, designing such a system may take decades and it can only  
    materialize if a lot of people work on it.  I can see a number of  
    reasonably independent tasks which have to be taken care of:

    1. To choose a formalization or formalizations of mathematics which  
    will be used to translate problems into type expressions. In the case  
    of multiple formalizations there should be modules which mechanically  
    translate from one to another.

    2. To design the proof-assistant part including modules which could  
    do computations (e.g. computational algebra)

    3. To understand what the system does when a request for a term of a  
    given type is submitted to the database.

    The basic operation is of course simple comparison with something  
    previously filed. In most cases however the submitted type expression  
    will be equivalent to a one already in the database not equal. On the  
    very elementary level this can be an equivalence which can be  
    recognized by some normalization procedure, using De Bruijn indexes  
    etc. On a slightly more complex level it can be say the permutation  
    of factors such as (A or B) versus (B or A).  More about this issue  
    below.

    Clearly the  system should consider both the original type and its  
    negation in parallel. It also should "split" combined types such as  
    (A or B) and (A and B) and analyze components separately. Finally, it  
    might look for types which obviously map to the one under  
    consideration and which have known terms.

    4. Implementation side which with at least two parts --  
    "networking" (where the "database" is kept, how it is done if it is  
    not centralized but distributed etc.) and "interface" (I personally  
    like drag-and-drop's :)) "Interface" part also includes the question  
    of what kind of hints one wants from the system when a complete  
    answer is not available e.g. if a user is trying to prove that  (A or  
    B) holds and the system can come up with a counterexample (a proof of  
    the negation) to A then should probably inform the user about it.  
    Similarly, if one tries to prove (A and B) and the system knows a  
    proof of A it should also let it be known.

    5. Eventually, there should be "daemons" which would  wonder around  
    the database, extend it and clean it up - this is an AI issue. It  
    might be real fun when we get there.

    It is clear that such a system can be useful only if it is good at  
    recognizing when two type expressions are equivalent. How easy or  
    hard it is depends a lot on the choice of the underlying  
    formalization. For example, the ZF formalization is notoriously bad  
    in this respect (also, it is not a type system but a first order  
    theory so the reduction of everything to the question of finding a  
    term of a particular type is not really applicable). If one writes   
    the following two statements:

    a. for all x in N such that x<1 one has x=0
    b. for all x in Z such that x>=0 and x<1 one has x=0

    in ZF they will look so different that it is hard to imagine a  
    program which will recognize their equivalence. Normally one would do  
    it but showing first that  the types N and Zplus=(all x in Z such  
    that x>=0) are equivalent.  In ZF however they are *not* equivalent  
    since it is easy to make a statement about one which is false for  
    another. E.g. empty set is an element of N but not of Zplus.

    My homotopy lambda calculus is an attempt to create a system which is  
    very good at dealing with equivalences. In particular it is supposed  
    to have the property that given any type expression F(T) depending on  
    a term subexpression t of type T and an equivalence t->t' (a term of  
    the type Eq(T;t,t')) there is a mechanical way to create a new  
    expression F' now depending on t' and an equivalence between F(T) and  
    F'(T') (note that to get F' one can not just substitute t' for t in F  
    -- the resulting expression will most likely be syntactically  
    incorrect).
-----------------------------------------------------------------------------


[-- Attachment #1.2: Type: text/html, Size: 11158 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Michael Shulman]

I met Voevodsky in 2010, when I was a postdoc at the University of
Chicago, and Steve Awodey invited me to CMU to hear Voevodsky talk
about his work on h-levels and univalence.  At the time I was still
struggling to wrap my head around type theory.  Voevodsky showed us
his Coq development, which ended with the construction of a function
assigning to each finite set its cardinality, and showing that Coq
could evaluate this function on the proof that finite sets are closed
under coproducts to compute something like 2+2=4.

Coming from homotopy theory and higher category theory, I found it
very natural to identify propositions with (-1)-types, and of course
every finite set should have a cardinality!  Finally, type theory
started to make sense to me.  This was the genius of his definitions
of h-level and univalence, which like many transformative innovations
seem inevitable in hindsight: they were the foundation stones of a
real bridge between type theory and higher category theory.

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 5080 bytes --]

Here is another old email from Vladimir to me.  He reports that he has 
found a model for
dependent type theory in simplicial sets and begun thinking about writing 
his own
proof assistant.

-----------------------------------------------------------------------------

From: Vladimir Voevodsky <vlad...@ias.edu>
Date: May 1, 2006 9:26:06 PM EDT (CA)
To: Vladimir Voevodsky <vlad...@ias.edu>
Subject: Re: computers and math and education

Dear Dan,

sorry for a slow reply. I am in a kind of a transitional state in  
my work on all this proof related stuff and could not decide what  
is the best way to proceed. I think I still need a week or two to  
get to a point where I know myself what I want to do next.

I remember what we talked about last time but do not remember  
anything about your code. What language are you using? What kind of  
formalism? Here is my story:

I have come a long way since our last conversations. I have learned  
to some extend three existing "proof assistants" (well, "learned"  
is a bit too strong....) Mizar (based on ZF-theory), PVS (based on  
simple type theory) and Coq (based on a polymorphic, dependent type  
system called 'calculus of inductive constructions' which is not  
really described anywhere. See the e-mail from Carlos Simpson below.).

I got convinced that dependent type systems is the best available  
framework for formalization of math. The first problem with these  
systems is that they lack(ed) "standard" model. I think I have  
invented such a model. It takes values in the homotopy category  
such that the model of the type of say groups is (equivalent to)  
the nerve of the groupoid of groups and isomorphisms.

Having this new semantics I made some progress in modification of  
existing type systems to make them more complete for this "H- 
model". The homotopy lambda calculus which I gave some talks about  
is this modification.  I am not entirely happy with the definition  
I have and keep thinking about how to make it better. I am also  
working on proving the existence of H-models for it and for some  
more basic type systems rigorously. This activity is basically a  
mixture of category theory and homotopy theory of simplicial sets  
with some basic type theory.  Below is a copy of my message to  
Peter May with one of he questions related to this activity.

Despite the fact that homotopy lambda calculus is far from being  
"done" I am pretty convinced that it is a step in the right  
direction. So I have started to work on a "proof assistant" based  
on this system. I figured that  it makes sense to program what  
there is and that in the process I get a better feeling for what  
has to be modified and how.

I have though about proof assistants quite a bit last year and in  
particular about what are they really good for or should be good  
for. I decided that for them to be useful it is crucial that they  
have "memory" which can be "queried". Simplifying things a bit I  
see the "workflow" as follows.

In type theory statements (propositions as they call it) are just  
types of a special kind (what this "kind" is becomes very clear in  
the H-lambda). Theorems are propositions which have members  
(members themselves encode proofs). Hence an ideal (and impossible)  
proof assistant would be a program where I can input a type  
expression and the system will return either a term (member) of  
this type or will tell me that this type has no members.

New type expressions are usually built from some previously known  
ones. Since one does not want to write all definitions from point  
zero there should be a library of existing types where one can get  
building blocks for the type expression which forms the query.

Hence the memory  - to contain all questions which have been asked  
previously (type expressions) and all answers which have been found  
(terms). This memory or at least some parts of it should be shared  
(using some kind of web sharing paradigm)  so that if someone  
places a query or find an answer to a query everybody else has  
access to it.

Right now I am thinking about the structure of such a memory. I  
feel this has to be done at least on conceptual level before  
everything else. My feeling is that it might get pretty large and  
that it is crucial to organize it in a way which makes using it  
*fast* for the computer so in particular I am thinking about an  
essentially binary format (not expressions themselves but a  
structure formed by already parsed expressions connected by  
references to each other). I also feel that it is Ok if it contains  
a lot of repeats and redundancy (e.g. a thousand slightly different  
definition of what a group is) since it is not to be directly  
accessed by humans and since it is not a problem for a computer to  
compare to each other a thousand arrays of length thousand.

That's where I am now. I have just started this memory thing and I  
hope to get a better feel for it in a week or two.

Volodia.

-----------------------------------------------------------------------------


[-- Attachment #1.2: Type: text/html, Size: 6414 bytes --]

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 3499 bytes --]

At https://en.wikipedia.org/wiki/Homotopy_type_theory Voevodsky says this:

"Also in 2009, Voevodsky worked out more of the details of a model of type
theory in Kan complexes, and observed that the existence of a universal Kan
fibration could be used to resolve the coherence problems for categorical
models of type theory. He also proved, using an idea of A. K. Bousfield, 
that
this universal fibration was univalent: the associated fibration of pairwise
homotopy equivalences between the fibers is equivalent to the paths-space
fibration of the base."

When I asked him about that, he showed me the email from Bousfield, 
answering Vladimir's question as forwarded by Peter May, containing
a very nice description of the idea, and here it is:

-----------------------------------------------------------------------------
Date:    Mon, 01 May 2006 10:10:30 CDT
To:      Peter May <m...@math.uchicago.edu>
cc:      jar...@uwo.ca, pgo...@math.northwestern.edu
From:    "A. Bousfield" <bo...@uic.edu>
Subject: Re: Simplicial question

Dear Peter,

I think that the answer to Voevodsky's basic question is "yes," and I'll
try to sketch a proof.

Since the Kan complexes X and Y are homotopy  equivalent, they share the
same minimal complex M, and we have trivial fibrations X -> M  and Y -> M
by Quillen's main lemma in "The geometric realization of a Kan fibration
."  Thus  X + Y -> M + M is also a trivial fibration where "+" gives the
disjoint union.  We claim that the composition of  X + Y -> M + M with the
inclusion  M + M >-> M x Delta^1 may be factored as the composition of an
inclusion X + Y >-> E with a trivial fibration  E -> M x Delta^1 such that
the counterimage of  M + M is  X + Y.  We may then obtain the desired
fibration

E  ->  M x Delta^1  ->  Delta^1

whose fiber over 0 is X and whose fiber over 1 is Y.

We have used a case of:

Claim. The composition of a trivial fibration A -> B with an inclusion B
-> C may be factored as the composition of an inclusion A >-> E  with a
trivial fibration  E -> C such that the counterimage of B is A.

I believe that this claim follows by a version of the usual iterative
construction of a Quillen factorization for A -> C using the "test"
cofibrations
Dot Delta^k >-> Delta^k
for all k. At each stage, we use maps from the "test" cofibrations
involving k-simplices of C outside of B.

I hope that this helps --  I haven't thought about Voevodsky's  more
general question.

Best regards,
Pete

    On Sun, 30 Apr 2006, Peter May wrote:

    Here is an extract from an email from Voevodsky (vlad...@ias.edu)

    -----------------

Q. Let X and Y be a pair of Kan simplicial sets which are homotopy
equivalent. Is there a Kan fibration E -> \Delta^1 such that its
fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an
iso)?

A more advanced version of the same question: let X' -> X  and X'' ->
X be two Kan fibrations which are fiberwise equivalent to each other
over X. Is there a kan fibration over X\times\Delta^1 whose fiber
over X\times 0 is isomorphic to X', fiber over  X\times 1 is
isomorphic to X'' and the homotopy between the two inclusions of X to
X\times\Delta^1 define the original equivalence (up to homotopy)?

I encountered this issue trying to write up a semantics for dependent
type systems with values in the homotopy category. which is in turn
related to the problem of creating computer programs for proof
verification.
-----------------------------------------------------------------------------


[-- Attachment #1.2: Type: text/html, Size: 5192 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Steve Awodey]

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

thanks for posting this Dan. 
It’s very interesting to learn the background of the discovery of univalence.

Steve

> On Oct 11, 2017, at 1:47 PM, Daniel R. Grayson <danielrich...@gmail.com <mailto:danielrich...@gmail.com>> wrote:
> 
> At https://en.wikipedia.org/wiki/Homotopy_type_theory <https://en.wikipedia.org/wiki/Homotopy_type_theory> Voevodsky says this:
> 
> "Also in 2009, Voevodsky worked out more of the details of a model of type
> theory in Kan complexes, and observed that the existence of a universal Kan
> fibration could be used to resolve the coherence problems for categorical
> models of type theory. He also proved, using an idea of A. K. Bousfield, that
> this universal fibration was univalent: the associated fibration of pairwise
> homotopy equivalences between the fibers is equivalent to the paths-space
> fibration of the base."
> 
> When I asked him about that, he showed me the email from Bousfield, 
> answering Vladimir's question as forwarded by Peter May, containing
> a very nice description of the idea, and here it is:
> 
> -----------------------------------------------------------------------------
> Date:    Mon, 01 May 2006 10:10:30 CDT
> To:      Peter May <m...@math.uchicago.edu <mailto:m...@math.uchicago.edu>>
> cc:      jar...@uwo.ca <mailto:jar...@uwo.ca>, pgo...@math.northwestern.edu <mailto:pgo...@math.northwestern.edu>
> From:    "A. Bousfield" <bo...@uic.edu <mailto:bo...@uic.edu>>
> Subject: Re: Simplicial question
> 
> Dear Peter,
> 
> I think that the answer to Voevodsky's basic question is "yes," and I'll
> try to sketch a proof.
> 
> Since the Kan complexes X and Y are homotopy  equivalent, they share the
> same minimal complex M, and we have trivial fibrations X -> M  and Y -> M
> by Quillen's main lemma in "The geometric realization of a Kan fibration
> ."  Thus  X + Y -> M + M is also a trivial fibration where "+" gives the
> disjoint union.  We claim that the composition of  X + Y -> M + M with the
> inclusion  M + M >-> M x Delta^1 may be factored as the composition of an
> inclusion X + Y >-> E with a trivial fibration  E -> M x Delta^1 such that
> the counterimage of  M + M is  X + Y.  We may then obtain the desired
> fibration
> 
> E  ->  M x Delta^1  ->  Delta^1
> 
> whose fiber over 0 is X and whose fiber over 1 is Y.
> 
> We have used a case of:
> 
> Claim. The composition of a trivial fibration A -> B with an inclusion B
> -> C may be factored as the composition of an inclusion A >-> E  with a
> trivial fibration  E -> C such that the counterimage of B is A.
> 
> I believe that this claim follows by a version of the usual iterative
> construction of a Quillen factorization for A -> C using the "test"
> cofibrations
> Dot Delta^k >-> Delta^k
> for all k. At each stage, we use maps from the "test" cofibrations
> involving k-simplices of C outside of B.
> 
> I hope that this helps --  I haven't thought about Voevodsky's  more
> general question.
> 
> Best regards,
> Pete
> 
>     On Sun, 30 Apr 2006, Peter May wrote:
> 
>     Here is an extract from an email from Voevodsky (vlad...@ias.edu <mailto:vlad...@ias.edu>)
> 
>     -----------------
> 
> 	Q. Let X and Y be a pair of Kan simplicial sets which are homotopy
> 	equivalent. Is there a Kan fibration E -> \Delta^1 such that its
> 	fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an
> 	iso)?
> 
> 	A more advanced version of the same question: let X' -> X  and X'' ->
> 	X be two Kan fibrations which are fiberwise equivalent to each other
> 	over X. Is there a kan fibration over X\times\Delta^1 whose fiber
> 	over X\times 0 is isomorphic to X', fiber over  X\times 1 is
> 	isomorphic to X'' and the homotopy between the two inclusions of X to
> 	X\times\Delta^1 define the original equivalence (up to homotopy)?
> 
> 	I encountered this issue trying to write up a semantics for dependent
> 	type systems with values in the homotopy category. which is in turn
> 	related to the problem of creating computer programs for proof
> 	verification.
> -----------------------------------------------------------------------------
> 
> 
> -- 
> 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 <https://groups.google.com/d/optout>.


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

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 1545 bytes --]

This email from Vladimir seems to be from a time when he had just learned 
more about Coq but had not yet started using it:

From: "Vladimir Voevodsky" <vlad...@ias.edu>
Subject: Re: theorem proving
Date: Wed, December 30, 2009 10:34 am
To: "Daniel R. Grayson" <d...@math.uiuc.edu>

Hi Dan,

thanks for the link. I have heard about this one (from coq-club actually on
which list I am since several years ago). All is well with me, all of the
Bloch-Kato papers are submitted to journals for about a year now and many 
are
accepted. 

I am thinking a lot these days about foundations of math and automated proof
verification. My old idea about a "univalent" homotopy theoretical models of
Martin-Lof type systems survived the verification stage an I am in the
process of writing things up.

I also took a course at the Princeton CS department which was for most part
about Coq and was very impressed both by how much can be proved in it in a
reasonable time and by how many young students attended (45, 35 undergrad +
10 grad!). 

How are you?

Vladimir. 


On Dec 29, 2009, at 8:43 PM, Daniel R. Grayson wrote:

> Volodya,
> 
> This seems to be a good theorem proving conference to attend this summer:
> 
>        https://sympa-roc.inria.fr/wws/arc/coq-club/2009-12/msg00057.html
> 
>                           Call for Papers
>         ITP 2010: Conference on Interactive Theorem Proving
>                 11-14 July 2010, Edinburgh, Scotland
>              http://www.floc-conference.org/ITP-cfp.html
> 
> I hope all is well for you.
> 
> Dan


[-- Attachment #1.2: Type: text/html, Size: 2196 bytes --]

Re: Vladimir Voevodsky

[Daniel R. Grayson]

[-- Attachment #1.1: Type: text/plain, Size: 93 bytes --]

PS: it is the oldest email I have from him with the word "univalent" or 
"univalence" in it.

[-- Attachment #1.2: Type: text/html, Size: 132 bytes --]

Re: Vladimir Voevodsky

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 2154 bytes --]

On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote:
>
> PS: it is the oldest email I have from him with the word "univalent" or 
> "univalence" in it.
>

 In the vein of bringing to public record  things that Vladimir said, here 
is a short interview.

-------- Forwarded Message --------
Subject: Re: historical question
Date: Thu, 22 Oct 2015 16:08:14 -0400
From: Vladimir Voevodsky <vlad...@ias.edu>
To: Martin Escardo <m.es...@cs.bham.ac.uk>
CC: Prof. Vladimir Voevodsky <vlad...@ias.edu>


> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk> 
wrote:
> 
> Hi Vladimir,
> 
> (0) When did you formulate hlevels in type theory?

Probably in early 2010

> (1) When did you formulate the univalence axiom?

Originally in 2005 as a property of morphisms (fibrations). In late 2009 as 
a formula in type theory.

> 
>    (And when did you give your model for it?)

In a sense in 2006, only I did not know how to model the Martin-Lof 
identity types and thought that different identity types will need to be 
introduced that will satisfy univalence but what other properties to 
require from them I did not know.

> 
> (2) When did you prove that univalence implies function extensionality?

July 2010.

> 
> I am giving a talk next week trying to rigorously explain the univalence
> axiom to classical mathematicians. This will involve, of course, trying
> to first explain Martin-Loef type theory, particularly the identity type.
> 
> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid
> model, in which they have a proto-form of univalence. Were you inspired
> by that, or were your thoughts independent of that?

I was not inspired by it. In fact I tried several times to understand what 
they are saying and never could.

> 
> (Also: what was your first reaction when you saw the identity type for
> the first time? Did you immediately connect it with path spaces?)

Not at all. I did not make this connection until late 2009. All the time 
before it I was hypnotized by the mantra that the only inhabitant of the Id 
type is reflexivity which made then useless from my point of view.

Vladimir.



[-- Attachment #1.2: Type: text/html, Size: 3024 bytes --]

Re: [HoTT] Re: Vladimir Voevodsky

[Michael Shulman]

Regarding (0), I'm fairly certain that h-levels were pretty solidly
established in the Coq code that he showed us at CMU in February 2010.
So if he did formulate them in "early 2010" it was very early in the
year.

On Thu, Oct 12, 2017 at 2:55 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote:
>>
>> PS: it is the oldest email I have from him with the word "univalent" or
>> "univalence" in it.
>
>
>  In the vein of bringing to public record  things that Vladimir said, here
> is a short interview.
>
> -------- Forwarded Message --------
> Subject: Re: historical question
> Date: Thu, 22 Oct 2015 16:08:14 -0400
> From: Vladimir Voevodsky <vlad...@ias.edu>
> To: Martin Escardo <m.es...@cs.bham.ac.uk>
> CC: Prof. Vladimir Voevodsky <vlad...@ias.edu>
>
>
>> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
>> wrote:
>>
>> Hi Vladimir,
>>
>> (0) When did you formulate hlevels in type theory?
>
> Probably in early 2010
>
>> (1) When did you formulate the univalence axiom?
>
> Originally in 2005 as a property of morphisms (fibrations). In late 2009 as
> a formula in type theory.
>
>>
>>    (And when did you give your model for it?)
>
> In a sense in 2006, only I did not know how to model the Martin-Lof identity
> types and thought that different identity types will need to be introduced
> that will satisfy univalence but what other properties to require from them
> I did not know.
>
>>
>> (2) When did you prove that univalence implies function extensionality?
>
> July 2010.
>
>>
>> I am giving a talk next week trying to rigorously explain the univalence
>> axiom to classical mathematicians. This will involve, of course, trying
>> to first explain Martin-Loef type theory, particularly the identity type.
>>
>> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid
>> model, in which they have a proto-form of univalence. Were you inspired
>> by that, or were your thoughts independent of that?
>
> I was not inspired by it. In fact I tried several times to understand what
> they are saying and never could.
>
>>
>> (Also: what was your first reaction when you saw the identity type for
>> the first time? Did you immediately connect it with path spaces?)
>
> Not at all. I did not make this connection until late 2009. All the time
> before it I was hypnotized by the mantra that the only inhabitant of the Id
> type is reflexivity which made then useless from my point of view.
>
> Vladimir.
>
>
> --
> 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.

Re: Vladimir Voevodsky

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 572 bytes --]

Also this may be of historical interest:

> I was visiting Fabien Morel in Munich in the Fall of 2009. He introduced 
me to Helmut Schwichtenberg. Helmut introduced me to Streicher and Hofmann. 
Then someone  pointed to me Bob Harper as the person who is probably 
closest to what I am interested and close to Princeton. I contacted Bob and 
we organized my visit to CMU. There Bob introduced me to Awodey. 

Vladimir.

On Oct 22, 2015, at 3:35 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

And also: how did you get in touch with the type theory crowd and when? M.


[-- Attachment #1.2: Type: text/html, Size: 1179 bytes --]

Re: Vladimir Voevodsky

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 742 bytes --]

And the last one of this thread on my historical questions to Vladimir in 
2015:


On Oct 22, 2015, at 4:50 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

One more question, if you don't mind, this time technical: what made
you conjecture that univalence implies function extensionality, before
you had a proof? This is a very interesting thought.


No, it was almost an accident. I started a new file in Foundations that was 
supposed to contain results that depend on the UA and then I guess I 
started to think whether the UA and function extensionality are independent 
and came up with a proof of UA => FA. 

I think it was a turning point since  this is were constructivists got 
really interested in the UA (and UF).

Vladimir

>
>

[-- Attachment #1.2: Type: text/html, Size: 2021 bytes --]