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,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 26324 invoked from network); 18 Nov 2022 16:56:37 -0000 Received: from mail-oa1-x3a.google.com (2001:4860:4864:20::3a) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:56:37 -0000 Received: by mail-oa1-x3a.google.com with SMTP id 586e51a60fabf-13d57d20818sf2629722fac.12 for ; Fri, 18 Nov 2022 08:56:37 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668790596; cv=pass; d=google.com; s=arc-20160816; b=WkGnFp5C9jQdpGMFuOUzFFnRnLLSk/zNL4sXxsl4Pa3b9jMApNZP8y1gErMNE96f8l XSmz/e3gOKwTWlwgh0fFht/d0OS1PUyBgVScNwLFsJBw5TuYga2rvoWtDq04HaBNPBGy 0hFHcdRv5epnbLBTF/OcPnyXWSV1NUi8y3RvgmHHODDZvna7XnCH2gfUV4PQ9Ar5/45W ZNsHEF4cESeeMgA5uxdtoi8pmoYznacJbtTMKhAJqGoZFuy6MsIS3SC75hnhFTLK+R1F 3w5oVH5iuA1wuP9PkjjW1yDw10maVnAqXY1vDdX705EyX7xgNL2sWnlrZPcCZIOfxfze hZ4g== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=pgqwbE+xsURGOqrWV1NLrbMXmDeqS1ax1cGqqBY2754=; b=h79xGae4nOn1Ro9NF0s4Fz5LDo5sAUc3YSOBNVKe+OKusUjiKVqUMCQW3warMmPWGl /ZAo0k/Qelbh3aFl2K07SGG/D9KI/z4T5IJkSu/I5vSbxSE80GSm3g6LLPrnPVOTqX4I qWs2ad+p3dFqBaebUUW4S0QUqz5BatT2lzMfBCAnliMdRryj3sqJrWdHkyE2wChXtqjw /lmAp2cy5anss9S+GYGel7zHEIefTICGlWPqS6nEOROLiXUSdEiDkUdQce0/yMOBY8ad SzK/iDv/yB5dRFZ0SxIQeEIMYxWkuEMKAGw1jcu6lRR/N45bruUHnI1mqKoK5h3M6nQA do8g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CSRqKdHk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=pgqwbE+xsURGOqrWV1NLrbMXmDeqS1ax1cGqqBY2754=; b=JqI83IEmRdxR2xE6g9ds4SBcpUycl/x7Xo4cXFw8d2y9NejuIFOrbr6tHBayUngnd7 cBBf+fXtx9GTtIAxUf3adV4hdtyrxosFqw9RsrCfqN6/FMVYbY+MOUcN/QgdAiOT/Hvp OWW5JNXLPeoM76u1d9cnyOzJD1fANvAPayjy8Vtcx526YIBhIvdVRoR+ogkMBWvldigJ H3QhO2KYs6HetLRzB5TayWFQ8TfDMJrdf3Y+e0f6E2yPre4JJjLzvOBVOH08LABT2clK ALHe2C0hklAdhdRF3dyuV6OK8QGwNyk00G0Oqo8Qb8CE7Denjw5DceQMvz54qITkrHJs L30Q== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=pgqwbE+xsURGOqrWV1NLrbMXmDeqS1ax1cGqqBY2754=; b=7VolIpyi+yfu0Ly8Ljk6w1ZDzUGJuU1FvAcBIdHqucQB0fMh1+AmwU6OTvSAx9H2n4 t7zgD3Qa5Wp+G7r+CKid9RdPgb0BQCc+P54EwTQuiSsYO20AV4zivgj1DP0AoLuwbLvN kKkztS0rulNHrZEhyK6q19LToRZ7/2wtJu0bVybgg+HhtJBBaZL9/V86mLoDs0UaPDP/ +wBR3RfktCp8dHuGgSxEPVixdDarIsL7p+MLyQE1RxlD3uBGy3kEq//qH1BwsYxKcKyo AS5novsmZ51eYdzd8ueWlZiSMaCF7UFYVZZh8dEoan9/JLIeGREBxI9DliwttBTlMHFy ZmLA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkudQ4PQQ40LcIHy+gO886qZ0/prTNY6PQlnY0AMr08rItVLj5/ fiVNSZArgpHrNAIHO4h6bc4= X-Google-Smtp-Source: AA0mqf5Uh9Xja5ViuGCm0lRu4xQFKhEX+kxpsls2IMjTWwgrT0tXS+5QLsjwisBGT/NJLEJB8tnF2w== X-Received: by 2002:a05:6870:288d:b0:136:c9c1:6737 with SMTP id gy13-20020a056870288d00b00136c9c16737mr4508842oab.146.1668790594835; Fri, 18 Nov 2022 08:56:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:1583:b0:345:9a88:c799 with SMTP id t3-20020a056808158300b003459a88c799ls1710689oiw.5.-pod-prod-gmail; Fri, 18 Nov 2022 08:56:33 -0800 (PST) X-Received: by 2002:a54:4595:0:b0:359:f10d:587c with SMTP id z21-20020a544595000000b00359f10d587cmr3832877oib.114.1668790593623; Fri, 18 Nov 2022 08:56:33 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668790593; cv=none; d=google.com; s=arc-20160816; b=DwTx0BOAtLJcOCS6bu678vSAey9urp0UdKYTuE4UWo/U8eBoXEnHHLByBueUdskgSM lr/8suDL/K1TEjIWYpmIdDeUALgTnUJWvMTuAiB4AcgyuorRPwWNroD5EzkE7ANcc2cE 8Aug72kDNOORs2e8gUb8snP5HpaF/RSm2DhCEestPHgTlH9bRi9toJ1+TScK8sGcDwgA EVOs6krmvb1nc3J/JQtTIhDc1S7MM2DzkhjTDBZhNLHA9Q9UCH7nb0k/Oe5enFqooZp7 a7qCN7x5MmEDJ8r0ZS+RVoy67kDfbpnS2auHKz8Cs5aGJ0tIV6lgDJ6RvOUE2C/+KdoN 8Oqg== 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:in-reply-to:references :mime-version:dkim-signature; bh=LGqCup21s9FVVC/9OdxqXL3cEeZNMDO9zWGl7Q091tw=; b=hlR6k2RG7MGsqS4uUhslwcfFXLoTmXmaN7MqVGbWUXoIdKoQ6y6bB8MaINdhX9LnkV ZzOBZYXnF0hrijq7w0oAD9g0mQ50+f9qegpxOIZPEenbaaE4V3UhtnBH3+SS4YuqFriN FwZ09k4YUnWq3NBKIqA+MWNXpXO30RhrRtV2vs3wN4HyVUT3bmoSWAxQicZ5bA9Hu6oM 28ilDneCG6ftrYzCCWkTipTTKhxbtY9ujotfp8w+Yp/KQfi+t09RXTrvb0y15yFYtSWI h/PQhtFzGSeAB2wx8sF7oxVxFZbkNIq9K+iWNEPax/3UwMLlwKBri/tyWLMaRPh61hEX g03Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CSRqKdHk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id f61-20020a9d03c3000000b0066d3e48f924si174055otf.2.2022.11.18.08.56.33 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 18 Nov 2022 08:56:33 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id v123so6309619ybv.5 for ; Fri, 18 Nov 2022 08:56:33 -0800 (PST) X-Received: by 2002:a25:d897:0:b0:6c0:3e01:18f3 with SMTP id p145-20020a25d897000000b006c03e0118f3mr7595226ybg.350.1668790593152; Fri, 18 Nov 2022 08:56:33 -0800 (PST) MIME-Version: 1.0 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> <19FCB983-3890-4113-9DD6-A76C2AFD8268@jonmsterling.com> In-Reply-To: <19FCB983-3890-4113-9DD6-A76C2AFD8268@jonmsterling.com> From: Michael Shulman Date: Fri, 18 Nov 2022 08:56:20 -0800 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Jon Sterling Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000082841505edc1969c" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=CSRqKdHk; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , --00000000000082841505edc1969c Content-Type: text/plain; charset="UTF-8" Thanks. It does sound like we mostly agree. I would probably argue that even for type theories in development, where we don't yet know that full definitional equality is decidable -- or intrinsically ill-behaved type theories like Lean, or Agda with non-confluent rewrite rules, where definitional equality *isn't* decidable -- there is still value in being able to reduce just substitutions. But I think that's a relatively minor point. Maybe we can work out some way to use words so that this underlying agreement is evident. For instance, can we find a third word to use alongside "admissible" and "derivable" to refer to operations/equalities like substitution and its theory, which hold in all reasonable models, and can be made admissible in some presentations, but more importantly can be eliminated in an equality-checking algorithm? On Fri, Nov 18, 2022 at 8:38 AM Jon Sterling wrote: > 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" > that > > matters, but there are real mathematical questions going on whatever > words > > 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 > the > > end that what I meant was "a rule that doesn't have to get used > explicitly > > 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 > generating > > operations/equalities". > > > > Similarly, I don't think the implicitness or explicitness of > substitutions > > in the syntax is what's crucial. If you formulate substitutions > > implicitly, then the statement you want is that substitution can be > defined > > as an "admissible" operation on the syntax. If you formulate > substitutions > > 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 > want > > 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 > case of deciding the rest of the equational theory. To me, it is basically > useless to have a decision procedure for "reducing substitutions but not > any other computations (like beta laws, etc.)". To put it another way, if I > don'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 > substitutions. > > 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 > important! 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 existing 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 being 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 > derivable unless we wish to degenerate the theory; the main examples that > have practical import are injectivity laws, which allow you to > deterministically reduce complex equality problems to simpler ones; without > these, elaboration and type checking would be essentially impossible > (whereas elaboration and typechecking are completely insensitive to the > question of whether substitution is admissible). Injectivity of type > constructors is the main example 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 > and it is, in some sense, the main topic that people like me study. My > experience has led me, however, to make a distinction between > admissibilities that matter (like injectivity laws) and ones that do not > matter at all (like substitution). Nonetheless, there are many roads to the > same idea, and the study of type theory and logic in terms of admissible > substitutions has been (and remains) an extremely reliable and effective > way to obtain well-behaved theories. All I am doing is trying to tease out > which parts of this process were essential, and which parts were incidental. > > Best, > Jon > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxB3-n6Udm86ZDZQTKUTYfgzjHWM6g85_-ANpo6pVsOqQ%40mail.gmail.com. --00000000000082841505edc1969c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks.=C2=A0 It does sound like we mostly agree.=C2= =A0 I would probably argue that even for type theories in development, wher= e we don't yet know that full definitional equality is decidable -- or = intrinsically ill-behaved type theories like Lean, or Agda with non-conflue= nt rewrite rules, where definitional equality *isn't* decidable -- ther= e is still value in being able to reduce just substitutions.=C2=A0 But I th= ink that's a relatively minor point.

Maybe we = can work out some way to use words so that this underlying agreement is evi= dent.=C2=A0 For instance, can we find a third word to use alongside "a= dmissible" and "derivable" to refer to operations/equalities= like substitution and its theory, which hold in all reasonable models, and= can be made admissible in some presentations, but more importantly can be = eliminated in an equality-checking algorithm?


On Fr= i, Nov 18, 2022 at 8:38 AM Jon Sterling <jon@jonmsterling.com> wrote:
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.=C2=A0 Ma= ybe the
> problem is that I still haven't found the words that will communic= ate my
> point to you.=C2=A0 I was trying to say that it isn't the word &qu= ot;admissible" that
> matters, but there are real mathematical questions going on whatever w= ords
> 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 cer= tain equality,
> and we got into a bit of this discussion.=C2=A0 But I felt like we agr= eed in the
> end that what I meant was "a rule that doesn't have to get us= ed explicitly
> by the conversion-checker", and that it was useful to distinguish= such
> things whatever we call them.=C2=A0 That's what I was trying to ge= t at with
> "rules that hold in all models and can be made to hold in a parti= cular
> presentation of the free model without being given explicitly as gener= ating
> operations/equalities".
>
> Similarly, I don't think the implicitness or explicitness of subst= itutions
> in the syntax is what's crucial.=C2=A0 If you formulate substituti= ons
> implicitly, then the statement you want is that substitution can be de= fined
> as an "admissible" operation on the syntax.=C2=A0 If you for= mulate substitutions
> explicitly, then the statement you want is that substitutions can be > eliminated by a computation.=C2=A0 Isn't this what you mean by &qu= ot;The equational
> theory of substitution in this situation (particularly, how to commute=
> substitutions past the modal forms) is the hard part"?=C2=A0 You = don't just want
> an equational theory for substitution -- the equations in an equationa= l
> theory are undirected -- but some kind of rewriting system that tells = you
> how to push a substitution inside the modal forms.=C2=A0 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 no= t any other computations (like beta laws, etc.)". To put it another wa= y, if I don't have an algorithm for full normalization (or at least dec= iding def.eq.), I really couldn't care less if I have an algorithm for = reducing substitutions.

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 impo= rtant! It just so happens, however, that substitutions are the main example= of something that is both admissible **and** exists in all reasonable mode= ls. Even in weak models, we have substitution up to isomorphism --- and no = existing solution to the Seely substitution coherence problem works by sayi= ng "Well, substitution is admissible, so we don't need it in the m= odel anyway". So the one place to look for an example of substitution-= admissibility being 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

--
You received this message because you are subscribed to the Google Groups &= quot;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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CADYavpxB3-n6Udm86ZDZQTKUTYfgzjHW= M6g85_-ANpo6pVsOqQ%40mail.gmail.com.
--00000000000082841505edc1969c--