41 views

### Daniel R. Grayson

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

---------- Forwarded message ----------

Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
From: Robbert Dijkgraaf

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.

Robbert

### Daniel R. Grayson

Oct 1, 2017, 12:54:43 AM10/1/17
to Homotopy Type Theory

### Thomas Streicher

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

### Peter LeFanu Lumsdaine

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

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

### Steve Awodey

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.

### Joyal, André

Oct 1, 2017, 11:06:56 AM10/1/17
to Peter LeFanu Lumsdaine, Homotopy Type Theory
Dear homotopy type theorists,

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.

-André J

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

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

### Nicolai Kraus

Oct 1, 2017, 4:06:53 PM10/1/17
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

Oct 1, 2017, 4:09:19 PM10/1/17
to Daniel R. Grayson, Homotopy Type Theory
Dear all,

This is very sad news indeed.

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

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.

### Andrew Polonsky

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

### Andrej Bauer

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

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

Andrej

### Martín Hötzel Escardó

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.

### Gershom B

Oct 5, 2017, 12:52:55 AM10/5/17
to Homotopy Type Theory
The NY Category Theory Seminar devoted tonight's session to the
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
Ny Category Seminar Oct 4.jpg

### Timothy Carstens

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.

### Thierry Coquand

Oct 5, 2017, 6:41:09 AM10/5/17
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

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)
Subject: Re: Fields Medal

...

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.

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

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

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.

### N. Raghavendra

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

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:

----------------------------------------------------------------------
Subject: Re: [HoTT] Voevodsky on formalizing type theory
To: "N. Raghavendra" <ra...@hri.res.in>
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 :)

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

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

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.

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

Date: May 1, 2006 9:26:06 PM EDT (CA)
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

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

Oct 11, 2017, 1:47:18 PM10/11/17
to Homotopy Type Theory

"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,
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.
-----------------------------------------------------------------------------

### Steve Awodey

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.

### Daniel R. Grayson

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:

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

Hi Dan,

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 +

How are you?

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

### Daniel R. Grayson

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.

### Martín Hötzel Escardó

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
To: Martin Escardo <m.es...@cs.bham.ac.uk>

> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
> (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.

### Michael Shulman

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.

### Martín Hötzel Escardó

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.

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ó

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