From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:ab0:5ea0:: with SMTP id y32-v6mr1653453uag.90.1527707273283; Wed, 30 May 2018 12:07:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9f:2546:: with SMTP id 64-v6ls4155767uaz.0.gmail; Wed, 30 May 2018 12:07:52 -0700 (PDT) X-Received: by 2002:ab0:5284:: with SMTP id v4-v6mr1666800uav.114.1527707272492; Wed, 30 May 2018 12:07:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527707272; cv=none; d=google.com; s=arc-20160816; b=qwq9SOoR5urHjZZXnaziQNl6UVMOYr4kaKUW7D/eJBbIDRkZFQ/zHCLRxcJNWBzPD0 C4lb81EgIhc9I4V582D/dMrcxVIkc3ex4Ky8nb6SebSg2dtLw/ktnW6qUZxRY2i2Hijs rOwS+uLovUww+ms7edihTt6GnUNPwwZXei+kVGM/2qesxffsr2O3BWvAND8ZNSMtsDcF llwkH1Ti0X6ZnCZ+Vn+B7X+rXZ1uajCkDyfoVY5GELNnmPur2V54qDBn68Ew0eNETM7L i2ns1gi38gWvOldhUed72qw5LN51SEUN/nufcsYXpGs2L69B6qXSimPNk+HXzSE4XIuR b5+g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=a76MGCR98iw1N91Am+zkCEAD4Mk2B4WZ9HpI2snwtnI=; b=SWD1M4IhqJ+z5wwMHHmidSSgC34btUfRLh3bfEK1ViUSK4/2KCrdBIsct/o3Xhr00m 29wXWDM+NV+kHd4aOo5bGe3n/CVHEbPxwkJF492xCnRNWlgiVT5CFSjG4N9X86HA9SOm 65uN0XRvABox+eTMTZTHhjEhG6aUtgUFZrs3PUlhjeTHQgwxaxm58UgGTXR40bmNN9Lt MpCPuTTJ5bIrtKNvMR9p/cgmKHO8Wc/Bnv4HzGHOAjjNMYkNKxjWtxAxC4jB0NgzvdX1 DasfaIJcuQekHrOO+zNTFevfMaQ6Q5wKoXGNk2sxcw6o+pv6iNCqN6QQa8VdXxkhgj/W F7/Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=13QXJteG; spf=neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x230.google.com (mail-yb0-x230.google.com. [2607:f8b0:4002:c09::230]) by gmr-mx.google.com with ESMTPS id 143-v6si664987vky.0.2018.05.30.12.07.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 12:07:52 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=13QXJteG; spf=neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x230.google.com with SMTP id d123-v6so6734412ybh.9 for ; Wed, 30 May 2018 12:07:52 -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; bh=a76MGCR98iw1N91Am+zkCEAD4Mk2B4WZ9HpI2snwtnI=; b=13QXJteG2XotpS8Ee5mrEsis9X5rWIJgGjia3MYuARqHwLudO8SSpB5BkIsLdN/R4s lZi1qdD4BiGM/ZkIGqWL79xmIlds4+dByRYco45IvL/Bx721VLf45nsbE4LUsbuPaxbQ t4mg3GLYoWLC1FTryyH70PPmUTeRfWt83l9dT+gfgykPuDbDOWwHeGn61UX1pOf24Ie6 ONGaSFkVIhWl0FFIhl8vzNtO4pMqFFJmJsek2jr7CbyDKUYCa3NKUItWQmqu8BqJEAvf X9mRwj5l8/XW1/zqCKwKQ8go2G/+L81RILJpLlSBnUoGGafaYO5+Qg5C81r8yLmgpomb jMKg== X-Gm-Message-State: ALKqPwfTp7EtqLfUMImiHvWmF4F2gb4ffKvxhwwgdtCWeUX6EuKF5Dx+ 9xQlWu4RqSio+0JRcZYVGMsAVofA X-Received: by 2002:a25:1605:: with SMTP id 5-v6mr2225863ybw.309.1527707271969; Wed, 30 May 2018 12:07:51 -0700 (PDT) Return-Path: Received: from mail-yw0-f175.google.com (mail-yw0-f175.google.com. [209.85.161.175]) by smtp.gmail.com with ESMTPSA id g145-v6sm5016328ywe.17.2018.05.30.12.07.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 30 May 2018 12:07:51 -0700 (PDT) Received: by mail-yw0-f175.google.com with SMTP id u124-v6so5224647ywg.0 for ; Wed, 30 May 2018 12:07:51 -0700 (PDT) X-Received: by 2002:a81:118c:: with SMTP id 134-v6mr2169219ywr.178.1527707270823; Wed, 30 May 2018 12:07:50 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Wed, 30 May 2018 12:07:30 -0700 (PDT) In-Reply-To: <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk> 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: Wed, 30 May 2018 12:07:30 -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" 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-structural > Mathematics, to mathematical hacking and a lack of abstraction. Indeed, 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 true -- IF you know what "structural/typed mathematics" means and you know what you are doing! The real problem is that if you learn untyped set 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 problem 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 algorithm to typecheck untyped syntax into typed syntax, but a full proof of the 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 algorithm that produces an *a priori* different typed syntax; how do I know that the "meaning" of what I write down doesn't depend on which typechecking algorithm I choose? The most natural way I can see to be 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 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.