From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 1 Jun 2018 10:07:32 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com> In-Reply-To: <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.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> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> Subject: Re: [HoTT] Re: Where is the problem with initiality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_9963_2141526700.1527872852380" ------=_Part_9963_2141526700.1527872852380 Content-Type: multipart/alternative; boundary="----=_Part_9964_518988207.1527872852380" ------=_Part_9964_518988207.1527872852380 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote: > > > > On 31 May 2018, at 12:05, Michael Shulman > wrote:=20 > >=20 > > It sounds like Thorsten and are both starting to repeat ourselves, so= =20 > > we should probably spare the patience of everyone else on the list=20 > > pretty soon. I'll just make my own hopefully-final point by saying=20 > > that if "properties of the typed algebraic syntax" can imply that the= =20 > > untyped stuff we write on the page has a *unique* typed denotation,=20 > > independent of a particular typechecking algorithm, as mentioned in my= =20 > > last email, then I'll (probably) be satisfied. =20 > > I am interested in this question of translating the untyped stuff we writ= e=20 > on the page into type theory.=20 > > To give a concrete example of what I am thinking of as untyped, but=20 > nevertheless conceptual and structural mathematics, I would point at Tom= =20 > Leinster=E2=80=99s elegant description of the solution to the problem of = Buffon=E2=80=99s=20 > needle, see the first paragraphs of the section =E2=80=9CWhat is category= theory?=E2=80=9D=20 > at=20 > https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_cate= go.html=20 > > I call this argument type free because I see no obvious or canonical way= =20 > to make the types precise enough in order to implement the proof in, say,= =20 > Agda. Even if this can be done, it is still important that mathematicians= =20 > can discuss this argument first without having to make the types precise.= =20 > So there will always be mathematics outside of type theory.=20 > I don't understand why you call this argument untyped. Do you feel that a= =20 formalization in set theory, which is untyped, would be easier than a=20 formalization in type theory? How is untypedness helping with this=20 argument?=20 Martin=20 ------=_Part_9964_518988207.1527872852380 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander= Kurz wrote:

> On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu= > wrote:
>=20
> It sounds like Thorsten and are both starting to repeat ourselves,= so
> we should probably spare the patience of everyone else on the list
> pretty soon. =C2=A0I'll just make my own hopefully-final point= by saying
> that if "properties of the typed algebraic syntax" can i= mply that the
> untyped stuff we write on the page has a *unique* typed denotation= ,
> independent of a particular typechecking algorithm, as mentioned i= n my
> last email, then I'll (probably) be satisfied. =C2=A0

I am interested in this question of translating the untyped stuff we wr= ite on the page into type theory.=20

To give a concrete example of what I am thinking of as untyped, but nev= ertheless conceptual and structural mathematics, I would point at Tom Leins= ter=E2=80=99s elegant description of the solution to the problem of Buffon= =E2=80=99s needle, see the first paragraphs of the section =E2=80=9CWhat is= category theory?=E2=80=9D at https://golem.ph.utexas.edu= /category/2010/03/a_perspective_on_higher_catego.html

I call this argument type free because I see no obvious or canonical wa= y to make the types precise enough in order to implement the proof in, say,= Agda. Even if this can be done, it is still important that mathematicians = can discuss this argument first without having to make the types precise. S= o there will always be mathematics outside of type theory.

=C2=A0I don't understand why you c= all this argument untyped. Do you feel that=20 a formalization in set theory, which is untyped, would be easier than a=20 formalization in type theory? How is untypedness helping with this argument= ?=C2=A0

Martin=C2=A0

------=_Part_9964_518988207.1527872852380-- ------=_Part_9963_2141526700.1527872852380--