From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 7 Nov 2017 14:49:30 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: <19E2F9D6-5BAE-4E4D-B262-B2CBB5A356C5@princeton.edu> References: <28b492f0-3d0f-4744-9a67-99bf24eae91c@googlegroups.com> <19E2F9D6-5BAE-4E4D-B262-B2CBB5A356C5@princeton.edu> Subject: Re: [HoTT] Voevodsky obituary in Nature MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_165_1304747778.1510094970403" ------=_Part_165_1304747778.1510094970403 Content-Type: multipart/alternative; boundary="----=_Part_166_2133490291.1510094970403" ------=_Part_166_2133490291.1510094970403 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Tuesday, 7 November 2017 21:50:24 UTC, Dimitris Tsementzis wrote: > > Dan, > > It is an interesting idea to refer to univalence as a =E2=80=9Cmechanism= =E2=80=9D rather=20 > than an =E2=80=9Caxiom=E2=80=9D. > > Even if you did it for expository reasons, I believe that in certain=20 > contexts it is a good phrase to adopt. > I very much like this way of expression, too, even though univalence became= =20 a mechanism for the first time with cubicaltt. Nevertheless, although Vladimir certainly didn't have a mechanism for=20 univalence, he envisioned its possibility, and even formulated a conjecture= =20 that is still unsettled, namely that if univalence implies that there is a= =20 *number* n:N with a property P(n), then we can find, metatheoretically,=20 using an algorithm, a *numeral* n':N (a closed term of type N) and a proof= =20 that univalence implies P(n'). No mechanism for univalence can currently=20 provide that, as far as I know. Martin=20 =20 > > Dimitris > > On Nov 7, 2017, at 16:40, Daniel R. Grayson > wrote: > > See https://www.nature.com/articles/d41586-017-05477-9 > > --=20 > You received this message because you are subscribed to the Google Groups= =20 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= =20 > email to HomotopyTypeThe...@googlegroups.com . > For more options, visit https://groups.google.com/d/optout. > > > ------=_Part_166_2133490291.1510094970403 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


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

It is an interestin= g idea to refer to univalence as a =E2=80=9Cmechanism=E2=80=9D rather than = an =E2=80=9Caxiom=E2=80=9D.

Even if you did it for expos= itory reasons, I believe that in certain contexts it is a good phrase to ad= opt.

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

Nevertheless, although V= ladimir 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 prop= erty P(n), then we can find, metatheoretically, using an algorithm, a *nume= ral* 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=C2=A0
=C2=A0

Dimitris

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


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/= d/optout.

------=_Part_166_2133490291.1510094970403-- ------=_Part_165_1304747778.1510094970403--