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 25776 invoked from network); 16 Nov 2022 09:52:36 -0000 Received: from mail-lj1-x238.google.com (2a00:1450:4864:20::238) by inbox.vuxu.org with ESMTPUTF8; 16 Nov 2022 09:52:36 -0000 Received: by mail-lj1-x238.google.com with SMTP id t9-20020a2e7809000000b00277524ccb02sf6589589ljc.1 for ; Wed, 16 Nov 2022 01:52:35 -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:to:from:from:to:cc:subject :date:message-id:reply-to; bh=6YCz+/YvyDuLlFeB6Dpp47bf+43AFNUXdQKYBkMODcQ=; b=nBNyFdew+2bKa/peXUQPX1i8rN/YZ8F69rHMPNriGKxhRd+j2j9kIWHqIMyvffhOsh h7gMEdLJ1LhEcVdkYzJCaBn8/5Es03QgjQNqyYKkESxzzL6tBYLQw37CbWBxdew2wOJU OoUTnEpbZ5PUivbEar8mTlMNMycf9NOVOnqps2A30YLl4YmWJ9bSTmaG4uwc81TbpbJS AKvyjbHCZpa4ssaImaH0pTuRbtHgjyDS9ICYNVDQYjA0VnsF+zDOjgZ6cqL+c+DLmHuH W3SCMnFf5pAYfheHY4OT8u7FMkIHwXmb4VlWWuJka8+3EVAVRwYShVpfkZYD6ySbW2yn PQyQ== 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:to:from:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=6YCz+/YvyDuLlFeB6Dpp47bf+43AFNUXdQKYBkMODcQ=; b=mXp1x8ZV9cdqxzHCfG4eg776w9gHLZb2KNRslu+4yi6m8s4OJPXOXYQNBVWlXkQLmK c1HPTGCTrt0SiI7E/KXmoJqIdj+kFwrkJJeqV6TDJI40smtqkeCzA7EPPZlvzN+s7HYh GfSC9QYSa9V9pXWexiPlQospOgZxG8HpxRGtpiKMFwkw33G7/xH+n37As3/6yOk1ueGf FPE61+61HpT4cdMfbNdms59g97fuoQS+BHCzTdjpzY5avo81nfaEwQiH/0DDjeHuyCcR zM2A6rBxmw1KtUBBObYnaiYuCeHyaYDrkaGhtAzZocPk2OK3zv3oEKs4gZtLH8+XMYxS 6S3w== X-Gm-Message-State: ANoB5pnUSw/jKMe8OnV1E4L2M0/8H1gEzvf2PRdVYntzjgPVYB49sO0y 7q4oGXEiq0nCQU1+ixb3VV8= X-Google-Smtp-Source: AA0mqf5hn3PF0v2uOeaVpwJvoBIF1Ci/GdK4YFertzODP5lYb9uNlHPK93XXf6syZoP8Xg6JVkWv2w== X-Received: by 2002:a2e:99c5:0:b0:277:e01:610e with SMTP id l5-20020a2e99c5000000b002770e01610emr7064143ljj.181.1668592355101; Wed, 16 Nov 2022 01:52:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:58ef:0:b0:494:6c7d:cf65 with SMTP id v15-20020ac258ef000000b004946c7dcf65ls4964919lfo.2.-pod-prod-gmail; Wed, 16 Nov 2022 01:52:32 -0800 (PST) X-Received: by 2002:ac2:5ded:0:b0:4a2:b387:8b19 with SMTP id z13-20020ac25ded000000b004a2b3878b19mr6656756lfq.284.1668592351993; Wed, 16 Nov 2022 01:52:31 -0800 (PST) Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id k8-20020a2ea268000000b0027737e93a12si590787ljm.0.2022.11.16.01.52.31 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Wed, 16 Nov 2022 01:52:31 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 422352B6D7D_374B2DFB for ; Wed, 16 Nov 2022 09:52:31 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id C17CB2B6D79_374B2DEF for ; Wed, 16 Nov 2022 09:52:30 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp4.nottingham.ac.uk with esmtp (Exim 4.94.2) (envelope-from ) id 1ovF5q-0001Ws-Mj for homotopytypetheory@googlegroups.com; Wed, 16 Nov 2022 09:52:30 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by mail.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17; Wed, 16 Nov 2022 09:52:30 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2375.17; Wed, 16 Nov 2022 09:52:30 +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; Wed, 16 Nov 2022 09:52:30 +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; Wed, 16 Nov 2022 09:52:27 +0000 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=XABIJqp6NMZkLxEBseHJ7K1BOVM+vTlCCcYLI1bXB6AUWHIMgpz6mvEv7VQsmL6JBOa9lls9dfwSW5RX+uHR65wGQWOHJAlwQMspkFtTEMnfK6xpdQRccmmcwWF3J0qUhWPDgzM45NeITL1W/xJbiUBWbwhdF1ITHAKqdRi4niMu/aFtCRnvzBX7uPJJmXmhEhmGYJOEsLrcAw8qofcu6GfvmFkwHo3UqfW+NMwd/L+J0Xbdtj9cfYGpsDXuFsi61aCxDMpb5XcgCFJroxA+ofCzZpy61IjvO2H0icvQhDj8bTT8FHFk6sFL5FmkuHa33VPs8+VqZrF/h831uil0pQ== 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=sBd/cKrsJCvKvN2YCC1S+oJC6ncXcSjFq8RW6Iup2XU=; b=grKeXlPN/Oesda12ik9ThJzG5I88HDUwsFX+jydBU/pkSIYlYwu6VvbhnKpKTuVvRkWmF0IGip9EPSTq6h7eeZ9TUO5kVz+pbarjiSnQnoQGWFAwWsXK50uGfvrELSUYQ1voIvto4hM6Mmzfwe7J6+1yjq6VhaayjbLq5CNFbWmTamWtpf1/QpfWriPCaZHfJwlcDMBQO3BjtSZgmo69nwXrL1wUKUL9/Tox7xKb2ei9hG6/C9dV1UKF7LzYbCX5q19rOXzt90mGV9RVTl7dAFMgkYXMk4eVF7xf7NmRZ0xPxogxq860UCKLACTQrbnDUQhBOhBJUgt/9OCt3/4MCA== 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 VI1PR06MB3213.eurprd06.prod.outlook.com (2603:10a6:802:d::20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5813.17; Wed, 16 Nov 2022 09:52:22 +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; Wed, 16 Nov 2022 09:52:22 +0000 From: "'Thorsten Altenkirch' via Homotopy Type Theory" To: 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/PKxdMv7Ua0F8AzWOt4mK5Amc4AgAC7XWE= Date: Wed, 16 Nov 2022 09:52:22 +0000 Message-ID: References: <96f15467-49c9-43cc-8868-40b1bdf2162dn@googlegroups.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_|VI1PR06MB3213:EE_ x-ms-office365-filtering-correlation-id: 0958ff6e-751e-4c9f-b8a0-08dac7b84272 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: rG1A6kllso5MrkidUptPQMRo+xAak3Amom9uTPmQfxmfp/Rlcddn6UxtNe6Wsy3y10jox9wQCSrMqHDOnXH9KUvsOGDbag0jpj5SdxdDQPvEPqBrko7cV6Tsn/8pcs+SmMRD6GkGhGekLQch475BGOKEHmWdOzD9vIFP9j6PXrLcbXR29BWuxk7CeHZC2fUbXMQRVyWWT3f8gy3lXzGKFXXCnbIjd2zp4MzlyFidamRITIuXDjRyJ7AwoPuL0mtqvkKrP71udT+Y6j7W7VmBmZ7k3ia2S8BfRyQkSFeR3Pnzbv24J1J1bqAKHabdNq4zTVvfYkWMYsCv5HZhvyEXCvxfnolCqSFyoZ3q9St1AarUSuNd96IOH1d7E+XC1jbEYwncDe2addch3RKvDSCaPEZ2T5kq1rPqtoR/fz3bD5lSyAfy7a9RjF4ZX1Z/sR6usBMVjLhY1G8h7vK/3LGL/z4gZ/WjnVvE0AkFhi5hZCS6s6otabmQ/hiRnJ6Snl7UcsDTTsYEaEe5nG2MQRdQfmOxySOVFnY+QwjXmKRtSyDd+nnLu9QB8sE6fKARVSwLrn4jZgxVljNtSKh9P0g4vmCIzR5A5gMXLQAzihWnbqlbx2V/cXlX+SR2FQFNGTF8BNuPrWJFkCS2icMUO3bNdpNDajEQKu7z7tVOPB962i5993FLoLALKuzP9ZMCABkoe/LkvB7RqT1UvkIpQK41whdv79jDj2E0dviR0CFNomD+tMLJpzS2BZ9I5Pnw5GlKGMxx2lnBqacoi2AdHVyWZkabdQ8CWC1bOT6j24st1XQ= 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)(376002)(366004)(396003)(39860400002)(136003)(346002)(451199015)(66899015)(38070700005)(33656002)(166002)(41300700001)(55016003)(86362001)(122000001)(38100700002)(9686003)(186003)(83380400001)(64756008)(41320700001)(26005)(8936002)(7696005)(6506007)(2906002)(53546011)(966005)(786003)(66476007)(5660300002)(71200400001)(110136005)(66446008)(66946007)(66556008)(91956017)(316002)(76116006)(52536014)(8676002)(478600001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?Windows-1252?Q?qZVGKWUdZ2jwNEw9m1ASRsINrgQk+DRLwNTnDcWhIq5XSMfkqEVgZ4MY?= =?Windows-1252?Q?7IWJpczGgsiItxJOT2ZdcPBk6eyM9wyh7fbQxtPjlqDJH/aPpkF6D59I?= =?Windows-1252?Q?+UFlO9xeNvRMOQgQHpaDQEGdoBkM3NNmt6nktNPkmNkO0zvtzu05xzrh?= =?Windows-1252?Q?PIE8CDtP8kUvJ+A7Ktn5zHd1bSI84JsYqk9Z2L6LbfvhzLfwvjtGm8pG?= =?Windows-1252?Q?YtA4gqnfCtrKdqFDuyhcIxc623YQdfoK+B/j3Y57cbCr5V0XYiGtVWPw?= =?Windows-1252?Q?4CObLJWasErbFl/0pgWYnC7v9wLILjevvDjex9qgBbvkjBDDiNb37HMt?= =?Windows-1252?Q?hHF8Cdyi9AEE3U9Ih2WwbGYcTowVD9Xx1upBEL0EgWGuZRRgOrFNshLr?= =?Windows-1252?Q?D1w4bHr6/peGr+mlZMEixDL0fv1uxpRZD9IBOykFifgAkkQvFgXGL9x/?= =?Windows-1252?Q?jUNzSSjPBDRrpiZSqJ1HxKKRdURGkoPrRdM7XrnOyUpOs91X912lRCw/?= =?Windows-1252?Q?is2Y03Fi6F3J17m4YvMWBeKFqYGqkYTYYCd4LVkG1kOUpZcW5DNitsww?= =?Windows-1252?Q?Cp+zKsUFtG91DUC2WOQSp+d+T16Du3N54t1+5BRKC7MbDa80XyiQkSSQ?= =?Windows-1252?Q?PeM+08jzjJxmrvxwywy3EswuKeeIAeu/doz6KO1Y+o+KaXqiPQAGIyKZ?= =?Windows-1252?Q?xCcv4EHVNDoUaMi1jUGFRSe+5Sl1vETmyex0wmCW4YJa9i0fSDV77m/3?= =?Windows-1252?Q?NvRiv4a24r5q1ZZ1l6HJCYgV0lYG75yXEWMCRewSULSHkTPnCbJJXOdw?= =?Windows-1252?Q?IeHoaMspKjTKIXCmuUU+BgQSLRRGDC+KEYiO8lLjxKh1H5SDVPW6CYVF?= =?Windows-1252?Q?tim+Pq6cev5k2CNd2T2v1j/8BZibNZJiZHBm8XHiUNKqYbUjUkCcrSfe?= =?Windows-1252?Q?6GsxfAPeY7ZczxjmFYmqe0rE8Isj/Mek5YjpYwkUDZMH0uj5vH5+E/Au?= =?Windows-1252?Q?SSDJBZ1wj2UrElmishR979CWDtp2RNWC9RWCp1rKYb29qlTJOe4yME1d?= =?Windows-1252?Q?osZwhib47CnCbr1jothUA7iyMkYMB6UaEIsLTYMV2pwxTcKElzjR7NNq?= =?Windows-1252?Q?qyd5InEeTXJ79R/W8FcDCenVhlAdBEYpqX6M8YhuVqy69KDvQtqN1YMl?= =?Windows-1252?Q?r6e8hz8fNF9UJvLAizTGH8StxEpWKDoBil2RziDyB/pAS7OQ+7MfBbEf?= =?Windows-1252?Q?HglVkZXKcpllOhTGzM64Vh93VYj4vLRbFz1naLdMSn13+QvhHSJJhQYL?= =?Windows-1252?Q?OA0b6E6+KsPWWmD24xDo0oOM2K1D8QhxTdT5YizwfB9b1kv2rnsntjFb?= =?Windows-1252?Q?ORb9bYzFFexav59LH9KpNm9AjdK3JbVxHejQ191gJSybjRKKq5quc9gI?= =?Windows-1252?Q?67+Dpaf3d/IJFH23mUxx5KPje9tQnSPQfKPFJBe0GN9cwmZcv3jDS4hq?= =?Windows-1252?Q?C57SroQ54o2ir884REusnLgxEt3IwXhu1RhOQykGq0F3XhoWXjdmM3x+?= =?Windows-1252?Q?hXZ6A0Aza776QGdbo73l1ckEvidnZVzSt9eXkp07iEc/JGfAastNOmn1?= =?Windows-1252?Q?jcIAiwLsVVwTOqpCnHtz/7jcrC6bnF3wkH/+kEIAH95wBbv1zFVdEGer?= =?Windows-1252?Q?WDJoltFw9KeYYDy8voz8AX7Iw9iFihUhEqIl1CXT18LPHXxZih7i2zCP?= =?Windows-1252?Q?2nzATwBB7xNRBBM8zzeMBdTyEbqsmg7RMmsrMaci?= Content-Type: multipart/alternative; boundary="_000_PAXPR06MB786979CA94519BCC98EDD32FCD079PAXPR06MB7869eurp_" 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: 0958ff6e-751e-4c9f-b8a0-08dac7b84272 X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Nov 2022 09:52:22.8914 (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: OMsCnhiDhNuTNzMwCsLMzMTsLo37NM4UaWy/e7d6qFm1nIGqG9TFcf79RtPks8f26Z+r201zGu3rR/sJS7KIh8/jSGPs9/TM4uDtO3fgYjfdZRFvKSJ5i7+lAxDGwVeB X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB3213 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.129 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_PAXPR06MB786979CA94519BCC98EDD32FCD079PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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.=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/PAXPR06MB786979CA94519BCC98EDD32FCD079%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB786979CA94519BCC98EDD32FCD079PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

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 approach which avoids talking about pre= terms you don=E2=80=99t really care about.

&nbs= p;

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

&nbs= p;

Cheers,

Thorsten<= o:p>

&nbs= p;

From: homotopytypetheory@googlegroups.com <= homotopytypetheory@googlegroups.com> on behalf of andrej.bauer@andrej.co= m <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 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 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/PAXPR06MB786979CA9451= 9BCC98EDD32FCD079%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB786979CA94519BCC98EDD32FCD079PAXPR06MB7869eurp_--