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 531 invoked from network); 1 Dec 2022 15:58:04 -0000 Received: from mail-lj1-x23a.google.com (2a00:1450:4864:20::23a) by inbox.vuxu.org with ESMTPUTF8; 1 Dec 2022 15:58:04 -0000 Received: by mail-lj1-x23a.google.com with SMTP id c18-20020a2ebf12000000b00279a72705fesf444146ljr.12 for ; Thu, 01 Dec 2022 07:58:04 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669910283; cv=pass; d=google.com; s=arc-20160816; b=knzT/46u68/zh7iFfR0p+x8lo2wrpCcg4BQLnSTw/XX03QLIQPAvnC2YPANBIjl0HC 8PvxqxAVoOW5EBavTPo7nzOpLVIT4PAlc/MTT9kDEA9+PJOj5XjF3pUkgGImpQxeSW05 ziCurc9HuOShcNgGglB4BVxR+XvV/4rFFaC2LXeUQv2VfLl6v0Vvj85EqeqdNSUJjLi1 csQD4jAx22To4LxdbY3BotSSLhZ8gk0sev/G/YFYVp14apSXMExx/CA3ANGBqoPMOf7F nyDw8KMq4a2r9TG4jf3e6XkWDZML3DdqeSGH6cer/r9o1MANe+FkjC9q5MwcD5P0dRsl k+AQ== 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:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :sender:dkim-signature:dkim-signature; bh=AFZfQsDk/uQDDrAcRjpA/ffsTK/7tQAMgovAVcmNo2k=; b=DXxWxgRNfbSuFBcjnPwaapsKiXkNOQ1s1xNiOw/dm2p70fS1SjBjxqVL2oZ4Evk+Up dYQCpCtMs1HC/fXS9q3N1NLHKbvTbDmQobbxaV9UXoMSyJsmBBPg4RDE4AOjRT7WMLov nPUGgTVrgyKH/xWRaTM6h1FbgevK8CJc8QVqXGhN75nTsSXA34Bot13Y2sDjPqcX5GFL vE/y13zIw/FN6288kfjWXamSm6BdlGcLsazALqWJEZ7RLAyOSQmGd190JFhDEMPU8AGv Zq75oWicG3m2GRON0dPS2qQQEeq7mYvy48M7E8FVxl24ZMO5RtL2K+KSaj6eV4RFmZVj k4rg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=n0DuUf9u; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::635 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:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :sender:from:to:cc:subject:date:message-id:reply-to; bh=AFZfQsDk/uQDDrAcRjpA/ffsTK/7tQAMgovAVcmNo2k=; b=UQ7brQaoyBcT9lWGbATqkXvCZKwPRfifET6Y+VkUd5Tui8RfzPRgOjANJPBzpbtrgi 91dchW0lZTC0Kome56RI1/zjofX1Hn8DojFmD3ZNFNNhi9hwfz5WDiRowOZLFTvcrl6k Cvd3jAa1ETkTiSr2B9ttE4Jy/8geIVoBZeJ0jfxaD6Xng/v4BkQGesU+k8DrFuFZMphx a2fTi/03oh2Y1K29AnM2/RUOdtuEAncj3DWnj637kLriRtc0h8YQfCGOx22y9hfZ4did vr7n/LnHn8ymcSRHKd3ex9pyvdXt6zlFQS/6lDdY65BOpw3fvXZuUBTetvmb5zCo1KJ7 bryw== 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:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :from:to:cc:subject:date:message-id:reply-to; bh=AFZfQsDk/uQDDrAcRjpA/ffsTK/7tQAMgovAVcmNo2k=; b=WlA01USU1ouaXO/oN4QQgu6IG6GTmGK/obcpTZP6KcW2PhHQYkirTYBB1ZdFsBMSbt 2isS9HysLR/nW4CUobHbjqgY2ZZUd18lnLkYEuffrUvO03TuJRHMoPPGa9at19VHLOVQ 8kIxqrdIAQCOhU8X5Dwg2BkwkBErVkE8DO5kg1byIEJSJTA3Ujl3C2gFTd33UjoIINsb iEF4AzEvyxTROuFnbYkDdAfIoCJ+Hxpjc+uraO/98zPuqZpLCTTsQb7ycxJwPYu3Veem s5Yt7Ep8dE1MCOoGK2xUonXAQQ+uT+yfd4u5GvoemMfT4Rp0c0Rd8CIlbog2lkWX0QHt ZoYw== 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 :from:references:cc:to: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=AFZfQsDk/uQDDrAcRjpA/ffsTK/7tQAMgovAVcmNo2k=; b=CL1NEKVqsu3w1Zun6nubZ02C1PxrDC+U/3afbM/xfhLu0XtZlYAyuT5Pe2cdp89vt4 npqxo+A1tTBhWD2zIBdLUV0gLNRK1cy4dCGFnkVvMYiSPVNmUL4rUZltxhoRuzUVA+zi 3Uf3KnIHlrI0tF2CWfxQmbezN/Muq8vKYxlP2wffc+GzdsmOmtFn7QQ5FLRBJnko/R3s kswVUAKX+svo+Dei+kdLexCXXfCcQ4a2EHoHNnYI87DSBBcqiOcgPaH8VWudDZda+gb5 IUQNM0YGPavuAsmU3d74uH+vJH97dFb6ErkrxEmhvgDvGgJ6SywIuBPj+AtX853/KnTD 20jw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pk4J5kNd0m4rS1MUGgSlVNfPD7OuZH/cBUcUUmnfe6Zf6FseLD4 nOzJhrVUwQA5odtmveE/6bs= X-Google-Smtp-Source: AA0mqf6EZpAJ0vf+Uhx/29qZ7h/HO3uKjHkj+EU7Y908IAupUxNUvNcBaUphZwnRJgD6blySaKfyIw== X-Received: by 2002:a2e:b004:0:b0:279:c02e:7457 with SMTP id y4-20020a2eb004000000b00279c02e7457mr3881280ljk.475.1669910283555; Thu, 01 Dec 2022 07:58:03 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:360f:b0:49a:b814:856d with SMTP id f15-20020a056512360f00b0049ab814856dls499137lfs.1.-pod-prod-gmail; Thu, 01 Dec 2022 07:58:01 -0800 (PST) X-Received: by 2002:ac2:4a8c:0:b0:4b5:4a26:b7a8 with SMTP id l12-20020ac24a8c000000b004b54a26b7a8mr616558lfp.134.1669910281493; Thu, 01 Dec 2022 07:58:01 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669910281; cv=none; d=google.com; s=arc-20160816; b=bFZMaIXych7FgNoCVdg1ZS6CCbjuT/Avv3kI+T75xywTO3PLWxjLcATxvidXeaBsCC cgnm7qjtJVKHdhYjHrjIzXEBItEzuGJnfjyZujcAJSKKPfDbX1rti9609OvFoy+nzOh8 9KXZwDcCqHKf3fT3BqF2nLzUVmfb0BZ9EulsYS5x837nmByyiQ2c22TTQJWoIfRF+gJ/ laIwUsyHbY8Z6oQExy14tqoNQmFubdizrn6491fd+LFWITu3LMIYO0cjZZm2sBkG9CVW cSQgCkfDxLjfV0c8RFsib35Ixq07FHrfJ4/rntmuw2NCs5uFSmBVxuBe3uskXNPJrSq8 rclQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=in-reply-to:from:references:cc:to:content-language:subject :user-agent:mime-version:date:message-id:dkim-signature; bh=gJ2i7/63ehSTXDAUzER9UYrLQbEnZzkruprAljW2578=; b=jaGpLYA3Enjq3jWN6oBTdxR3jiwyvos/MmNt+242H0xHtesMFHloysiC+3r4IFglmC bGZbJLppRZaK9Q26h37O4EvyhdQQclG1A7yUIEVVfc+KXTDCvNvQuQlfj/kjyEHxqqBQ YTWwUGDXbOebu7KA40r/YRYHos5w4VN6vMqXlIFtGZvj413eEJE2M45IvVrcFRxD3n+2 PZj+M3+vbKylp+HrDy9Jtniqtght8rKGIGjZNunLCorwsBfWJ1U0eJ7MCn2XRAQQXPZy lWyybKUFnRKaeQU9OEn7n/lEiw/NHZ95oQn1Z2yKmesPtswjJH8Qwadequ6YDesnHcSf C0vQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=n0DuUf9u; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::635 as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ej1-x635.google.com (mail-ej1-x635.google.com. [2a00:1450:4864:20::635]) by gmr-mx.google.com with ESMTPS id m6-20020a056512358600b004b01b303713si190146lfr.8.2022.12.01.07.58.01 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 07:58:01 -0800 (PST) Received-SPF: pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::635 as permitted sender) client-ip=2a00:1450:4864:20::635; Received: by mail-ej1-x635.google.com with SMTP id vp12so5221674ejc.8 for ; Thu, 01 Dec 2022 07:58:01 -0800 (PST) X-Received: by 2002:a17:906:1412:b0:7a0:3313:a775 with SMTP id p18-20020a170906141200b007a03313a775mr47194822ejc.474.1669910280920; Thu, 01 Dec 2022 07:58:00 -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 r23-20020a170906281700b007c0b9500129sm352683ejc.68.2022.12.01.07.58.00 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 07:58:00 -0800 (PST) Content-Type: multipart/alternative; boundary="------------zasRaybQiTZAbHsav2uhOGz3" Message-ID: Date: Thu, 1 Dec 2022 16:57:59 +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 To: Jon Sterling Cc: Michael Shulman , Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory References: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> From: Andreas Nuyts 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=n0DuUf9u; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::635 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. --------------zasRaybQiTZAbHsav2uhOGz3 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Right, but when looking for a model that misses a substitution operation=20 and is not contrived, you're not going to find it among the models that=20 try to respect equality, because that isn't even statable in the model.=20 When you drop both the requirement of supporting substitution, and of=20 respecting equality, then your search space has grown enough that=20 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 you=20 > 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 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 general=20 >> 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 f= or=20 >> functions cannot even be stated in that model, let alone asked to=20 >> hold. So a model that fails to have a substitution operation=20 >> necessarily also disrespects the equational theory of a language with=20 >> such a =CE=B2-rule. Prettyprinting indeed disrespects =CE=B2=CE=B7-equal= ity. >> >> 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 if=20 >> you ever face any practical problems when abandoning a split-context=20 >> system in favour of MTT. If you're thinking in particular about a=20 >> system with crisp and non-crisp variables: such a system is=20 >> implemented by Andrea in agda-flat. At the last Agda meeting, we have=20 >> been investigating how mature the current modality system in Agda is=20 >> and how feasible it is to support full MTT. One thing we observed is=20 >> that - of all the parallel modality systems implemented in Agda - the=20 >> cohesive one (of which only the flat and non-flat modalities are=20 >> exposed to the user) is actually the one that adheres to the=20 >> discipline of MTT (by having a third "squash" modality that=20 >> 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 sure=20 >> that the variable's modal annotation is =E2=89=A4 the composition of the= =20 >> locks, i.e. the modality of the position where we currently are and=20 >> 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 that=20 >>> 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 p= robably >>> 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 wor= d >>> 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/CADYavpyohZmqoArAp= d2vdE%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/a60dce1b-8ad7-3d07-8232-92a811b3bb62%40gmail.com. --------------zasRaybQiTZAbHsav2uhOGz3 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 th= e 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/S0956796820000= 076
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 cannot 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-equ= ality.

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 l= ocks, 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 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?
>

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 Homo= topyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Ho= motopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%= 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/a60dce1b-8ad7-3d07-8232-92a811b3bb62%40gmail.com.=
--------------zasRaybQiTZAbHsav2uhOGz3--