Vladimir Voevodsky

[Daniel R. Grayson]

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

[Daniel R. Grayson]

And there is this:  https://www.ias.edu/news/2017/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

[Peter LeFanu Lumsdaine]

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.

[Steve Awodey]

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.

[Joyal, André]

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

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

[Andrei Rodin]

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

[Nicolai Kraus]

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

[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

[Marcelo Fiore]

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.

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

[Andrew Polonsky]

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

[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

[Martín Hötzel Escardó]

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.

[Gershom B]

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

[Timothy Carstens]

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.

[Thierry Coquand]

 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

[Daniel R. Grayson]

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

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

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

[N. Raghavendra]

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

> The following message from the director of the Institute for Advanced

> Study in Princeton announces sad news: ...

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

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

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

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

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

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

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

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

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

Raghu.

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

[Daniel R. Grayson]

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.

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

[Daniel R. Grayson]

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.

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

[Steve Awodey]

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.

[Daniel R. Grayson]

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

[Daniel R. Grayson]

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

[Martín Hötzel Escardó]

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.

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

[Martín Hötzel Escardó]

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.

[Martín Hötzel Escardó]

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