277 views

Skip to first unread message

Oct 1, 2017, 12:25:36 AM10/1/17

to Homotopy Type Theory

Dear Colleagues,

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

sad news:

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

Oct 1, 2017, 12:54:43 AM10/1/17

to Homotopy Type Theory

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

Oct 1, 2017, 4:07:28 AM10/1/17

to Daniel R. Grayson, Homotopy Type Theory

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

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

Oct 1, 2017, 9:18:57 AM10/1/17

to Homotopy Type Theory

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 HomotopyTypeTheory+unsub...@googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

Oct 1, 2017, 10:48:31 AM10/1/17

to Daniel R. Grayson, Homotopy Type Theory

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

--

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.

Oct 1, 2017, 11:06:56 AM10/1/17

to Peter LeFanu Lumsdaine, Homotopy Type Theory

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

To unsubscribe from this group and stop receiving emails from it, send an email to
HomotopyTypeThe...@googlegroups.com.

Oct 1, 2017, 1:08:05 PM10/1/17

to Homotopy Type Theory

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

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

Oct 1, 2017, 4:06:53 PM10/1/17

to HomotopyT...@googlegroups.com

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

May he rest in peace.

Nicolai

Oct 1, 2017, 4:09:19 PM10/1/17

to Daniel R. Grayson, Homotopy Type Theory

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

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

Oct 2, 2017, 9:20:12 AM10/2/17

to Homotopy Type Theory

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.

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.

> email to HomotopyTypeTheory+unsub...@googlegroups.com.

Oct 2, 2017, 10:00:33 AM10/2/17

to Homotopy Type Theory

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

Oct 2, 2017, 11:22:33 AM10/2/17

to Homotopy Type Theory

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

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

Oct 4, 2017, 6:52:43 PM10/4/17

to Homotopy Type Theory

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.

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.

Oct 5, 2017, 12:52:55 AM10/5/17

to Homotopy Type Theory

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

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

Oct 5, 2017, 2:08:17 AM10/5/17

to Homotopy Type Theory

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.

Oct 5, 2017, 6:41:09 AM10/5/17

to HomotopyT...@googlegroups.com

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

Oct 5, 2017, 9:38:20 AM10/5/17

to Homotopy Type Theory

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>

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

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).

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

Oct 6, 2017, 1:41:29 AM10/6/17

to Homotopy Type Theory

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.

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.

Oct 7, 2017, 2:42:51 AM10/7/17

to Daniel R. Grayson, Univalent Mathematics, Homotopy Type Theory

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: ...
> The following message from the director of the Institute for Advanced

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/

Oct 11, 2017, 11:26:23 AM10/11/17

to Homotopy Type Theory

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.

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

Oct 11, 2017, 1:47:18 PM10/11/17

to Homotopy Type Theory

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>

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.

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

Oct 11, 2017, 3:12:48 PM10/11/17

to Daniel R. Grayson, Homotopy Type Theory

thanks for posting this Dan.

It’s very interesting to learn the background of the discovery of univalence.

Steve

--

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.

Oct 12, 2017, 3:06:20 PM10/12/17

to Homotopy Type Theory

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:

>

>

> Call for Papers

> ITP 2010: Conference on Interactive Theorem Proving

> 11-14 July 2010, Edinburgh, Scotland

>

> I hope all is well for you.

>

> Dan

Oct 12, 2017, 3:24:26 PM10/12/17

to Homotopy Type Theory

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

Oct 12, 2017, 5:55:11 PM10/12/17

to Homotopy Type Theory

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.

Oct 12, 2017, 6:21:46 PM10/12/17

to Martín Hötzel Escardó, Homotopy Type Theory

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.

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.

Oct 14, 2017, 5:12:08 PM10/14/17

to Homotopy Type Theory

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.

Oct 14, 2017, 5:20:39 PM10/14/17

to Homotopy Type Theory

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

Reply all

Reply to author

Forward

0 new messages