From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 31147 invoked from network); 18 Nov 2022 13:06:03 -0000 Received: from mail-wm1-x33b.google.com (2a00:1450:4864:20::33b) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 13:06:03 -0000 Received: by mail-wm1-x33b.google.com with SMTP id r186-20020a1c44c3000000b003d0005ff848sf2128198wma.2 for ; Fri, 18 Nov 2022 05:06:03 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668776762; cv=pass; d=google.com; s=arc-20160816; b=d9l/BawWY9kl1alMN0KPIGDG7/pJn2naJqrHbknU/NziO/qJxWrchKtJCI+JHNQW6c QUg4lGjwgQCdco/Z9HiZA05psGcqMTR2yeIKdfx/t2mpIrGn7oDo01pCTbM98ZKEO1J/ jdBb3l3Fjx0TV0QSCPdSGajqToyTuQlWRc9GhSoTMwFb0CIk5a6m/P6Ycyv1RtwGCHnn BF9vWGGjQzoKdrwW3v0xH++gXpeYORxc5GNCH1f+I2t1oXcnSREe/3UxftWM59ekUuv+ nc+0onqfcW2dzk1q9pE4Q4jMC7c66hhFD2RiJv086Vq1tJlZZMiJSdL+Sl9URxGiHjBT ipww== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-transfer-encoding :mime-version:references:in-reply-to:message-id:date:subject:cc:to :from:feedback-id:sender:dkim-signature; bh=sCiiz5u2VoGdDb4lTuZRj5ZN1jNy+LJtWAYyfMAPkYw=; b=kmooRjNqGDxc2VtnpYCGC0HgsobUf1PFKAEJ7MwBF14yGf/ANjBw9XVUyQYTgfqPf6 sNK/wVDtWxJvZSlaFQnavwGAv2EhlAct3HKAwjvcNbGzIqApsOjHYcnhVuEPa/UIRMWq Er4bP1JOX7KiTVKvywIX5AZbnBhwr0y9WdRTPG4Pid2mOI2x4CZ2UEI3R3lgOKJL2GHg xLvUuGeqUA9DU3ReeMXuJr0whXzBcKWJUm3ORjRaF74oMl7DmBtt2xGhm2BZIZks4bnH G1TvpCp/8TICMeQyoVTLJV9oAm/AgEZDiKo1sRQWiRlbTJsRAifUGoojezwEyYvi9kqG jx5A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=JiRoTO9J; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=jcM2rk+t; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.21 as permitted sender) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-transfer-encoding:mime-version:references :in-reply-to:message-id:date:subject:cc:to:from:feedback-id:sender :from:to:cc:subject:date:message-id:reply-to; bh=sCiiz5u2VoGdDb4lTuZRj5ZN1jNy+LJtWAYyfMAPkYw=; b=gh6yIUhK2vmm78hvX+3A5ZEjS2xmum8utCtgD/aWxyh4WaVZXmt9ouHavHkwYIS+yJ tv31fQkJHrS6aJPIFoJ2ttSnGPvLQuWkFZpHS80Iae/1vhUmDHkpGD4IgC935KGSV+k+ zgCsbYg9mOnz+PPLgReMvoIJVNWvVGXYx6eUuqLTR0T/asMFA0u8ld8mLE9Qk7KxZSEJ zHY2Yu14nmeuw33QSoKBzG2Fs9R6YCds59SJKhbhTD0gc6DjCYFDCRctH6omfkdL0735 X3p7mXa8mepYzpH7cWlodgT4yziw+Awx3aYB1i7MWaxS6nRehjLrEy4Vi8IXkXn9jcHb 6aJA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=sCiiz5u2VoGdDb4lTuZRj5ZN1jNy+LJtWAYyfMAPkYw=; b=YY6717vnBIyzm1vZt0DPwaponHCMgc1upoxZCxJrMD8eZiS+9SH0EkcB48371Iyo/8 ylAnXkoYHtgFG7cllMpl5pQzz15n4PYS1YMPvWfUSTx6MDauq7mQQIxqQK3xRSNTIFUT iYolPueHK/rAXKFwXVubCsrEI7g4vjCxLporilxjo0yFhRhxxlF3rPpp8DgrGmBldaYQ 2df/nIecKzPDOYSQobVQCFL8zR1HuJE+/+wLvnlA9p0+9CBy1g2CcYj0WUomm3XrdBW9 bTlsQ+EBe+w/XyHD3ExtqNvGKpd2FMd9HHp289KA+d0ZAPI2M9FHY7sdlcj112vEE4Yh YqkA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pn2/7k1a2j/4LlS+ZOymFfx9uW+To9RXNVA3vAm4wiTq5K0hclH fA5UW/sZ2YgyFn5eZ0/J5rA= X-Google-Smtp-Source: AA0mqf7544Qepit0Wl76JJtspfamkPWya3A6mx6KvUp/l+KWdGf4hndupxqGxuDMTTyzqUMfkXKNOw== X-Received: by 2002:a05:600c:210c:b0:3cf:6af4:c4fa with SMTP id u12-20020a05600c210c00b003cf6af4c4famr4941825wml.117.1668776762057; Fri, 18 Nov 2022 05:06:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a7b:ce96:0:b0:3cd:d7d0:14b6 with SMTP id q22-20020a7bce96000000b003cdd7d014b6ls2580350wmj.1.-pod-control-gmail; Fri, 18 Nov 2022 05:06:00 -0800 (PST) X-Received: by 2002:a05:600c:a0c:b0:3cf:a851:d2ef with SMTP id z12-20020a05600c0a0c00b003cfa851d2efmr8495779wmp.88.1668776759887; Fri, 18 Nov 2022 05:05:59 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668776759; cv=none; d=google.com; s=arc-20160816; b=vYWMoWNfZtEBMdO3dsIavlwqgx0vMMUWenJi0gaWf4wLz6is51blWtMuDwsBIdbGC8 z323cwqdgfSSYYmkq8sFUWBZa1dW2qJQQBSQViz8IiHhFoyhMHvQOQPXRv9jVUE3VSq6 KopNqgkH4rI3plFif0aZYEhiXioblV6A2Z7qTsgi04ZiFvkRyeOOd7crhgxgSGnySh1j +ROhGleKk9ms2QVGgO26pT9su9OyAtCzo2/BzyIVT0TYA7t1e4srneGoDPIOP0KEwiof 8/jyMqyzQsQqAhUwfAjAH5gXNp/lhVvL8xkWej4FPcbT8guLYAQW6HhkCJ4pr5dNZGsh apPQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:dkim-signature :dkim-signature; bh=Xk2aqu+aBDVMUN7fxh+vcSAP2yfIFrAESqGu0V70C50=; b=JrSzkY9jcgSbu5eB7NydfuLN0S8+KFCK1vZsjGgHs7O/FsEb67sIKanoXehz6waVUb +3LfSDmAKRh14UUkhTpJlGvidnMb/2jfnuzllV5PWiANdLlWJDPnm1OEQgHexSxRkuSH 1Mqm/GZB6LZjcRob9sEG2xbfDIOSY8Ce9mKu8H9tAdThSGWXUrg/s5dvZ0NhYOKuzeRO E3EB47j2SkmCCwsIleRgytqq0ICZNlL5LcFbqDYtF5+sGvoo1q8hnkMY7mFSFqzH/Pjy Plw/5h8jjalQl1v4W9LH5MhNLTQHHXmPmQIVSn+3G4j7aPqFrIuMIh1CM4FHo0aGTAiy +bwQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=JiRoTO9J; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=jcM2rk+t; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.21 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout5-smtp.messagingengine.com (wout5-smtp.messagingengine.com. [64.147.123.21]) by gmr-mx.google.com with ESMTPS id l65-20020a1c2544000000b003c6e63dcbb3si390853wml.1.2022.11.18.05.05.59 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 05:05:59 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.21 as permitted sender) client-ip=64.147.123.21; Received: from compute2.internal (compute2.nyi.internal [10.202.2.46]) by mailout.west.internal (Postfix) with ESMTP id 86A3E32005BC; Fri, 18 Nov 2022 08:05:57 -0500 (EST) Received: from mailfrontend2 ([10.202.2.163]) by compute2.internal (MEProxy); Fri, 18 Nov 2022 08:05:57 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgdegkecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenuc fjughrpefhvfevufffoffkjghfgggtgfesthhqmhdtredtjeenucfhrhhomheplfhonhcu ufhtvghrlhhinhhguceojhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtf frrghtthgvrhhnpeelfeevuddvgffgvdekleduhfevgeefieeitdefieduudekuefgkeef veevteefjeenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhroh hmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 18 Nov 2022 08:05:56 -0500 (EST) From: Jon Sterling To: Michael Shulman Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Fri, 18 Nov 2022 08:05:55 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <21B50B02-4107-4854-8015-99EA4B14EBA5@jonmsterling.com> In-Reply-To: <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=JiRoTO9J; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=jcM2rk+t; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.21 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , Maybe just to put a finer point on it, re: the calculus example (and then I= 'll try to shut up, I have alreadyspoken too much): I subscribe to the viewpoint of the HoTT book regarding the practice of inf= ormal mathematics (or at least, I subscribe to a version of the viewpoint o= f the HoTT book which I think at least some of its authors held, including = Steve Awodey with whom I have discussed this topic at length in the past). = Things like terms, variables, and substitution do not actually arise in inf= ormal mathematics: instead, we work *directly* with things that are functio= ns of other things. Thus when doing informal mathematics, if we say "term" = we usually mean something that someone might more precisely refer to as an = "element". (But let me not open that can of worms!) In that sense, it would be completely incorrect to say that when doing math= ematics and we have a function `f(x) =3D x^2 + 1`, to evaluate f at 3 we mu= st apply a syntactical operation that recursively walks a syntax tree and r= eplaces a placeholder with 3. The function `f` has the same ontological sta= tus as a tree or as a friend or as a piece of stone: it is not a piece of c= ode that tracks a function, rather it is *actually* a function --- in the s= ame way that a stone is not a representation of an object, but an actual ob= ject. Thus to evaluate `f(3)`, we use what we know about `f`: namely that i= t is the function associated to the law that relates any number to the succ= essor of its square. So in ordinary math, "substitution" tends to be a fa=C3=A7on de parler for = an operation that is not really syntactical at all but is instead intrinsic= ally constitutive of the informal notion of a "mapping", which exists long = before any logicians could attempt to intervene with their syntactical gest= iculations... (By the way: truly syntactic substitution also arises *separa= tely* in mathematics, by the way, when thinking about free extensions of al= gebraic objects (like rings of the form R[x]). But this is a very specializ= ed usage, and if we are being precise we will always distinguish between an= element of R[x] and the function it encodes.) It is true that it is possible to put aside this ontology, and think of mat= hematical objects in terms of their encodings and then make sure to only sp= eak of syntactical operations that track mathematical operations (e.g. well= -typed substitutions, but not ill-typed substitutions). But this is the way= of logicians, and it is not really pertinent to the practice of everyday m= athematics. Mathematics abstracts over these things, and we try to work "di= rectly" with the objects we are concerned with, regardless of where we fall= on the ancient debate of the "real-ness" of these objects. I fear we have veered off topic from the original question! But I think it = would be great if we could put this debate to rest once and for all --- I a= m constantly amazed to be the syntactician in the room, but having semantic= ists insist to me that the study of syntax needs raw terms and variables an= d admissible substitution, etc. If it were needed, then I would certainly h= ave noticed it by now! The world of syntax is far richer than can be descri= bed with mere trees or strings, and many of us who study syntax for a livin= g have moved on from that viewpoint. ;-) Best, Jon On 18 Nov 2022, at 7:47, Jon Sterling wrote: > On 17 Nov 2022, at 21:35, Michael Shulman wrote: > >> As far as the mathematical study of type theories and their models goes, >> that may be true. But I believe that when talking about the way type >> theories are used in practice, either on paper or in a proof assistant, >> there is still a difference. >> >> Suppose I am teaching a calculus class, and I define f(x) =3D x^2 + 1 an= d I >> want to evaluate f(3). I don't write >> >> f(3) =3D (x^2+1)[3/x] =3D (x^2)[3/x] + 1[3/x] =3D 3^2 + 1 =3D 9 + 1 =3D = 10. >> >> Instead, I jump right to f(3) =3D 3^2+1, because substitution is an oper= ation >> that happens immediately in my head, not a computational step analogous = to >> 3^2 =3D 9. Similarly, the user of a proof assistant never types or sees >> substitution as part of the syntax; it is an operation *on* syntax that >> happens behind the scenes. > > By the way, I find this calculus example to be supremely uncompelling ---= not because I am hung up on the fact that it pertains to a presentation, b= ut because mathematics is full of equations that we basically agree not to = mention at various times. > > It is also not particularly helpful to your point to bring up implementat= ion, where it is extremely common to eschew implicit substitution for expli= cit substitutions --- or to use a mix of the two... In neither case are the= details of this presented to the user, however, because the gender of an a= ngel is not useful information to mere humans who use proof assistants. > > Best, > Jon --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/21B50B02-4107-4854-8015-99EA4B14EBA5%40jonmsterling.com.