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, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 16189 invoked from network); 18 Nov 2022 06:20:16 -0000 Received: from mail-oa1-x38.google.com (2001:4860:4864:20::38) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 06:20:16 -0000 Received: by mail-oa1-x38.google.com with SMTP id 586e51a60fabf-13c6efaa955sf1921434fac.11 for ; Thu, 17 Nov 2022 22:20:16 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668752414; cv=pass; d=google.com; s=arc-20160816; b=Lx7vBSTdBAHH2ZEN+uMrngqt+w9oFYyt6n3pzbiBc6TarnI5Qboa7EZE1jkFZb8m68 D1YuhTHKL6pCyI4SoH7OkMFTsC/JMwuwwrXYpqUWXxC5im0kJBUcTho40JbkaCP43FFN 3hlN9tu3W2JIWPFfxV0mdXSoLPbZCRzk3GyvixZ01cEtP6zHnzYnbBRljXO5vA4x/Zql AM9sU72dWc4DMw86aLo4T8YKWaLTp5UwgFrBwUhFkJ6GFuuTRIa0KeFexHmLZL3/2dbT 98bBlitaBvvoTvDr3Z1QKx00JMuq39l4VhJkdwKVwM9appfKcXrO/ymTOcJUEBkPUViv tM9Q== 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:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=DkoMRpyUZvQSaFf4DZu0aDpJuFqIuQx6AvNFQLIrhm8=; b=iExpl9HYDVLsYb4ZDxfV2Gw6a8eV+jU3lQKkY93BlojiUikvKPqMD3LJSXXTyHqPr6 oNxDbNdsJEipFvYFKceBdshTVaBfl3NSYGgzCIRryJzxC6OqBE3KpjFRPS+M6/0O1ghL /Fq1HIXkyeRlJxcz76NcjQnZ9IDfzC4j8DLlzZbLl+feM8C2dKsDur1+P/19FsYiWu3s oFV5FEQVaLrpZFLVxZVD3SS9nwxiP1rj5UGnNbdSpHIeg9S/AlJGddyZEr+HRamhaQDB hife4HkFgSbu/i6roV/hCvKdsUWaPbno4UCAyDBHqyYcfMn9Ah8JY3Q7C8OXtj1uO+RM Xlfg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=SG4WzlSs; spf=pass (google.com: domain of tom.hirschowitz@gmail.com designates 2607:f8b0:4864:20::1033 as permitted sender) smtp.mailfrom=tom.hirschowitz@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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=DkoMRpyUZvQSaFf4DZu0aDpJuFqIuQx6AvNFQLIrhm8=; b=DBLmMVT3y6ktoh2auWpeC+DcwQPgvPMpDuV8OOff14KM/7PEAgmTJ1PRac1iCESpT8 UFp5p3C/dUBKnGEYqFjIh2NLx7TH1o9hV6RooyU6BRHvLnxvoZlbNGR0jSz1GKeIaQgO g4JH0lXAuakmqtcZpEiH2RumsTIxNDJ6Z51Tj4BVm/LNi4ahCgbOhM9unRj4qJwywu2z fTfWOKwjQj5ZHXoGcSwYjjSpi7Hv18TIBXsKD6NYfa0Nt/ogHthb6eMyR3YgBQmJZ97i FpmJzqOWTWb2cruAHO60e0qVcqoYUUQfXCaypVq4Lmz9OGib6PJSLwfaorLgnoaVQRBx OLxw== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=DkoMRpyUZvQSaFf4DZu0aDpJuFqIuQx6AvNFQLIrhm8=; b=lEXbmQrQRiOvXOR3LOHv/R6yQfOQyBCzXNm6cQu445dIr4IIShAwkYOa+J19f5DDXz l/7sV4OVqB/1jtVml2nWtp4/Qkgh/HS6TrXQgT0QtV94QRKxU7vwcAABDs09qy12c3jD h0ORV0qRZ/uC58foCzvgcf7ixGOMG+n4AIADFoqCT15xWIHOBmsDhbBtckot4UmgpAGB A7Q+cz9MjDpeR8uht773ZkRWfFdY3ye/iFAg9zB9Z3ILMBw5Pke2N9v9zLRF0Bj7MY8I dH+67ySS7piQ/jgkJ1+UoursmjplXlAGfBWarAmP9SvScEWb0P0pD4ctn0YAgj6zQONV DPAg== 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: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=DkoMRpyUZvQSaFf4DZu0aDpJuFqIuQx6AvNFQLIrhm8=; b=Bm9VVYJlmYtr1joHkB0EgfSKJHD8uRGoXMAMqKRH3j+OUKuyhaX5Fy6wEdIcmEQiSv SoSMMxwtxuhzbpYNIMcJhsXWhhdgTAPAOXKGd3atbya+UlOHBTwL0QzdORYt9wGQhvJk lPmrsOf94zpOhSYu6TLAHokzfrj7vQNC7HP/Cn+OAZFT83vcQoPIYekoHTSjL6yckLnQ B65q345bioO9/fv3fHJBZXOOrXlygww2t7x6DJpPKAGmDQ8AijotFYfwa7VsJPY0kUsR SHK9YmRck24tz+hmO8+o3AARoSaM8BbHvL4eKWKRwDPBRAEMF+DBMcmHN9aZaf9umwC+ Z6fQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5plLTOz2PhQGeWT3d7vIVOaL2FQ4DHMt69OgK95CHiS35Yul5XdU XklwNUp84MdBnaS+7D5/6nM= X-Google-Smtp-Source: AA0mqf4eUA3zfPePyZ6wYoeFAt5u5M7Ua1Be4j71NW1JZGGvO00AhXcL8v/uGswNHlX5DGJeK65Kag== X-Received: by 2002:a05:6808:11c9:b0:35a:9331:8cbb with SMTP id p9-20020a05680811c900b0035a93318cbbmr2756902oiv.201.1668752413998; Thu, 17 Nov 2022 22:20:13 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:5301:b0:13d:21ad:3b97 with SMTP id j1-20020a056870530100b0013d21ad3b97ls1494042oan.4.-pod-prod-gmail; Thu, 17 Nov 2022 22:20:12 -0800 (PST) X-Received: by 2002:a05:6870:4987:b0:13b:9f17:5f89 with SMTP id ho7-20020a056870498700b0013b9f175f89mr6382778oab.166.1668752412698; Thu, 17 Nov 2022 22:20:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668752412; cv=none; d=google.com; s=arc-20160816; b=Dz93qnaGZiiDw7PetMYuhLVjqhW6Xbbs/UCAFiTHBvGYLrIpkcijdtyjWkJ0CTAoer O9YIcSD1IPLWHIMT3yCCjuVK7Zm6hnGZyKw5+P6kQFMB+ov6910hrskXZP5SP426LP0m AAHcPBm92FtjPiR/AHX92pTULbWvk7f0uKhMvQdNb5eitCySBpECHvXSRNLTeUGo7k/u uUwdQD8lekauh/HENBWj9q5c/7z9Iyvae740IWzzEe8QIoTr7H0wjehwLeShKyYE0Cv7 L5mZZ+9PJCd8ZstT7C6N+TdP/Ek/TW/H0l8G/9O11/0UV/ONwtyh6+wTFEPQkDvDJDH4 X9Vg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=RAbDRhl0Lby1t7MWPw+QgKsunKK44bma13msjq3ZQFE=; b=w1QgbVm5GncFSDRlbCeitB4+TAaMWcP15cO6e2vlc0E89yyJjTbGuvpIq2osWw4dKQ joWTqr8EFw4UC40IX9f4jqtTxLRax0Ijpj3zd4ho2wWWWW/nuRRE/ZNMqgyoKrzsMUuz KsVyNYoVNu5LH0LmI45sXtwG+pf9L65+qG5tWLUmHFe6rCtvb4cHn3JH82d8saqPLWe4 iKWv+RN3OaQxwGCeiHenb+tkRHn2PfDTy8LcRrKL7cT742Yk8Uk0GCZdrqnFMPdisjT2 uR9rCLyVyupMZ0l8K+4NFamUAdg02i0u4o4Di/2zLuU8Q29IIaBKmE90+6RX9G0Wot3L kTpg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=SG4WzlSs; spf=pass (google.com: domain of tom.hirschowitz@gmail.com designates 2607:f8b0:4864:20::1033 as permitted sender) smtp.mailfrom=tom.hirschowitz@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pj1-x1033.google.com (mail-pj1-x1033.google.com. [2607:f8b0:4864:20::1033]) by gmr-mx.google.com with ESMTPS id k7-20020a4ae287000000b00476ba3a3008si177927oot.1.2022.11.17.22.20.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 17 Nov 2022 22:20:12 -0800 (PST) Received-SPF: pass (google.com: domain of tom.hirschowitz@gmail.com designates 2607:f8b0:4864:20::1033 as permitted sender) client-ip=2607:f8b0:4864:20::1033; Received: by mail-pj1-x1033.google.com with SMTP id t17so2972864pjo.3 for ; Thu, 17 Nov 2022 22:20:12 -0800 (PST) X-Received: by 2002:a17:902:e5d2:b0:188:f4ca:97b1 with SMTP id u18-20020a170902e5d200b00188f4ca97b1mr4828562plf.139.1668752411871; Thu, 17 Nov 2022 22:20:11 -0800 (PST) MIME-Version: 1.0 References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> In-Reply-To: From: Tom Hirschowitz Date: Fri, 18 Nov 2022 07:19:59 +0100 Message-ID: Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000ba4ddd05edb8b24b" X-Original-Sender: tom.hirschowitz@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=SG4WzlSs; spf=pass (google.com: domain of tom.hirschowitz@gmail.com designates 2607:f8b0:4864:20::1033 as permitted sender) smtp.mailfrom=tom.hirschowitz@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: , --000000000000ba4ddd05edb8b24b Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Only valid for simply-typed languages, so not (yet) contradicting Jon's claim: admissibility of substitution is important in the development of Howe's method for proving that applicative bisimilarity is a congruence. Essentially, the reason is that it provides a simpler induction principle. This is implicit in my recent work with Peio Borthelle and Ambroise Lafont on a categorical framework for Howe's method (e.g., [1]), used as motivation for "A unified treatment of structural definitions on syntax..." [2], and explicitly used (and extended to operations other than substitution) in ongoing work on a generalisation of [1]. More generally, I suspect that it is useful in programming language theory, where people tend to work with extrinsic presentations. [1] https://hal.archives-ouvertes.fr/hal-02966439v6 [2] https://hal.archives-ouvertes.fr/hal-03633933 Le ven. 18 nov. 2022 =C3=A0 03:35, Michael Shulman a =C3=A9crit : > As far as the mathematical study of type theories and their models goes, > that may be true. But I believe that when talking about the way type > theories are used in practice, either on paper or in a proof assistant, > there is still a difference. > > Suppose I am teaching a calculus class, and I define f(x) =3D x^2 + 1 and= I > want to evaluate f(3). I don't write > > f(3) =3D (x^2+1)[3/x] =3D (x^2)[3/x] + 1[3/x] =3D 3^2 + 1 =3D 9 + 1 =3D 1= 0. > > Instead, I jump right to f(3) =3D 3^2+1, because substitution is an > operation that happens immediately in my head, not a computational step > analogous to 3^2 =3D 9. Similarly, the user of a proof assistant never t= ypes > or sees substitution as part of the syntax; it is an operation *on* synta= x > that happens behind the scenes. > > Yes, this is a property of a particular *presentation* of a free structur= e > rather than a property of the structure itself, but that doesn't > intrinsically make it unimportant. Groups and group presentations are bo= th > important. Maybe you want to say that "a type theory" refers to the free > structure rather than its presentation, but choosing to use words in that > way doesn't by itself make "presentations of type theories" (or whatever > you call them) less important. Maybe you want to define an "admissible > rule" to be a property that holds in the syntax but fails in some actual > models; but that doesn't make "rules that hold in all models and can be > made to hold in a particular presentation of the free model without being > given explicitly as generating operations/equalities" (or whatever you ca= ll > them) less important. > > I do agree that Andrej's formulation sounds backwards. In practice (in m= y > experience) one doesn't write the rules down first and then try to figure > out what kind of substitution is admissible. Instead one decides what th= e > substitution rule should be, and *then* (hopefully) works out a way of > presenting the syntax to make that substitution rule admissible. This is > particularly tricky for modal type theories, where the categorically > "obvious" rules do not admit substitution, and leads to the introduction = of > split contexts as used in the BFP paper. I have trouble imagining how I > could have written that paper if I had been forced to write explicit > substitutions everywhere. Thorsten and Jon, do you maintain that all the > work that's gone into figuring out ways to present modal type theories wi= th > "admissible substitution" is meaningless? > > On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling wrote= : > >> Indeed, I echo Thorsten's comment =E2=80=94 to put it another way, even = being >> able to tell whether these rules are derivable or only admissible is lik= e >> knowing what an angel's favorite TV show is (in other words, a form of >> knowledge that cannot be applied toward anything by human beings). At le= ast >> for structural type theory, there is nothing worth saying that cannot be >> phrased in a way that does not depend on whether structural rules are >> admissible or derivable. It may be that admissiblity of structural rules >> starts to play a role in substructural type theory, however, but this is >> not my area of expertise. >> >> 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. Absent such a notion= of >> model and evidence that it is at all compelling/useful, we would have to >> conclude that worrying about admissibility vs. derivability of structura= l >> rules in the official presentation of type theory is fundementally >> misguided. >> >> On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory >> wrote: >> >> That depends on what presentation of Type Theory you are using. Your >> remarks apply to the extrinsic approach from the last millennium. More >> recent presentation of Type Theory built in substitution and weakening a= nd >> use an intrinsic approach which avoids talking about preterms you don=E2= =80=99t >> really care about. >> >> >> >> https://dl.acm.org/doi/10.1145/2837614.2837638 >> >> >> >> Cheers, >> >> Thorsten >> >> >> >> *From:* homotopytypetheory@googlegroups.com < >> homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.co= m >> >> *Date:* Tuesday, 15 November 2022 at 22:39 >> *To:* Homotopy Type Theory >> *Subject:* Re: [HoTT] Question about the formal rules of cohesive >> homotopy type theory >> >> > Does this also include the structural rules of type theory such as th= e >> substitution and weakening rules? >> >> I would just like to point out that substutition and weakening typically >> are not part of the rules. They are shown to be admissible. In this spir= it, >> the question should have been: what is the precise version of substituti= on >> and weakening (which is a special case of substitution) that is admissib= le >> in cohesive type theory? >> >> With kind regards, >> >> Andrej >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/D66F4584-A005-4F69-= 8E75-E976E0FF9957%40andrej.com >> . >> >> This message and any attachment are intended solely for the addressee >> and may contain confidential information. If you have received this >> message in error, please contact the sender and delete the email and >> attachment. >> >> Any views or opinions expressed by the author of this email do not >> necessarily reflect the views of the University of Nottingham. Email >> communications with the University of Nottingham may be monitored >> where permitted by law. >> >> >> >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB786979CA94= 519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com >> >> . >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-= A444-13FA43EDD1CF%40jonmsterling.com >> >> . >> > -- > 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/CADYavpxcTpvy6%2BBS%= 2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%40mail.gmail.com > > . > --=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/CAHE5TSNXhvH4QH08fW1mOk8Qn7sGPCfTzRN37rfhMxeQEqyVqA%40ma= il.gmail.com. --000000000000ba4ddd05edb8b24b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Only valid for simply-typed languages, so not (yet) contra= dicting Jon's claim: admissibility of substitution is important in the = development of Howe's method for proving that applicative bisimilarity = is a congruence. Essentially, the reason is that it provides a simpler indu= ction principle. This is implicit in my recent work with Peio Borthelle and= Ambroise Lafont on a categorical framework for Howe's method (e.g., [1= ]), used as motivation for "A unified treatment of structural definiti= ons on syntax..." [2], and explicitly used (and extended to operations= other than substitution) in ongoing work on a generalisation of [1].=C2=A0=

More generally, I suspect that it is useful in prog= ramming language theory, where people tend to work with extrinsic presentat= ions.


Le=C2=A0ven. 18 = nov. 2022 =C3=A0=C2=A003:35, Michael Shulman <shulman@sandiego.edu> a =C3=A9crit=C2=A0:
As far= as the mathematical study of type theories and their models goes, that may= be true.=C2=A0 But I believe that when talking about the way type theories= are used in practice, either on paper or in a proof assistant, there is st= ill a difference.

Suppose I am teaching a calculus= class, and I define f(x) =3D x^2 + 1 and I want to evaluate f(3).=C2=A0 I = don't write

f(3) =3D (x^2+1)[3/x] =3D (x^2)[3/= x] + 1[3/x] =3D 3^2 + 1 =3D 9=C2=A0+ 1 =3D 10.

Ins= tead, I jump right to f(3) =3D 3^2+1, because substitution is an operation = that happens immediately in my head, not a computational step analogous to = 3^2 =3D 9.=C2=A0 Similarly, the user of a proof assistant never types or se= es substitution as part of the syntax; it is an operation *on* syntax that = happens behind the scenes.

Yes, this is a prop= erty of a particular *presentation* of a free structure rather than a prope= rty of the structure itself, but that doesn't intrinsically make it uni= mportant.=C2=A0 Groups and group presentations are both important.=C2=A0 Ma= ybe you want to say that "a type theory" refers to the free struc= ture rather than its presentation, but choosing to use words in that way do= esn't by itself make "presentations of type theories" (or wha= tever you call them) less important.=C2=A0 Maybe you want to define an &quo= t;admissible rule" to be a property that holds in the syntax but fails= in some actual models; but that doesn't make "rules that hold in = all models and can be made to hold in a particular presentation of the free= model without being given explicitly as generating operations/equalities&q= uot; (or whatever you call them) less important.

I do agree that Andrej's formulation sounds backwards.=C2=A0 In prac= tice (in my experience) one doesn't write the rules down first and then= try to figure out what kind of substitution is admissible.=C2=A0 Instead o= ne decides what the substitution rule should be, and *then* (hopefully) wor= ks out a way of presenting the syntax to make that substitution rule admiss= ible.=C2=A0 This is particularly tricky for modal type theories, where the = categorically "obvious" rules do not admit substitution, and lead= s to the introduction of split contexts as used in the BFP paper.=C2=A0 I h= ave trouble imagining how I could have written that paper if I had been for= ced to write explicit substitutions everywhere.=C2=A0 Thorsten and Jon, do = you maintain that all the work that's gone into figuring out ways to pr= esent modal type theories with "admissible substitution" is meani= ngless?

On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com= > wrote:
<= /u>

Indeed, I echo Thorsten's comment =E2=80=94 to put it= another way, even being able to tell whether these rules are derivable or = only admissible is like knowing what an angel's favorite TV show is (in= other words, a form of knowledge that cannot be applied toward anything by= human beings). At least for structural type theory, there is nothing worth= saying that cannot be phrased in a way that does not depend on whether str= uctural rules are admissible or derivable. It may be that admissiblity of s= tructural rules starts to play a role in substructural type theory, however= , but this is not my area of expertise.

It is revealing that nobody has proposed a notion of **mode= l** of type theory in which the admissible structural rules do not hold; th= is would be the necessary form taken by any evidence for the thesis that it= is important for structural rules to not be derivable. Absent such a notio= n of model and evidence that it is at all compelling/useful, we would have = to conclude that worrying about admissibility vs. derivability of structura= l rules in the official presentation of type theory is fundementally misgui= ded.


On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' = via Homotopy Type Theory wrote:

That depends on what presentation of Type Theo= ry you are using. Your remarks apply to the extrinsic approach from the las= t millennium. More recent presentation of Type Theory built in substitution= and weakening and use an intrinsic approach which avoids talking about pre= terms you don=E2=80=99t really care about.

=C2=A0

https://dl.acm.org/doi/10.1145/2837614.28376= 38

=C2=A0

Cheers,

Thorsten

=C2=A0

From: <= span style=3D"font-size:12pt;color:black">homotopytypetheory@googlegroups.com= <homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.com <andrej.= bauer@andrej.com>
Date: Tuesday, 15 November 2022 at 22:39
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com&g= t;
Subject: Re: [HoTT] Question about the formal rules of cohesive homo= topy type theory

>=C2=A0 Does this also= include the structural rules of type theory such as the substitution and w= eakening rules?

I would just like to point out that substutition and weakening typically ar= e not part of the rules. They are shown to be admissible. In this spirit, t= he question should have been: what is the precise version of substitution a= nd weakening (which is a special case of substitution) that is admissible i= n cohesive type theory?

With kind regards,

Andrej

--
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/HomotopyTypeTheor= y/D66F4584-A005-4F69-8E75-E976E0FF9957%40andrej.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.
--
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= /PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlo= ok.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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-= 13FA43EDD1CF%40jonmsterling.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/msgid/HomotopyTypeTheory/CADYavp= xcTpvy6%2BBS%2B-5yjOjVFkdXFHdmCX0U3Qre2J6t8Lfh_g%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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAHE5TSNXhvH4QH08fW1mOk8Qn7sGPCfT= zRN37rfhMxeQEqyVqA%40mail.gmail.com.
--000000000000ba4ddd05edb8b24b--