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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, NICE_REPLY_A,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 2151 invoked from network); 1 Dec 2022 16:10:03 -0000 Received: from mail-lf1-x138.google.com (2a00:1450:4864:20::138) by inbox.vuxu.org with ESMTPUTF8; 1 Dec 2022 16:10:03 -0000 Received: by mail-lf1-x138.google.com with SMTP id b34-20020a0565120ba200b004a2542bd072sf991184lfv.2 for ; Thu, 01 Dec 2022 08:10:03 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669911003; cv=pass; d=google.com; s=arc-20160816; b=NoJA8BvxZtlb6MZ5Uazx27wGGrUQU3HIOiop+rTmrYXu8wwiL0uRW0Epx4J7LV4CcH jdolQeEAk0mXQMAYeqUCFnY54YHIyivuEplO0DF5i/eyGzx1SBBR3Mco2SAx283BKeVu vL4VTULyBx4ENp5vyUk/8ahtzSMWMoCJdXdqCWlTy9QIgtq23errZfGmus/MEOnW6XiQ qFfyZJwc0K0s4ecUPnqY3K/2HF6afwLz9+yDOryt9tJioMiRfvCEpzVqq6Xig5O/56oI hS3dh7e9eb7UE2eVJvSLPG74DPjj3aGbmJvC736U21XsD0dEx3FCpxVy/BPDq4xRhTIw NS5g== 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:in-reply-to:references:cc:to:from :content-language:subject:user-agent:mime-version:date:message-id :sender:dkim-signature:dkim-signature; bh=fcDWOMnAD+HsPfYG3rxID1ewzMUwZ+YmE4g1pqnxs+8=; b=HZ1h1tu4ljvuT1m1azCaI3tkyOBBdJmb+e5CoHUfJnc9j7wW9nEfgUaQQuMuwg2U1g 7jkpvXeeKTYSOT/8T2SWmFu69qmaIsbqB1oHgZidqdhIfdQ9lRnCp8gfrovdjCFQBINr ObbSkh63fXyCEyeYOURYqM50J+GtLRMy7zA7Cx0StHNABmmwMZYzgVRo7BR+bkjUiR8K GlXW1F13+/9HzkuaVZZ9HaGd6ScuG3Tc3uAb7Y7uiQtfPHzeKylvosogEAT/x5Ux+LzG xY+RKGzlCIxnDGIPiNN+YvQ7gW81pndfyqJbUvGLACvzEUN6QEvnk0IUroIST6zoa4Kl PJXA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=PiLQWrv7; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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:in-reply-to:references:cc:to:from :content-language:subject:user-agent:mime-version:date:message-id :sender:from:to:cc:subject:date:message-id:reply-to; bh=fcDWOMnAD+HsPfYG3rxID1ewzMUwZ+YmE4g1pqnxs+8=; b=Rd062EFPQ0y6pQqHflvdxDVAkBqBzTxBmIuFLMdk3N7qVwdHE3O1Hxhea2FnMctgdP 7sw4gatKHNU+b2CbWars9rOof9wQzoo3Lwqw5SogTTSagfuoWwBD2iOzVgY39GF9AH40 TU8myhTcfIQ3utiQkwvdCnLT2HAxuXwZYg7QTEzzG4oKWrSAg00rsLNopWdgEV4M5803 Kaq0CP8D9Jzx34GMwJah+5a18IMUANvHefIYTBXqtPsRqwJbGz48XsvJti/Ttys1rpqC LW+K5Tkb3NUcXlbxbDu40YpSOEDOV1zONvzl7vHsBn1V2aLzgb+el8TXM/JROIHslAJn g0wQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.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:in-reply-to:references:cc:to:from :content-language:subject:user-agent:mime-version:date:message-id :from:to:cc:subject:date:message-id:reply-to; bh=fcDWOMnAD+HsPfYG3rxID1ewzMUwZ+YmE4g1pqnxs+8=; b=PRcrXxHHRrKLrPlcutlYNpKLv7EbCptZNz6gHrwrF0wjhcuZ2IIzESqD03jnVDp7Av CSwHN9XRe+udbES7Bo1T8L8zJydfJ2SPGbk/Ujf5dJi5Q7ruU5ScYxvuPLno9jlL7ZLZ EjhfMfJepxoPDJ0PGDLsmlKAOj8zA6O1ngrben/qL7I+02TxDfmX7HMO+fpNGdfRknTG qL12U7JjWERoY1woZWPzyqadD7Z4vcgoXKlaqfXaYTnb9ruNaLrW//j/UNEkW2torvty tq0rMj6+XenH9yAmxTqBoXnOvL8DN/jK2Ci+jVncbG3ngH5NJw9u9QwtaHcwhbPHtZfl UZrg== 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:in-reply-to :references:cc:to:from:content-language:subject:user-agent :mime-version:date:message-id:x-gm-message-state:sender:from:to:cc :subject:date:message-id:reply-to; bh=fcDWOMnAD+HsPfYG3rxID1ewzMUwZ+YmE4g1pqnxs+8=; b=D4rV4oSTI6KYiQ2o1NcFDBl5IPCU1k8EVUY0iyJL6t+4TjR70wdjtI4UoebGUsKO/H qsKijjkQeQhxCQFRMOx7YgbBxizHbS9pHQwfdjfvVrF/YCiGgWp4ai/00AnFNRBiex1x TrGX4J2PqR+Ym+7BtzNyXFs4xHKupWtDwCkAPhVvG5PuptSVCJilSyyPzmfOlbKMNVex 5ni83QhdADxpTf+Iu+PkkKBGOztDJ6b9NQmOEahyyvbqeBHbVr+tXz4/m97zWkdZX5jl ooCJugqLxFHPwfwctOEalb2CDCnn6CnGbPkKhWW/ChQscZZFYM5VdOBjSBdSOE6qngdV Vinw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5plYI+9Y05P7uJERdDZHlfHfw7bndZvJ1DQgbPxGu5W4yRQsGSjD VNogKMOQ2/5ApSbhf9cGdTM= X-Google-Smtp-Source: AA0mqf48MoK/j2RWyyzPlEF4RTrobpioFlxNeVUoVJ1q/Og8gbGqO3V/dhQkhC0nkLTDm9qVynVoeg== X-Received: by 2002:a05:6512:32cf:b0:4af:e82f:6013 with SMTP id f15-20020a05651232cf00b004afe82f6013mr20015758lfg.36.1669911002853; Thu, 01 Dec 2022 08:10:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:651c:88a:b0:26b:db66:8dd4 with SMTP id d10-20020a05651c088a00b0026bdb668dd4ls418108ljq.8.-pod-prod-gmail; Thu, 01 Dec 2022 08:10:00 -0800 (PST) X-Received: by 2002:a05:651c:1070:b0:276:ac05:b821 with SMTP id y16-20020a05651c107000b00276ac05b821mr23223787ljm.84.1669911000809; Thu, 01 Dec 2022 08:10:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669911000; cv=none; d=google.com; s=arc-20160816; b=NBJgQ/TNRSZjhaFpe7IMd6f+0sXQllF1ro8ErZBcTtVootv0IgY6QfWhuT8yVE9eM6 vhbDBi7u+PMkCqlMl64x5iTr3hFuzlp6R5YxtRG1QYzjxv9ranU/SsN8qVlswLq8SNUv nBsNgWcZqCbvCX7PXZajm0Rsp2cK/1LAGh2BvCczIbta/L5UO15aYopHIEVUAmpPEA3E dUEg8BQOtEaP/4xMGM8TAFAL6+r2c+OuoZbwNFzETT9YQhQyOhqIVzyXBWAUUblfo62i fR1LsDLvtgi8Tl66ZthBFb174Z/hHcRjRRlBKxNsT4Ivs3XKC6E6xE2+jm3cJdXNrlZ6 0LXg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=in-reply-to:references:cc:to:from:content-language:subject :user-agent:mime-version:date:message-id:dkim-signature; bh=ssOQBCfSowpwTWzkFCnbQfX3VbSu49CFnmynIqTEw8M=; b=R4BRUo7DCOUmronz6qflSrw78gYFj0NCD3ocfVHJHRj45ZPIvFPDFh3q094JTuvv13 6xgjShTJdvBgFoc8IJ5nzuLSHbS7/OaBYqbGjuC1Ja2CT8l2SoOFmfvd+wdPmD8SAmR4 ghhKbwg8Zw7oyq0QlH/UsRLwvI76V4KyOKNCsFNvIdO3TQcFYhAQ8MF4/kn0Tq/a9Ujj V6jEGDE1pHUvHCfmt7MroyouPzAnQ7ZWp4ibRrS8mHOcLYJaFRp/DoFuNdNdpM9Qx2DE vbla75ccEnwHAvxPxvOhPg/zEBk3cSYhk/BjHNCeWzcocixDHBg9eIYPp7AaVMmRnHX2 s/aQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=PiLQWrv7; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ej1-x62a.google.com (mail-ej1-x62a.google.com. [2a00:1450:4864:20::62a]) by gmr-mx.google.com with ESMTPS id c2-20020ac25f62000000b004b49cc7bf6asi209945lfc.9.2022.12.01.08.10.00 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 08:10:00 -0800 (PST) Received-SPF: pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::62a as permitted sender) client-ip=2a00:1450:4864:20::62a; Received: by mail-ej1-x62a.google.com with SMTP id e27so5285709ejc.12 for ; Thu, 01 Dec 2022 08:10:00 -0800 (PST) X-Received: by 2002:a17:906:f2cb:b0:78d:e645:9f7d with SMTP id gz11-20020a170906f2cb00b0078de6459f7dmr9712080ejb.572.1669910999531; Thu, 01 Dec 2022 08:09:59 -0800 (PST) Received: from ?IPV6:2a02:2c40:500:a006:6c66:8658:3dfa:383? ([2a02:2c40:500:a006:6c66:8658:3dfa:383]) by smtp.googlemail.com with ESMTPSA id vf6-20020a170907238600b007bebfc97f44sm1911127ejb.75.2022.12.01.08.09.58 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 08:09:58 -0800 (PST) Content-Type: multipart/alternative; boundary="------------BOzavX41UCXwC7GlvXPXNihU" Message-ID: <74bff49b-91b0-8b55-5cb1-10ce815ce470@gmail.com> Date: Thu, 1 Dec 2022 17:09:58 +0100 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:102.0) Gecko/20100101 Thunderbird/102.4.2 Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Content-Language: en-US From: Andreas Nuyts To: Jon Sterling Cc: Michael Shulman , Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory References: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> In-Reply-To: X-Original-Sender: andreasnuyts@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=PiLQWrv7; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , This is a multi-part message in MIME format. --------------BOzavX41UCXwC7GlvXPXNihU Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Actually, I think I disagree on a deeper level: To say that a model (in the sense of algebraic theories) respects the=20 equational theory of a language, does not *only* mean that the=20 evaluation of syntactic programs in that model respects equality. It=20 also means that the evaluation of programs containing subterms that are=20 actually quoted elements from the model, respects equality.=20 (Algebraically speaking, the model should be an Eilenberg-Moore-algebra=20 for the quotiented version of the term monad.) But since *admissible*=20 substitution is undefined for such quoted elements, this cannot be=20 stated (the term monad cannot be quotiented satisfactorily). So while it's true that "you can still check in the admissible-subst=20 scenario whether the interpretation function respects the beta law on=20 all terms", this is a much weaker property than respecting the=20 equational theory of the language. But I agree that my statement "Prettyprinting indeed disrespects=20 =CE=B2=CE=B7-equality." made it sound as evidence of something, whereas I w= as=20 merely arguing that it's a drawback that you cannot reasonably complain=20 about if you were looking for a model without substitution in the first=20 place. On 01.12.22 16:57, Andreas Nuyts wrote: > Right, but when looking for a model that misses a substitution=20 > operation and is not contrived, you're not going to find it among the=20 > models that try to respect equality, because that isn't even statable=20 > in the model. When you drop both the requirement of supporting=20 > substitution, and of respecting equality, then your search space has=20 > grown enough that prettyprinters can be found in it. > > On 01.12.22 16:54, Jon Sterling wrote: >> The issue regarding the beta law is kind of spurious: one of course=20 >> states the beta law using the ADMISSIBLE substitution action. The=20 >> problem with pretty printing is that it is indeed not satisfying the=20 >> beta law but this has absolutely nothing to do with substitution =E2=80= =94=20 >> you can still check in the admissible-subst scenario whether the=20 >> interpretation function respects the beta law on all terms, and in=20 >> this case it just happens that it doesn=E2=80=99t. >> >>> On Dec 1, 2022, at 3:40 PM, Andreas Nuyts =20 >>> wrote: >>> >>> =EF=BB=BF Hi everyone, >>> >>> I finally found time to read up on this lengthy conversation. >>> >>> Jon wrote: >>> >>> It is revealing that nobody has proposed a notion of **model** >>> of type theory in which the admissible structural rules do not >>> hold; this would be the necessary form taken by any evidence for >>> the thesis that it is important for structural rules to not be >>> derivable. >>> >>> >>> I think, on the contrary, that such models are not acknowledged as=20 >>> being models, because the language without substitution is in=20 >>> general not really the language of interest. An example of a model=20 >>> disrespecting substitution is the prettyprinter by Allais, Atkey,=20 >>> Chapman, McBride & McKinna (2021): >>> https://doi.org/10.1017/S0956796820000076 >>> Indeed, substitution is no longer possible after prettyprinting, but=20 >>> all other language constructs are supported. Note that if a=20 >>> substitution operation is unavailable in a model, then the =CE=B2-rule= =20 >>> for functions cannot even be stated in that model, let alone asked=20 >>> to hold. So a model that fails to have a substitution operation=20 >>> necessarily also disrespects the equational theory of a language=20 >>> with such a =CE=B2-rule. Prettyprinting indeed disrespects =CE=B2=CE=B7= -equality. >>> >>> Mike wrote: >>> >>> MTT is also not equivalent to split-context theories, and IMHO >>> is less pleasant to work with in practice. >>> >>> >>> I'm reluctant to postulate here that any split-context theory is=20 >>> equivalent to some instance of MTT, but I would be quite surprised=20 >>> if you ever face any practical problems when abandoning a=20 >>> split-context system in favour of MTT. If you're thinking in=20 >>> particular about a system with crisp and non-crisp variables: such a=20 >>> system is implemented by Andrea in agda-flat. At the last Agda=20 >>> meeting, we have been investigating how mature the current modality=20 >>> system in Agda is and how feasible it is to support full MTT. One=20 >>> thing we observed is that - of all the parallel modality systems=20 >>> implemented in Agda - the cohesive one (of which only the flat and=20 >>> non-flat modalities are exposed to the user) is actually the one=20 >>> that adheres to the discipline of MTT (by having a third "squash"=20 >>> modality that effectively removes variables from the context). >>> Both regarding usability and equivalence, do not be misled by the=20 >>> invasive-looking locks. These locks have two confluent histories: >>> - there is a history of fitch-style logics, >>> - there is a history of modal logics with left-division. When=20 >>> implementing Menkar, which was intended as a proof assistant for=20 >>> general multimode systems with left division, I observed at some=20 >>> point that the left division of all modalities in the context=20 >>> actually never needs to be computed and can thus be regarded as a=20 >>> context /constructor/, rather than as an operation (i.e.=20 >>> admissibility of left division was not required, in none of the=20 >>> senses of the word mentioned so far). Modal Agda does use an eagerly=20 >>> computed left division. These systems with left division are very=20 >>> closely related to dual context systems. >>> >>> I think usability is hard to judge because there isn't yet good tool=20 >>> support to experiment with. But I believe that it can grow on the=20 >>> user. A lock simply means "we've moved into a modal subterm". The=20 >>> position of the lock in the context is important in order to keep=20 >>> track of which variables were introduced before/after moving into=20 >>> that modal subterm. When using a variable, you just need to make=20 >>> sure that the variable's modal annotation is =E2=89=A4 the composition = of=20 >>> the locks, i.e. the modality of the position where we currently are=20 >>> and where we want to use the variable. >>> >>> I am happy to discuss this matter further if you have any questions=20 >>> or doubts. >>> >>> Best regards, >>> Andreas Nuyts >>> >>> On 18.11.22 18:14, Michael Shulman wrote: >>>> That's an interesting question.=C2=A0 I was thinking of operations and= =20 >>>> equalities, and annotations are neither of those, but I can see=20 >>>> that they're somewhat similar in spirit.=C2=A0 But I find it even more= =20 >>>> difficult to imagine how to define this phenomenon precisely in a=20 >>>> way that would include them... >>>> >>>> On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling =20 >>>> wrote: >>>> >>>> On 18 Nov 2022, at 11:56, Michael Shulman wrote: >>>> >>>> > Thanks.=C2=A0 It does sound like we mostly agree.=C2=A0 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.=C2=A0 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.=C2=A0 For instance, can we find a third wo= rd >>>> 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? >>>> > >>>> >>>> Cool, it's a relief to start getting this cleared up! I really >>>> agree with you that there is a need for terminology to describe >>>> the situation you mention, and maybe even more, there is a need >>>> to define this phenomenon... >>>> >>>> I wonder if we can think of more concrete examples of this. For >>>> instance, in many versions of syntax (like bidirectional ones) >>>> we can choose to drop certain annotations because they will be >>>> available as part of the flow of information in the elaboration >>>> algorithm. Would these be an example of the phenomenon you are >>>> describing, or is it something different? >>>> >>>> Best, >>>> Jon >>>> >>>> --=20 >>>> You received this message because you are subscribed to the Google=20 >>>> Groups "Homotopy Type Theory" group. >>>> To unsubscribe from this group and stop receiving emails from it,=20 >>>> send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>> To view this discussion on the web visit=20 >>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArA= pd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com=20 >>>> . >>> > --=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/74bff49b-91b0-8b55-5cb1-10ce815ce470%40gmail.com. --------------BOzavX41UCXwC7GlvXPXNihU Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Actually, I think I disagree on a deeper level:
To say that a model (in the sense of algebraic theories) respects the equational theory of a language, does not *only* mean that the evaluation of syntactic programs in that model respects equality. It also means that the evaluation of programs containing subterms that are actually quoted elements from the model, respects equality. (Algebraically speaking, the model should be an Eilenberg-Moore-algebra for the quotiented version of the term monad.) But since *admissible* substitution is undefined for such quoted elements, this cannot be stated (the term monad cannot be quotiented satisfactorily).
So while it's true that "you can still check in the admissible-subst scenario whether the interpretation function respects the beta law on all terms", this is a much weaker property than respecting the equational theory of the language.

But I agree that my statement "Prettyprinting indeed disrespects =CE=B2=CE=B7-equality." made it sound as evidence of something, whereas= I was merely arguing that it's a drawback that you cannot reasonably complain about if you were looking for a model without substitution in the first place.

On 01.12.22 16:57, Andreas Nuyts wrote:<= br>
Right, but when looking for a model that misses a substitution operation and is not contrived, you're not going to find it among the models that try to respect equality, because that isn't even statable in the model. When you drop both the requirement of supporting substitution, and of respecting equality, then your search space has grown enough that prettyprinters can be found in it.

On 01.12.22 16:54, Jon Sterling wrote:
The issue regarding the beta law is kind of spurious: one of course states the beta law using the ADMISSIBLE substitution action. The problem with pretty printing is that it is indeed not satisfying the beta law but this has absolutely nothing to do with substitution =E2=80=94 you= can still check in the admissible-subst scenario whether the interpretation function respects the beta law on all terms, and in this case it just happens that it doesn=E2=80=99t.

On Dec 1, 2022, at 3:40 PM, Andreas Nuyts <andreasnuyts@gmail.com> wrote:

=EF=BB=BF Hi everyone,

I finally found time to read up on this lengthy conversation.

Jon wrote:

It is revealing that nobody has proposed a notion of **model** of type theory in which the admissible structural rules do not hold; this would be the necessary form taken by any evidence for the thesis that it is important for structural rules to not be derivable.
I think, on the contrary, that such models are not acknowledged as being models, because the language without substitution is in general not really the language of interest. An example of a model disrespecting substitution is the prettyprinter by Allais, Atkey, Chapman, McBride & McKinna (2021):
https://doi.org/10.1017/S09567968200= 00076
Indeed, substitution is no longer possible after prettyprinting, but all other language constructs are supported. Note that if a substitution operation is unavailable in a model, then the =CE=B2-rule for functions cann= ot even be stated in that model, let alone asked to hold. So a model that fails to have a substitution operation necessarily also disrespects the equational theory of a language with such a =CE=B2-rule. Prettyprinting indeed disrespects =CE=B2=CE=B7-equality.

Mike wrote:

MTT is also not equivalent to split-context theories, and IMHO is less pleasant to work with in practice.

I'm reluctant to postulate here that any split-context theory is equivalent to some instance of MTT, but I would be quite surprised if you ever face any practical problems when abandoning a split-context system in favour of MTT. If you're thinking in particular about a system with crisp and non-crisp variables: such a system is implemented by Andrea in agda-flat. At the last Agda meeting, we have been investigating how mature the current modality system in Agda is and how feasible it is to support full MTT. One thing we observed is that - of all the parallel modality systems implemented in Agda - the cohesive one (of which only the flat and non-flat modalities are exposed to the user) is actually the one that adheres to the discipline of MTT (by having a third "squash" modality that effectively removes variables from the context).
Both regarding usability and equivalence, do not be misled by the invasive-looking locks. These locks have two confluent histories:
- there is a history of fitch-style logics,
- there is a history of modal logics with left-division. When implementing Menkar, which was intended as a proof assistant for general multimode systems with left division, I observed at some point that the left division of all modalities in the context actually never needs to be computed and can thus be regarded as a context constructor, rather than as an operation (i.e. admissibility of left division was not required, in none of the senses of the word mentioned so far). Modal Agda does use an eagerly computed left division. These systems with left division are very closely related to dual context systems.

I think usability is hard to judge because there isn't yet good tool support to experiment with. But I believe that it can grow on the user. A lock simply means "we've moved into a modal subterm". The position of the lock in the context is important in order to keep track of which variables were introduced before/after moving into that modal subterm. When using a variable, you just need to make sure that the variable's modal annotation is =E2=89=A4 the composition of the locks, i.e. the modality of the position where we currently are and where we want to use the variable.

I am happy to discuss this matter further if you have any questions or doubts.

Best regards,
Andreas Nuyts

On 18.11.22 18:14, Michael Shulman wrote:
That's an interesting question.=C2=A0 I was thinking of operations and equalities, and annotations are neither of those, but I can see that they're somewhat similar in spirit.=C2=A0 But I find it even more difficult to imagine how to define this phenomenon precisely in a way that would include them...

On Fri, Nov 18, 2022 at 8:59 AM Jon Sterling <jon@jonmsterling.com> wrote:
On 18 Nov 2022, at 11:56, Michael Shulman wrote:

> Thanks.=C2=A0 It does sound like we mostly agree.=C2= =A0 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.=C2=A0 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.=C2=A0 For instance, can we fin= d 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?
>

Cool, it's a relief to start getting this cleared up! I really agree with you that there is a need for terminology to describe the situation you mention, and maybe even more, there is a need to define this phenomenon...

I wonder if we can think of more concrete examples of this. For instance, in many versions of syntax (like bidirectional ones) we can choose to drop certain annotations because they will be available as part of the flow of information in the elaboration algorithm. Would these be an example of the phenomenon you are describing, or is it something different?

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 Ho= motopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZ= Q%40mail.gmail.com.



--
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://groups.google.com/d/msg= id/HomotopyTypeTheory/74bff49b-91b0-8b55-5cb1-10ce815ce470%40gmail.com.=
--------------BOzavX41UCXwC7GlvXPXNihU--