From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:4481:: with SMTP id l1-v6mr1435722pld.48.1527764762369; Thu, 31 May 2018 04:06:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:ba18:: with SMTP id k24-v6ls10794557pff.0.gmail; Thu, 31 May 2018 04:06:01 -0700 (PDT) X-Received: by 2002:a62:13c3:: with SMTP id 64-v6mr1310147pft.50.1527764761263; Thu, 31 May 2018 04:06:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527764761; cv=none; d=google.com; s=arc-20160816; b=Qw5ci3L9BPaZrBrmfN8ZDovf5Nj7iXP8gMOwbuTaZMYhUgzS+RLitSw60ZWBLIm5yc ZZpKo/xq0rT8tlRW4ITi1hu7MuAgNGAaFMb6/o57UHapK+oTStkQlHKkytlnZ2Czn5fp xmEI0CFPXFFMnQEvLZJRV3g+k4/PSIyxAJzmBRn73+gnu/SH/vANYLJejaVB+xnhu8QX 7gLI4QX0yMhKLmlTpXbxmqQ/TjfgtBLUC78mthoXAE42H4/8T6fiXNPAdj7+VE7GF9qA vU+BGhLJ32D1nWwOtuwqjRpxttikPqM/RCEu/0Euz9OrB/OvDHUda7dt8gadPX/pJSDs mBWw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=WIaYhZJqqoCCSOuJGw+iHOK51R3jDtMGM/ZtT4/snPw=; b=K9ihn22IBeTLGfpHnjGKBDPkr7Ref8Atr2liWjxa0UFi8RrgnsY5SaoYn+Sq/aDCzn AFwtivluwEmujoYcMdVj8DsGfoOl9K1vrVDC6IpsfZjQ4W+Ute4e30KZ2R7da6z4+lTm BLgQkhj3Sf+M7W7wZ66OXyrcQfh3H1Qxmfkvw2eHcRiSJYscnM2EjdcgvL5UUNHaOt7M QmetTO6UVqrdfZWllYrYiLbJqFk8PXscfTJpUstIjkxgpJAtCg3JrOxNqDhk1cLvN/kx TGNwooVIhIlk7GHgH0Oa8itMLZfXHdKsgQ2PkJPF1oC4z3agXFH9C2vg6dbWerbA7dze edBA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=03cjhS/J; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x234.google.com (mail-yb0-x234.google.com. [2607:f8b0:4002:c09::234]) by gmr-mx.google.com with ESMTPS id q6-v6si887224plr.5.2018.05.31.04.06.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 04:06:01 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=03cjhS/J; spf=neutral (google.com: 2607:f8b0:4002:c09::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x234.google.com with SMTP id q62-v6so5957859ybg.5 for ; Thu, 31 May 2018 04:06:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=WIaYhZJqqoCCSOuJGw+iHOK51R3jDtMGM/ZtT4/snPw=; b=03cjhS/JsGQugTa+IK8zOHnOhZ+xl2LIlGATDUI6BWVt5iIKDrQsKfzoNxTbepyaB2 CdCI5AUeGM6z/iYk041HlQNxwf9QW99DtVWSua968HCZjtnXC8sCaE2AqqUd1axfiDsl Jde95kHpRwpnHb6vGQ15BmvVy8naqg2WONp881BreP3bzHz1itoS8PO//xHpsZ02NVpr 08L8exDHUhNPLS6VFbX0RlXG6b2f7/IbmCG7FuSB7cKo2NR5qUw2d50fPj/nTcIdLP6n 6kyrWsJVd1AdlB12aaX7woqPrAETgcv9xgoC7vcwAPVAxopVOM6PwyPTeQi3IxGnyA8c Oi3Q== X-Gm-Message-State: ALKqPwf4i4aVsNM2srer+mV9Ns+ljWRgwIWXvoBTLIqjYR4Rfyi9o8Es D2UcBBYHotYUYKldHttHcHeLyMJb X-Received: by 2002:a25:e5c8:: with SMTP id c191-v6mr3526908ybh.485.1527764760340; Thu, 31 May 2018 04:06:00 -0700 (PDT) Return-Path: Received: from mail-yw0-f171.google.com (mail-yw0-f171.google.com. [209.85.161.171]) by smtp.gmail.com with ESMTPSA id q62-v6sm290832ywg.2.2018.05.31.04.05.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 May 2018 04:05:59 -0700 (PDT) Received: by mail-yw0-f171.google.com with SMTP id v131-v6so4238584ywg.2 for ; Thu, 31 May 2018 04:05:59 -0700 (PDT) X-Received: by 2002:a81:38d6:: with SMTP id f205-v6mr3331219ywa.63.1527764759118; Thu, 31 May 2018 04:05:59 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Thu, 31 May 2018 04:05:38 -0700 (PDT) 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> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> From: Michael Shulman Date: Thu, 31 May 2018 04:05:38 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Where is the problem with initiality? To: Thorsten Altenkirch Cc: Alexander Kurz , Thomas Streicher , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. (But at present I don't see how it can do that without also essentially implying the initiality theorem for untyped syntax.) Thanks everyone for a very interesting discussion! 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 ap= proach to Mathematics is preferable but then when we talk about type theory= itself it is preferable to consider untyped objects first. Doesn't solving= the initiality problem just means that you have establish a view on the un= typed objects which doesn't depend on them? If we apply the idea of structu= ral Mathematics to type theory itself, isn't it clear that we should take t= he algebraic view as the fundamental definition? And indeed, using the idea= of HITs combined with inductive-inductive it turns out that we can just gi= ve an inductive definition of the initial object in this algebraic view. Th= is is nice because indeed HITs were not invented for this particular purpos= e! > > And yes we have to relate this abstract initial object to the stuff we wr= ite or type in or create by clicking somewhere (indeed linear syntax may be= a thing of the past anyway). We can do this by just establishing propertie= s 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 printing= trees. > > Thorsten > > > =EF=BB=BFOn 30/05/2018, 20:07, "homotopyt...@googlegroups.com on behalf o= f Michael Shulman" wrote: > > 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 = those out > > that represent natural numbers. Untyped thinking leads to non-struc= tural > > Mathematics, to mathematical hacking and a lack of abstraction. Ind= eed, the > > impossibility to hide anything in an untyped universe is one of the= diseases > > of contemporary Mathematics. > > > > ... > > > > The problem is that people still use untyped Mathematics. > > 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. > > 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. > > 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. > > > > > > > > > > > > > > > > > This message and any attachment are intended solely for the address= ee > > and may contain confidential information. If you have received this > > message in error, please contact the sender and delete the email an= d > > attachment. > > > > Any views or opinions expressed by the author of this email do not > > necessarily reflect the views of the University of Nottingham. Emai= l > > communications with the University of Nottingham may be monitored > > where permitted by law. > > > > > > > > -- > > You received this message because you are subscribed to the Google = Groups > > "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, s= end an > > email to HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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. > > > > > > 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. > > 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. > > > > > -- > You received this message because you are subscribed to the Google Groups= "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.