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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 20085 invoked from network); 18 Nov 2022 11:36:00 -0000 Received: from mail-lf1-x138.google.com (2a00:1450:4864:20::138) by inbox.vuxu.org with ESMTPUTF8; 18 Nov 2022 11:36:00 -0000 Received: by mail-lf1-x138.google.com with SMTP id b34-20020a0565120ba200b004a2542bd072sf1659872lfv.2 for ; Fri, 18 Nov 2022 03:36:00 -0800 (PST) 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:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from:from:to:cc :subject:date:message-id:reply-to; bh=QmML9130M0VJUgjwaVH4v+zlIrZ27x0lZ7N70nXQt2s=; b=HaaAg0hmb75bbivDsu/L4BueqVKO+yS5ENICi0/dR9+DnewxzSV3nwMECcBa8WlMPe GBMCnWwUOvRoaHVKRXv1rFGVLlYrZrPKSGuZQ9YfZfMEOIhCyN1+SuRGvbxnfIzYQ6jn HsHLUtA5ILxaxOY8nbF6BrFkDuSCZXPaHXYnJ5tI6G/ZF8fLLyFxy4VhHgJyNO64Sg5A Dv4W8Z1IiKw2HypyiwS5M0gOympnqG7lbyRkmirDCxhR7w00chMRUIsozerNi1I+xyRc w1i+UW4bG28oJen/4P3SKIkOjQhmLPYM7yTjDUzqHhtu+SA923ra6oDHpZhdiKBsk9FA VqaA== 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:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=QmML9130M0VJUgjwaVH4v+zlIrZ27x0lZ7N70nXQt2s=; b=HWiSUEMMeufssYUrIf3IzBDE0Cjyq6FLAKzHiuhoecGKZH+uz0nMqnk3F2pW3F9vae 25Fy6675pgAdSUgwsoPncB+hxQshIxbNdFFlKeZiWAq6pWXKju/O91qrCzzFff8lO83t ElJOAZIt1yPSED3b9Btl2NFyV8x6FY4Qr0bdPTkcdak8TAgGcimbBOznEhE+k6ChHTSa FPi+Ci0O53wcV+emQsi38AKfEjPS4ZwrmIr/Gd/GMhCAr6X+9AHYm0wcvfRwzg4S95gK FPwXzmYsvKMk9mUGwCYg/T1f4CQR83kkhpZaKG4OQrXsN+3OzXayEfMlL7SZNsWxoMXQ iTGA== X-Gm-Message-State: ANoB5pl6esOiHmGZnrrhbQe2ZdWTQXE80T4sR4uGcOCzpj9pSoIm0OSD rtdSvQFW6RrqT5WAVz8ltbg= X-Google-Smtp-Source: AA0mqf42rnhIvgfvN/LIWdDucpkTdw2QKoYDZAX0HAobf02T4LDyJ+bkdDCfk0hbnkbnWaNlbVeKHw== X-Received: by 2002:a05:6512:128f:b0:4a2:4d89:aa58 with SMTP id u15-20020a056512128f00b004a24d89aa58mr2404167lfs.646.1668771358490; Fri, 18 Nov 2022 03:35:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:651c:2391:b0:26b:db66:8dd4 with SMTP id bk17-20020a05651c239100b0026bdb668dd4ls873800ljb.8.-pod-prod-gmail; Fri, 18 Nov 2022 03:35:55 -0800 (PST) X-Received: by 2002:a2e:88d3:0:b0:277:72a:41a5 with SMTP id a19-20020a2e88d3000000b00277072a41a5mr2607574ljk.352.1668771355315; Fri, 18 Nov 2022 03:35:55 -0800 (PST) Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTPS id 1-20020ac25f01000000b004b069b33a43si127339lfq.3.2022.11.18.03.35.55 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 18 Nov 2022 03:35:55 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 85EB52EAB46_3776E1AB; Fri, 18 Nov 2022 11:35:54 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id C8BE62EE5AC_3776E19F; Fri, 18 Nov 2022 11:35:53 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp3.nottingham.ac.uk with esmtp (Exim 4.94.2) (envelope-from ) id 1ovzez-00070W-Nq; Fri, 18 Nov 2022 11:35:53 +0000 Received: from UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) by mail.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17; Fri, 18 Nov 2022 11:35:53 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.2.986.5; Fri, 18 Nov 2022 11:35:53 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17 via Frontend Transport; Fri, 18 Nov 2022 11:35:53 +0000 Received: from EUR02-AM0-obe.outbound.protection.outlook.com (128.243.226.54) by mail.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17; Fri, 18 Nov 2022 11:35:53 +0000 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=jLSlS3WytJ6i1SaaTgUUCHn06f0Qb0etqzwRCf6IH/SbVWGGpz9FY/LwupsvWpMCFXvvKLtG1/N2pi/pFPAmvUv93gfAZ0uEjUq16FIshPa0ypjenxRlyIGYvk0TE5GCX2hFFUh89CFnt9/Jwdie6iwyTNCYIJX5Z7KLOcyObEvdolCrhzRS7d9FAuPsOll2MwDSlzhFX4KW0+bH7AYgJWGHxcF/rF0gt0P42ihc1CZyEmhrbob2Mgnww/a5WGjbGCW3XrNqYJH6vKfQpDvfc1rAVa6I4lpPBuKhmTwinUjqzJ0l1D7xGIxoARn+bsQAc8TEg64wAfd9N0cQjXsxVg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=o2dRcADtCqFK7OETM3U31MJ4PbJMVqOYSFWrhJR1Ij4=; b=Iod4oEsYu2+lfOzo08MvHNIPxxnHSSbXYkRcxD1OJezJx+hqCjhBlUSdb6vKJPPnRQw2UoLq7Mb3W2YSDe1tSd8N4wUuNfk0ly4+GKopIrV1CiaUthHRtHZHC+VQZFVNOxn6YVdeXgJ7+RKJDxmPiVskMEgUCujEVsZbmyXAANCfqvCRTzY/94mazzXI3KczX0BLD2xS5I9Gr6UJWnMeIMzCPQPJxp9paQhFh0znPQ/hu6rLB5LuNB6LIZjjjKaYe9pSLkNuuEYIPsOTPMUTunOtDzohhjrWE8k/JMS00yykLI2zDhX6Iz8neDPUvGxYYvJkPYy6hR5CkC/jMCXd4w== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=exmail.nottingham.ac.uk; dmarc=pass action=none header.from=exmail.nottingham.ac.uk; dkim=pass header.d=exmail.nottingham.ac.uk; arc=none Received: from PAXPR06MB7869.eurprd06.prod.outlook.com (2603:10a6:102:1a0::20) by AM5PR0601MB2465.eurprd06.prod.outlook.com (2603:10a6:203:78::22) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5813.19; Fri, 18 Nov 2022 11:35:50 +0000 Received: from PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::e78d:a974:264a:14ca]) by PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::e78d:a974:264a:14ca%5]) with mapi id 15.20.5813.018; Fri, 18 Nov 2022 11:35:50 +0000 From: "'Thorsten Altenkirch' via Homotopy Type Theory" To: Michael Shulman , Jon Sterling CC: andrej.bauer , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy type theory Thread-Topic: [HoTT] Question about the formal rules of cohesive homotopy type theory Thread-Index: AQHY9iNbq/PKxdMv7Ua0F8AzWOt4mK5Amc4AgAC7XWGAAdHagIAA2Z4AgACSZPw= Date: Fri, 18 Nov 2022 11:35:50 +0000 Message-ID: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.com> <41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF@jonmsterling.com> In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-publictraffictype: Email x-ms-traffictypediagnostic: PAXPR06MB7869:EE_|AM5PR0601MB2465:EE_ x-ms-office365-filtering-correlation-id: c971039b-47fc-4f9c-bea1-08dac9590b1f x-ld-processed: 67bda7ee-fd80-41ef-ac91-358418290a1e,ExtAddr x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: ME880HhnxWwJBestrQ1dDVSbYvV6ursigJjfkgf/MJUo7ClwVqnqnGkyKYQ5OKsa3/Pk1mOypy6h8qmq7ZdJ3pWuZu3+A6cX0v1XLs/2ru/v51k0t09Cw3MWTaYBmaF6EJGmvjQMTx8Kfdkjl5EZfAiAgAa97Ef3ziLzQFmiKc2ouCyeDikWwq3FjSpmCcv/jZrWpxPfzL++z/EdB8bqFCutb4sEixJr9DPK63TmRJUEbuZt+TU05sM6OJicVVbMQO69SUQKR0V32seNtSRBmYP0+e3uOG3UfKb8FrvNbhA7wLfmq5iAdIYm68lOosPfdhqmaGY9YHhslsRlFXgKchWH1mXrh0Z0+bpk0+Gun58TM1Vbg1VppZfz5hc1/MoI5VfMxm1ZHC/qyWqVZ6yA4AekqCB0aZGyLl5oAuZ/4GDyBkvwXLGoGynnYbbGqrOGn0BgOgqgW3d+XgLCQ5ldwo1SAvOMu1KsaXLXlz06USQyabz7se14K8VhTqs1rXIBJ0iWhhUicyfCQ8ssiooCm+ROvsL4mVqOwZ38Zr5jobvq6d6sr+wBsA8aXUuMDb5/SNUq1K9f5GW1r15lTMQJHlrKExRtnOK1/WuChjK3WCwMugbNHCrJfJzQ74SxX1gwMhXFSVxyVdpjQjvjpAeuJc9f5llvu+szI5VJYrm4SSLhFWIeLf5yEyJhqaH96YODvXXZZH9Dy1WkQ1ljo3s7Q9ibIHnZ55t3LzMhj6YMy28= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:PAXPR06MB7869.eurprd06.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230022)(396003)(136003)(346002)(376002)(366004)(39860400002)(451199015)(41320700001)(2906002)(66574015)(122000001)(83380400001)(66446008)(8936002)(5660300002)(966005)(786003)(64756008)(66476007)(9326002)(91956017)(8676002)(110136005)(86362001)(53546011)(7696005)(6506007)(38100700002)(166002)(186003)(9686003)(54906003)(26005)(66556008)(316002)(66946007)(66899015)(76116006)(52536014)(45080400002)(38070700005)(71200400001)(478600001)(4326008)(55016003)(33656002)(41300700001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?Windows-1252?Q?+bW0LIAycmUwmCzq29B5ZsdVyPKQJyGWpeStINbSQT8+PNjCii2Q+WZE?= =?Windows-1252?Q?d57WcpP4Xr/B4N7SilJb4c+4Fy1IzkHf855w54kHHnxRja84updshQLY?= =?Windows-1252?Q?s+urnPqLyVeK4G5oij1lxxl8brjiwSRlv0C5vSs0dwVlt/4tzp+4QY2J?= =?Windows-1252?Q?5TQw2PmkY9GwDAYhk5BC8SVvsZXJqdhAKzgwqGPfbfR4z5eZ35bSsujs?= =?Windows-1252?Q?1KgTBDKVR26gtqW4PTKFh4oqbayxA5FLFZBmEEATQrPFAeIrgbmFgBv0?= =?Windows-1252?Q?q9ajlBSFPw5rwfAeTXXTSfTqa4k1lm4LGrwNC8Na0oSjhD8TL3ONpGLA?= =?Windows-1252?Q?wrVuMru1BZB7uIoaANbe4X1iwHkFhGQHVR13VZHwsLxs5yerYbCmVml5?= =?Windows-1252?Q?JjULLejtjlbvtvKnKH3TXKiA1cIIy/jU/hxwJUyXOkzBT1jt7Go+MeG/?= =?Windows-1252?Q?5XA2O7lLj8dyfwRQVYVjOEGs2qoZpm5pLNmMCBVjlFS6rfyVd2iLhyiI?= =?Windows-1252?Q?ni0l4e+sLSnnAsO0elniAfB/qoTd79LRRn8jYgy/SZNNoloU97F5KQun?= =?Windows-1252?Q?8QOESAahTlgbczjPiQ/rDvo9F9E5GKwSCJK3RSkLuPkwjy7+px8MO8YV?= =?Windows-1252?Q?O31jyCZzh20Mz6hiYwKyQqUt+/Dh64HtnvnIZt96ev8h204vlcXYWaQP?= =?Windows-1252?Q?n0P8f/UH8EpETsKD2qi38NkN9opUT7cgXLg0Et11MzliadHejsG8oj6P?= =?Windows-1252?Q?FtaZC2VTy65BjEb0alobchZPr94AXSi+nxA86IYpJb+gDZR8TdUd5i4r?= =?Windows-1252?Q?Gn7LRYgMBG7upqU0k2edJHd/zKyXJA4/BtLWF7uysE5uKkdefQZVW3pm?= =?Windows-1252?Q?tM/aBaiIqxKDyHpENfcIXHpw000kvMxssC0cC7KjNiAG7rndmQtiMBGF?= =?Windows-1252?Q?v96FLk05uLGckIO5mecRFLVsFYkjXlpnXybaslSCuu1KbdqaQ3by0RCp?= =?Windows-1252?Q?xIYGd6C1nIYteDihDWl5ziHc8RTwWo3NzSA7BBKHMu4zIjWmsuIZTLCM?= =?Windows-1252?Q?1yAsRwSJBRqzgWrPF9IDmjsq7KPPr4c7kvoOIkm1VseQqMfatfbQh0hz?= =?Windows-1252?Q?pvosMxlho1OIzPRB6ylQJzhRSws5NeftxRT15kDFAByzUA6GWW/N2zYB?= =?Windows-1252?Q?F2igSWgmE68GFrExHuDKFF3cQzTqLaUC5Gzx4C1hbc0vPQE/mizyVPiq?= =?Windows-1252?Q?lVR1BHVRQgXxIdLFNpBsG1KYzvaGkO0BYZGTQQx2papU0RJ1HC7r27Nb?= =?Windows-1252?Q?ArQXsWU9Pp13wRh+HH8LC/EhY/9koHuFtelm8VrJAZgIMPl7MnHVlxK1?= =?Windows-1252?Q?Zg6Trpm+S4UET7ZELHwcEs/LZ0kt1Dysnub7Cs9i105kFweKPLzK2UeC?= =?Windows-1252?Q?jcTt4UlmGx1VXCAL7HMtJgmShU5oZdvSbcLeJnGMKmOM3zNFS+7hlZco?= =?Windows-1252?Q?xFOARQ0p2pjZeU/49Ip2m5R59vqcouaauKjU3ec52sDw/1z0tpqgbth9?= =?Windows-1252?Q?fhtRgtKaSNs3tNBFCEJHsRH39wtArYtNeM9Q4LBMISs9MwWlxFIiQOG3?= =?Windows-1252?Q?Fk50illxKzJzWWQJmzXMBNUk2FJfM4B7ydWO/91tUYJzBKOCInJlkAYZ?= =?Windows-1252?Q?tc/rQJGnNQnWejVehxhxSJOEk+CxGnhgEGmU0OQU1Be6LwMRemGIMW49?= =?Windows-1252?Q?VUxdc9xphCwgRrNfoNGV3mf5Ktz74xQqcsHT9uTR?= Content-Type: multipart/alternative; boundary="_000_PAXPR06MB7869899326D6A5C41CC20CB9CD099PAXPR06MB7869eurp_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: PAXPR06MB7869.eurprd06.prod.outlook.com X-MS-Exchange-CrossTenant-Network-Message-Id: c971039b-47fc-4f9c-bea1-08dac9590b1f X-MS-Exchange-CrossTenant-originalarrivaltime: 18 Nov 2022 11:35:50.1623 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: pitSJAZo4Zfaj4MIPpr7S2wkOcO3S9Dum6bzpaMUFiH0CaFRBzCm1ffRr6WFVwwoPNPtzMPf0phrY2A8mShyaZyCAU8ZUgmISQF/ey6OyhSwgbwv/17ubXSvCB6K3BxR X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM5PR0601MB2465 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk X-Original-From: Thorsten Altenkirch Reply-To: Thorsten Altenkirch 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: , --_000_PAXPR06MB7869899326D6A5C41CC20CB9CD099PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Mike, Certainly I would never claim that anybody=E2=80=99s work is meaningless, b= ut I think that understanding and presentation can often by improved by usi= ng an appropriate level of abstraction. Often the obvious and na=C3=AFve ch= oice isn=E2=80=99t the best option. I experience this a lot with students w= ho often use strings to represent syntactic objects like expressions. One o= f my mantras is =E2=80=9Cuse trees not strings=E2=80=9D =E2=80=93 I even ma= de a youtube video about it. Now most people accept that we should use trees to represent syntax but man= y still believe that typing should be extrinsic: ie we first define untyped= syntax (using trees) and then a typing relation. In my view they make a si= milar mistake as my students using strings but on a different level. When I= think about type theory I only want to talk about typed objects. Propertie= s like subject reduction, admissibility of substitution etc are just noise = caused by using an inappropriate level of abstraction. The essence of what = we want to say becomes clear once we overcome these misleading traditions. = This becomes even more essential once we deal with dependent types where th= e overhead often becomes unbearable. Now people we say that we do need to implement and verify programs like typ= e checkers. That is true and it is similar to the need for parsers to trans= late from strings to trees. My understanding of a parser is that it is the = partial inverse of the printing function which translates trees into string= s. Similarly a type checker is the partial inverse of a function from intri= nsically typed terms to untyped terms. Hence yes we do need to implement th= e whole toolchain of parsers, typecheckers and when we implement a type sys= tem but its specification should happen on the top. I haven=E2=80=99t worked on modal type theories but I suspect that they can= and should be presented intrinsically. I refer to Jon=E2=80=99s comments o= n this topic. Cheers, Thorsten From: Michael Shulman Date: Friday, 18 November 2022 at 02:36 To: Jon Sterling Cc: Thorsten Altenkirch (staff) , andrej.ba= uer , Homotopy Type Theory Subject: Re: [HoTT] Question about the formal rules of cohesive homotopy ty= pe theory As far as the mathematical study of type theories and their models goes, th= at may be true. But I believe that when talking about the way type theorie= s are used in practice, either on paper or in a proof assistant, there is s= till 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 operati= on that happens immediately in my head, not a computational step analogous = to 3^2 =3D 9. Similarly, the user of a proof assistant never types or sees= substitution as part of the syntax; it is an operation *on* syntax that ha= ppens behind the scenes. Yes, this is a property of a particular *presentation* of a free structure = rather than a property of the structure itself, but that doesn't intrinsica= lly make it unimportant. Groups and group 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 pr= operty that holds in the syntax but fails in some actual models; but that d= oesn't make "rules that hold in all models and can be made to hold in a par= ticular presentation of the free model without being given explicitly as ge= nerating operations/equalities" (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 figure o= ut what kind of substitution is admissible. Instead one decides what the s= ubstitution rule should be, and *then* (hopefully) works out a way of prese= nting the syntax to make that substitution rule admissible. This is partic= ularly tricky for modal type theories, where the categorically "obvious" ru= les do not admit substitution, and leads to the introduction of split conte= xts as used in the BFP paper. I have trouble imagining how I could have wr= itten that paper if I had been forced to write explicit substitutions every= where. Thorsten and Jon, do you maintain that all the work that's gone int= o figuring out ways to present modal type theories with "admissible substit= ution" 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 bei= ng 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 kn= owledge that cannot be applied toward anything by human beings). At least f= or structural type theory, there is nothing worth saying that cannot be phr= ased in a way that does not depend on whether structural rules are admissib= le 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 theo= ry 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 fo= r structural rules to not be derivable. Absent such a notion of model and e= vidence that it is at all compelling/useful, we would have to conclude that= worrying about admissibility vs. derivability of structural rules in the o= fficial presentation of type theory is fundementally misguided. On 16 Nov 2022, at 4:52, 'Thorsten Altenkirch' via Homotopy Type Theory wro= te: That depends on what presentation of Type Theory you are using. Your remark= s apply to the extrinsic approach from the last millennium. More recent pre= sentation of Type Theory built in substitution and weakening and use an int= rinsic approach which avoids talking about preterms you don=E2=80=99t reall= y care about. https://dl.acm.org/doi/10.1145/2837614.2837638 Cheers, Thorsten From: homotopytypetheory@googlegroups.com > on behalf of 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 homotopy ty= pe theory > Does this also include the structural rules of type theory such as the s= ubstitution 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-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 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.e= urprd06.prod.outlook.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 https://groups.google.com/d/msgid/= HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A444-13FA43EDD1CF%40jonmsterling.com<= https://groups.google.com/d/msgid/HomotopyTypeTheory/41C2FBD7-7C3B-4D6D-A44= 4-13FA43EDD1CF%40jonmsterling.com?utm_medium=3Demail&utm_source=3Dfooter>. 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. --=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/PAXPR06MB7869899326D6A5C41CC20CB9CD099%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB7869899326D6A5C41CC20CB9CD099PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hi Mike,<= o:p>

&nbs= p;

Certainly= I would never claim that anybody=E2=80=99s work is meaningless, but I thin= k that understanding and presentation can often by improved by using an app= ropriate level of abstraction. Often the obvious and na=C3=AFve choice isn=E2=80=99t the best option. I experience this a l= ot with students who often use strings to represent syntactic objects like = expressions. One of my mantras is =E2=80=9Cuse trees not strings=E2=80=9D = =E2=80=93 I even made a youtube video about it. <= /o:p>

&nbs= p;

Now most = people accept that we should use trees to represent syntax but many still b= elieve that typing should be extrinsic: ie we first define untyped syntax (= using trees) and then a typing relation. In my view they make a similar mistake as my students using strings but on= a different level. When I think about type theory I only want to talk abou= t typed objects. Properties like subject reduction, admissibility of substi= tution etc are just noise caused by using an inappropriate level of abstraction. The essence of what we wan= t to say becomes clear once we overcome these misleading traditions. This b= ecomes even more essential once we deal with dependent types where the over= head often becomes unbearable.

&nbs= p;

Now peopl= e we say that we do need to implement and verify programs like type checker= s. That is true and it is similar to the need for parsers to translate from= strings to trees. My understanding of a parser is that it is the partial inverse of the printing function whi= ch translates trees into strings. Similarly a type checker is the partial i= nverse of a function from intrinsically typed terms to untyped terms. Hence= yes we do need to implement the whole toolchain of parsers, typecheckers and when we implement a type syst= em but its specification should happen on the top.

&nbs= p;

I haven= =E2=80=99t worked on modal type theories but I suspect that they can and sh= ould be presented intrinsically. I refer to Jon=E2=80=99s comments on this = topic.

&nbs= p;

Cheers,

Thorsten<= o:p>

&nbs= p;

From: Michael Shulman <= ;shulman@sandiego.edu>
Date: Friday, 18 November 2022 at 02:36
To: Jon Sterling <jon@jonmsterling.com>
Cc: Thorsten Altenkirch (staff) <psztxa@exmail.nottingham.ac.uk&g= t;, andrej.bauer <andrej.bauer@andrej.com>, Homotopy Type Theory <= homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Question about the formal rules of cohesive homo= topy type theory

As far as the mathematical study of type theories an= d their models goes, that may be true.  But I believe that when talkin= g 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 sub= stitution is an operation that happens immediately in my head, not a comput= ational step analogous to 3^2 =3D 9.  Similarly, the user of a proof a= ssistant never types or sees substitution as part of the syntax; it is an operation *on* syntax that happens behind the= scenes.

 

Yes, this is a property of a particular *presentatio= n* of a free structure rather than a property of the structure itself, but = that doesn't intrinsically make it unimportant.  Groups and group pres= entations are both important.  Maybe you want to say that "a type theory" refers to the free structure ra= ther than its presentation, but choosing to use words in that way doesn't b= y itself make "presentations of type theories" (or whatever you c= all them) less important.  Maybe you want to define an "admissible rule" to be a property that holds in the syntax b= ut 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 call them) less important.

 

I do agree that Andrej's formulation sounds backward= s.  In practice (in my experience) one doesn't write the rules down fi= rst and then try to figure out what kind of substitution is admissible.&nbs= p; Instead one decides what the substitution rule should be, and *then* (hopefully) works out a way of presenting the s= yntax 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 with "admissible sub= stitution" is meaningless?

 

On Thu, Nov 17, 2022 at 5:37 AM Jon Sterling <jon@jonmsterling.com> 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 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 l= east 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 ad= missible or derivable. It may be that admissiblity of structural rules starts to play a role in substructur= al 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 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 misguided.

 

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

That depends on what presentation of Type Theory you are using. Your r= emarks apply to the extrinsic approach from the last millennium. More recent presentation of Type Theory built in substitu= tion and weakening and 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 <homotopytypetheor= y@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 t= he 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 in 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/HomotopyTypeTheory/D66F4584-A005-4F69-8E7= 5-E976E0FF9957%40andrej.com.

This message and any attachment are inte=
nded solely for the addressee
and may contain confidential information=
. If you have received this
message in error, please contact the sen=
der and delete the email and
attachment. 
 
Any views or opinions expressed by the a=
uthor of this email do not
necessarily reflect the views of the Uni=
versity of Nottingham. Email
communications with the University of No=
ttingham may be monitored 
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/PAXPR06MB786979CA94519= BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.<= /span>

--
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/41C2FBD7-7C3B-4D6D-A44= 4-13FA43EDD1CF%40jonmsterling.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/PAXPR06MB7869899326D6= A5C41CC20CB9CD099%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB7869899326D6A5C41CC20CB9CD099PAXPR06MB7869eurp_--