From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 5 Jun 2018 15:19:20 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <299441c8-2760-48cd-b052-02b2bb4d361f@googlegroups.com> In-Reply-To: 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> Subject: Re: [HoTT] Re: Where is the problem with initiality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_30624_1542573835.1528237160806" ------=_Part_30624_1542573835.1528237160806 Content-Type: multipart/alternative; boundary="----=_Part_30625_708875025.1528237160806" ------=_Part_30625_708875025.1528237160806 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Tuesday, 5 June 2018 09:37:41 UTC+1, David Roberts wrote: > > There is an... "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.html > The 'ideal proof assistant' is described as being based on ZFC here: > https://cs.nyu.edu/pipermail/fom/2018-May/021026.html > 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/021023.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. And that they are concerned with "how much" a foundation can prove, rather than "what" a foundation talks about *natively*? (As opposed to via ZFC-set avatars.) What univalent mathematics proposes is that infty-groupoids are the primitive objects of mathematics, rather than ZFC sets (imprecisely mirrored by 1-groupoids). We call these things types (bad terminology, inherited from history). >From this point of view, the above FOM discussion is completely misguided. (As you already know.) The point of univalent foundations is that we should be able to talk about the objects we have in mind directly as they are, rather than via ZFC avatars. It is not that we worship types. Martin ------=_Part_30625_708875025.1528237160806 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


On Tuesday, 5 June 2018 09:37:41 UTC+1, David Robe= rts wrote:
There is an... &quo= t;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.html<= /a>
The 'ideal proof assistant' is described as being based on ZFC = here:
https://cs.nyu.edu/pipermail/fom/2018-May/021026.html<= /a>
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.h= tml


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_30625_708875025.1528237160806-- ------=_Part_30624_1542573835.1528237160806--