From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 5 Jun 2018 15:54:39 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <581e9092-7f93-4915-8752-ec68e80c4a6f@googlegroups.com> In-Reply-To: <299441c8-2760-48cd-b052-02b2bb4d361f@googlegroups.com> References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <299441c8-2760-48cd-b052-02b2bb4d361f@googlegroups.com> Subject: Re: [HoTT] Re: Where is the problem with initiality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_37115_1805736503.1528239279558" ------=_Part_37115_1805736503.1528239279558 Content-Type: multipart/alternative; boundary="----=_Part_37116_1697687875.1528239279558" ------=_Part_37116_1697687875.1528239279558 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable ("Imprecisely mirrored by 0-groupoids" - apologies for the typo.) On Tuesday, 5 June 2018 23:19:20 UTC+1, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3 wrote: > > > > On Tuesday, 5 June 2018 09:37:41 UTC+1, David Roberts wrote: >> >> There is an... "interesting" discussion going on at the fom mailing=20 >> list at present, the usual suspects included, about set theory-based=20 >> proof assistants, which might provide either a source of entertainment= =20 >> or frustration. It is enlightening when considering what people think=20 >> about typed vs untyped.=20 >> >> Univalent foundations gets a mention here:=20 >> https://cs.nyu.edu/pipermail/fom/2018-May/021012.html=20 >> The 'ideal proof assistant' is described as being based on ZFC here:=20 >> https://cs.nyu.edu/pipermail/fom/2018-May/021026.html=20 >> Friedman proclaims he is completely ignorant of the issues and that he= =20 >> has never gotten close to getting dirty with details, but is happy to=20 >> weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html=20 >> The discussion continues this month here:=20 >> https://cs.nyu.edu/pipermail/fom/2018-June/021030.html=20 >> >> > May I humbly say that the FOM list is mainly concerned with the=20 > foundations of mathematics of hlevel 2, or 0-types.=20 > > And that they are concerned with "how much" a foundation can prove, rathe= r=20 > than "what" a foundation talks about *natively*? (As opposed to via=20 > ZFC-set avatars.) > > What univalent mathematics proposes is that infty-groupoids are the=20 > primitive objects of mathematics, rather than ZFC sets (imprecisely=20 > mirrored by 1-groupoids).=20 > > We call these things types (bad terminology, inherited from history).=20 > > From this point of view, the above FOM discussion is completely misguided= .=20 > (As you already know.) > > The point of univalent foundations is that we should be able to talk abou= t=20 > the objects we have in mind directly as they are, rather than via ZFC=20 > avatars. =20 > > It is not that we worship types. > > Martin > > ------=_Part_37116_1697687875.1528239279558 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
("Imprecisely mirrored by 0-groupoids" - apologi= es for the typo.)

On Tuesday, 5 June 2018 23:19:20 UTC+1, Mart=C3=AD= n H=C3=B6tzel Escard=C3=B3 wrote:


On Tuesday, 5 June 2018 09:37:41 UTC+1, Davi= d Roberts wrote:
There is an... &qu= ot;interesting" discussion going on at the fom mailing
list at present, the usual suspects included, about set theory-based
proof assistants, which might provide either a source of entertainment
or frustration. It is enlightening when considering what people think
about typed vs untyped.

Univalent foundations gets a mention here:
https://cs.nyu.edu/pipermail/fom/2018-May/021012.htm= l
The 'ideal proof assistant' is described as being based on ZFC = here:
https://cs.nyu.edu/pipermail/fom/2018-May/021026.htm= l
Friedman proclaims he is completely ignorant of the issues and that he
has never gotten close to getting dirty with details, but is happy to
weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/02= 1023.html
The discussion continues this month here:
https://cs.nyu.edu/pipermail/fom/2018-June/021030.= html


May I humbly say that the FOM list= is mainly concerned with the foundations of mathematics of hlevel 2, or 0-= types.=C2=A0

And that they are concerned with &quo= t;how much" a foundation can prove, rather than "what" a fou= ndation talks about *natively*?=C2=A0 (As opposed to via ZFC-set avatars.)<= /div>

What univalent mathematics proposes is that infty-= groupoids are the primitive objects of mathematics, rather than ZFC sets (i= mprecisely mirrored by 1-groupoids).=C2=A0

We call= these things types (bad terminology, inherited from history).=C2=A0
<= div>
From this point of view, the above FOM discussion is com= pletely misguided. (As you already know.)

The poin= t of univalent foundations is that we should be able to talk about the obje= cts we have in mind directly as they are, rather than via ZFC avatars.=C2= =A0=C2=A0

It is not that we worship types.

Martin

------=_Part_37116_1697687875.1528239279558-- ------=_Part_37115_1805736503.1528239279558--