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 23227 invoked from network); 1 Dec 2022 14:40:15 -0000 Received: from mail-ed1-x539.google.com (2a00:1450:4864:20::539) by inbox.vuxu.org with ESMTPUTF8; 1 Dec 2022 14:40:15 -0000 Received: by mail-ed1-x539.google.com with SMTP id f17-20020a056402355100b00466481256f6sf998428edd.19 for ; Thu, 01 Dec 2022 06:40:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1669905614; cv=pass; d=google.com; s=arc-20160816; b=Rf8g5gdKuDBUbh+XnvJ5cxze7x6b9fEZQoiiu2pX1w8+o3OdxnemOYe4IRE+IOUiON X03TsiVx9hdI2UN9bqDr563OEQCwuSd63u7j8P4eIAeCaUsEb+ZUZx1Icg1V7ObNRFxj FIsoecJ146biPe9wyYLCUtW6sNV+ZpCNplO+YRieS14kgpgIgQEVcEGWjFc+iCDaa1wm YLI21saIhIiWtJAkTfweLNiPUEO6ptKfztMsnXoCvmKzvKETyRgaiWsR46j5l098wNWH UipY7L8QAOQuyysJJtnR+u6fMXpNxoqLqB795hri9CwzIEMVtmTI+etvXd88YfHPQR4p SBbw== 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=5JkId3jBeUsR3Db4SxuTE40NqPPDf2QFZKUq5kfVVig=; b=AUbAXeehfa1IvFu79SrYhbKd7XDYDv/ENZXs3NxxSBwqZIH3uuN0XVB8tOQkdlnPvC 8/rq+9RTnQE7BrpMR3aXFIBLmUvFbMDa5BDFl5Xm+z1TRgtvZ0YvYlfJd3onuitjkoki P+9y1h5EP77oN9FqLZL6qrrDv33QgcncYNIcdzAWnjsfAvTrptapvWSA0E1Ew7TmGSlH 1+aiOIjZvP2dn/zftXnOjfnyisfvRo38sJXUQ+ILVcZV7S0FnwhQggHG2tjW2jERvO35 8h8ytckUbctII2YriO8sGIv78xUS1kH5iQDk4jH1fVw+JqqcOBYiqvUc+fkCTVA/pKBN hnbQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=qCBvji07; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::52e 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=5JkId3jBeUsR3Db4SxuTE40NqPPDf2QFZKUq5kfVVig=; b=ICH/H43ef978DFZOacBgdaasjiJlc2kPBBpL6k6oAfJfGahMATg50/qo4yZm9a0e9J VhpEfifLTx4g12XgCzUg+gl8WGFK8s1lVHBX/lYbC/63JyIDpPnye2WM3i8qbptJdIMa Wc84HH4KKtjVdMK6nxpvrADh/WLTALGr/jfM7a0WF/oC0vQl38aoSbX8rpzC4m/EpIht lcFjDUoAj+jFSIhYEe8Mb82NyJRG76cO5WPiP/ix7Qw2kZfxC09ufeKvwjlenSSnEMLj sTXh0FXaHikmcZSJrCnv5oHxGiC69mqrtIFtTdxXri4rhD3IImQljF7JDf7Xs0NpSy5/ 2JnQ== 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=5JkId3jBeUsR3Db4SxuTE40NqPPDf2QFZKUq5kfVVig=; b=XcHO9HS0RAYPgyEW+ND7BUJWa3tnva+v28zMsi0spzSEa1yEav2Hh+1RbTORCGGtVn t+ARDEGqFwCd7TfQ54cfzqG2058Jy4GVfyJNzDTsUSkQP/H78Bql2YWROfRwEhBtIwDZ 2ze1N/yN/b/mA9pEYGCyxB9NDUCLu47d6s18YnNwAEn+DYz07WCooaQaSPumK4vATMGL s0ypoo31B4QJQ9BaQ8iafGiSja8ALpu7T17pEKaf7YbyeobJhLdPnPk6L89dP8dnc/nf MTWY/WybIlCDtl2DZVEGQLgjhpQqG7k2+pdsF9VyZaexBWM7V+sNylG25oT0y++Ek98h AUTg== 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=5JkId3jBeUsR3Db4SxuTE40NqPPDf2QFZKUq5kfVVig=; b=BDi6KKnW6l7bNbeiijOw9dM4QpC75QilDq5Ps4XmK2Clz9jt9Eduf4V4L9Kg/8mwAB wVX3THAUybnBXPVSkyfzO1F+hg0ke8VM/0koEMWkkNE+cNU1vpNVSDzHlooK0fksk6pt zydp6IpUhlylMQ+PQgJfYQQkubuqh7dmjZW7A7sMHasx2UXsu+GSPJnn9r3rq7G6NkxE hf7r+10W7Q/6TicCFKQlawsPqGEyRboSwkn33sRR8PvnRrmvm6gO5rFxZz3HXYBBkEH5 wSMdgm+1syNbbUhATjW73VprdAnAg6XBM8CnSbJ/jL5LaQn0DRZnr2vaJOhPorwW6RKJ QECg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkIffpJ3nLr3RCqFvXl9P2F7Jn0kXEcLYaLK1ukatp8AXA4p5kD aGsw5IpS3FNGWhRngvTyiX8= X-Google-Smtp-Source: AA0mqf7ey4n2q5kZjxZmubINo17H0ti9voNBH36EMU4wxkBm3yhuqdjTWN+wj6gRAXhFsjwA501k+g== X-Received: by 2002:a17:906:c251:b0:7be:88ed:3d4d with SMTP id bl17-20020a170906c25100b007be88ed3d4dmr21300312ejb.268.1669905613671; Thu, 01 Dec 2022 06:40:13 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:6858:b0:78d:e7b8:d105 with SMTP id a24-20020a170906685800b0078de7b8d105ls1134558ejs.8.-pod-prod-gmail; Thu, 01 Dec 2022 06:40:11 -0800 (PST) X-Received: by 2002:a17:906:369b:b0:78d:34a:f466 with SMTP id a27-20020a170906369b00b0078d034af466mr56349579ejc.162.1669905611347; Thu, 01 Dec 2022 06:40:11 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669905611; cv=none; d=google.com; s=arc-20160816; b=pR6Xsr32iNGzdODZvW+W3g61OY4hA0vudySOI/XAo73lGJRLkWFPAM39+HJ64XHn0l U7AVQD7NhIgEi00jxBIVELVreH1KbmMiJ6qt3zdCFpKD77wNufi1RQ/ABW2xED1zOWfV 5SZYQqrw2lPxKeIe5Cgl9yQT4JVvIWlZ1auTE42oqpJEhdLe7SPYjUtV+iHiPdV+F7JH yEcaJJ0kzZ2cKgENb8DHVeF85O+zSGQgAaFQp/vl7GrHQN3z17wRuf+qFe0JVraetcYc zfyXrliud7A9KJZgOGBriv+xevekakBRbYktXbxS2M/imcUWIXkT6mg32qt4WwS/vnAV csYw== 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=7L2wHRxS8Psy8lTb2sXbFOaxB33KuEsUVRvnOpb3n8Q=; b=cdVQWGTfcT38/Yq2AWcptJlfiUPbZNzrconH2UkA347PAh+ATrzR7Tqlh2/Hj1XtdF fWHLE+av7ybnmtiy9yKAcnxPiJWRccivfP4TYC6xBIy6XswTPBY8vnfzd2EPHl7Nx6Lr EeastR26HXvrSAGGx4lnqPyJ4pkVkaXo5kEco7l377KIxyCu1WZdnoo4tnRBrUaVn9E/ hzh8d975cw5ANqPc4trihcdx1Evc4EORI4jgTp0ncsQ+SX2gaX//dUyM7JFAupzzoz8D EO/e03/Z30v8b6oAOrzkHgt+jdUO3TnEXw2w7nHRw5vfja9AuVPlP8sfu6ZfBpbjfCw5 HEvg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=qCBvji07; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::52e as permitted sender) smtp.mailfrom=andreasnuyts@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52e.google.com (mail-ed1-x52e.google.com. [2a00:1450:4864:20::52e]) by gmr-mx.google.com with ESMTPS id w20-20020a170907271400b007ba8b8a416fsi246232ejk.2.2022.12.01.06.40.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 06:40:11 -0800 (PST) Received-SPF: pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::52e as permitted sender) client-ip=2a00:1450:4864:20::52e; Received: by mail-ed1-x52e.google.com with SMTP id s5so2591881edc.12 for ; Thu, 01 Dec 2022 06:40:11 -0800 (PST) X-Received: by 2002:a50:fe0e:0:b0:46a:cb3b:d117 with SMTP id f14-20020a50fe0e000000b0046acb3bd117mr26843682edt.103.1669905610886; Thu, 01 Dec 2022 06:40:10 -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 q10-20020a056402032a00b004587f9d3ce8sm1783022edw.56.2022.12.01.06.40.09 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 01 Dec 2022 06:40:10 -0800 (PST) Content-Type: multipart/alternative; boundary="------------SqwzVGtD3lKHe80iSjP04nmc" Message-ID: <4d352fc9-c4d3-2304-1510-17cd653513a8@gmail.com> Date: Thu, 1 Dec 2022 15:40:09 +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: Michael Shulman , Jon Sterling Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory 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> 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=qCBvji07; spf=pass (google.com: domain of andreasnuyts@gmail.com designates 2a00:1450:4864:20::52e 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. --------------SqwzVGtD3lKHe80iSjP04nmc Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable 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=20 models, because the language without substitution is in general not=20 really the language of interest. An example of a model disrespecting=20 substitution is the prettyprinter by Allais, Atkey, Chapman, McBride &=20 McKinna (2021): https://doi.org/10.1017/S0956796820000076 Indeed, substitution is no longer possible after prettyprinting, but all=20 other language constructs are supported. Note that if a substitution=20 operation is unavailable in a model, then the =CE=B2-rule for functions=20 cannot even be stated in that model, let alone asked to hold. So a model=20 that fails to have a substitution operation necessarily also disrespects=20 the equational theory of a language with such a =CE=B2-rule. Prettyprinting= =20 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 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 system=20 with crisp and non-crisp variables: such a system is implemented by=20 Andrea in agda-flat. At the last Agda meeting, we have been=20 investigating how mature the current modality system in Agda is and how=20 feasible it is to support full MTT. One thing we observed is that - of=20 all the parallel modality systems implemented in Agda - the cohesive one=20 (of which only the flat and non-flat modalities are exposed to the user)=20 is actually the one that adheres to the discipline of MTT (by having a=20 third "squash" modality that effectively removes variables from the=20 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 general=20 multimode systems with left division, I observed at some point that the=20 left division of all modalities in the context actually never needs to=20 be computed and can thus be regarded as a context /constructor/, rather=20 than as an operation (i.e. admissibility of left division was not=20 required, in none of the senses of the word mentioned so far). Modal=20 Agda does use an eagerly computed left division. These systems with left=20 division are very 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 user.=20 A lock simply means "we've moved into a modal subterm". The position of=20 the lock in the context is important in order to keep track of which=20 variables were introduced before/after moving into that modal subterm.=20 When using a variable, you just need to make sure that the variable's=20 modal annotation is =E2=89=A4 the composition of the locks, i.e. the modali= ty of=20 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=20 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 difficu= lt=20 > to imagine how to define this phenomenon precisely in a way that would=20 > 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.=C2=A0 It does sound like we mostly agree.=C2=A0 I would pro= bably > 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 > > --=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, send=20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpyohZmqoArApd2= vdE%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/4d352fc9-c4d3-2304-1510-17cd653513a8%40gmail.com. --------------SqwzVGtD3lKHe80iSjP04nmc Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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.=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@jo= nmsterling.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 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.=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 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 HomotopyTy= peTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/Homotopy= TypeTheory/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/4d352fc9-c4d3-2304-1510-17cd653513a8%40gmail.com.=
--------------SqwzVGtD3lKHe80iSjP04nmc--