Voevodsky obituary in Nature

[Daniel R. Grayson]

See https://www.nature.com/articles/d41586-017-05477-9

[Dimitris Tsementzis]

Dan,

It is an interesting idea to refer to univalence as a “mechanism” rather than an “axiom”.

Even if you did it for expository reasons, I believe that in certain contexts it is a good phrase to adopt.

Dimitris

On Nov 7, 2017, at 16:40, Daniel R. Grayson <danielrich...@gmail.com> wrote:

See https://www.nature.com/articles/d41586-017-05477-9

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

[Martín Hötzel Escardó]

On Tuesday, 7 November 2017 21:50:24 UTC, Dimitris Tsementzis wrote:

Dan,

It is an interesting idea to refer to univalence as a “mechanism” rather than an “axiom”.

Even if you did it for expository reasons, I believe that in certain contexts it is a good phrase to adopt.

I very much like this way of expression, too, even though univalence became a mechanism for the first time with cubicaltt.

Nevertheless, although Vladimir certainly didn't have a mechanism for univalence, he envisioned its possibility, and even formulated a conjecture that is still unsettled, namely that if univalence implies that there is a *number* n:N with a property P(n), then we can find, metatheoretically, using an algorithm, a *numeral* n':N (a closed term of type N) and a proof that univalence implies P(n'). No mechanism for univalence can currently provide that, as far as I know.

Martin 

 

Dimitris

On Nov 7, 2017, at 16:40, Daniel R. Grayson <danielrich...@gmail.com> wrote:

See https://www.nature.com/articles/d41586-017-05477-9

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

[Martín Hötzel Escardó]

On Tuesday, 7 November 2017 22:49:30 UTC, Martín Hötzel Escardó wrote:

On Tuesday, 7 November 2017 21:50:24 UTC, Dimitris Tsementzis wrote:

Dan,

It is an interesting idea to refer to univalence as a “mechanism” rather than an “axiom”.

Even if you did it for expository reasons, I believe that in certain contexts it is a good phrase to adopt.

I very much like this way of expression, too, even though univalence became a mechanism for the first time with cubicaltt.

Nevertheless, although Vladimir certainly didn't have a mechanism for univalence, he envisioned its possibility, and even formulated a conjecture that is still unsettled, namely that if univalence implies that there is a *number* n:N with a property P(n), then we can find, metatheoretically, using an algorithm, a *numeral* n':N (a closed term of type N) and a proof that univalence implies P(n').

The conjecture said that we can find a numeral n':N and a proof that univalence implies n=n' . 

Here is what he actually conjectured:

"

Conjecture 1 There is a terminating algorithm which for any term nn of type nat constructed

with the use of the univalence axiom outputs a pair (nn 0 , pf ) where nn 0 is a term of type nat

constructed without the use of the univalence axiom and pf is a term of type paths nat nn nn 0 (i.e.

a proof that nn 0 = nn). The term pf may use the univalence axiom.

"

 http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf

Martin