From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sat, 14 Oct 2017 14:20:39 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <238074f9-7688-4069-9d3a-0f4247726602@googlegroups.com> In-Reply-To: <99076355-ec0b-40db-a88b-6ad359db99f4@googlegroups.com> References: <69c716dc-7fbf-4c07-a128-21c75fc996da@googlegroups.com> <82f74559-e82f-4773-bd7d-2886bd9b38fb@googlegroups.com> <164e6589-5d92-4642-add6-fdbe7439d164@googlegroups.com> <99076355-ec0b-40db-a88b-6ad359db99f4@googlegroups.com> Subject: Re: Vladimir Voevodsky MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_20631_644025051.1508016039629" ------=_Part_20631_644025051.1508016039629 Content-Type: multipart/alternative; boundary="----=_Part_20632_481741104.1508016039629" ------=_Part_20632_481741104.1508016039629 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 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 > > ------=_Part_20632_481741104.1508016039629 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
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 conjectu= re 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=20 started to think whether the UA and function extensionality are=20 independent and came up with a proof of UA =3D> FA.=C2=A0

I think it was a turning point = since =C2=A0this is were constructivists got really interested in the UA (a= nd UF).

Vladimir<= /div>

------=_Part_20632_481741104.1508016039629-- ------=_Part_20631_644025051.1508016039629--