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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 29018 invoked from network); 18 Nov 2022 12:48:16 -0000 Received: from mail-lj1-x240.google.com (2a00:1450:4864:20::240) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 12:48:16 -0000 Received: by mail-lj1-x240.google.com with SMTP id q9-20020a05651c054900b002791e4a143dsf1688596ljp.10 for ; Fri, 18 Nov 2022 04:48:16 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668775695; cv=pass; d=google.com; s=arc-20160816; b=yvJGGE/DfLP7AI3Tw7cuEQnh6/fBCaVKVRAkvQfnb5USVr2Y2OBpXgulMgB3m58XbR kxEvoJlSurMhmhHOQgS7ztDKfDBlZpdyJMJbvvgrGbjMMkY9w+WfzkuLmgV43aTfxsbd PFi/tcVwYRjvJswZ2jlJ4gzX0sEL6o+u3OegsYhmGhcfU3kHXVfFzokZ65vX1Rpos3EF 0IrF+AXPV6oCGhJPF0wgALVyjed4zyhwNAm57N8XBLIlZbwysXjsVVEK1RdFJlY/DPwI j0iTreJJYSKDZy4QBmEvWWAbyo+OGUjAnjMb3FLfK38jdXFPLVnCLLL8uZ+cIEWHQW52 uMlA== 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=du+XTXVef38SMVY24QV2nPS//nfweThU/ecBkPq+qc4=; b=Ui608gkrNuHIuU+eEP7rookBQaUsK8NYIvjHVRblUJ+9vqAJFlOKimmtJd4Uo0joAU nqgf5D65gcE5eIe/yPpKAAQYSFf1qYv//imY1+goG4eDd3VfGie1gP4PF1QsmA/aOVE0 wNEjeNayc0XmoH7mDJR83HgBAkFWT5K9BsU2OdlkMJdNVS6QinU6XeIoSrJpuBtUw5DP +dlxTEuIzo3ezKyzkPOhDJZgTFxjtNMKYVJMUJdqfA6Dzm1Chs9h7Fz39IUqqaMTtgCZ fp9epgmfOUwMKBw7I7ivOkM05LrlJzfNk01crSsf4IHcRLRh04a2Qq+8WeCIkv3VOiQ8 XZSg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=eDUQaRoo; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b="VrkJ/ecU"; 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=du+XTXVef38SMVY24QV2nPS//nfweThU/ecBkPq+qc4=; b=YSE4QwtMFVeqppdDYcA4G98EvHfKCp4M/Yz5TYjyhUBQdUyL5m+5z0eSogS22Cgqfr fKvTLR6KbsUo3ZqjpNj0njP4zxR8xUn3jyXpSu1DhlBRAz83vGMnywWP8dmqIYQ/dYLv B2T8EAjsVZD8161qjaZFogpPwQF4wl+E3H2aZzslPUdKgS2m/M17ajDzCtFH/LfA/Ufw Gs3oQI/Kca5Pf2TEl5THYkyl5DLRQyGsVbXtJMVgiq7nQKD+nXltN51n20DpOqUVTlTi mbL83ZLFVAnC3f5FYjxiUZou/w1+7Nx4E23ahAYr4DyTnclQMMPWL6nbjTPebCcrHAmb eKPQ== 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=du+XTXVef38SMVY24QV2nPS//nfweThU/ecBkPq+qc4=; b=K5ytkOb5yID/2a6l71Q5ZB0mjh4Qr/wmXSJgOkf8ryaLUVcWtmpSr/t8oki1eJh2yc rrDmbTbxEU4zPy2A37qUlIMOGtVklYcvXr0fJ7Od/D6Dt6jtmbMj9YfsdpZJILxZQqY6 jk61C2vvbCXm40sb9TkqKzMriVWYVVRmi9rNO0y+TVDdN+OIcvXki1fnWs+NoLKipx3N 6s311bEaEtwn3BTcEh66OHoSGRhtagq5l0gavFuR3v4poPOJpmUxo4mYlLRlZlWid9c4 /T0XCyRefP62UlqvKj0ZOQUzpKKvpnISdK5AapoM6+eKCWxMV1EjZbF0UeJVWSw3MpEJ C7xA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pnH94/azzDUuESgjEp+CtLBp4Sk1VewUpCUDbAGJQ0AhMjdhoGk /8dOlSqo9E+h0YI7zSS5EIc= X-Google-Smtp-Source: AA0mqf57NGDRt1KNP1j4U6YI7o3qqM7jiSo9pPamiJLPMGxeDjcYwWRqm0Tl0sSJE+OADfTIlwYxUQ== X-Received: by 2002:a05:651c:10b8:b0:277:2217:c7e1 with SMTP id k24-20020a05651c10b800b002772217c7e1mr2453898ljn.407.1668775694924; Fri, 18 Nov 2022 04:48:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b8d6:0:b0:277:2e6e:e039 with SMTP id s22-20020a2eb8d6000000b002772e6ee039ls902307ljp.9.-pod-prod-gmail; Fri, 18 Nov 2022 04:48:11 -0800 (PST) X-Received: by 2002:a2e:b0cd:0:b0:277:4e6:d43f with SMTP id g13-20020a2eb0cd000000b0027704e6d43fmr2308804ljl.503.1668775691859; Fri, 18 Nov 2022 04:48:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668775691; cv=none; d=google.com; s=arc-20160816; b=p7rFSVvhlB30cJW6BQBDcyLmKOisAr3MXqcqk7ziRkZB0p/7aJf6dwiU8dv+d9faz1 3JlXnjVBq97Iz2opmZGqEsSIYE0K2foxv6y+VTmxlAvfyE81eka4F5oM+5m4qbYWeodg yuMK9+NRCEyycaUp5pevLP2PEYVaB7RwDx5CljKQXK5O2Zc/IXaNFTNvbw0vrz1CO6Xw sqN3CMUjWo67jVfOXcpDmp+5/SLZKWhK+kSMTyynk9DxHEbTWFdBK3T2yKIfkJuEarHf hsQvD4qH1o0qpPacBbAClMdjLi9KR9SZ5Z3f8WYoUlZTDG41W0PQvURLj+3cT9Nb1TLT b6mw== 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=NPXRNdlR5WrKR/HbqfvYZ9vYY8b4bU/ARndbXvkfYLg=; b=Yt7W7YjRrPBgdA0MuEoETgzfvseErgYOe17yBb+xCWZ0wW68AjCbJAjuL9wHiCXT+J Mx0/jmKeAXg9sXfHjEK8G+8f12H+sZKifPcVtM5i5TWrt8XM2vrbgzE7yB/p37D5kr6w G7xNXtFjDUOur/xelWRNUNBQmHQBRZtAjAKmHHNc9o7JXniVyy+db/olMeuegRIN43c1 EEX9X4igNUfwZzEV3iOzS5IfC3YC3CZWyPfHwr/94QlBr2G+jwXOt90efVsKzkAdP+nh Rjg7tOs+dYR11o/gEkJcVIHgEJ6KmmMdr9fUPw7KA4ozFurmOfJ8+fE9bw96nyeUmTa0 FEZw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=eDUQaRoo; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b="VrkJ/ecU"; 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 c19-20020a056512075300b00492ce810d43si143606lfs.10.2022.11.18.04.48.11 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 04:48:11 -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 compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 0171B3200AE0; Fri, 18 Nov 2022 07:48:08 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Fri, 18 Nov 2022 07:48:09 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgdeggecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenuc fjughrpefhvfevufffoffkjghfgggtgfesthhqmhdtredttdenucfhrhhomheplfhonhcu ufhtvghrlhhinhhguceojhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtf frrghtthgvrhhnpeetueegieeuvdehvdegtefhieeljeelveeuueeljeffgfegtedviefg geduieelueenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhroh hmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 18 Nov 2022 07:48:07 -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 07:47:56 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> In-Reply-To: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@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=eDUQaRoo; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b="VrkJ/ecU"; 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: , 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 and= 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 1= 0. > > Instead, I jump right to f(3) =3D 3^2+1, because substitution is an opera= tion > that happens immediately in my head, not a computational step analogous t= o > 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 --- n= ot because I am hung up on the fact that it pertains to a presentation, but= because mathematics is full of equations that we basically agree not to me= ntion at various times. It is also not particularly helpful to your point to bring up implementatio= n, where it is extremely common to eschew implicit substitution for explici= t substitutions --- or to use a mix of the two... In neither case are the d= etails of this presented to the user, however, because the gender of an ang= el 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/9B3B568C-452A-4919-A149-CF7C1E91CDAE%40jonmsterling.com.