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=-0.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,MIME_HTML_ONLY, MIME_HTML_ONLY_MULTI,MPART_ALT_DIFF,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 15774 invoked from network); 18 Nov 2022 10:59:12 -0000 Received: from mail-pg1-x53e.google.com (2607:f8b0:4864:20::53e) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 10:59:12 -0000 Received: by mail-pg1-x53e.google.com with SMTP id h185-20020a636cc2000000b0046fc6e0065dsf2943487pgc.5 for ; Fri, 18 Nov 2022 02:59:12 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668769150; cv=pass; d=google.com; s=arc-20160816; b=Uz6+uxfx/yjg2TSm3RhbUZVke+XxwngB6ilMho+72k69fbWJ0pj+60ds5O0hPAl6qc 5M4nC7ihxNZkvtnFWTRtM8U0ZT0qCvS9exPDKAVbUOz7IolI/H0qNlCQPusMye6+d1BL CMIXhZkLnywjQQ0ZzSCCg058o+k5HzFnjQjUsKUojOBAegr11uuBqfOjh2O6wYZV35M6 4azUqamilj4WuATj24l0e5dHYuJ8DFZR12JYf1LH80ATe7TQHru21D0pxxTMbT/DqNyD W3vDAcc+O5ytuAxOJWwX5gjMsYeZe3URxn+h1mvhzKjriCbyaH96dYBg14flZi2VTBqS QDQQ== 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:in-reply-to:cc:references :message-id:date:subject:mime-version:from:content-transfer-encoding :feedback-id:sender:dkim-signature; bh=RqaEBnjTZ9em4lVCwEdELTxadcVj/6CB1c2LTYONGGQ=; b=lJhDvGy/RXa1LXYJDGhV7VlzirDeFXFa9zTFOXnP58yvvwCz1jePoXGyOjtKU+bNlA 19n5nBJHvyCOTlIiAkqAGMWlZznM29GaSOdf6LFzpmer3tvSNYttFLUb5oJSKJSX73wu fn4BkY5kw5ZvtzyfHJKxIykwNh3JJwFh/TV+oXWdtgO4I5OOKxvrhXGH+7l3SrXjeTTt Qe3W9yIjoQsUhkLRSdFA0Tl2bGX3EM8ASkP6PeQZLA/YVZ5tlkjMG2zSDl8axMidDCw1 ZOJt5PoOC4jmH9zrW2vCUphZGdCmfha+mZB4fHyZFA/7Mk1Yd5S91lVskitRDqTbVIhp JuRg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=ixOKys8r; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GfHnjIZ5; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.28 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:to:in-reply-to:cc:references:message-id:date :subject:mime-version:from:content-transfer-encoding:feedback-id :sender:from:to:cc:subject:date:message-id:reply-to; bh=RqaEBnjTZ9em4lVCwEdELTxadcVj/6CB1c2LTYONGGQ=; b=i6rwCR00YBQQdu9K1sr7pPzXn1VR9qiD0WWWPcHzoRBVZdCQZwGKv8crkVQmprXi7h D67HB7EZLEIm9Pi1Xx6HlU5AQT+fWxW/rZCyQ0x/pXEwcXJaLBIpGOWZCu9HfMxVqVld 54XMF2OiDXAzV7XxDN9bOdABWju5LkeQ/lUG3jDrybjQCE+BvzR6kh/UNxvFiZG40E33 9i+7kFHhu098QLNXAuRNUS9shs1/nKarTml78K48+mn7Dtm7CxgsTDZSY7//rja+Rfvx NFwZ7cWxz8uQR4u3JoBewEqFURQxK7RZG01BPMR4qBYADmV/XIRybvLGvSmAJggyLn7W gz9w== 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:in-reply-to :cc:references:message-id:date:subject:mime-version:from :content-transfer-encoding:feedback-id:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=RqaEBnjTZ9em4lVCwEdELTxadcVj/6CB1c2LTYONGGQ=; b=gkDp2gkN9EnBhhSnLo0rwFVWrq1/88E1bRB4ALdGmu5KKUX1/pWxcuQa8uiasGJa1W WOknaC8D7+EvpTryjk5GtpR8QALZ+IWCD0cHtzh2VXAGlvtSVWuQypdQ4xvtdMQYNbtY /v2wwQEBvTBO9p6KJ6v0RYBhzP0+EAG4fMqRBge73PctleKiUTQEK1Ii1AVSdvBW71jq odSvihvcRZ+GoYbG8N79U9yguusJTceZF9Ymme1pz7eMX/6hrm2Q5BJFa2jxtdAGOCwq Xg5TMmfa2iiAnec08X9mjP+pOc8OeFJn1CflHYcqjKfDJPNVkEYj2VM2au32+dZaATV2 dj/w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pnf4Lms1hplY2msWta8Hg26pUEmjqVKESsHMf/vty8eyI/qnZ2o T5Lhu+TKQnqpNYty2h3Hu7k= X-Google-Smtp-Source: AA0mqf4tFcb0wwoX20K/2OJeWBfH/ZFdvUG09aLIOR4KiLz5tHzCEr4J+82tzf0Le6AIVKxA4Kx3kw== X-Received: by 2002:a17:902:ccc7:b0:17d:8a77:518f with SMTP id z7-20020a170902ccc700b0017d8a77518fmr7098276ple.22.1668769149200; Fri, 18 Nov 2022 02:59:09 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:1816:0:b0:56c:1251:19d with SMTP id 22-20020a621816000000b0056c1251019dls2463939pfy.0.-pod-prod-gmail; Fri, 18 Nov 2022 02:59:07 -0800 (PST) X-Received: by 2002:a62:2587:0:b0:56c:bfe:1cd7 with SMTP id l129-20020a622587000000b0056c0bfe1cd7mr7253364pfl.83.1668769147077; Fri, 18 Nov 2022 02:59:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668769147; cv=none; d=google.com; s=arc-20160816; b=RWyh1IH3KJf3PmPdseI+6QzlqX61xbECxsxkk4VlTmq8wRyas1s8mPfR+/hRChTKLz 0fwu5TsCA+2uDd5XI8q5mzTFUMD1bahH7DlJ6DooZT6XacfyVO0lwQp0b+Dkws1+yV3u 7+bKUtmsubZYeiSupoPFjkZXy+84XXuHqw3pthkPPhjBeVAvLM8nWu3Y8J0CgaIgUARS 8/FVOUdvCe7JFe22KzBkN+KM6oG0Yi/jUUHd3ZGzRtdcu4SaQlrTCof6nwHpb/IpO2mD w+J9bXXqqkZr9Bp0ErFSVP7heYtZBrqKC+HK9koeyEEO9OANWlLltiVK7jXWOfiSeAuE SToA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:feedback-id:dkim-signature :dkim-signature; bh=14fcPQkxX2Ik/sv43oLTq7xzsgKGal61iuEScjcJSPw=; b=oJ+OdGS6thtRSQYNeB8jCpSkVgB6vCvB+2kOoRWloj0lIcb93w7b1DXKPDhqmFiG9w 3wzA7Ie7HzVDHyaT6BUjNt7xaFbsnCCYsMS0oY0qMNW8tD9UkGoUPQC2XaxSPJSRJyBK 0Bhs+a+ITf9N0N3K62zucEDKdh+58fRbsemJOhcfzeprhun3HykrIJ/dk2BwAdGgP+p+ /ybnUAkGFebNKKi2skWtrQLQbc8NPvLDYxGOcyo07yHmlP/TFscaAug50PFeyThKpH56 cv7nISykOCohUqSoMoQczXb7EOUDbpS5TROPWYra/JzHaE+wz2I+PL9WgZ0ZSdNbmzH2 l9HQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=ixOKys8r; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GfHnjIZ5; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.28 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from out4-smtp.messagingengine.com (out4-smtp.messagingengine.com. [66.111.4.28]) by gmr-mx.google.com with ESMTPS id lp17-20020a17090b4a9100b00213352256f5si204653pjb.3.2022.11.18.02.59.06 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 18 Nov 2022 02:59:06 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.28 as permitted sender) client-ip=66.111.4.28; Received: from compute2.internal (compute2.nyi.internal [10.202.2.46]) by mailout.nyi.internal (Postfix) with ESMTP id 031685C0569; Fri, 18 Nov 2022 05:59:06 -0500 (EST) Received: from mailfrontend2 ([10.202.2.163]) by compute2.internal (MEProxy); Fri, 18 Nov 2022 05:59:06 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrhedtgddvvdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenqfhnlhihuchonhgvuchprghrthculdeh uddmnecujfgurheptgfghfggufffkfhfvegjvffosegrjehmrehhtdejnecuhfhrohhmpe flohhnucfuthgvrhhlihhnghcuoehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomheq necuggftrfgrthhtvghrnhepvdelgeefueduhedthfffteduudeutdetleduffefheffke efleegjeehkeektdelnecuffhomhgrihhnpegrtghmrdhorhhgpdhgohhoghhlvgdrtgho mhenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Fri, 18 Nov 2022 05:59:05 -0500 (EST) Content-Type: multipart/alternative; boundary=Apple-Mail-6BBA1771-808F-4CAA-A99A-AD471B096FE2 Content-Transfer-Encoding: 7bit From: Jon Sterling Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Fri, 18 Nov 2022 05:58:54 -0500 Message-Id: References: Cc: Thorsten Altenkirch , "andrej.bauer" , Homotopy Type Theory In-Reply-To: To: Michael Shulman X-Mailer: iPhone Mail (20B79) 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=ixOKys8r; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=GfHnjIZ5; spf=pass (google.com: domain of jon@jonmsterling.com designates 66.111.4.28 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: , --Apple-Mail-6BBA1771-808F-4CAA-A99A-AD471B096FE2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Mike, thanks for your comments =E2=80=94 regarding modal type theory, p= lease note that there are state of the art general modal type theories that= do not employ admissible substitution! MTT is one of them.  

So what was the impact of the sear= ch for admissible substitution in the end? The point was absolutely not =E2= =80=9Cto make it admissible because admissibility is important=E2=80=9D but= rather to discover what the correct equational rules of substitution are i= n the presence of difficult modal constructs.  The equational theory o= f substitution in this situation (particularly, how to commute substitution= s past the modal forms) is the hard part, and it was this that was the real= topic of the study of substitution in modal type theory. This is equally p= ertinent in the admissible and derivable styles, and the difference between= the latter is somewhat less important.

On Nov 17, 2022, at 9:35 PM, Michael Shulman <shulman@s= andiego.edu> wrote:

=
=EF=BB=BF
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 10.

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.  Similar= ly, the user of a proof assistant never types or sees substitution as part = of the syntax; it is an operation *on* syntax that happens behind the scene= s.

Yes, this is a property of a particular *pr= esentation* of a free structure rather than a property of the structure its= elf, but that doesn't intrinsically make it unimportant.  Groups and g= roup presentations are both 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 syn= tax 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/equaliti= es" (or whatever you call them) less important.

I do agree that Andrej's formulation sounds backwards.  In practice = (in my experience) one doesn't write the rules down first and then try to f= igure out what kind of substitution is admissible.  Instead one decide= s what the substitution rule should be, and *then* (hopefully) works out a = way of presenting the syntax to make that substitution rule admissible.&nbs= p; This is particularly tricky for modal type theories, where the categoric= ally "obvious" rules do not admit substitution, and leads to the introducti= on of split contexts as used in the BFP paper.  I have trouble imagini= ng how I could have written that paper if I had been forced to write explic= it substitutions everywhere.  Thorsten and Jon, do you maintain that a= ll the work that's gone into figuring out ways to present modal type theori= es with "admissible substitution" is meaningless?

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

Indeed, I echo Thorsten's comment =E2=80=94 to put it ano= ther 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 w= ords, a form of knowledge that cannot be applied toward anything by human b= eings). At least 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 structura= l rules starts to play a role in substructural type theory, however, but th= is 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 Homo= topy 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.

 

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

 

Cheers,

Thorsten

 

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

>  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 "= 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 "= 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 "= 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.co= m/d/msgid/HomotopyTypeTheory/BCA282F3-9B07-48A3-8E8D-1D110BE2854B%40jonmste= rling.com.
--Apple-Mail-6BBA1771-808F-4CAA-A99A-AD471B096FE2--