From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:bf05:: with SMTP id p5-v6mr718328wrh.27.1527793371026; Thu, 31 May 2018 12:02:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:98f6:: with SMTP id w109-v6ls12553214wrb.2.gmail; Thu, 31 May 2018 12:02:50 -0700 (PDT) X-Received: by 2002:adf:e4ca:: with SMTP id v10-v6mr283796wrm.10.1527793370111; Thu, 31 May 2018 12:02:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527793370; cv=none; d=google.com; s=arc-20160816; b=rGs7G2IbKyvWyDKZr0a3F/QMmZlrKZCfJft5VPR7D0x4aHRzctWRFoDnlj7jUUptya vV/cHFcvhupKlXvi9LskTE+oEAxiNnTGTw43nfsppnyXHptvwORXY3pOo7CHk+50KE+N 3gVnZT+xvSfRgWFpHGIVezB0MKkfK+xwHCV/eRp7khB+4wG9JdraEEy+q0r4uJkEpXg+ SrvpctuLn9TJg7NIOH0EqKMINy5Q7stXWCBnegmTPWy4Zm7bKJLj22DwIBrzo+X8S8Bx wRuqRLfTeLr6WI6gLEnox9xruIkOLHXN4Xx8fxJxCTIjRNfckC+5yv3oNL2TsKlHGgKt BAeg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature :arc-authentication-results; bh=oD2J6wfp/ralPjoF2LSdpnUMWQWV/kbhH7ugOBshxPs=; b=k66dhEqtYP/96bJcqooBXA5/c35za5vi5phPTDbQjEBV/32NCnIbWUsu9Dd6hBSAjN fFCbYanBwJ7LfbidGQnRei71hciLe8w1+463N+XBwTpBRrPeMLDOY1hrCMjj514rOifO E9uo7FVRxJOlIM1w0B8+gGv2AafnLn1NNK6+AVGBUOv8t19CI4yvkE8pFSmYOVLbiXh4 FKGu23LaLsi/iZMTIQuLZ+sIeWcZAzBIL87Pp1UOx14rcvSbuTdXHNHtTccUTEiTzAiH Y8OW6lC2lzmdJ1o6VDVonCb0M1QfN4E2uWY2eDAqkKIbATZ7lEtOsFV8BzGP82IiNaZ6 FOxw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=LUdQQmm8; spf=pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c0c::236 as permitted sender) smtp.mailfrom=axh...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wr0-x236.google.com (mail-wr0-x236.google.com. [2a00:1450:400c:c0c::236]) by gmr-mx.google.com with ESMTPS id v12-v6si3953wmc.2.2018.05.31.12.02.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 12:02:50 -0700 (PDT) Received-SPF: pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c0c::236 as permitted sender) client-ip=2a00:1450:400c:c0c::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=LUdQQmm8; spf=pass (google.com: domain of axh...@gmail.com designates 2a00:1450:400c:c0c::236 as permitted sender) smtp.mailfrom=axh...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wr0-x236.google.com with SMTP id w7-v6so22063057wrn.6 for ; Thu, 31 May 2018 12:02:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=oD2J6wfp/ralPjoF2LSdpnUMWQWV/kbhH7ugOBshxPs=; b=LUdQQmm8Cc+fXdlJx21Ugd5ycOu3okUQHgBgpOLZ1CnlBTVSDH/2hunn7eaXmOSFB4 lsriSJ2YlCapBQGpnB4ba9GFNJIhnRh8KWG63xIQ3lq+y152jo/Q8IWWsroE46q/dhEv tF9jy8Kbaiaid8xANlSWY/cTLoCioEy3g6XjvQdl7qJcmo4e/Qdp3MlpyMnaFU5pekUJ qAgZFWQ0EeEqEcXbU9Hz4Un/8OC9Tvo8slouDF2o9R7fqzI9Eao0UukOKaIHJzFrNsFr cYfOAXKIWGyBgiYqw858m090+X/kqB2K1w5JlEPR/z6x8dGqfRxHkqrnDjA9WQsXfCG9 Umbw== X-Gm-Message-State: ALKqPwfrzgqYyyxQwbisbt9GmcCqUZEFs2AFX9rFx+LSAG1/6HJVmzfd WqOiPmcRHUaTWWcXUTjt+Is= X-Received: by 2002:adf:9162:: with SMTP id j89-v6mr6369887wrj.196.1527793369743; Thu, 31 May 2018 12:02:49 -0700 (PDT) Return-Path: Received: from [192.168.0.21] (cpc86287-nfds17-2-0-cust224.8-2.cable.virginm.net. [86.8.41.225]) by smtp.gmail.com with ESMTPSA id 44-v6sm87758876wrv.47.2018.05.31.12.02.48 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 12:02:48 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.2 \(3445.5.20\)) Subject: Re: [HoTT] Re: Where is the problem with initiality? From: Alexander Kurz In-Reply-To: Date: Thu, 31 May 2018 20:02:47 +0100 Cc: Thorsten Altenkirch , Thomas Streicher , "homotopyt...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <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> To: Michael Shulman X-Mailer: Apple Mail (2.3445.5.20) > On 31 May 2018, at 12:05, Michael Shulman 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. I'll just make my own hopefully-final point by saying > that if "properties of the typed algebraic syntax" can imply that the > untyped stuff we write on the page has a *unique* typed denotation, > independent of a particular typechecking algorithm, as mentioned in my > last email, then I'll (probably) be satisfied. =20 I am interested in this question of translating the untyped stuff we write = on the page into type theory.=20 To give a concrete example of what I am thinking of as untyped, but neverth= eless conceptual and structural mathematics, I would point at Tom Leinster= =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 ca= tegory theory?=E2=80=9D at https://golem.ph.utexas.edu/category/2010/03/a_p= erspective_on_higher_catego.html I call this argument type free because I see no obvious or canonical way to= make the types precise enough in order to implement the proof in, say, Agd= a. Even if this can be done, it is still important that mathematicians can = discuss this argument first without having to make the types precise. So th= ere will always be mathematics outside of type theory. If we want to routinely translate this kind of mathematics into type theory= , we need to develop software that is either doing this automatically, or, = more realistically, at least helps the mathematician to do this translation= quickly enough, without decreasing their productivity by orders of magnitu= de. As far as I can see, we are very far away from this. Is anybody aware of re= search trying to solve this problem? I would imagine that one needs for example automatic (or semi-automatic) tr= anslations between the natural language that mathematicians use and the lan= guage of type theory. Automatic type annotation is only part of the problem= . Googling shows up a little bit here and there, but I would be interested = to know if anybody knows of serious ongoing work in this direction. All the best, Alexander > (But at present I > don't see how it can do that without also essentially implying the > initiality theorem for untyped syntax.) >=20 > Thanks everyone for a very interesting discussion! >=20 > On Thu, May 31, 2018 at 3:06 AM, Thorsten Altenkirch > wrote: >> It appears somehow inconsequential to say on the one hand that a typed a= pproach to Mathematics is preferable but then when we talk about type theor= y itself it is preferable to consider untyped objects first. Doesn't solvin= g the initiality problem just means that you have establish a view on the u= ntyped objects which doesn't depend on them? If we apply the idea of struct= ural Mathematics to type theory itself, isn't it clear that we should take = the algebraic view as the fundamental definition? And indeed, using the ide= a of HITs combined with inductive-inductive it turns out that we can just g= ive an inductive definition of the initial object in this algebraic view. T= his is nice because indeed HITs were not invented for this particular purpo= se! >>=20 >> And yes we have to relate this abstract initial object to the stuff we w= rite or type in or create by clicking somewhere (indeed linear syntax may b= e a thing of the past anyway). We can do this by just establishing properti= es of the typed algebraic syntax, e.g. decidability and type inference in a= way similar as we can understand parsing as the partial inverse of printin= g trees. >>=20 >> Thorsten >>=20 >>=20 >> =EF=BB=BFOn 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf = of Michael Shulman" wrote: >>=20 >> On Wed, May 30, 2018 at 5:05 AM, Thorsten Altenkirch >> wrote: >>> Set theory is untyped and conceptually misleading, to >>> talk about all natural numbers you quantify over all sets singling thos= e out >>> that represent natural numbers. Untyped thinking leads to non-structura= l >>> Mathematics, to mathematical hacking and a lack of abstraction. Indeed,= the >>> impossibility to hide anything in an untyped universe is one of the dis= eases >>> of contemporary Mathematics. >>>=20 >>> ... >>>=20 >>> The problem is that people still use untyped Mathematics. >>=20 >> I agree entirely with this. Some set theorists like to say that the >> untypedness of set theory is not a problem because one can still do >> "structural" (i.e. typed) mathematics inside set theory. This is tru= e >> -- IF you know what "structural/typed mathematics" means and you know >> what you are doing! The real problem is that if you learn untyped se= t >> theory as "the" foundation of mathematics, then it requires an extra >> step of *learning* to work structurally, i.e. to "forget about" the >> ability to do untyped things. Personally, I have noticed this proble= m >> most when I am refereeing papers -- it seems to be a frequent source >> of errors to, for instance, make a non-structural definition and then >> use it in ways that would only make sense if it were structural. >>=20 >> However, the "typedness of mathematics" is for me a *semantic* >> statement: the "real objects" of mathematics are typed, but that >> doesn't necessarily mean that the *language we use to talk about them= * >> must (or even can) be typed. There are "more semantic" notions of >> "typed syntax", but ultimately what we actually write down is untyped= , >> so somewhere there is a necessary step of "typechecking" it. >>=20 >> Moreover, I currently still believe that we need not just an algorith= m >> to typecheck untyped syntax into typed syntax, but a full proof of th= e >> initiality theorem for a structure built out of untyped syntax. The >> problem is that I want to be sure I know what is denoted by the >> untyped syntax I write down. Maybe you have a typechecking algorithm >> that compiles it into typed syntax and thereby gives it a semantic >> meaning, but maybe someone else has a different typechecking algorith= m >> that produces an *a priori* different typed syntax; how do I know tha= t >> the "meaning" of what I write down doesn't depend on which >> typechecking algorithm I choose? The most natural way I can see to b= e >> sure of this is to show that untyped syntax assembles into the same >> initial structure that typed syntax does. >>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>>=20 >>> This message and any attachment are intended solely for the addressee >>> and may contain confidential information. If you have received this >>> message in error, please contact the sender and delete the email and >>> attachment. >>>=20 >>> Any views or opinions expressed by the author of this email do not >>> necessarily reflect the views of the University of Nottingham. Email >>> communications with the University of Nottingham may be monitored >>> where permitted by law. >>>=20 >>>=20 >>>=20 >>> -- >>> You received this message because you are subscribed to the Google Grou= ps >>> "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send = an >>> email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >>=20 >> -- >> You received this message because you are subscribed to the Google Gr= oups "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, sen= d an email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >>=20 >>=20 >>=20 >>=20 >>=20 >> This message and any attachment are intended solely for the addressee >> and may contain confidential information. If you have received this >> message in error, please contact the sender and delete the email and >> attachment. >>=20 >> Any views or opinions expressed by the author of this email do not >> necessarily reflect the views of the University of Nottingham. Email >> communications with the University of Nottingham may be monitored >> where permitted by law. >>=20 >>=20 >>=20 >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout.