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 28526 invoked from network); 18 Nov 2022 17:14:56 -0000 Received: from mail-vs1-xe3e.google.com (2607:f8b0:4864:20::e3e) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 17:14:56 -0000 Received: by mail-vs1-xe3e.google.com with SMTP id k2-20020a056102004200b003aa0eb4d8adsf1566524vsp.20 for ; Fri, 18 Nov 2022 09:14:56 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668791694; cv=pass; d=google.com; s=arc-20160816; b=kS282awAjgcYX7eFJ6IU4Lqd50iLaTQmrUUcrtQWhNudmC6QqJPg5B4xLM87VSX2Me CI2q2vd1GSKzX/Zjtsqxx+rCcSKaF3aifbC6trRImmuRGXIQhTWA4YI+3YDWoOBdvhxE pAUH7SAfru34JUBnT/TA851Z09wWeUi0TTF0M8Um4n4t4VmRohg/39bmp8PpS0zM+lzH RkKSQEyMmQJzVaITsWLVTTvn5j3oPeFguxmN9l+CYHU52AzBPhkB4U/DzaKXJ3pcpGIv 5MfaG/kvypLtrWVdac8aQfNzTed1+lJPrSStmfVrE0p6vweWdwRVOCar+0ms+UUuDSQX 885g== 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=+OP0HgCMmfLsU7eU81I+KSWhDjdWHvdCr1XEv42wHio=; b=VmVae8D78iUbQ9itqiyMVblHSY6nP7c0+ywQdFALOGtpMxuAalW3v7BMAhg3X5Rf9Q CRScsgZ+3YFIJV2H99LZDui4aR0Dyp6DWMkpUluS3NS1L7PIBY/tP5urU/fQHFGdYpSc Lu4ZUl2ZsIvAFxP9/gwwbbdmqX0k8ieDFNK9gLWRWSkvNKRHC/Nzz5TnEpSOoAmAPRE1 3ho8GK5rmidAN4r++WFJCtrq7A8H+wBzMVGduUywHJUPdUTniiu/tinDQ++e2T/ABxHw OQpC6giraVKXpAYdM/MwLneYUeDQNmlhhYZP/dKLFf4MUJuS+aSHSURTF0ZtPHQ5F0ZV uttA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=NUeVKaT5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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=+OP0HgCMmfLsU7eU81I+KSWhDjdWHvdCr1XEv42wHio=; b=h8yPhqsRV4d6y3K1rFu8g8jzSVR78eW21yuNOsbLoHB29vkEAuvsTNTZr5fId+rTrj LUoeWSxmGdlJVFavxBZrAIxkdnhu1MkN2I3ubHWYOTVKwVREymgTs6Sew+9n5DTeOGss 8UhWdxB4Cp8zipigbjoYbnWObbQajvHgelWXjadfo8CBSOPh68J6Zcyj1FID0IPH5jq1 +jtJe2OhBxuTiUblHdrVxsKjrCTv+a+WaC6mtxHGQHlV1wbqrbHZOSH8DD8U42/011G+ pPQrjZRAGKrSGPRdod3DPWWTegURKdxLSyJipGjqeplYvnAuQ37fz7P4rSKg3alFEDl0 VmJA== 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=+OP0HgCMmfLsU7eU81I+KSWhDjdWHvdCr1XEv42wHio=; b=W8XuATSMQeKNisddw3UNf8XWS9aPWEmgAuPkh0GXqgqUKytUtWUCKyqxSZqy06jQOP dtlZVnPzxIFCeJKuaIpTW3B9RnTzcxVe1tG/v3sd25WzIRrZZu5dHAYV6h2dhLUbsfiF FWIZl5sJ8kY7JQQXNrCTspHSn/lI4gQDEDlaD68sR7NoIlUlKTCRnmWrT1OVwIVEZyTe WB+V3CdGEKB+7bIyY2FfjdfzLUWAo9AnQAxpPt51nvUqd/OJHO8W3UjKhStWFUNr+VIk LMgnPbUk1wfT5cfLYPzSEpo1MET6Th6tlZfZ9dqX2XFsd9rLcpMLuCDM1ThAnQ1h88HD HYXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pnWfg8WJPcl4P5ZAUu/WBYUsvRBPbIIiX7KIg7GU1sQ/qpXNs0W oy4wLX6+6AcsJXM5RzQ8RQs= X-Google-Smtp-Source: AA0mqf6taslqb4bnN/JtdbsM9lXgYAkrM2e77+x6hI9RV/l8bMig4YgyUdD7c/rqK48IFTj97/9b3Q== X-Received: by 2002:a67:f6d8:0:b0:3a7:1137:247b with SMTP id v24-20020a67f6d8000000b003a71137247bmr4738701vso.54.1668791694090; Fri, 18 Nov 2022 09:14:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:1c08:0:b0:3b4:4e41:3c89 with SMTP id c8-20020a1f1c08000000b003b44e413c89ls647713vkc.6.-pod-prod-gmail; Fri, 18 Nov 2022 09:14:52 -0800 (PST) X-Received: by 2002:a1f:5c55:0:b0:3b7:6786:18fe with SMTP id q82-20020a1f5c55000000b003b7678618femr4401819vkb.20.1668791692730; Fri, 18 Nov 2022 09:14:52 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668791692; cv=none; d=google.com; s=arc-20160816; b=UHzGBXTe5iXwMAm1NP9bHVwgYHDpbePBcS/bN2d2xKZyfkB2NyO/EgEzxnT8H51CTO /ljXuRQD9ss93BAhEDdIfiXpFQXWtKacBi6ycgoVOPy6px9/jXyCnGYAqrulWfGPe0vA F3daU0o3xD3aTiIxTv1g6jafgl4kXXwTjGa1uN+Vrm9r14paGYBqwG9+qqorDmPIaxZq 8vTTxBq0OclahuDSauO+C6S7gg/5F2jCZOw0VZVavOXmfkYiIM9+EDTu1IsIlAtZQ6n+ N3Ng2FN6uu8kn5ZZXBZ2md84HpAAyCOKA8MjTRk1h4WFkrfg4bF/yHZdpm18HzsHo5E+ FxRg== 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=bOyH7X9vwSAwZEvE2D58Nl0546bq3tMWCxAGZw4BpFs=; b=GM2WFdqMy33xDWBor0uvfYzgJ3wq0p+4KUFBa6/Gkx1bm8ZIcYd+SVqthA1aLf9BEc +Z+Vw4XwdQSEW29Z6tl7P4TKWEMwO0KZ0S95VMJlaOc3+noUWf5OKrtq1jk9OUNPaPo2 O0d8yhUrg7LY+UG9lIdlyEVMhWmqZ43aPkZvni2gkNeTUisIfPmm0fN4tTnx2oGzADpK n8/Hg1dgOvLePRMru0jQzfoOhXobgtaW87AjzWAYI+aUs9Z4uWg202/ejznUCff5ttFp 5vxNyj93JI3kmBRfexjhXOKcDMNskVOy0fW4yvx4kqGc5MzPMu40b/JE0Dr82Xv/tm23 ql0A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=NUeVKaT5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-yb1-xb31.google.com (mail-yb1-xb31.google.com. [2607:f8b0:4864:20::b31]) by gmr-mx.google.com with ESMTPS id s207-20020a1f90d8000000b003bbd00e2339si228610vkd.4.2022.11.18.09.14.52 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 18 Nov 2022 09:14:52 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 as permitted sender) client-ip=2607:f8b0:4864:20::b31; Received: by mail-yb1-xb31.google.com with SMTP id f201so6350278yba.12 for ; Fri, 18 Nov 2022 09:14:52 -0800 (PST) X-Received: by 2002:a25:ed10:0:b0:6d0:5d59:dba1 with SMTP id k16-20020a25ed10000000b006d05d59dba1mr6814938ybh.68.1668791692320; Fri, 18 Nov 2022 09:14:52 -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> In-Reply-To: <92CA5128-A764-47EA-8ECD-B6931F7EA7AF@jonmsterling.com> From: Michael Shulman Date: Fri, 18 Nov 2022 09:14:39 -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="000000000000067b7905edc1d834" 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=NUeVKaT5; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b31 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: , --000000000000067b7905edc1d834 Content-Type: text/plain; charset="UTF-8" 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 wrote: > On 18 Nov 2022, at 11:56, Michael Shulman wrote: > > > 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? > > > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BGp%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com. --000000000000067b7905edc1d834 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
That's an interesting question.=C2=A0 I was thinking o= f operations and equalities, and annotations are neither of those, but I ca= n 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> w= rote:
On 18 Nov = 2022, at 11:56, Michael Shulman wrote:

> Thanks.=C2=A0 It does sound like we mostly agree.=C2=A0 I would probab= ly argue that
> even for type theories in development, where we don't yet know tha= t full
> definitional equality is decidable -- or intrinsically ill-behaved typ= e
> 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 rela= tively 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 wi= th you that there is a need for terminology to describe the situation you m= ention, 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, i= n many versions of syntax (like bidirectional ones) we can choose to drop c= ertain annotations because they will be available as part of the flow of in= formation in the elaboration algorithm. Would these be an example of the ph= enomenon you are describing, or is it something different?

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= ://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2vdE%2BG= p%2BsVczpw95TDy9xvDnMStMj%3DZQ%40mail.gmail.com.
--000000000000067b7905edc1d834--