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 28750 invoked from network); 17 Nov 2022 13:37:11 -0000 Received: from mail-wr1-x439.google.com (2a00:1450:4864:20::439) by inbox.vuxu.org with ESMTPUTF8; 17 Nov 2022 13:37:11 -0000 Received: by mail-wr1-x439.google.com with SMTP id u13-20020adfa18d000000b00236566b5b40sf707085wru.9 for ; Thu, 17 Nov 2022 05:37:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1668692229; cv=pass; d=google.com; s=arc-20160816; b=oOM81jI6febS6Sqnth66YnetvxHaJSWF5cpgLuHPxS7nVp5xUyOpeWoL2j+nZoUbbl LavAU0n/Tn8/Wy/uB8gdw7aX/jD2UwbJyuASJQxEidEc1HHdjwh9KYlqS6mEPbbdbvBu YEfrB+QsPDS1Z4Rh3f9KPYYT6lIuT8KLUSr8P3Bs0owEzkgHLA7vaOFJVcQMYlh/HnrE rIDn87YNevAB6dUm+boMS5cFJ95ddNdZKsclpw7NLv/hx5z9f8WYjoIuIaaHigZ4LtAc 5E26Nf+O/d/T0gxy7H16pXx9ebkNqbICfzATiYWlES0udmAGNbPnifXHRn+8q5Rv9Fck ZU4A== 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:mime-version :references:in-reply-to:message-id:date:subject:cc:to:from :feedback-id:sender:dkim-signature; bh=AVnrDQVi7qcjocK00zIvMIR3mLtQty7lwUoWHkGcL/s=; b=Ou0B9RxZAMQ1ZTcBDcUeJvMKuet3+D4+NIzvsaDqQ2aZwaYGfYGYyabznfCT0iE4Kj qL01g5NqG/qGOWaBbKeb96+LCTAI7MCrUSfQOOFum5EmCS2mGLbpGMit+7KF1Zg4UP6P sOGE0fPRLACD8W+Q4NnsRYQK5YnWA8XfJ9XHUB/C0r6g+Id/Kcs2eXQ0GeMaA4lighqX dYp6e5xMCRLIDzSosfsvHja1WRB1EU0aTBAJJU9lYhn5/iNBRXKfjH8OZycpGG9Pr2aD j4L+QEh5NdKFArkyIRQCYhOjgjggbot9G4ZNn+r9vh9dD/Yr3Q3um+XBOoEUrhuX+WFu 32lQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=QtASwJly; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=r30NwZCJ; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 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: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=AVnrDQVi7qcjocK00zIvMIR3mLtQty7lwUoWHkGcL/s=; b=E5xfEVtEltzKNmcjT2zADSls6oiJSqdpTcIWxAMbnJiOVsO3pmwEDbu491fBKMrf9V qcMhH8JzkU9zOJPjDSQN1Sx48fABNICn3jIF+J+mz9O1p9vYPI+trlygeyREJ0BoR1yo 86K6yXB/7DMN6fgqXa8Lg/Uhq2xamOsvZGBQV+OmWVNTfiGSwHJVqrJrx1C83NnNiZP2 +9BYoeumBryEoKSS2eDbsU5kgIzqQXTCgkYo98vmU3oApo9IO3k1ZO1hKKxkdhpwwq+e QC0FxGZo2aJ3WK84ge12ka3X2r0UNHm4qVEDcjnYlTyQTbjCWGZtPGMvz7E8kWY8A1ie DQqw== 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 :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=AVnrDQVi7qcjocK00zIvMIR3mLtQty7lwUoWHkGcL/s=; b=asg5vontVG7M072q9ix91ej+Afcgd/YC4wpMmB9kcwUEKj3XPR5B5lSYWq8jJurVbO EVXnyiWOCnCumy8k+eIy4nEt4OrmOX6lXu82x0JHab69qzPG0iqDItEqbL5VZF1zWd2d mlvQHSqm/u0oH915k/iAZJrkpqlzDMbqxEcCqo7gtYflxYiak+6dZOaftrRfS8r4Ersn KE8cloZTiakPc4KR2dQYYyh25PDHY6imDMMJS09q6+4dQEgFVqmaZ2QIJQftt8G61hy2 Sr//FcIri2bxpBGFAOdYmyp+vd1xGA9nJvYjjp+oRzJql+GGCYxdHi3s2Sxp95XehleY AveQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ANoB5pk3JhAsXUar0GS6HwXY6VYYNHfQqYdkAq9AvSDbNOqUKc0jw3r8 G7k51sOrZVi8EviH25itFJM= X-Google-Smtp-Source: AA0mqf5BaUezFDbduXAeoP64a4toNQa/xPWE0Z3eBR3GsyIeejxHhJ2Qyz0bwAvUAt/RWNmR+GJiWA== X-Received: by 2002:adf:ecc8:0:b0:22e:3694:a5c2 with SMTP id s8-20020adfecc8000000b0022e3694a5c2mr1502262wro.656.1668692229633; Thu, 17 Nov 2022 05:37:09 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:234:b0:22c:d34e:768c with SMTP id l20-20020a056000023400b0022cd34e768cls21697wrz.0.-pod-prod-gmail; Thu, 17 Nov 2022 05:37:07 -0800 (PST) X-Received: by 2002:adf:f189:0:b0:241:bc9e:a238 with SMTP id h9-20020adff189000000b00241bc9ea238mr303703wro.558.1668692227333; Thu, 17 Nov 2022 05:37:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1668692227; cv=none; d=google.com; s=arc-20160816; b=SHdiAh6HsYwU4+aUybxGY+w25ViXEFJnR4vszq8QVGvPzm/raKjUs2b7VY8KGbwg/3 0G6GSdsXIwKhDZ/GJ/mUTPJyzhq7P0bW5ZDJa2aUJnJ0DyvUCmn2LEyD+rbpSka9smTY qOepG8xr6Vw8vz0upJfp9UYqOYLk1Kn48RPnc8nYDIqzTU8LXP1aOyiRkXJznCRZYLcf iCGxi9pJkyV4kZBz6f92AfQB7R+2ltJ/CZHhMtzJP8VLmfEuKwhqPW1lEamZk/tzXuqc 5mAUXiLyaPkSMRtq07p1zwIhvIFv6w+if8P0u4zRF4Qmvr+gKwiMnM59e+Er3gb+0unr eTfQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=embedded-html:mime-version:references:in-reply-to:message-id:date :subject:cc:to:from:feedback-id:dkim-signature:dkim-signature; bh=nExSkqttH3zwJmU6msH3mnChr2fVPbvS2RERmo51nlg=; b=s4Ln3JYfZn86DjqK0og5hP+ayUUg+hCTtNgHsd/yidlA5nyr/mK/9wUfa4V7mSuTlO gx1EFILDfbZ7QmX09YxMdIGyYaK+WDYsrXZ7TCSKhe216yu2GDWS9L4iHVwEMHK29tRT 38RE38691ILR5x1oqEgHUCPEaFyT6QcgWbrudF3w9RKs7NgvgLXahnGIz/HbCo6QwItX XtHIx8MjRMrFxTb7IuUmR5CeYcAJd2+jPGJDXrfjH1QOetCffEwaNgsifihtlRjG+8PP OQbOFPxdaxhQMhvZghwFp+ZatolEfQeIHGtzmGfmOHrXJRln0Ob0CkErlkPS9Bg0uHwz 3jNA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jonmsterling.com header.s=fm2 header.b=QtASwJly; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=r30NwZCJ; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 as permitted sender) smtp.mailfrom=jon@jonmsterling.com Received: from wout1-smtp.messagingengine.com (wout1-smtp.messagingengine.com. [64.147.123.24]) by gmr-mx.google.com with ESMTPS id f187-20020a1c38c4000000b003cf567afb1fsi285044wma.3.2022.11.17.05.37.06 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 17 Nov 2022 05:37:06 -0800 (PST) Received-SPF: pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 as permitted sender) client-ip=64.147.123.24; Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id A0EAD3200CAF; Thu, 17 Nov 2022 08:37:04 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute3.internal (MEProxy); Thu, 17 Nov 2022 08:37:04 -0500 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvgedrgeekgdehfecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefhvfevufffoffkjghfgggt segrtdhmreertdejnecuhfhrohhmpeflohhnucfuthgvrhhlihhnghcuoehjohhnsehjoh hnmhhsthgvrhhlihhnghdrtghomheqnecuggftrfgrthhtvghrnhephfeuudeugfdvheef gfehjefgkeevjeegvdeuieffueduffegteffheelueeihfevnecuffhomhgrihhnpegrtg hmrdhorhhgpdhgohhoghhlvgdrtghomhenucevlhhushhtvghrufhiiigvpedtnecurfgr rhgrmhepmhgrihhlfhhrohhmpehjohhnsehjohhnmhhsthgvrhhlihhnghdrtghomh X-ME-Proxy: Feedback-ID: if544409e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Thu, 17 Nov 2022 08:37:03 -0500 (EST) From: Jon Sterling To: Thorsten Altenkirch Cc: "andrej.bauer" , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Date: Thu, 17 Nov 2022 08:36:51 -0500 X-Mailer: MailMate (1.14r5895) Message-ID: <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> In-Reply-To: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="=_MailMate_97B3481D-8A14-48C9-A8BB-515DF280F7FB_=" Embedded-HTML: [{"plain":[1205,2492],"uuid":"746399E4-CD4D-4947-AF1C-855B0419A4B5"}] 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=QtASwJly; dkim=pass header.i=@messagingengine.com header.s=fm1 header.b=r30NwZCJ; spf=pass (google.com: domain of jon@jonmsterling.com designates 64.147.123.24 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_97B3481D-8A14-48C9-A8BB-515DF280F7FB_= Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Indeed, I echo Thorsten's comment =E2=80=94 to put it another way, even bei= ng=20 able to tell whether these rules are derivable or only admissible is=20 like knowing what an angel's favorite TV show is (in other words, a form=20 of knowledge that cannot be applied toward anything by human beings). At=20 least for structural type theory, there is nothing worth saying that=20 cannot be phrased in a way that does not depend on whether structural=20 rules are admissible or derivable. It may be that admissiblity of=20 structural rules starts to play a role in substructural type theory,=20 however, but this is not my area of expertise. It is revealing that nobody has proposed a notion of **model** of type=20 theory in which the admissible structural rules do not hold; this would=20 be the necessary form taken by any evidence for the thesis that it is=20 important for structural rules to not be derivable. Absent such a notion=20 of model and evidence that it is at all compelling/useful, we would have=20 to conclude that worrying about admissibility vs. derivability of=20 structural rules in the official presentation of type theory is=20 fundementally misguided. On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory=20 wrote: > That depends on what presentation of Type Theory you are using. Your=20 > remarks apply to the extrinsic approach from the last millennium. More=20 > recent presentation of Type Theory built in substitution and weakening=20 > and use an intrinsic approach which avoids talking about preterms you=20 > don=E2=80=99t really care about. > > https://dl.acm.org/doi/10.1145/2837614.2837638 > > Cheers, > Thorsten > > From: homotopytypetheory@googlegroups.com=20 > on behalf of=20 > andrej.bauer@andrej.com > Date: Tuesday, 15 November 2022 at 22:39 > To: Homotopy Type Theory > Subject: Re: [HoTT] Question about the formal rules of cohesive=20 > homotopy type theory >> Does this also include the structural rules of type theory such as=20 >> the substitution and weakening rules? > > I would just like to point out that substutition and weakening=20 > typically are not part of the rules. They are shown to be admissible.=20 > In this spirit, the question should have been: what is the precise=20 > version of substitution and weakening (which is a special case of=20 > substitution) that is admissible in cohesive type theory? > > With kind regards, > > Andrej > > -- > 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/D66F4584-A005-4F69-8= E75-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. > > > > > --=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/PAXPR06MB786979CA945= 19BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.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/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com. --=_MailMate_97B3481D-8A14-48C9-A8BB-515DF280F7FB_= Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Indeed, I echo Thorsten's commen= t =E2=80=94 to put it another way, even being able to tell whether these ru= les are derivable or only admissible is like knowing what an angel's favori= te TV show is (in other words, a form of knowledge that cannot be applied t= oward 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 depe= nd on whether structural rules are admissible or derivable. It may be that = admissiblity of structural rules starts to play a role in substructural typ= e 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 Homo= topy Type Theory wrote:

That depe= nds on what presentation of Type Theory you are using. Your remarks apply t= o the extrinsic approach from the last millennium. More recent presentation= of Type Theory built in substitution and weakening and use an intrinsic ap= proach which avoids talking about preterms you don=E2=80=99t really care ab= out.

 

https://dl.acm.org/doi/= 10.1145/2837614.2837638

 

Cheers,

Thorsten<= /span>

 

From: ho= motopytypetheory@googlegroups.com <homotopytypetheory@googlegroups.com&g= t; 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>=
Subject: Re: [HoTT] Question about the formal rules of cohesive homo= topy type theory

>  Does this al= so include the structural rules of type theory such as the substitution and= weakening 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/HomotopyTypeTheory/D66F4584-A005-4F= 69-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/PAXPR06MB786979CA= 94519BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.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/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmste= rling.com.
--=_MailMate_97B3481D-8A14-48C9-A8BB-515DF280F7FB_=--