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 22389 invoked from network); 18 Nov 2022 16:23:18 -0000 Received: from mail-lj1-x23d.google.com (2a00:1450:4864:20::23d) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 16:23:18 -0000 Received: by mail-lj1-x23d.google.com with SMTP id t9-20020a2e7809000000b00277524ccb02sf1915034ljc.1 for ; Fri, 18 Nov 2022 08:23:18 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668788595; cv=pass; d=google.com; s=arc-20160816; b=rRKizjt4+mXeXAhqgb8SOK57MAI1djqPxsa6ar+3y5leXCMKRCGM3MmiNfIBD6Wa04 PUqBc7dgYMlDOjEI/gm08rRrVG7RfDJT2s5EHCsiskBpVWae4x+KZIEWH4bvasRmKmxo uitYGhVOjxNvp/9OrmA+C/4QRYqelQvR7yJQmtrwjYREQYCkm6+lVHfftXebBvPJeBM1 XAY7ZGKoDXF83AHZ5gDDSnSfF00CEB7T6TZgerjyTwKWgs2ASQX/IjfLit5Yrv9vgsg9 dWug+6tnwE3jIq0GUP2tQHsB4pYQ2FBN77s3ThwzHJCH6pITYc4O3mkh6iCQ1AU7oFq5 NL7w== 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:embedded-html :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:sender :dkim-signature; bh=9tZtIWeUY0C54peWMKhMGhhCZsKI8a3l5TLkAjjo1EY=; b=HSnB9PLOeE8X7i4uH8XpUH9I9NCDDIRIRQFsGqsPtdE6Lurof/WX9AOs/lrs5JLpoG 55sti87kWtSIEv5gboONB5XkphnEWC2FLuTQILAnRXIR2/p1tNC1mYHlnWtOILs/fXZK bwo55QsNrK8TYRMwjN2QJeJMH8znJ4E+FElqM+v1VByljQK5C/yWn2lVfehivq9rXmRs iIZxUfka5LA5hjNngwPp/FJEnW+NUK9IvoiXskXfEmHLU3LRxBzd8iRhxPhv48756W41 3oIrIrwsc9mS/QGpaiCL/oN7vcbdJKYs00GbQP4AkmA6ap85p9SuifXNM4ymR8dOAp8J uBng== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=j3XnhJ1L; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=H3o45RwD; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 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:embedded-html:content-transfer-encoding :mime-version:references:in-reply-to:message-id:date:subject:cc:to :from:feedback-id:sender:from:to:cc:subject:date:message-id:reply-to; bh=9tZtIWeUY0C54peWMKhMGhhCZsKI8a3l5TLkAjjo1EY=; b=LV4FnHhjMhXaoZTQWCcoVfxGWvV+PXFtAJL2vxE97Er8Co5CmELW6zGReLuvif1EOz xTZxO1oipiI2xbIcjP14++ojJweileorJSZNAandJkOwysiaLwq80GOOuDYKGPgAAt2e xK1ALDcM7dFFizFxUzu+qOKYdqT9WZevC6H64Ngx+2bRkJGhsppDy6zQfmaeizqDFl7n QqNTc+uHTMaRLhkAQ57uc8HeDaUiWIbc5/7k2F+Flj2HwNHPQX7nSV4NVM4CSJI83w7H 5KtsyMOB664WDyzbBla5bNwPgG8buod7B1TrKZcVbrW3x1FUFrgEhFyEUrP+0q2v84+X MANQ== 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:embedded-html :content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:feedback-id:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=9tZtIWeUY0C54peWMKhMGhhCZsKI8a3l5TLkAjjo1EY=; b=cTdGIVtSrINJmqYYzyF9sdN52wGVJXM8VHauA6eQtaE4ZZKYuEneYw7P3w7B9elOHf FU5H/ToRfbk+Y9Xsm7AE+3HeqkhGIj7roeyG3Fxgwvlf2ji8qI9aFPoqLqxDiguIGvf3 CG0yD/UTk5d6VygmW87dz1wtOLUuql+vHgNw4tijuYuBAJYcUCjYyyHPUTk2zGSr3D5+ UaMBXKp/oLi83tgFocdEme4JO8+9tB9RH1/hB4gCB0eMu+PzjX9v1LnNxJeb0xV1QLLe 5+CS9QddXOVkMFDW5za0d1hkR8DfujtjgItx7TWrk+f6rRgJHgpKkzKdAtFZrCBUlohk Fy5A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pkI39TwjN2VNShnuRG/fNTytDdGYwH0icnBSLh/dHwT2FuMYCuQ y17kfEUDnMSwizeYQas2FS0= X-Google-Smtp-Source: AA0mqf6n5z+LYxqCBsTnK1Jfo4sAi3fUxrA+UO3pxVg96VnHcxPYmjejUgSDm6KvOXCsJ0vv7GpcEQ== X-Received: by 2002:ac2:5935:0:b0:499:d6f9:5b3d with SMTP id v21-20020ac25935000000b00499d6f95b3dmr2571736lfi.69.1668788595601; Fri, 18 Nov 2022 08:23:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:a54a:0:b0:26e:76e9:3567 with SMTP id e10-20020a2ea54a000000b0026e76e93567ls1025083ljn.11.-pod-prod-gmail; Fri, 18 Nov 2022 08:23:12 -0800 (PST) X-Received: by 2002:a2e:8685:0:b0:277:13a5:83ce with SMTP id l5-20020a2e8685000000b0027713a583cemr2494545lji.426.1668788592879; Fri, 18 Nov 2022 08:23:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668788592; cv=none; d=google.com; s=arc-20160816; b=sHZTOR7vey9G4FXTDuQbpbwYCWS0aifIzfNwdu+8VBBfBhEaGWIw5qXC+fDhctIjcd oRcRG+Yw+KvjOK5kvHvjMzVEPn1xOz6tLMiDPrv8oIzLBEQQkREA0g/5Q9CA2rdQjrP1 Nz1R1TZWVRNVkVi4jP8OhjPPIvmczj2ReWZeImk0ie2kEaMQ42EN+oLY+QbNWNUpsGpX QuAQvWByfNoRMcB19vgHo8Wzev9cU21ItwLysPf0tqn7kA5zKEH6ymEAfLjIlKF2vaCa 2qZ0UlQ0OAXBJNLaZRZwRz5kavXG6uCwMt5wwGWp7IsR/iu5PkjzV6++pqlwzVP7lv+L BwCQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=embedded-html:content-transfer-encoding:mime-version:references :in-reply-to:message-id:date:subject:cc:to:from:feedback-id :dkim-signature:dkim-signature; bh=ixHUR0XTEx1tJLipsPL4aDrpKLQIyVmLd7nV14NJCXA=; b=v9yYly9x1XrLMHH/oCKhCidsuNnW264uJwsuKQt4V34DJj2cFl4cph0iLJxaP0qcuI V63/qN6PNVX1hd+wnBelghp6LJMHqI5GAPzPZaKAz6zRBOAFQYg1H2av1zoTEZBIbHBv J/lEl8prYDyNgBvkC5CI47Nw0L+oXu31LhHNJEtG3NiRacHlKcZZUEgX+wcTYtvmAz3N 2Ao6NgorQud6YIdc1h79CtbknjLb7fi7qxGLMEEPjjxdjNSnwtWx4n//uwW4l2kIfV4V nypJVtvZ2DHEJWGxHyMGJbe9nbswCehDZt6MaisdS2ORoG5oboNIu58RC1XpGaywWYBg mCKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=j3XnhJ1L; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=H3o45RwD; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout2-smtp.messagingengine.com (wout2-smtp.messagingengine.com. [64.147.123.25]) by gmr-mx.google.com with ESMTPS id f16-20020a05651c02d000b0027760dd5b20si152833ljo.3.2022.11.18.08.23.12 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 08:23:12 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 as permitted sender) client-ip=64.147.123.25; Received: from compute2.internal (compute2.nyi.internal [10.202.2.46]) by mailout.west.internal (Postfix) with ESMTP id F3D23320079B; Fri, 18 Nov 2022 11:23:09 -0500 (EST) Received: from mailfrontend2 ([10.202.2.163]) by compute2.internal (MEProxy); Fri, 18 Nov 2022 11:23:10 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgdekkecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenuc fjughrpefhvfevufffoffkjghfgggtgfesrgekmherredtjeenucfhrhhomheplfhonhcu ufhtvghrlhhinhhguceojhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucggtf frrghtthgvrhhnpeejhffftdeugfevueelleevfeegueefkeeugeevgeffteelfeduvedv vdeigfejhfenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhroh hmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 18 Nov 2022 11:23:09 -0500 (EST) From: Jon Sterling To: Michael Shulman Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Fri, 18 Nov 2022 11:22:56 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <4D4B5058-E159-4139-8713-979EC5E1D3BA@jonmsterling.com> In-Reply-To: References: MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=_MailMate_7626D3E2-4925-49FA-8EFC-2F985C557654_=" Content-Transfer-Encoding: 8bit Embedded-HTML: [{"plain":[50,1153],"uuid":"1F96436F-829E-4C0B-A75C-F4C445F5F26C"}] 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=j3XnhJ1L; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=H3o45RwD; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.25 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: , --=_MailMate_7626D3E2-4925-49FA-8EFC-2F985C557654_= Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable On 18 Nov 2022, at 11:16, Michael Shulman wrote: > On Fri, Nov 18, 2022 at 2:59 AM Jon Sterling =20 > wrote: > >> Hi Mike, thanks for your comments =E2=80=94 regarding modal type theory,= =20 >> please >> note that there are state of the art general modal type theories that=20 >> do >> not employ admissible substitution! MTT is one of them. >> > > Split-context modal type theories can also be presented without=20 > admissible > substitutions. Making substitutions explicit is easy; it's making=20 > them > admissible that's hard. And as far as I understand it, MTT does=20 > satisfy > the primary desideratum when making substitutions admissible, namely=20 > that > all rules have a fully general context in their conclusion. > > MTT is also not equivalent to split-context theories, and IMHO is less > pleasant to work with in practice. I believe there should be some way=20 > to > combine the ideas of the two theories. > > By the way, in the followup paper "Modalities and parametric adjoints"=20 > by > Gratzer, Cavallo, Kavvos, Guatto, and Birkedal (three of whom are also > authors of the MTT paper) we read "The admissibility of substitution=20 > is a > central property of type theory, and indeed of all logic" (section=20 > IB). The real reason it is central is that making substitution admissible=20 forces you to figure out the equational theory of substitutions (as I=20 said), not the other way around. You are free to consult the other=20 authors of that paper, and I guarantee to you that they will confirm my=20 analysis. Admissibility seems to have been cargo-culted, as people=20 forgot the reason why it was important in the first place. It is important to recall that the first admissible rule was *cut* in=20 Gentzen's analysis of sequent calculus, but Gentzen's cut-free sequent=20 calculus is eliminating not only substitution but also all computational=20 redexes simultaneously (this is due to the way that sequent calculus is=20 arranged). This kind of admissibility is much more useful than mere=20 admissibility of substitution, because it gives a normal-forms=20 presentation, which (unlike mere admissible substitution) actually has a=20 ton of practical applications (not just deciding equivalence, but also=20 proof search, etc.). So I would characterize my viewpoint as an=20 essentially orthodox one, though the language we use to say these things=20 in 2022 is very different from what was available in the 1930s. --=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/4D4B5058-E159-4139-8713-979EC5E1D3BA%40jonmsterling.com. --=_MailMate_7626D3E2-4925-49FA-8EFC-2F985C557654_= Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

On 18 Nov 2022, at 11:16, Michae= l Shulman wrote:

The real reason it is central is that making substitution a= dmissible forces you to figure out the equational theory of substitutions (= as I said), not the other way around. You are free to consult the other aut= hors of that paper, and I guarantee to you that they will confirm my analys= is. Admissibility seems to have been cargo-culted, as people forgot the rea= son why it was important in the first place.

It is important to recall that the first admissible rule wa= s *cut* in Gentzen's analysis of sequent calculus, but Gentzen's cut-free s= equent calculus is eliminating not only substitution but also all computati= onal redexes simultaneously (this is due to the way that sequent calculus i= s arranged). This kind of admissibility is much more useful than mere admis= sibility of substitution, because it gives a normal-forms presentation, whi= ch (unlike mere admissible substitution) actually has a ton of practical ap= plications (not just deciding equivalence, but also proof search, etc.). S= o I would characterize my viewpoint as an essentially orthodox one, though = the language we use to say these things in 2022 is very different from what= was available in the 1930s.

--
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/4D4B5058-E159-4139-8713-979EC5E1D3BA%40jonmste= rling.com.
--=_MailMate_7626D3E2-4925-49FA-8EFC-2F985C557654_=--