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 24169 invoked from network); 18 Nov 2022 16:38:47 -0000 Received: from mail-lj1-x23b.google.com (2a00:1450:4864:20::23b) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:38:47 -0000 Received: by mail-lj1-x23b.google.com with SMTP id o19-20020a2e90d3000000b00278fb21e30esf1930097ljg.3 for ; Fri, 18 Nov 2022 08:38:47 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668789526; cv=pass; d=google.com; s=arc-20160816; b=TCNGqbX8RilaxLBOVIiZ1Dv0vS8c6W845l0Q74vaLPrkIu+b6Zgv1LcU4gdQ1PTtso zHxx0UPRcJMNwzh3PmCp/gzglMlkza9FK5w+pXbaqpSw4FfJoV6zMqrQKjz8d4jQXJif k7gIfn5I6/6VFVk4Hjfo45By0JlseudHckGLvf1iQ898gPW5flGX288DxC+O98EIrbwi zuEpsjyizUVmXyOvAmN12L0cnS3QpRAQMlnUpyWJ1eSCJq0RNLEQnw1oL86vCcqHaTUh xwqZF3paQFOTs8LUxwv/Flmg/EMmWbluQwSSLZ54lBnU9j9hbML6GUyQGIIl0s+QDBHL AKDQ== 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=8e3uR5m7RyO6y8szzGQfEN9ifG9zYvuOz6e7SEiJoiY=; b=qn19GcnnIeaq0wxpFdxXpKguL3Tb3dDSXtwGpMBqh6mVdwM+PV2W9ogXrntORgrqct vO94uFCCg/QiY7MbDVUfGoeuYeEfM5iRReQTwSD3VXFJoutAppkXkdeoWNTdpnIqcQZJ 99QMnb9qht7kPRKowdLMlNgOVHqygQO3LvSExvvZ6J7jPOxJ7xZNXvGl7/sRm8oBgEFW 7cDwG8tqy+cwFqhFsqcerohA9ELm/Be34A7KJqOK0t2a06WIn2gDQRb5A3CixMzybogh FppJ96lAfJowCBlprhd2puA07qKDim2zPmm156Nh+cF2lehfav1lxpNUgD0J1QhOqLWD dVCw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=EzBRbH35; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=hJV1FVhA; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 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=8e3uR5m7RyO6y8szzGQfEN9ifG9zYvuOz6e7SEiJoiY=; b=RvkWFkR7ei4btgRI3UbAmOsVazYW1x7H7bODKIYe9cAORamEVmK8PUaV7elpyBZFtg zbN7mOreYQ3KbJqXixqbUxnekHVzCbbIAZl+3e20QbGL+CVL1t2fwkhx+I8bkjP986pz mjkaZZEihwIDwRY1cKWsz3wqNZ+hKMVTqBHHa/l4MbUSGvSzrkgmYg7eVkoEliU97d2K LvmFIGaUHQWTJxyZix1aWqSiiNu03kM/qf3oXev8GVhznlIohwIFZSRNk1JAmoRRbkNQ O4+sZLHjWMvt+hjOmzSEbqiMc0/eP4VGhrYHHnoPLflnAvQtekiPbG5HTZzmQbOL3lqF VzIg== 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=8e3uR5m7RyO6y8szzGQfEN9ifG9zYvuOz6e7SEiJoiY=; b=6tcnbQl8avdojCQqs6r8Lz5r7LwsBgleCu3ft6kPuwFhw5vW8CQVr4xIGdQ2ofLlYb nXY+lK0rYYysgOcbHBAG2m7qobkLZmWp50SUPgsrvf5Dl9WE5GCVN5VqR8MKqOlIA8IQ BOdldNNllw+yLklRC4tiCbeGljZHO9ax4S4jUdrFOcOAka0qfluh0+zxmLTsDFzxdo5/ UDK7UGjvNdlyIlB7gwEIgT2ZumHgqpmfv64hmH0J1u2YiCYeOiXK5/Zu9U2FaVvUyxTl 1ZfDlwrTY2YIWystBz0Ksd7fRyG/a4MQBu6/4LUUpkIH+5H2gqdyro7DY6uLE5jsA3Ew dryA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pnYacJrKP8hk1mDD081++YlFcGvpJS3XDS3zdEFKGp+5TWEeZap wsm0GFbRUC+2dvKqMTKmf5g= X-Google-Smtp-Source: AA0mqf6ChKuRVFrGnTz2T8osp+b+dIZVL65mojGwXN/HZ30CVtMsqxXQIaODU/1lJmuU9OyAFYOqFw== X-Received: by 2002:a19:6d1a:0:b0:4a0:44bb:d1a8 with SMTP id i26-20020a196d1a000000b004a044bbd1a8mr3212764lfc.556.1668789526385; Fri, 18 Nov 2022 08:38:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:651c:98a:b0:277:4af7:14ea with SMTP id b10-20020a05651c098a00b002774af714eals1037478ljq.2.-pod-prod-gmail; Fri, 18 Nov 2022 08:38:43 -0800 (PST) X-Received: by 2002:a2e:2a82:0:b0:277:13ef:53c9 with SMTP id q124-20020a2e2a82000000b0027713ef53c9mr2600319ljq.90.1668789523806; Fri, 18 Nov 2022 08:38:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668789523; cv=none; d=google.com; s=arc-20160816; b=jBFj5cXFrzbpgeeeURO4tyPXDKJoksK3blWqgp5K0WQL0rTqoKNDVBTl2XcyJeOby1 uzQcGzGOEhnr6ubshNVzAFRxVup3zKGBCoWlCobBJGjJLQpLKdIU6J82sPmc8G7513Hk DCU8u9IVcXvSaHSalxqM4FS6tc1gQMe/JR5BLuPU3CLlfKw8SGSl11ezjTsWlDDw/5Tk +vSPxEnDlqpEn1WMclCgrqnoeRE0s7QPBBlOyQXy7N4GHzAdw7zBQ9DNQadleiGmE1Zf LKyWqPN6bHcHiRACC/lyGIOL0KqLyphaMd+Di0NhPmJ+dFEmFvD09kxqt7YrUSC5frwl ABMg== 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=xYI+stoMzeOAneOHWILLYS1+YRT+XAAUmi814s0xC1I=; b=D5y3y1mdxWuIxO10qKviCQgPdCPyQ4djk/kUrqE4ZP9b2IAsVjfqm7/NcLU5WsMu8N +DIZY5kzur9v6/58ku1qyEHmFHYjql9nehSai2+RGc5sWYDocf0gkZa+oU4s9uHmGJI6 Jmuan+JJSSO7QwdTuEcOuIhJWxpQmi84jYPeF2P7WWMhA6zkBymIACCVmpB9cxSSx2CH 4cbBxlTky7TSWFocjujOd3f/8aYtN4pAAL6Py0ZDPdjA8AnpbyBK0zHo2dAJr2BDwxvO AmfvZRNvk6tvWHpMpseKn8XajOcBtbtZWHIVAT/9ckVMOxczVeGts2gvgNMooArFWPJf wbzA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=EzBRbH35; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=hJV1FVhA; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id e19-20020a05651236d300b004b4b625cfecsi164680lfs.4.2022.11.18.08.38.43 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 08:38:43 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) client-ip=64.147.123.25; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 040F13200B81; Fri, 18 Nov 2022 11:38:40 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Fri, 18 Nov 2022 11:38:41 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgdelvdcutefuodetggdotefrodftvf 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 11:38:40 -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 11:38:39 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <19FCB983-3890-4113-9DD6-A76C2AFD8268@jonmsterling.com> In-Reply-To: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> <9B3B568C-452A-4919-A149-CF7C1E91CDAE@jonmsterling.com> <21B50B02-4107-4854-8015-99EA4B14EBA5@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=EzBRbH35; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=hJV1FVhA; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 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: , Hi Mike, Thanks for this! I think we are getting a lot closer. On 18 Nov 2022, at 11:25, Michael Shulman wrote: > In general, I feel like we are still talking past each other. Maybe the > problem is that I still haven't found the words that will communicate my > point to you. I was trying to say that it isn't the word "admissible" th= at > matters, but there are real mathematical questions going on whatever word= s > you use to talk about them. > > Last summer when I was explaining something about HOTT to a group that I > think included you, I used the phrase "admissible" for a certain equality= , > and we got into a bit of this discussion. But I felt like we agreed in t= he > end that what I meant was "a rule that doesn't have to get used explicitl= y > by the conversion-checker", and that it was useful to distinguish such > things whatever we call them. That's what I was trying to get at with > "rules that hold in all models and can be made to hold in a particular > presentation of the free model without being given explicitly as generati= ng > operations/equalities". > > Similarly, I don't think the implicitness or explicitness of substitution= s > in the syntax is what's crucial. If you formulate substitutions > implicitly, then the statement you want is that substitution can be defin= ed > as an "admissible" operation on the syntax. If you formulate substitutio= ns > explicitly, then the statement you want is that substitutions can be > eliminated by a computation. Isn't this what you mean by "The equational > theory of substitution in this situation (particularly, how to commute > substitutions past the modal forms) is the hard part"? You don't just wa= nt > an equational theory for substitution -- the equations in an equational > theory are undirected -- but some kind of rewriting system that tells you > how to push a substitution inside the modal forms. Whether the > substitutions are part of the syntax or not isn't the point. > I agree with a lot of what you have written here, but maybe not all of it. = Let me put it my own way, which is probably similar to what you are getting= at --- I see deciding the equational theory of substitution as a special c= ase of deciding the rest of the equational theory. To me, it is basically u= seless to have a decision procedure for "reducing substitutions but not any= other computations (like beta laws, etc.)". To put it another way, if I do= n't have an algorithm for full normalization (or at least deciding def.eq.)= , I really couldn't care less if I have an algorithm for reducing substitut= ions. Regarding things that exist in the syntax but not necessarily in all models= , this is indeed the point of admissibility and it's really really importan= t! It just so happens, however, that substitutions are the main example of = something that is both admissible **and** exists in all reasonable models. = Even in weak models, we have substitution up to isomorphism --- and no exis= ting solution to the Seely substitution coherence problem works by saying "= Well, substitution is admissible, so we don't need it in the model anyway".= So the one place to look for an example of substitution-admissibility bein= g important in type theory is actually a non-example. Not all admissible rules are as useless as this! To the contrary, there ARE= very important examples of different admissible rules that must not be der= ivable unless we wish to degenerate the theory; the main examples that have= practical import are injectivity laws, which allow you to deterministicall= y reduce complex equality problems to simpler ones; without these, elaborat= ion and type checking would be essentially impossible (whereas elaboration = and typechecking are completely insensitive to the question of whether subs= titution is admissible). Injectivity of type constructors is the main examp= le of an important admissible rule, but there are many more examples (and I= expect, based on our conversations about HOTT over the summer) that there = will be a lot more interesting and important ones to discover in the coming= years. So in case it clarifies me, I think admissibility is extremely important an= d it is, in some sense, the main topic that people like me study. My experi= ence has led me, however, to make a distinction between admissibilities tha= t matter (like injectivity laws) and ones that do not matter at all (like s= ubstitution). Nonetheless, there are many roads to the same idea, and the s= tudy of type theory and logic in terms of admissible substitutions has been= (and remains) an extremely reliable and effective way to obtain well-behav= ed theories. All I am doing is trying to tease out which parts of this proc= ess were essential, and which parts were incidental. 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/19FCB983-3890-4113-9DD6-A76C2AFD8268%40jonmsterling.com.