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=-0.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,MIME_HTML_ONLY, MIME_HTML_ONLY_MULTI,MPART_ALT_DIFF,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 32588 invoked from network); 1 Dec 2022 15:55:07 -0000 Received: from mail-lf1-x13f.google.com (2a00:1450:4864:20::13f) by inbox.vuxu.org with ESMTPUTF8; 1 Dec 2022 15:55:07 -0000 Received: by mail-lf1-x13f.google.com with SMTP id l7-20020a19c207000000b004a471b5cbabsf968654lfc.18 for ; Thu, 01 Dec 2022 07:55:07 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669910106; cv=pass; d=google.com; s=arc-20160816; b=tXGz9bcKKUKx4mOUaj/P1kxF0rZ66eC1TJNVzACYraPRfCSBhWE6kX9r+2SwaKQo++ b5NxlfXq1e5XP0PJTf7eOxHBLyCKcHmgKv9+LZBtqbJ/bOJ26UUbl+4VO9PhPBR9l3s+ 0D1qNvZGvdWpBZ/3Md2D8qjFKCcHZnc4cpP89X/sFGTm4m164mKFyCBWmz8ZvKX7B4aJ y+7woxLYVIA8JF+f/AHqL5V/B26emP56iZLJwKY8NP+XY0fucVEuj8FwXH8bgvNT5Rgb fJAx2yIg0T3CjoEEBAugel50zGkc5IUOXQ4l+Fpn7a/iLcXPNdIOLeiZuml6N2LqfNHI NxWw== 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:to:in-reply-to:cc:references :message-id:date:subject:mime-version:from:content-transfer-encoding :feedback-id:sender:dkim-signature; bh=hN+rGk9PxlAF8jq9bSvrbkEDpBbLybDbHjekWRBU5bg=; b=qbFfRVEaKfiNkbERsxcjYgweGPsuuFvm6Is9gHwCgB/6Z8Imd1VYkAOx0YDKx8Vkyi BVTy2wNpbjDCjIeX6fCB7QpGbHe8nE9Hd/gk28/aUMPXawWAe3EQWNbtMLs74rP1ZgnV 1ZJNtt/xSnJ7CJHZZDH1qgTMvk4yJDWku27QNBiBORifLLR46A63rt7dmY7LLRLLPgwZ eO2LaFw00h7VZXR+SSPNtTyx2CO/hg31U8Dv0X2YOCt8V7tBnT4NyO0zDQpvlE0XQZiW 9nOcBis3QDYqvIYHgukq0wAz2PcnoxZ2MQ3O4pYt6J6GRb6G+sIEzLlaN0pLnL0W/VsC 5O0g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=FLSYEgOl; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GqeoA7gt; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 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:to:in-reply-to:cc:references:message-id:date :subject:mime-version:from:content-transfer-encoding:feedback-id :sender:from:to:cc:subject:date:message-id:reply-to; bh=hN+rGk9PxlAF8jq9bSvrbkEDpBbLybDbHjekWRBU5bg=; b=If3DSrPKQOqJW0yaZ0QrmmXYw1qm8hmypcAAgTsCUXKVX4CpmIv+ZxGTBqBoa17u4p 5M3hWNwajwL8z0xHIHVbxna1WtAyrOCJO0a60S6Jsf975xt7qsLCB1PgiQ8zO+HbKoqF fpOfxrurf7IF+XiJBUmHBOiZ7NkQxT5sL2k9C2rdy5rFfe9vRsEZ/quMWc8z8GuIlm5F gXFy0tbxc+dTyXQ/ti+1C1Q8YBUCMrqLK5ikNPJV0uDDp1yZUXPQywyEGXIWlfSzO0F6 cfrcfy8BwUkFUGWbFmhSMrKESFHr9RCu2aEaCxwnLt0hZcf0ulzt4WjDND49lark95ls R+tw== 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:to:in-reply-to :cc:references:message-id:date:subject:mime-version:from :content-transfer-encoding:feedback-id:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=hN+rGk9PxlAF8jq9bSvrbkEDpBbLybDbHjekWRBU5bg=; b=C5JDPAmQVKdKiSD7DOoQMfQNgwQ5SD/VFwnQsNlZpfNxAvX/AEPOefR5tgV0LuryrO ZYXdozqY5z0zbCClTqCig/Ozqk986hkiHhVWs+I+L8bdrctHmTgUagUGtdI89dIDrETK UXkqcaf33hU5tXWkl/88gXNIuDfiedVB1mD9wzuKA0kqOd+oszMQodan3+weyaTMa2aL m0qbiIYGIQfQyDFt9ZN5w/gyIQJK/8IavCtCKBMzd7lYSCxpXtFm0Z8jz/ljZSnSZqSN UkNLhtkIg+mozryAyUaYJkDWFmvSrkTL2ISujldIf4bI397LtFM9e52YQkurW35p794H xCyQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkW7m49YU9F0qTHkDWVD2fq4gxoRzRwfpQzicV8bWKyRe8EfBR3 I/TCG/QnEEDRj770qF6gQNU= X-Google-Smtp-Source: AA0mqf5+WkuOWCYXgI4Ih2NFLrWoW5J9U/fLLLMWIN4GdrIln51QrFlYoXf5g0FzJ9OPqpj6rvp60g== X-Received: by 2002:a2e:9d50:0:b0:26f:db16:4735 with SMTP id y16-20020a2e9d50000000b0026fdb164735mr21985122ljj.323.1669910105940; Thu, 01 Dec 2022 07:55:05 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:4e8a:0:b0:4b5:3cdf:5a65 with SMTP id o10-20020ac24e8a000000b004b53cdf5a65ls495356lfr.2.-pod-prod-gmail; Thu, 01 Dec 2022 07:55:03 -0800 (PST) X-Received: by 2002:a05:6512:401f:b0:4b4:b78a:ad8a with SMTP id br31-20020a056512401f00b004b4b78aad8amr20817977lfb.249.1669910102940; Thu, 01 Dec 2022 07:55:02 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669910102; cv=none; d=google.com; s=arc-20160816; b=rDueOEopw3Ruts/VF9EJbXM7KinCWaJ0PokhvYB/JoQaRdn+OrDCvCyHjnX4ru32PO FwIKb3fA+6/z9Sm4ENMZDxidfqbyOQDCwaXWiCeA8ET9wEy7qMBwIWR0UX7KtAcuEvKW LAHZL91tGJjYCsUuHxTkqfM2BJTboZ5RrwqqpRSgvZNh9Kp67B3Lfl7jAi6FbWi33M1a 2BF+RvsffXFbOxo2ImxAiXd15jQIaX/AB1UwSjo+LRuwwUe2134JV4SNE3sgFlqAwlfo Ka4dm2F1OFKg+ONAiDpMb3ATXfJuaNv/Kky03ikk5w4bWpp6KZCj3rfhb4YPNyR0iZ2j lL8Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:feedback-id:dkim-signature :dkim-signature; bh=NpK35P/wma4w2FE6/AamqU4X3GEe+tM4iUtZBy4VEME=; b=ywVWF/pgCSvDKmZ+GUXblacw9bX4rDWAWlT0UpQluLDI+UniSKBJUTqVm+wOGVLN6/ uWw2ns0csMWlRso1AYwYfZOLWWaN8CS0zcHDgWcxl55pvb94E1Lu27b8FKVBomc4pq1u n/hBFVdi5A7rWpkZf5CrhG2DI2GigPBLoBWfjcGVBmShQP2GEZz0mKcsNO1806f/+u2b VB8dJZdpNbCvulpjERTUQITqHUoJooDxe9SDWWT23LbutZvAiZY4k8JUjF0uW0RvLOQi E++hXg0NMWZW7d1hdxA1mctnCnnaN/fSf6vMUyoGPWjlZn3chp+yNsaUXGbMyjbSgiLc KiCg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=FLSYEgOl; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GqeoA7gt; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout1-smtp.messagingengine.com (wout1-smtp.messagingengine.com. [64.147.123.24]) by gmr-mx.google.com with ESMTPS id p14-20020a2ea4ce000000b0027760dd5b20si178175ljm.3.2022.12.01.07.55.02 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 01 Dec 2022 07:55:02 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 as permitted sender) client-ip=64.147.123.24; Received: from compute2.internal (compute2.nyi.internal [10.202.2.46]) by mailout.west.internal (Postfix) with ESMTP id 0548A32009BA; Thu, 1 Dec 2022 10:54:59 -0500 (EST) Received: from mailfrontend2 ([10.202.2.163]) by compute2.internal (MEProxy); Thu, 01 Dec 2022 10:55:00 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvhedrtdehgdekfecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenqfhnlhihuchonhgvuchprghrthculdeh uddmnecujfgurheptgfghfggufffkfhfvegjvffosegrjehmrehhtdejnecuhfhrohhmpe flohhnucfuthgvrhhlihhnghcuoehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomheq necuggftrfgrthhtvghrnhepvdejtdelvedvhffhtdettddtueegueffffdtteelkeekhf eggeefffefjeetfeeunecuffhomhgrihhnpeguohhirdhorhhgpdhgohhoghhlvgdrtgho mhenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Thu, 1 Dec 2022 10:54:58 -0500 (EST) Content-Type: multipart/alternative; boundary=Apple-Mail-32B2AB16-C6A9-4E84-9300-0C950C28BDA6 Content-Transfer-Encoding: 7bit From: Jon Sterling Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Thu, 1 Dec 2022 16:54:45 +0100 Message-Id: References: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> Cc: Michael Shulman , Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory In-Reply-To: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> To: Andreas Nuyts X-Mailer: iPhone Mail (20B79) 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=FLSYEgOl; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GqeoA7gt; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 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: , --Apple-Mail-32B2AB16-C6A9-4E84-9300-0C950C28BDA6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 pr= etty 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 i= n the admissible-subst scenario whether the interpretation function respect= s 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@gmai= l.com> wrote:

=EF=BB=BF =20 =20 =20 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/S0956796820000076
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= -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.  I was thinking= of operations and equalities, and annotations are neither of those, but I can see that they're somewhat similar in spirit.  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.  It does sound like we mostly agree.  I wo= uld 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 thir= d 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 Hom= otopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTyp= eTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gm= ail.com.

=20

--
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.co= m/d/msgid/HomotopyTypeTheory/EF8B5670-D703-4EB7-89A8-D25FBE7464B4%40jonmste= rling.com.
--Apple-Mail-32B2AB16-C6A9-4E84-9300-0C950C28BDA6--