* Voevodsky obituary in Nature @ 2017-11-07 21:40 Daniel R. Grayson 2017-11-07 21:51 ` [HoTT] " Dimitris Tsementzis 0 siblings, 1 reply; 4+ messages in thread From: Daniel R. Grayson @ 2017-11-07 21:40 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 55 bytes --] See https://www.nature.com/articles/d41586-017-05477-9 [-- Attachment #1.2: Type: text/html, Size: 79 bytes --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Voevodsky obituary in Nature 2017-11-07 21:40 Voevodsky obituary in Nature Daniel R. Grayson @ 2017-11-07 21:51 ` Dimitris Tsementzis 2017-11-07 22:49 ` Martín Hötzel Escardó 0 siblings, 1 reply; 4+ messages in thread From: Dimitris Tsementzis @ 2017-11-07 21:51 UTC (permalink / raw) To: Daniel R. Grayson; +Cc: Homotopy Type Theory [-- Attachment #1: Type: text/plain, Size: 762 bytes --] 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 <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: 1724 bytes --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Voevodsky obituary in Nature 2017-11-07 21:51 ` [HoTT] " Dimitris Tsementzis @ 2017-11-07 22:49 ` Martín Hötzel Escardó 2017-11-07 23:11 ` Martín Hötzel Escardó 0 siblings, 1 reply; 4+ messages in thread From: Martín Hötzel Escardó @ 2017-11-07 22:49 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1451 bytes --] 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 <daniel...@gmail.com > <javascript:>> 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 <javascript:>. > For more options, visit https://groups.google.com/d/optout. > > > [-- Attachment #1.2: Type: text/html, Size: 3251 bytes --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Voevodsky obituary in Nature 2017-11-07 22:49 ` Martín Hötzel Escardó @ 2017-11-07 23:11 ` Martín Hötzel Escardó 0 siblings, 0 replies; 4+ messages in thread From: Martín Hötzel Escardó @ 2017-11-07 23:11 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2167 bytes --] 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 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 <daniel...@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. >> >> >> [-- Attachment #1.2: Type: text/html, Size: 4036 bytes --] ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2017-11-07 23:11 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-11-07 21:40 Voevodsky obituary in Nature Daniel R. Grayson 2017-11-07 21:51 ` [HoTT] " Dimitris Tsementzis 2017-11-07 22:49 ` Martín Hötzel Escardó 2017-11-07 23:11 ` 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).