From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 7 Nov 2017 15:11:58 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <380b537f-f78f-4bbb-9357-c55e8cd60b47@googlegroups.com> In-Reply-To: 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_223_1569776528.1510096318490" ------=_Part_223_1569776528.1510096318490 Content-Type: multipart/alternative; boundary="----=_Part_224_849855032.1510096318490" ------=_Part_224_849855032.1510096318490 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Tuesday, 7 November 2017 22:49:30 UTC, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 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 =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=20 > became 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 conjectu= re=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 proo= f=20 > that univalence implies P(n').=20 > The conjecture said that we can find a numeral n':N and a proof that=20 univalence implies n=3Dn' .=20 Here is what he actually conjectured: " Conjecture 1 There is a terminating algorithm which for any term nn of type= =20 nat constructed with the use of the univalence axiom outputs a pair (nn 0 , pf ) where nn 0= =20 is a term of type nat constructed without the use of the univalence axiom and pf is a term of=20 type paths nat nn nn 0 (i.e. a proof that nn 0 =3D 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=20 > =20 > >> >> Dimitris >> >> On Nov 7, 2017, at 16:40, Daniel R. Grayson =20 >> wrote: >> >> See https://www.nature.com/articles/d41586-017-05477-9 >> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >> >> >> ------=_Part_224_849855032.1510096318490 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


On Tuesday, 7 November 2017 22:49:30 UTC, Mart=C3= =ADn H=C3=B6tzel Escard=C3=B3 wrote:


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

It is an interesti= ng 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 expo= sitory reasons, I believe that in certain contexts it is a good phrase to a= dopt.

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 envisione= d 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 pro= perty P(n), then we can find, metatheoretically, using an algorithm, a *num= eral* n':N (a closed term of type N) and a proof that univalence implie= s P(n').

The conjecture sa= id that we can find a numeral n':N and a proof that univalence implies = n=3Dn' .=C2=A0

Here is what he actually conjec= tured:

"
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 ) wher= e nn 0 is a term of type nat
constructed without the use of the u= nivalence axiom and pf is a term of type paths nat nn nn 0 (i.e.
= a proof that nn 0 =3D nn). The term pf may use the univalence axiom.
<= /div>
"
=C2=A0http://www.math.ias.edu/vladimir/files/uni= valent_foundations_project.pdf

Martin
= No mechanism for univalence can currently provide that, as far as I know.

Martin=C2=A0
=C2=A0

<= /div>
Dimitris

On = Nov 7, 2017, at 16:40, Daniel R. Grayson <daniel...@= gmail.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.c= om.
For more options, visit https://groups.google.com= /d/optout.

------=_Part_224_849855032.1510096318490-- ------=_Part_223_1569776528.1510096318490--