* Vladimir Voevodsky
@ 2017-10-01 4:25 Daniel R. Grayson
2017-10-01 4:54 ` Daniel R. Grayson
` (11 more replies)
0 siblings, 12 replies; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-01 4:25 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 917 bytes --]
Dear Colleagues,
The following message from the director of the Institute for Advanced Study
in Princeton announces
sad news:
---------- Forwarded message ----------
Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
From: Robbert Dijkgraaf
Subject: Sad news
Dear Colleagues,
It is with a heavy heart that I write to share some very sad news. Our dear
colleague and friend, Vladimir Voevodsky, Professor in the School of
Mathematics, passed away unexpectedly this morning.
Vladimir was a truly extraordinary mathematician and integral part of our
community. His death is a tremendous loss for the Institute and for the
world. We will all miss him dearly and extend our deepest condolences to
Vladimir’s family and his many colleagues and collaborators around the
world.
We will soon be sharing more information about a gathering to celebrate
Vladimir’s life and legacy.
Robbert
[-- Attachment #1.2: Type: text/html, Size: 2706 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
@ 2017-10-01 4:54 ` Daniel R. Grayson
2017-10-01 8:07 ` [HoTT] " Thomas Streicher
2017-10-01 13:18 ` Peter LeFanu Lumsdaine
2017-10-01 14:48 ` [HoTT] " Steve Awodey
` (10 subsequent siblings)
11 siblings, 2 replies; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-01 4:54 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 69 bytes --]
And there is this: https://www.ias.edu/news/2017/vladimir-voevodsky
[-- Attachment #1.2: Type: text/html, Size: 90 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-01 4:54 ` Daniel R. Grayson
@ 2017-10-01 8:07 ` Thomas Streicher
2017-10-01 13:18 ` Peter LeFanu Lumsdaine
1 sibling, 0 replies; 27+ messages in thread
From: Thomas Streicher @ 2017-10-01 8:07 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: 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
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-01 4:54 ` Daniel R. Grayson
2017-10-01 8:07 ` [HoTT] " Thomas Streicher
@ 2017-10-01 13:18 ` Peter LeFanu Lumsdaine
2017-10-01 15:06 ` Joyal, André
1 sibling, 1 reply; 27+ messages in thread
From: Peter LeFanu Lumsdaine @ 2017-10-01 13:18 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 1557 bytes --]
A huge shock, and a massive loss for our field.
Vladimir contributed so much to what the field is today. Most obviously,
with his own direct contributions and early insights into working in type
theory without UIP; also through his influence within the field, with a
strong and well-articulated vision of topics he felt were important to work
on (most concretely, directing and co-ordinating the work of many
contributors in the UniMath library); and of course also through his
outreach to a wider mathematics audience, helping to put type theory and
formalisation on the radar of many people who otherwise might not have
given it attention or interest.
He was always stimulating and insightful, if not always easy to work with —
extremely mathematically exacting. His views and goals were often
idiosyncratic and surprising, but always came from extremely
well-thought-out mathematical grounds, that one might disagree with but
could never dismiss.
We’ve lost a huge contributor and leader in the field, and will all be the
poorer for it.
–Peter.
On Sun, Oct 1, 2017 at 6:54 AM, Daniel R. Grayson <
danielrich...@gmail.com> wrote:
> And there is this: https://www.ias.edu/news/2017/vladimir-voevodsky
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
[-- Attachment #2: Type: text/html, Size: 2268 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
2017-10-01 4:54 ` Daniel R. Grayson
@ 2017-10-01 14:48 ` Steve Awodey
2017-10-01 17:08 ` Andrei Rodin
` (9 subsequent siblings)
11 siblings, 0 replies; 27+ messages in thread
From: Steve Awodey @ 2017-10-01 14:48 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 1760 bytes --]
A tragic loss of a great mathematician and a profound intellect.
Vladimir was the founder and leader of Univalent Foundations, and his loss is a terrible blow.
He suffered for his gifts and he gave us much to be grateful for.
I personally enjoyed his friendship and suffered his scorn, and the former was worth the latter.
Steve
> On Oct 1, 2017, at 12:25 AM, Daniel R. Grayson <danielrich...@gmail.com> wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our dear colleague and friend, Vladimir Voevodsky, Professor in the School of Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our community. His death is a tremendous loss for the Institute and for the world. We will all miss him dearly and extend our deepest condolences to Vladimir’s family and his many colleagues and collaborators around the world.
>
> We will soon be sharing more information about a gathering to celebrate Vladimir’s life and legacy.
>
> Robbert
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
[-- Attachment #2: Type: text/html, Size: 4607 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* RE: [HoTT] Re: Vladimir Voevodsky
2017-10-01 13:18 ` Peter LeFanu Lumsdaine
@ 2017-10-01 15:06 ` Joyal, André
0 siblings, 0 replies; 27+ messages in thread
From: Joyal, André @ 2017-10-01 15:06 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine, Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 2981 bytes --]
Dear homotopy type theorists,
A very sad news.
My first contact with Vladimir and his ideas was at a meeting in Oberwolfach in 2011.
He gave a series of talks on constructive mathematics and homotopy theory, framed
as a tutorial with the proof assistant Coq.
His notion of a contractible object and of an equivalence were striking.
I had a hard time understanding his ideas, because they were described very formally.
He apparently distrusted informal expressions of mathematical ideas.
One evening, he expressed the opinion that Peano arithmetic was inconsistent!
He later came to distrust the applications of his ideas to homotopy theory!
The contributions of Voevodsky to mathematics and to type theory will forever remain.
Thank you Vladimir!
-André J
________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Peter LeFanu Lumsdaine [p.l.lu...@gmail.com]
Sent: Sunday, October 01, 2017 9:18 AM
To: Homotopy Type Theory
Subject: Re: [HoTT] Re: Vladimir Voevodsky
A huge shock, and a massive loss for our field.
Vladimir contributed so much to what the field is today. Most obviously, with his own direct contributions and early insights into working in type theory without UIP; also through his influence within the field, with a strong and well-articulated vision of topics he felt were important to work on (most concretely, directing and co-ordinating the work of many contributors in the UniMath library); and of course also through his outreach to a wider mathematics audience, helping to put type theory and formalisation on the radar of many people who otherwise might not have given it attention or interest.
He was always stimulating and insightful, if not always easy to work with — extremely mathematically exacting. His views and goals were often idiosyncratic and surprising, but always came from extremely well-thought-out mathematical grounds, that one might disagree with but could never dismiss.
We’ve lost a huge contributor and leader in the field, and will all be the poorer for it.
–Peter.
On Sun, Oct 1, 2017 at 6:54 AM, Daniel R. Grayson <danielrich...@gmail.com<mailto:danielrich...@gmail.com>> wrote:
And there is this: https://www.ias.edu/news/2017/vladimir-voevodsky
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com<mailto:HomotopyTypeThe...@googlegroups.com>.
For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 8306 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
2017-10-01 4:54 ` Daniel R. Grayson
2017-10-01 14:48 ` [HoTT] " Steve Awodey
@ 2017-10-01 17:08 ` Andrei Rodin
2017-10-01 20:06 ` [HoTT] " Nicolai Kraus
` (8 subsequent siblings)
11 siblings, 0 replies; 27+ messages in thread
From: Andrei Rodin @ 2017-10-01 17:08 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1994 bytes --]
This is a horrible news. In addition to being a mathematician of genius
Vladimir had a genuine interest to the history and philosophy of his
discipline; I owe Vladimir hours of extremely tensed discussions on Euclid
(Vladimir read both the Elements and the Proclus' Commentary very
carefully), Grassmann (whose writings he studied perhaps more than any
other historical source). Our last short exchange in LQ in Stockholm was on
Aristotle: Vladimir told me that he had big plans of studying the history
of logic. Vladimir had a fantastic capacity of understanding another
person's ideas immediately following only some hints - or at least this is
my personal experience with Vladimir.
We were not close friends but all our meetings and talks were always very
friendly; in 2015 he was my extremely attentive host in IAS. I lost an
important person in my life with Vladimir's unexpected death. Good buy
Vladimir.
Andrei
On Sunday, 1 October 2017 08:25:36 UTC+4, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our
> community. His death is a tremendous loss for the Institute and for the
> world. We will all miss him dearly and extend our deepest condolences to
> Vladimir’s family and his many colleagues and collaborators around the
> world.
>
> We will soon be sharing more information about a gathering to celebrate
> Vladimir’s life and legacy.
>
> Robbert
>
[-- Attachment #1.2: Type: text/html, Size: 3751 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (2 preceding siblings ...)
2017-10-01 17:08 ` Andrei Rodin
@ 2017-10-01 20:06 ` Nicolai Kraus
2017-10-01 20:08 ` Chris Kapulkin
` (7 subsequent siblings)
11 siblings, 0 replies; 27+ messages in thread
From: Nicolai Kraus @ 2017-10-01 20:06 UTC (permalink / raw)
To: HomotopyTypeTheory
[-- Attachment #1: Type: text/plain, Size: 1793 bytes --]
Truly sad news. I did not know Vladimir well, but I had the privilege to
talk with him and get his advice at several occasions. Much of what I
have been doing during the last couple of years was either directly or
indirectly based on some of Vladimir's many ideas, most importantly
maybe his observation that homotopy/truncation levels can be defined
internally in type theory.
May he rest in peace.
Nicolai
On 01/10/17 05:25, Daniel R. Grayson wrote:
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our
> dear colleague and friend, Vladimir Voevodsky, Professor in the School
> of Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of
> our community. His death is a tremendous loss for the Institute and
> for the world. We will all miss him dearly and extend our deepest
> condolences to Vladimir’s family and his many colleagues and
> collaborators around the world.
>
> We will soon be sharing more information about a gathering to
> celebrate Vladimir’s life and legacy.
>
> Robbert
> --
> You received this message because you are subscribed to the Google
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to HomotopyTypeThe...@googlegroups.com
> <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout.
[-- Attachment #2: Type: text/html, Size: 4653 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (3 preceding siblings ...)
2017-10-01 20:06 ` [HoTT] " Nicolai Kraus
@ 2017-10-01 20:08 ` Chris Kapulkin
2017-10-02 13:20 ` Marcelo Fiore
2017-10-02 14:00 ` Andrew Polonsky
` (6 subsequent siblings)
11 siblings, 1 reply; 27+ messages in thread
From: Chris Kapulkin @ 2017-10-01 20:08 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: 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
On Sun, Oct 1, 2017 at 12:25 AM, Daniel R. Grayson
<danielrich...@gmail.com> wrote:
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced Study
> in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our dear
> colleague and friend, Vladimir Voevodsky, Professor in the School of
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our
> community. His death is a tremendous loss for the Institute and for the
> world. We will all miss him dearly and extend our deepest condolences to
> Vladimir’s family and his many colleagues and collaborators around the
> world.
>
> We will soon be sharing more information about a gathering to celebrate
> Vladimir’s life and legacy.
>
> Robbert
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-01 20:08 ` Chris Kapulkin
@ 2017-10-02 13:20 ` Marcelo Fiore
0 siblings, 0 replies; 27+ messages in thread
From: Marcelo Fiore @ 2017-10-02 13:20 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 4075 bytes --]
Dear All,
This is shocking news indeed.
I only got to know Vladimir quite recently, while he kindly came to visit
me
at the end of April, before the Big Proof INI programme. He arrived at the
Computer Lab and immediately wanted to discuss mathematics, specifically
that of type systems, which we did on the first day and regularly
thereafter.
It took us a bit of time to understand how to interact mathematically with
each other, but we got there. In the process, we did some work together
and I got fond of him. It is a real shame that he won't be around;
personally
because we had plans but, most importantly, for the loss that it represents
to the field.
Marcelo Fiore.
On Sunday, 1 October 2017 21:09:19 UTC+1, Krzysztof Kapulkin wrote:
>
> Dear all,
>
> This is very sad news indeed.
>
> For the past three decades, Vladimir has been a leading figure in
> mathematics, making landmark contributions to several areas: algebraic
> geometry, homotopy theory, and number theory, among others. In his
> work he settled multiple open problems, including the conjectures of
> Milnor and Bloch-Kato, and his insights led to the creation of whole
> new areas of mathematics such as motivic homotopy theory and homotopy
> type theory.
>
> Vladimir's style of doing mathematics can be compared only to
> Grothendieck's. Those of us who had an honor of working with him know
> that, faced with a problem, he would always rethink its basic
> definitions and assumptions, to find an elegant and clean solution. He
> saw structure where the rest of us were only able to see chaos.
>
> In all aspects of his work, Vladimir was a visionary. He put forward
> ideas that seemed unrealistic at first, and then systematically
> completed them. He had a clear set of principles that he followed, but
> he was not stubborn. On the contrary, even as a beginning graduate
> student, I consistently felt that Vladimir treated me, and everyone
> else, with an incredible amount of respect and would come to every
> conversation ready to change his opinion.
>
> Vladimir has shaped the way I think about mathematics and how I
> perceive the beauty of it. Every single conversation that we had made
> me a better mathematician, and I still have to come to terms with the
> fact that there are so many questions I will not get to ask him.
>
> Our community has lost its creator and the greatest of its members. I
> have lost a mentor, a collaborator, and a friend.
>
> Chris Kapulkin
>
> On Sun, Oct 1, 2017 at 12:25 AM, Daniel R. Grayson
> <daniel...@gmail.com <javascript:>> wrote:
> > Dear Colleagues,
> >
> > The following message from the director of the Institute for Advanced
> Study
> > in Princeton announces
> > sad news:
> >
> > ---------- Forwarded message ----------
> > Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> > From: Robbert Dijkgraaf
> > Subject: Sad news
> >
> > Dear Colleagues,
> >
> > It is with a heavy heart that I write to share some very sad news. Our
> dear
> > colleague and friend, Vladimir Voevodsky, Professor in the School of
> > Mathematics, passed away unexpectedly this morning.
> >
> > Vladimir was a truly extraordinary mathematician and integral part of
> our
> > community. His death is a tremendous loss for the Institute and for the
> > world. We will all miss him dearly and extend our deepest condolences to
> > Vladimir’s family and his many colleagues and collaborators around the
> > world.
> >
> > We will soon be sharing more information about a gathering to celebrate
> > Vladimir’s life and legacy.
> >
> > Robbert
> >
> > --
> > You received this message because you are subscribed to the Google
> Groups
> > "Homotopy Type Theory" group.
> > To unsubscribe from this group and stop receiving emails from it, send
> an
> > email to HomotopyTypeThe...@googlegroups.com <javascript:>.
> > For more options, visit https://groups.google.com/d/optout.
>
[-- Attachment #1.2: Type: text/html, Size: 5105 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (4 preceding siblings ...)
2017-10-01 20:08 ` Chris Kapulkin
@ 2017-10-02 14:00 ` Andrew Polonsky
2017-10-02 15:22 ` [HoTT] " Andrej Bauer
` (5 subsequent siblings)
11 siblings, 0 replies; 27+ messages in thread
From: Andrew Polonsky @ 2017-10-02 14:00 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1248 bytes --]
An incredible life, full of incredible service to the science and the
mathematical community.
May he finally find peace -- and then harmony -- that was grudged him by
the human world.
Andrew
On Sunday, October 1, 2017 at 6:25:36 AM UTC+2, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our
> community. His death is a tremendous loss for the Institute and for the
> world. We will all miss him dearly and extend our deepest condolences to
> Vladimir’s family and his many colleagues and collaborators around the
> world.
>
> We will soon be sharing more information about a gathering to celebrate
> Vladimir’s life and legacy.
>
> Robbert
>
[-- Attachment #1.2: Type: text/html, Size: 3075 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (5 preceding siblings ...)
2017-10-02 14:00 ` Andrew Polonsky
@ 2017-10-02 15:22 ` Andrej Bauer
2017-10-04 22:52 ` Martín Hötzel Escardó
` (4 subsequent siblings)
11 siblings, 0 replies; 27+ messages in thread
From: Andrej Bauer @ 2017-10-02 15:22 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (6 preceding siblings ...)
2017-10-02 15:22 ` [HoTT] " Andrej Bauer
@ 2017-10-04 22:52 ` Martín Hötzel Escardó
2017-10-05 4:52 ` [HoTT] " Gershom B
2017-10-05 10:41 ` [HoTT] " Thierry Coquand
2017-10-05 13:38 ` Daniel R. Grayson
` (3 subsequent siblings)
11 siblings, 2 replies; 27+ messages in thread
From: Martín Hötzel Escardó @ 2017-10-04 22:52 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2137 bytes --]
During the Types 2011 meeting in Bergen, I went outside to have
fresh air in a coffee break. Then there was this guy, and we said
hello to each other without asking for names or formal
introductions. He apologized that he was trying to concentrate on
his talk to be given after the break. I nevertheless, perhaps
impolitely, asked what his talk was going to be about. It was
going to be about a homotopical model of type theory (this is
what he said, but in the talk the topic was size). Then I said I
was looking at topological models of type theory myself. He asked
me to explain, which I did. Then he gave his talk. And after that
we met again and had a long conversation, we went together in a
boat trip with the conference crowd, and then we had dinner in
the same table, with many discussions.
I never suspected, at that time, I was talking to a Fields
Medalist. He was just somebody giving an interesting talk in a
conference. After the meeting, when I was back home, he asked me,
by email, what the topology of the universe is, in the models I
was considering.
M.
On Sunday, 1 October 2017 05:25:36 UTC+1, Daniel R. Grayson wrote:
>
> Dear Colleagues,
>
> The following message from the director of the Institute for Advanced
> Study in Princeton announces
> sad news:
>
> ---------- Forwarded message ----------
> Date: Sat, 30 Sep 2017 17:38:57 -0400 (EDT)
> From: Robbert Dijkgraaf
> Subject: Sad news
>
> Dear Colleagues,
>
> It is with a heavy heart that I write to share some very sad news. Our
> dear colleague and friend, Vladimir Voevodsky, Professor in the School of
> Mathematics, passed away unexpectedly this morning.
>
> Vladimir was a truly extraordinary mathematician and integral part of our
> community. His death is a tremendous loss for the Institute and for the
> world. We will all miss him dearly and extend our deepest condolences to
> Vladimir’s family and his many colleagues and collaborators around the
> world.
>
> We will soon be sharing more information about a gathering to celebrate
> Vladimir’s life and legacy.
>
> Robbert
>
[-- Attachment #1.2: Type: text/html, Size: 418124 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-04 22:52 ` Martín Hötzel Escardó
@ 2017-10-05 4:52 ` Gershom B
2017-10-05 6:08 ` Timothy Carstens
2017-10-05 10:41 ` [HoTT] " Thierry Coquand
1 sibling, 1 reply; 27+ messages in thread
From: Gershom B @ 2017-10-05 4:52 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 827 bytes --]
The NY Category Theory Seminar devoted tonight's session to the
commemoration of Vladimir. We had prior conducted a multi-year group
read of the HoTT book. We had a little discussion of motivic homotopy
theory and the Bloch–Kato conjecture, though none of us are terribly
familiar with the topic. We also read aloud some of the tributes to
him written by others, and concluded with a mathematical discussion of
the initiality conjecture and B- and C-systems.
We took the photo attached (which is rather blurry, due to being taken
by a camera with a timer) at the end. Behind us on the right is the
definition of a C-system, and on the left is the univalence axiom.
HIs contributions were immense, his vision was far-reaching, and the
impact of his work will continue to unfold in years to come.
—Gershom
[-- Attachment #2: Ny Category Seminar Oct 4.jpg --]
[-- Type: image/jpeg, Size: 197578 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-05 4:52 ` [HoTT] " Gershom B
@ 2017-10-05 6:08 ` Timothy Carstens
0 siblings, 0 replies; 27+ messages in thread
From: Timothy Carstens @ 2017-10-05 6:08 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 2072 bytes --]
A few years ago, one of the mailing lists advertised a foundations talk he
was to give at the Harvard math department. I flew out to Boston and snuck
in, figuring the Harvard people would assume I was MIT and conversely. I
was found-out, though, as people were filing out after his talk; of course
everyone knows everyone else.
I knew his work from my days as a geometer. It was the sort of thing you
see in grad school and it impresses its beauty upon you forever. I came out
because I'd heard this and that about HoTT and it seemed like a good
opportunity to peek into that world. He seemed surprised that someone not
in-the-know would make the trip. We talked for a bit. He was generous with
his time in a way that struck me as incredibly humble. To the extent that
mathematicians have fans, he was good to his.
On Wed, Oct 4, 2017 at 9:52 PM, Gershom B <gers...@gmail.com> wrote:
> The NY Category Theory Seminar devoted tonight's session to the
> commemoration of Vladimir. We had prior conducted a multi-year group
> read of the HoTT book. We had a little discussion of motivic homotopy
> theory and the Bloch–Kato conjecture, though none of us are terribly
> familiar with the topic. We also read aloud some of the tributes to
> him written by others, and concluded with a mathematical discussion of
> the initiality conjecture and B- and C-systems.
>
> We took the photo attached (which is rather blurry, due to being taken
> by a camera with a timer) at the end. Behind us on the right is the
> definition of a C-system, and on the left is the univalence axiom.
>
> HIs contributions were immense, his vision was far-reaching, and the
> impact of his work will continue to unfold in years to come.
>
> —Gershom
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
[-- Attachment #2: Type: text/html, Size: 2704 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Vladimir Voevodsky
2017-10-04 22:52 ` Martín Hötzel Escardó
2017-10-05 4:52 ` [HoTT] " Gershom B
@ 2017-10-05 10:41 ` Thierry Coquand
1 sibling, 0 replies; 27+ messages in thread
From: Thierry Coquand @ 2017-10-05 10:41 UTC (permalink / raw)
To: HomotopyT...@googlegroups.com
[-- Attachment #1: Type: text/plain, Size: 2766 bytes --]
Thanks to Jeremy Avigad, I learnt in February 2010 about Vladimir’s IAS presentation<https://www.youtube.com/watch?v=84vW1hQLFu8>
about foundations of mathematics and homotopy theory. I found it absolutely
fascinating, since it suggested a systematic way to attack one of the main problem of type
theory: how to represent equality, and in particular, what should be the equality type
for the universe. The first conversation we had, Chiemsee June 2010, was about
the fact that, in his model, universes are “homogeneous”, contrary to a stratified
picture where the first universe is the collection of sets, the second the collection
of groupoids and so on.
Vladimir had a unique sensibility for foundational issues. Just to give an example, he
was <https://www.youtube.com/watch?v=GGyKR4BhUGw> clearly concerned<https://www.youtube.com/watch?v=GGyKR4BhUGw>, as one should be, by the fact that the axiom of choice is needed
to prove that a fully faithful and essentially surjective functor is an equivalence. His
formalism gives a way to address this question.
He was also unique in his ability to formalise mathematics. It seemed that he was
thinking directly in dependent type theory. His definitions of contractibility and
equivalence are truly beautiful, as his formal proofs in his UniMath library.
He was humble and really kind in discussions, always trying to explain things as clearly
as possible
As Edward Frenkel wrote “there was a lot of light” and this light will be greatly missed.
Thierry
On 5 Oct 2017, at 00:52, Martín Hötzel Escardó <escardo...@gmail.com<mailto:escardo...@gmail.com>> wrote:
During the Types 2011 meeting in Bergen, I went outside to have
fresh air in a coffee break. Then there was this guy, and we said
hello to each other without asking for names or formal
introductions. He apologized that he was trying to concentrate on
his talk to be given after the break. I nevertheless, perhaps
impolitely, asked what his talk was going to be about. It was
going to be about a homotopical model of type theory (this is
what he said, but in the talk the topic was size). Then I said I
was looking at topological models of type theory myself. He asked
me to explain, which I did. Then he gave his talk. And after that
we met again and had a long conversation, we went together in a
boat trip with the conference crowd, and then we had dinner in
the same table, with many discussions.
I never suspected, at that time, I was talking to a Fields
Medalist. He was just somebody giving an interesting talk in a
conference. After the meeting, when I was back home, he asked me,
by email, what the topology of the universe is, in the models I
was considering.
M.
[-- Attachment #2: Type: text/html, Size: 4746 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (7 preceding siblings ...)
2017-10-04 22:52 ` Martín Hötzel Escardó
@ 2017-10-05 13:38 ` Daniel R. Grayson
2017-10-06 5:41 ` [HoTT] " Michael Shulman
2017-10-11 15:26 ` Daniel R. Grayson
` (2 subsequent siblings)
11 siblings, 1 reply; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-05 13:38 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 8699 bytes --]
Here is the relevant part of the oldest email I have from Vladimir about
computer proof:
-----------------------------------------------------------------------------
Date: Tue, 10 Sep 2002 09:15:21 -0400 (EDT)
From: Vladimir Voevodsky <vlad...@ias.edu>
To: d...@math.uiuc.edu
Subject: Re: Fields Medal
...
Vladimir.
PS I am thinking again about the applications of computers to pure
math. Do you know of anyone working in this area? I mean mostly some
kind of a computer language to describe mathematical structures, their
properties and proofs in such a way that ultimately one may have
mathematical knowledge archived and logically verified in a fixed
format.
-----------------------------------------------------------------------------
And here is a brainstorm of his about a computer oracle based on "homotopy
lambda-calculus". Notice that the concepts of h-level and univalence are
already present, at least in some prescient form. (Vladimir recently told
me
that he thought his concept of h-level is much more important than the
univalence axiom.) You may also notice the early appearance of Brazil.
-----------------------------------------------------------------------------
From: Vladimir Voevodsky <vlad...@ias.edu>
Subject: Re: computers and math and education
Date: Fri, 29 Sep 2006 15:51:36 -0400
To: d...@math.uiuc.edu
Dear Dan,
what you write about the conference is very interesting. Before I get
into more detailed comments, a request -- if you learn about some
interesting meetings related to this stuff please let me know.
> The main lesson for me (from all the sessions, not that one tale)
> is that these
> systems are mainly usable by the creator, because the creator can
> more or less
> remember the names of 200 trivial theorems. It won't scale up
> unless searching
> is improved. I think you have mentioned to me that searching is
> what you are
> thinking about.
My whole concept of what one should aim at while developing
"productivity software" for pure math has been evolving lately in the
following direction.
Let us start with what would be a perfect system of such sort (such a
system is impossible but let's ignore it for a moment).
Ideally one wants a math oracle. A user inputs a type expression and
the system either returns a term of this type or says that it has no
terms. The type expression may be "of level 0" i.e. it can correspond
to a statement in which case a term is a proof and the absence of
terms means that the statement is not provable. It may be "of level
1" e.g. it might be the type of solutions of an equation. In that
case the system produces a solution or says that there are non. It
may be "of level 2" e.g. It might be the type of all solvable groups
of order 35555. In that case the system produces an example of such a
group etc.
A realistic approximation of such an oracle may look as follows.
Imagine a web-based system with a lot of users (both "creators" and
"consumers") and a very large "database". Originally the database is
empty (or, rather, contains only the primitive "knowledge" a-la
axioms). User A (say in Princeton) inputs a type expression and
builds up a term of this type either in one step (just types it in)
or in many steps using the standard proof-assistant capabilities of
the system. Both the original and all the intermediate type
expressions which occur in the process are filed (in the real time)
in the database. Enter user B (somewhere in Brazil), who inputs
another type expression and begins the process of constructing a term
of his type. All the intermediate type expressions which show up as
well as their negations are filed and also compared in real time with
the ones already in the database. If a match occurs the user is
informed that this and that type has been considered before and the
following terms of this type are known (or it negation has been and
terms are known in which case one assumes that the original type has
no terms). Eventually, the database is large enough such that in
many cases the system will work like an oracle i.e. will provide
information on terms of the type which user B is interested in.
Clearly, designing such a system may take decades and it can only
materialize if a lot of people work on it. I can see a number of
reasonably independent tasks which have to be taken care of:
1. To choose a formalization or formalizations of mathematics which
will be used to translate problems into type expressions. In the case
of multiple formalizations there should be modules which mechanically
translate from one to another.
2. To design the proof-assistant part including modules which could
do computations (e.g. computational algebra)
3. To understand what the system does when a request for a term of a
given type is submitted to the database.
The basic operation is of course simple comparison with something
previously filed. In most cases however the submitted type expression
will be equivalent to a one already in the database not equal. On the
very elementary level this can be an equivalence which can be
recognized by some normalization procedure, using De Bruijn indexes
etc. On a slightly more complex level it can be say the permutation
of factors such as (A or B) versus (B or A). More about this issue
below.
Clearly the system should consider both the original type and its
negation in parallel. It also should "split" combined types such as
(A or B) and (A and B) and analyze components separately. Finally, it
might look for types which obviously map to the one under
consideration and which have known terms.
4. Implementation side which with at least two parts --
"networking" (where the "database" is kept, how it is done if it is
not centralized but distributed etc.) and "interface" (I personally
like drag-and-drop's :)) "Interface" part also includes the question
of what kind of hints one wants from the system when a complete
answer is not available e.g. if a user is trying to prove that (A or
B) holds and the system can come up with a counterexample (a proof of
the negation) to A then should probably inform the user about it.
Similarly, if one tries to prove (A and B) and the system knows a
proof of A it should also let it be known.
5. Eventually, there should be "daemons" which would wonder around
the database, extend it and clean it up - this is an AI issue. It
might be real fun when we get there.
It is clear that such a system can be useful only if it is good at
recognizing when two type expressions are equivalent. How easy or
hard it is depends a lot on the choice of the underlying
formalization. For example, the ZF formalization is notoriously bad
in this respect (also, it is not a type system but a first order
theory so the reduction of everything to the question of finding a
term of a particular type is not really applicable). If one writes
the following two statements:
a. for all x in N such that x<1 one has x=0
b. for all x in Z such that x>=0 and x<1 one has x=0
in ZF they will look so different that it is hard to imagine a
program which will recognize their equivalence. Normally one would do
it but showing first that the types N and Zplus=(all x in Z such
that x>=0) are equivalent. In ZF however they are *not* equivalent
since it is easy to make a statement about one which is false for
another. E.g. empty set is an element of N but not of Zplus.
My homotopy lambda calculus is an attempt to create a system which is
very good at dealing with equivalences. In particular it is supposed
to have the property that given any type expression F(T) depending on
a term subexpression t of type T and an equivalence t->t' (a term of
the type Eq(T;t,t')) there is a mechanical way to create a new
expression F' now depending on t' and an equivalence between F(T) and
F'(T') (note that to get F' one can not just substitute t' for t in F
-- the resulting expression will most likely be syntactically
incorrect).
-----------------------------------------------------------------------------
[-- Attachment #1.2: Type: text/html, Size: 11158 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-05 13:38 ` Daniel R. Grayson
@ 2017-10-06 5:41 ` Michael Shulman
0 siblings, 0 replies; 27+ messages in thread
From: Michael Shulman @ 2017-10-06 5:41 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (8 preceding siblings ...)
2017-10-05 13:38 ` Daniel R. Grayson
@ 2017-10-11 15:26 ` Daniel R. Grayson
2017-10-11 17:47 ` Daniel R. Grayson
2017-10-12 19:06 ` Daniel R. Grayson
11 siblings, 0 replies; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-11 15:26 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 5080 bytes --]
Here is another old email from Vladimir to me. He reports that he has
found a model for
dependent type theory in simplicial sets and begun thinking about writing
his own
proof assistant.
-----------------------------------------------------------------------------
From: Vladimir Voevodsky <vlad...@ias.edu>
Date: May 1, 2006 9:26:06 PM EDT (CA)
To: Vladimir Voevodsky <vlad...@ias.edu>
Subject: Re: computers and math and education
Dear Dan,
sorry for a slow reply. I am in a kind of a transitional state in
my work on all this proof related stuff and could not decide what
is the best way to proceed. I think I still need a week or two to
get to a point where I know myself what I want to do next.
I remember what we talked about last time but do not remember
anything about your code. What language are you using? What kind of
formalism? Here is my story:
I have come a long way since our last conversations. I have learned
to some extend three existing "proof assistants" (well, "learned"
is a bit too strong....) Mizar (based on ZF-theory), PVS (based on
simple type theory) and Coq (based on a polymorphic, dependent type
system called 'calculus of inductive constructions' which is not
really described anywhere. See the e-mail from Carlos Simpson below.).
I got convinced that dependent type systems is the best available
framework for formalization of math. The first problem with these
systems is that they lack(ed) "standard" model. I think I have
invented such a model. It takes values in the homotopy category
such that the model of the type of say groups is (equivalent to)
the nerve of the groupoid of groups and isomorphisms.
Having this new semantics I made some progress in modification of
existing type systems to make them more complete for this "H-
model". The homotopy lambda calculus which I gave some talks about
is this modification. I am not entirely happy with the definition
I have and keep thinking about how to make it better. I am also
working on proving the existence of H-models for it and for some
more basic type systems rigorously. This activity is basically a
mixture of category theory and homotopy theory of simplicial sets
with some basic type theory. Below is a copy of my message to
Peter May with one of he questions related to this activity.
Despite the fact that homotopy lambda calculus is far from being
"done" I am pretty convinced that it is a step in the right
direction. So I have started to work on a "proof assistant" based
on this system. I figured that it makes sense to program what
there is and that in the process I get a better feeling for what
has to be modified and how.
I have though about proof assistants quite a bit last year and in
particular about what are they really good for or should be good
for. I decided that for them to be useful it is crucial that they
have "memory" which can be "queried". Simplifying things a bit I
see the "workflow" as follows.
In type theory statements (propositions as they call it) are just
types of a special kind (what this "kind" is becomes very clear in
the H-lambda). Theorems are propositions which have members
(members themselves encode proofs). Hence an ideal (and impossible)
proof assistant would be a program where I can input a type
expression and the system will return either a term (member) of
this type or will tell me that this type has no members.
New type expressions are usually built from some previously known
ones. Since one does not want to write all definitions from point
zero there should be a library of existing types where one can get
building blocks for the type expression which forms the query.
Hence the memory - to contain all questions which have been asked
previously (type expressions) and all answers which have been found
(terms). This memory or at least some parts of it should be shared
(using some kind of web sharing paradigm) so that if someone
places a query or find an answer to a query everybody else has
access to it.
Right now I am thinking about the structure of such a memory. I
feel this has to be done at least on conceptual level before
everything else. My feeling is that it might get pretty large and
that it is crucial to organize it in a way which makes using it
*fast* for the computer so in particular I am thinking about an
essentially binary format (not expressions themselves but a
structure formed by already parsed expressions connected by
references to each other). I also feel that it is Ok if it contains
a lot of repeats and redundancy (e.g. a thousand slightly different
definition of what a group is) since it is not to be directly
accessed by humans and since it is not a problem for a computer to
compare to each other a thousand arrays of length thousand.
That's where I am now. I have just started this memory thing and I
hope to get a better feel for it in a week or two.
Volodia.
-----------------------------------------------------------------------------
[-- Attachment #1.2: Type: text/html, Size: 6414 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (9 preceding siblings ...)
2017-10-11 15:26 ` Daniel R. Grayson
@ 2017-10-11 17:47 ` Daniel R. Grayson
2017-10-11 19:06 ` [HoTT] " Steve Awodey
2017-10-12 19:06 ` Daniel R. Grayson
11 siblings, 1 reply; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-11 17:47 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 3499 bytes --]
At https://en.wikipedia.org/wiki/Homotopy_type_theory Voevodsky says this:
"Also in 2009, Voevodsky worked out more of the details of a model of type
theory in Kan complexes, and observed that the existence of a universal Kan
fibration could be used to resolve the coherence problems for categorical
models of type theory. He also proved, using an idea of A. K. Bousfield,
that
this universal fibration was univalent: the associated fibration of pairwise
homotopy equivalences between the fibers is equivalent to the paths-space
fibration of the base."
When I asked him about that, he showed me the email from Bousfield,
answering Vladimir's question as forwarded by Peter May, containing
a very nice description of the idea, and here it is:
-----------------------------------------------------------------------------
Date: Mon, 01 May 2006 10:10:30 CDT
To: Peter May <m...@math.uchicago.edu>
cc: jar...@uwo.ca, pgo...@math.northwestern.edu
From: "A. Bousfield" <bo...@uic.edu>
Subject: Re: Simplicial question
Dear Peter,
I think that the answer to Voevodsky's basic question is "yes," and I'll
try to sketch a proof.
Since the Kan complexes X and Y are homotopy equivalent, they share the
same minimal complex M, and we have trivial fibrations X -> M and Y -> M
by Quillen's main lemma in "The geometric realization of a Kan fibration
." Thus X + Y -> M + M is also a trivial fibration where "+" gives the
disjoint union. We claim that the composition of X + Y -> M + M with the
inclusion M + M >-> M x Delta^1 may be factored as the composition of an
inclusion X + Y >-> E with a trivial fibration E -> M x Delta^1 such that
the counterimage of M + M is X + Y. We may then obtain the desired
fibration
E -> M x Delta^1 -> Delta^1
whose fiber over 0 is X and whose fiber over 1 is Y.
We have used a case of:
Claim. The composition of a trivial fibration A -> B with an inclusion B
-> C may be factored as the composition of an inclusion A >-> E with a
trivial fibration E -> C such that the counterimage of B is A.
I believe that this claim follows by a version of the usual iterative
construction of a Quillen factorization for A -> C using the "test"
cofibrations
Dot Delta^k >-> Delta^k
for all k. At each stage, we use maps from the "test" cofibrations
involving k-simplices of C outside of B.
I hope that this helps -- I haven't thought about Voevodsky's more
general question.
Best regards,
Pete
On Sun, 30 Apr 2006, Peter May wrote:
Here is an extract from an email from Voevodsky (vlad...@ias.edu)
-----------------
Q. Let X and Y be a pair of Kan simplicial sets which are homotopy
equivalent. Is there a Kan fibration E -> \Delta^1 such that its
fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an
iso)?
A more advanced version of the same question: let X' -> X and X'' ->
X be two Kan fibrations which are fiberwise equivalent to each other
over X. Is there a kan fibration over X\times\Delta^1 whose fiber
over X\times 0 is isomorphic to X', fiber over X\times 1 is
isomorphic to X'' and the homotopy between the two inclusions of X to
X\times\Delta^1 define the original equivalence (up to homotopy)?
I encountered this issue trying to write up a semantics for dependent
type systems with values in the homotopy category. which is in turn
related to the problem of creating computer programs for proof
verification.
-----------------------------------------------------------------------------
[-- Attachment #1.2: Type: text/html, Size: 5192 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-11 17:47 ` Daniel R. Grayson
@ 2017-10-11 19:06 ` Steve Awodey
0 siblings, 0 replies; 27+ messages in thread
From: Steve Awodey @ 2017-10-11 19:06 UTC (permalink / raw)
To: Daniel R. Grayson; +Cc: Homotopy Type Theory
[-- Attachment #1: Type: text/plain, Size: 4586 bytes --]
thanks for posting this Dan.
It’s very interesting to learn the background of the discovery of univalence.
Steve
> On Oct 11, 2017, at 1:47 PM, Daniel R. Grayson <danielrich...@gmail.com <mailto:danielrich...@gmail.com>> wrote:
>
> At https://en.wikipedia.org/wiki/Homotopy_type_theory <https://en.wikipedia.org/wiki/Homotopy_type_theory> Voevodsky says this:
>
> "Also in 2009, Voevodsky worked out more of the details of a model of type
> theory in Kan complexes, and observed that the existence of a universal Kan
> fibration could be used to resolve the coherence problems for categorical
> models of type theory. He also proved, using an idea of A. K. Bousfield, that
> this universal fibration was univalent: the associated fibration of pairwise
> homotopy equivalences between the fibers is equivalent to the paths-space
> fibration of the base."
>
> When I asked him about that, he showed me the email from Bousfield,
> answering Vladimir's question as forwarded by Peter May, containing
> a very nice description of the idea, and here it is:
>
> -----------------------------------------------------------------------------
> Date: Mon, 01 May 2006 10:10:30 CDT
> To: Peter May <m...@math.uchicago.edu <mailto:m...@math.uchicago.edu>>
> cc: jar...@uwo.ca <mailto:jar...@uwo.ca>, pgo...@math.northwestern.edu <mailto:pgo...@math.northwestern.edu>
> From: "A. Bousfield" <bo...@uic.edu <mailto:bo...@uic.edu>>
> Subject: Re: Simplicial question
>
> Dear Peter,
>
> I think that the answer to Voevodsky's basic question is "yes," and I'll
> try to sketch a proof.
>
> Since the Kan complexes X and Y are homotopy equivalent, they share the
> same minimal complex M, and we have trivial fibrations X -> M and Y -> M
> by Quillen's main lemma in "The geometric realization of a Kan fibration
> ." Thus X + Y -> M + M is also a trivial fibration where "+" gives the
> disjoint union. We claim that the composition of X + Y -> M + M with the
> inclusion M + M >-> M x Delta^1 may be factored as the composition of an
> inclusion X + Y >-> E with a trivial fibration E -> M x Delta^1 such that
> the counterimage of M + M is X + Y. We may then obtain the desired
> fibration
>
> E -> M x Delta^1 -> Delta^1
>
> whose fiber over 0 is X and whose fiber over 1 is Y.
>
> We have used a case of:
>
> Claim. The composition of a trivial fibration A -> B with an inclusion B
> -> C may be factored as the composition of an inclusion A >-> E with a
> trivial fibration E -> C such that the counterimage of B is A.
>
> I believe that this claim follows by a version of the usual iterative
> construction of a Quillen factorization for A -> C using the "test"
> cofibrations
> Dot Delta^k >-> Delta^k
> for all k. At each stage, we use maps from the "test" cofibrations
> involving k-simplices of C outside of B.
>
> I hope that this helps -- I haven't thought about Voevodsky's more
> general question.
>
> Best regards,
> Pete
>
> On Sun, 30 Apr 2006, Peter May wrote:
>
> Here is an extract from an email from Voevodsky (vlad...@ias.edu <mailto:vlad...@ias.edu>)
>
> -----------------
>
> Q. Let X and Y be a pair of Kan simplicial sets which are homotopy
> equivalent. Is there a Kan fibration E -> \Delta^1 such that its
> fiber over 0 is X (up to an iso) and its fiber over 1 is Y (up to an
> iso)?
>
> A more advanced version of the same question: let X' -> X and X'' ->
> X be two Kan fibrations which are fiberwise equivalent to each other
> over X. Is there a kan fibration over X\times\Delta^1 whose fiber
> over X\times 0 is isomorphic to X', fiber over X\times 1 is
> isomorphic to X'' and the homotopy between the two inclusions of X to
> X\times\Delta^1 define the original equivalence (up to homotopy)?
>
> I encountered this issue trying to write up a semantics for dependent
> type systems with values in the homotopy category. which is in turn
> related to the problem of creating computer programs for proof
> verification.
> -----------------------------------------------------------------------------
>
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.
[-- Attachment #2: Type: text/html, Size: 8061 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
` (10 preceding siblings ...)
2017-10-11 17:47 ` Daniel R. Grayson
@ 2017-10-12 19:06 ` Daniel R. Grayson
2017-10-12 19:24 ` Daniel R. Grayson
11 siblings, 1 reply; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-12 19:06 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 1545 bytes --]
This email from Vladimir seems to be from a time when he had just learned
more about Coq but had not yet started using it:
From: "Vladimir Voevodsky" <vlad...@ias.edu>
Subject: Re: theorem proving
Date: Wed, December 30, 2009 10:34 am
To: "Daniel R. Grayson" <d...@math.uiuc.edu>
Hi Dan,
thanks for the link. I have heard about this one (from coq-club actually on
which list I am since several years ago). All is well with me, all of the
Bloch-Kato papers are submitted to journals for about a year now and many
are
accepted.
I am thinking a lot these days about foundations of math and automated proof
verification. My old idea about a "univalent" homotopy theoretical models of
Martin-Lof type systems survived the verification stage an I am in the
process of writing things up.
I also took a course at the Princeton CS department which was for most part
about Coq and was very impressed both by how much can be proved in it in a
reasonable time and by how many young students attended (45, 35 undergrad +
10 grad!).
How are you?
Vladimir.
On Dec 29, 2009, at 8:43 PM, Daniel R. Grayson wrote:
> Volodya,
>
> This seems to be a good theorem proving conference to attend this summer:
>
> https://sympa-roc.inria.fr/wws/arc/coq-club/2009-12/msg00057.html
>
> Call for Papers
> ITP 2010: Conference on Interactive Theorem Proving
> 11-14 July 2010, Edinburgh, Scotland
> http://www.floc-conference.org/ITP-cfp.html
>
> I hope all is well for you.
>
> Dan
[-- Attachment #1.2: Type: text/html, Size: 2196 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-12 19:06 ` Daniel R. Grayson
@ 2017-10-12 19:24 ` Daniel R. Grayson
2017-10-12 21:55 ` Martín Hötzel Escardó
0 siblings, 1 reply; 27+ messages in thread
From: Daniel R. Grayson @ 2017-10-12 19:24 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 93 bytes --]
PS: it is the oldest email I have from him with the word "univalent" or
"univalence" in it.
[-- Attachment #1.2: Type: text/html, Size: 132 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-12 19:24 ` Daniel R. Grayson
@ 2017-10-12 21:55 ` Martín Hötzel Escardó
2017-10-12 22:21 ` [HoTT] " Michael Shulman
2017-10-14 21:12 ` Martín Hötzel Escardó
0 siblings, 2 replies; 27+ messages in thread
From: Martín Hötzel Escardó @ 2017-10-12 21:55 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 2154 bytes --]
On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote:
>
> PS: it is the oldest email I have from him with the word "univalent" or
> "univalence" in it.
>
In the vein of bringing to public record things that Vladimir said, here
is a short interview.
-------- Forwarded Message --------
Subject: Re: historical question
Date: Thu, 22 Oct 2015 16:08:14 -0400
From: Vladimir Voevodsky <vlad...@ias.edu>
To: Martin Escardo <m.es...@cs.bham.ac.uk>
CC: Prof. Vladimir Voevodsky <vlad...@ias.edu>
> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
wrote:
>
> Hi Vladimir,
>
> (0) When did you formulate hlevels in type theory?
Probably in early 2010
> (1) When did you formulate the univalence axiom?
Originally in 2005 as a property of morphisms (fibrations). In late 2009 as
a formula in type theory.
>
> (And when did you give your model for it?)
In a sense in 2006, only I did not know how to model the Martin-Lof
identity types and thought that different identity types will need to be
introduced that will satisfy univalence but what other properties to
require from them I did not know.
>
> (2) When did you prove that univalence implies function extensionality?
July 2010.
>
> I am giving a talk next week trying to rigorously explain the univalence
> axiom to classical mathematicians. This will involve, of course, trying
> to first explain Martin-Loef type theory, particularly the identity type.
>
> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid
> model, in which they have a proto-form of univalence. Were you inspired
> by that, or were your thoughts independent of that?
I was not inspired by it. In fact I tried several times to understand what
they are saying and never could.
>
> (Also: what was your first reaction when you saw the identity type for
> the first time? Did you immediately connect it with path spaces?)
Not at all. I did not make this connection until late 2009. All the time
before it I was hypnotized by the mantra that the only inhabitant of the Id
type is reflexivity which made then useless from my point of view.
Vladimir.
[-- Attachment #1.2: Type: text/html, Size: 3024 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: [HoTT] Re: Vladimir Voevodsky
2017-10-12 21:55 ` Martín Hötzel Escardó
@ 2017-10-12 22:21 ` Michael Shulman
2017-10-14 21:12 ` Martín Hötzel Escardó
1 sibling, 0 replies; 27+ messages in thread
From: Michael Shulman @ 2017-10-12 22:21 UTC (permalink / raw)
To: Martín Hötzel Escardó; +Cc: 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.
On Thu, Oct 12, 2017 at 2:55 PM, Martín Hötzel Escardó
<escardo...@gmail.com> wrote:
> On Thursday, 12 October 2017 20:24:26 UTC+1, Daniel R. Grayson wrote:
>>
>> PS: it is the oldest email I have from him with the word "univalent" or
>> "univalence" in it.
>
>
> In the vein of bringing to public record things that Vladimir said, here
> is a short interview.
>
> -------- Forwarded Message --------
> Subject: Re: historical question
> Date: Thu, 22 Oct 2015 16:08:14 -0400
> From: Vladimir Voevodsky <vlad...@ias.edu>
> To: Martin Escardo <m.es...@cs.bham.ac.uk>
> CC: Prof. Vladimir Voevodsky <vlad...@ias.edu>
>
>
>> On Oct 22, 2015, at 3:32 PM, Martin Escardo <m.es...@cs.bham.ac.uk>
>> wrote:
>>
>> Hi Vladimir,
>>
>> (0) When did you formulate hlevels in type theory?
>
> Probably in early 2010
>
>> (1) When did you formulate the univalence axiom?
>
> Originally in 2005 as a property of morphisms (fibrations). In late 2009 as
> a formula in type theory.
>
>>
>> (And when did you give your model for it?)
>
> In a sense in 2006, only I did not know how to model the Martin-Lof identity
> types and thought that different identity types will need to be introduced
> that will satisfy univalence but what other properties to require from them
> I did not know.
>
>>
>> (2) When did you prove that univalence implies function extensionality?
>
> July 2010.
>
>>
>> I am giving a talk next week trying to rigorously explain the univalence
>> axiom to classical mathematicians. This will involve, of course, trying
>> to first explain Martin-Loef type theory, particularly the identity type.
>>
>> One thing between you and Martin-Loef is Hofmann-Streicher's groupoid
>> model, in which they have a proto-form of univalence. Were you inspired
>> by that, or were your thoughts independent of that?
>
> I was not inspired by it. In fact I tried several times to understand what
> they are saying and never could.
>
>>
>> (Also: what was your first reaction when you saw the identity type for
>> the first time? Did you immediately connect it with path spaces?)
>
> Not at all. I did not make this connection until late 2009. All the time
> before it I was hypnotized by the mantra that the only inhabitant of the Id
> type is reflexivity which made then useless from my point of view.
>
> Vladimir.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-12 21:55 ` Martín Hötzel Escardó
2017-10-12 22:21 ` [HoTT] " Michael Shulman
@ 2017-10-14 21:12 ` Martín Hötzel Escardó
2017-10-14 21:20 ` Martín Hötzel Escardó
1 sibling, 1 reply; 27+ messages in thread
From: Martín Hötzel Escardó @ 2017-10-14 21:12 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 572 bytes --]
Also this may be of historical interest:
> I was visiting Fabien Morel in Munich in the Fall of 2009. He introduced
me to Helmut Schwichtenberg. Helmut introduced me to Streicher and Hofmann.
Then someone pointed to me Bob Harper as the person who is probably
closest to what I am interested and close to Princeton. I contacted Bob and
we organized my visit to CMU. There Bob introduced me to Awodey.
Vladimir.
On Oct 22, 2015, at 3:35 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
And also: how did you get in touch with the type theory crowd and when? M.
[-- Attachment #1.2: Type: text/html, Size: 1179 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
* Re: Vladimir Voevodsky
2017-10-14 21:12 ` Martín Hötzel Escardó
@ 2017-10-14 21:20 ` Martín Hötzel Escardó
0 siblings, 0 replies; 27+ messages in thread
From: Martín Hötzel Escardó @ 2017-10-14 21:20 UTC (permalink / raw)
To: Homotopy Type Theory
[-- Attachment #1.1: Type: text/plain, Size: 742 bytes --]
And the last one of this thread on my historical questions to Vladimir in
2015:
On Oct 22, 2015, at 4:50 PM, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:
One more question, if you don't mind, this time technical: what made
you conjecture that univalence implies function extensionality, before
you had a proof? This is a very interesting thought.
No, it was almost an accident. I started a new file in Foundations that was
supposed to contain results that depend on the UA and then I guess I
started to think whether the UA and function extensionality are independent
and came up with a proof of UA => FA.
I think it was a turning point since this is were constructivists got
really interested in the UA (and UF).
Vladimir
>
>
[-- Attachment #1.2: Type: text/html, Size: 2021 bytes --]
^ permalink raw reply [flat|nested] 27+ messages in thread
end of thread, other threads:[~2017-10-14 21:20 UTC | newest]
Thread overview: 27+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2017-10-01 4:25 Vladimir Voevodsky Daniel R. Grayson
2017-10-01 4:54 ` Daniel R. Grayson
2017-10-01 8:07 ` [HoTT] " Thomas Streicher
2017-10-01 13:18 ` Peter LeFanu Lumsdaine
2017-10-01 15:06 ` Joyal, André
2017-10-01 14:48 ` [HoTT] " Steve Awodey
2017-10-01 17:08 ` Andrei Rodin
2017-10-01 20:06 ` [HoTT] " Nicolai Kraus
2017-10-01 20:08 ` Chris Kapulkin
2017-10-02 13:20 ` Marcelo Fiore
2017-10-02 14:00 ` Andrew Polonsky
2017-10-02 15:22 ` [HoTT] " Andrej Bauer
2017-10-04 22:52 ` Martín Hötzel Escardó
2017-10-05 4:52 ` [HoTT] " Gershom B
2017-10-05 6:08 ` Timothy Carstens
2017-10-05 10:41 ` [HoTT] " Thierry Coquand
2017-10-05 13:38 ` Daniel R. Grayson
2017-10-06 5:41 ` [HoTT] " Michael Shulman
2017-10-11 15:26 ` Daniel R. Grayson
2017-10-11 17:47 ` Daniel R. Grayson
2017-10-11 19:06 ` [HoTT] " Steve Awodey
2017-10-12 19:06 ` Daniel R. Grayson
2017-10-12 19:24 ` Daniel R. Grayson
2017-10-12 21:55 ` Martín Hötzel Escardó
2017-10-12 22:21 ` [HoTT] " Michael Shulman
2017-10-14 21:12 ` Martín Hötzel Escardó
2017-10-14 21:20 ` Martín Hötzel Escardó
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).