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 15529 invoked from network); 1 Dec 2022 18:00:38 -0000 Received: from mail-vs1-xe39.google.com (2607:f8b0:4864:20::e39) by inbox.vuxu.org with ESMTPUTF8; 1 Dec 2022 18:00:38 -0000 Received: by mail-vs1-xe39.google.com with SMTP id k2-20020a676f02000000b003b0ad24798esf1318620vsc.0 for ; Thu, 01 Dec 2022 10:00:38 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669917636; cv=pass; d=google.com; s=arc-20160816; b=ulRIzM45FifNwXA/oikXSNhH2URWu97lESyDKV8olBpfzlqZdfvadjHqOCMfvjf7dI 9SiZwyoz3nINigVoklO+GRBzSmgC2eI9wXbcPkwU1JZm94XLp+DQKivfkg/weD43QgqC ARS5k7AkG76jOytD4XreJibsTNCJVOtKoh9n2xZBZMQvHf3m4uy54WqVQ6UmJ0CWlrpq cuTJPcxUZI4Rb0wv6MdMsTglwrk9uIIT/meHjk4cJk5h4odyIQ1mCcGIWZauppdzQQ4T crbWlA5kgF/eVJVD8eC2Mrsb3XJiX5zfMZIJt/47JATTk6l6+QbXJ1HVzq+du2kxnolz rGEw== 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=8Li1GEI9ve/1H6oYZ3XztPFkVwVpNLUgpvpD3yvBpDU=; b=rQ6xERtBfrc78g8VVA+asIcZboWO+Sy0FSH1Pi9/KBsvJlv/eur14rZOfiJES5O8e4 qWILS6vLF/j0/4h8NeUPGQNymnfdHMBOurlof2C0wIoakpscXvsrclZyaRk/urGGnhcJ 4gqORfL3SOekF9zJh0efWTWuiqeJSDPdqf5ZNHMVLkn2nKTdRFNS2XRMjhWC2BZQR/6v YswCWM8PV3IIf+BNS0My0XyUUtIfy6yhOocE7An+DkgjfbfTjp4sEt+JsOYo6HXwt39I WFtXqC3d7wLmKfrEhqLS5SfTwR1juHwE6QTnln7GYu+k/JHzdxh3loBBD08/4Qi2uE/a KILA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=TvOAkiwW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 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=8Li1GEI9ve/1H6oYZ3XztPFkVwVpNLUgpvpD3yvBpDU=; b=DHTAWaoigvHZ8H/HhaADHzgIwsOhxw6OldjmOFjOJlBsGyFH9lfC0iPnekB0Luc49i UzWsVr8msWwuh9J6SxLzQTUM0Iqhekn0TQfYxRJbO+P+jW9wPOvxJLIozjL7aAzHW8lD HgTP0rCp9Qo/+F842Hq4+LoNuZ3FsXD5FS2tnmlCtTY5d/sAX78SShHzjo7P46HdW78D XYQ0G8zY7HJFPSR2u54wVZ5c8UlFY8xCtCqDw8Qkg6r4Am5jDZu4+5nrHxY76CqM63pD iwn6X9IYk9Gmdh4sM2LeM6vrKGjjX+OXn1x0yZ/ww9liznSKuB3XFMxjNx/FUrGSxdMo bYOQ== 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=8Li1GEI9ve/1H6oYZ3XztPFkVwVpNLUgpvpD3yvBpDU=; b=eEzc+lpoY4tsiZlDJ5c12KjatBfRPNIaO4zENLyt+x/UMtbsNgOmbIflq4yyjwIG/5 S1WgbcTeFG1TfmTa0ioZeM/LcFEyYoM/6Zu53yWYUnrPJ7+msKCYDwdBjNOTICNG+oNk nRJk3ofj5noJt5ruCSsZ2RCpcc9bct7eClEfnGACWdh1Oi6ubCr0y3igZd+1D3LXyV8w NWcvk4QU4edAAzqiAS2neKIyYdh4MdOPwZqXSLH24DefO/dd0/v271RzrrxP4a+3OpHN uhc7hzMBEBKhh0oRaUFMlNLmR32kI7ye+0/zE8+smcIG38i+mYzM07e15+w1BYZLrKkI WmKw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pmhxZ5onE9ubyI9HxDqLyJDP+a7cRuVYZjblOVVek3wvvJTFJ6X xq6k0enQouiKdcSVDWYvxy8= X-Google-Smtp-Source: AA0mqf63tg1jLw1vidz4UppLlB8vPiqnOVYk/cpOHUmKarIhIpqVjuLLn07G2bbvTf5N+1R/q6qpHg== X-Received: by 2002:a05:6102:310f:b0:3ac:a71f:de2d with SMTP id e15-20020a056102310f00b003aca71fde2dmr29399311vsh.1.1669917635981; Thu, 01 Dec 2022 10:00:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:e048:0:b0:3b0:e9d9:3013 with SMTP id n8-20020a67e048000000b003b0e9d93013ls639471vsl.0.-pod-prod-gmail; Thu, 01 Dec 2022 10:00:34 -0800 (PST) X-Received: by 2002:a67:d311:0:b0:3aa:7bcc:3acc with SMTP id a17-20020a67d311000000b003aa7bcc3accmr33023485vsj.15.1669917633995; Thu, 01 Dec 2022 10:00:33 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669917633; cv=none; d=google.com; s=arc-20160816; b=T7+XGKbWqpsvRZwDxtxyTFsQoQI42qx3HAbZNv0kxryHELUuJ3MoYAmOhZtBdHL6+Q F0UKt94MaWM0kkwG0vY+mOi0TSFqSake6Pw1YFOJgv3Ba97IOULEYA3oCuCBrhr1TS9Q ySazGESi2tokND04qQB+YX3vD0nXRo6jDFha1UREitbxJUFSTfLC5jd5aKdO+6Azc7OU b9lcdPAuiNLfNlcavvlQ3/9zCrS8alNcFoiN8gCuCZxF0po27iW4k/CsaNMXgix5IMyP 4w6rBCn60BR7dcw9Tq2CFWb4jd9x52g36UP4hd3+01ez7fk32TL2be1eCYKvg3wOvOrb NRIA== 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=A+077pO1AnfEHhhWUJK0gnsQeuROJHcbbgS1S9alBZ0=; b=tPkZCfRqpbsM+3JdZZb3rLenRyeptghc0NEV9xhWZMSnTCUQnptXmTg7pZyeKGo2oV c8Vd9v/TP5Lh1VzyvuGedpyGT3pGuSmuDTx3CjTXZIZZlhT8/8liKejBnNAhGYKYvQcL LTgqq5Ma5fohzNGu3pbiGHJ1FmbdGDs1LLGjUlppfTqg6N1JnT6HXqFF0I+EShftrs+/ QnSb67bBLLjGvqEbKEjmc5fgwWoSlk54NWpV6ubMJ6D7LmQkWyziphjdUdn4v+E69xsq BL4rQqgIfNKFHT7aTivTUEMBGIqnwwxWTtjBDlYG7GvolhPrP0ql45Ov5k9AqDU3L62d nCTA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=TvOAkiwW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb35.google.com (mail-yb1-xb35.google.com. [2607:f8b0:4864:20::b35]) by gmr-mx.google.com with ESMTPS id u7-20020ab03c47000000b004192f334e13si612956uaw.2.2022.12.01.10.00.33 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 10:00:33 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) client-ip=2607:f8b0:4864:20::b35; Received: by mail-yb1-xb35.google.com with SMTP id 13so2084116ybf.4 for ; Thu, 01 Dec 2022 10:00:33 -0800 (PST) X-Received: by 2002:a25:ed10:0:b0:6d0:5d59:dba1 with SMTP id k16-20020a25ed10000000b006d05d59dba1mr59619648ybh.68.1669917633571; Thu, 01 Dec 2022 10:00: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> <92CA5128-A764-47EA-8ECD-B6931F7EA7AF@jonmsterling.com> <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> In-Reply-To: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> From: Michael Shulman Date: Thu, 1 Dec 2022 10:00:22 -0800 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Andreas Nuyts Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000005a87fe05eec7ff8e" 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=TvOAkiwW; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 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: , --0000000000005a87fe05eec7ff8e Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thu, Dec 1, 2022 at 6:40 AM Andreas Nuyts wrote= : > 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 variable= s > 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 posit= ion where > we currently are and where we want to use the variable. > This is a reasonable point. I do think, however, that tool support is not necessary to evaluate usability. A really usable theory should also be usable informally, as in the HoTT Book and my BFP paper. This is what I have trouble with for locking modal type theories; but it's certainly possible that I could train myself to do it. It certainly takes some mental training to use split-context modal type theories informally too. A more serious and mathematical issue is that MTT requires all modalities to be right adjoints, semantically, because you have to have some operation to interpret the locking functors on contexts. (And FitchTT even requires those left adjoints to themselves be (parametric) right adjoints.) This seems a serious restriction on the kinds of situations we can model. One can argue that the process of interpreting a split-context theory involves building a new category of contexts (some generalized kind of comma category, perhaps) that *does* interpret such context operations, and therefore could also interpret MTT. But we don't have a general theory of this yet. To be precise, given an arbitrary 2-category M of modes, I would like there to be a corresponding instance of a general modal type theory that can be interpreted in any M-shaped diagram of suitable categories, with all the morphisms of M corresponding to syntactic modalities, and not requiring the existence of any additional adjoints in the semantics. The LSR fibrational framework achieves this for simple type theories, but I don't think there is any published framework that achieves it for dependent type theories. Best, Mike --=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/CADYavpzCJLHMmB4ZPCX8Cn0_agLcD5_UZ1KsAkZZ8m0bLqHGKA%40ma= il.gmail.com. --0000000000005a87fe05eec7ff8e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Thu, Dec 1, 2022 = at 6:40 AM Andreas Nuyts <andreasnuyts@gmail.com> wrote:
=20 =20 =20
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&qu= ot;. 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 composit= ion of the locks, i.e. the modality of the position where we currently are and where we want to use the variable.

<= /div>
This is a reasonable point.

I do think, however, that tool support is not necessary to evaluate=20 usability.=C2=A0 A really usable theory should also be usable informally, a= s=20 in the HoTT Book and my BFP paper.=C2=A0 This is what I have trouble with f= or locking modal type theories;=20 but it's certainly possible that I could train myself to do it.=C2=A0 I= t certainly takes some mental training to use split-context modal type theo= ries informally too.

A more serious and mathem= atical issue is that MTT requires all modalities to be right adjoints, sema= ntically, because you have to have some operation to interpret the locking = functors on contexts.=C2=A0 (And FitchTT even requires those left adjoints = to themselves be (parametric) right adjoints.)=C2=A0 This seems a serious r= estriction on the kinds of situations we can model.

One can argue that the process of interpreting a split-context=20 theory involves building a new category of contexts (some generalized=20 kind of comma category, perhaps) that *does* interpret such context=20 operations, and therefore could also interpret MTT.=C2=A0 But we don't = have a general theory of this yet.

To be precise, given= an arbitrary 2-category M of modes, I would like there to be a correspondi= ng instance of a general modal type theory that can be interpreted in any M= -shaped diagram of suitable categories, with all the morphisms of M corresp= onding to syntactic modalities, and not requiring the existence of any addi= tional adjoints in the semantics.=C2=A0 The LSR fibrational framework achie= ves this for simple type theories, but I don't think there is any publi= shed framework that achieves it for dependent type theories.

=
Best,
Mike

--
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/CADYavpzCJLHMmB4ZPCX8Cn0_agLcD5_U= Z1KsAkZZ8m0bLqHGKA%40mail.gmail.com.
--0000000000005a87fe05eec7ff8e--