From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:f40a:: with SMTP id g10mr14021200wro.117.1589112005089; Sun, 10 May 2020 05:00:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:9544:: with SMTP id 62ls5169851wrs.1.gmail; Sun, 10 May 2020 05:00:03 -0700 (PDT) X-Received: by 2002:adf:fad0:: with SMTP id a16mr14382186wrs.149.1589112003856; Sun, 10 May 2020 05:00:03 -0700 (PDT) Return-Path: Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTPS id s22si887680wme.0.2020.05.10.05.00.03 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 10 May 2020 05:00:03 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 86BF36CE582_EB7ECC3B for ; Sun, 10 May 2020 12:00:03 +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 uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 3625C6CDA33_EB7ECC3F for ; Sun, 10 May 2020 12:00:03 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp3.nottingham.ac.uk with esmtp (Exim 4.85) (envelope-from ) id 1jXkcg-0007I1-UD; Sun, 10 May 2020 13:00:03 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by exchangeSMTP.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.1531.3; Sun, 10 May 2020 12:59:58 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Sun, 10 May 2020 12:59:58 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) 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.1531.3 via Frontend Transport; Sun, 10 May 2020 12:59:58 +0100 Received: from EUR05-VI1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.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.1531.3; Sun, 10 May 2020 12:59:58 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=XP+6u2WxBC8vP45Luay6S0SNVLBZBm9jwdsy3/Xy0M9FnfYuwIdvYRA7J2HR6a/1w5Rx4zEasH0timqHUC1pzMSOu0DbzNoqLhTiB5aNedFLBmhdBZffcInVdYv2PHdL9i9RxhhiHbzMEroFThlY4x3Re96UUNP30gPltRlxQNL5oxI7F5mWMcyjN2hJocEfdv3tmMUT4p2PRHaDT529oSakOaDFZ6Fwt4BraCOvmoqKP6Xe/guIhbIcgboGoQFOFEryE8bsjwtRPso4k18Q6J1HkGJ0LhrZzfihJ4kPn+hL9UXn7LA5v9ZGKtBviEQhb7xYjg34VFlhwgvrKNEX5A== 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-SenderADCheck; bh=4OF+gS4DycoPTm3HHqjm/PGjG8R7PxwStzTKtnjXrrc=; b=V1KTSnbbFGl37rtkGnRaWdVo6jBYlqxZLfECKIVNQBB4tFgjKBJzGyRCsIM8h32+ZrcIpu4bZ8zhC+1yWioZVNmq8zR78bu0HmRxnxumsoVA0lH0dzY9dyUFMCZd0mQOgr+L32HNLZ19JNpBzgsMJNT7D2Q1wBwktcKwbYaqesiZxdzdFMe/75dKO2jhnLlIx/qFoNZxgiXablx+6nadWw2ymSwNszLj+s/W0u3qTLEuKfoKok2ZfhSx3yaZ5X7RrNkHXUIQKxuOSl/5onNkcm6IGziexHcJ7XSb1MIh0WtR7gidDkAq1rWnqElipCsMnZzE2rDOuqHdavXG4aWAzg== 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 AM6PR06MB5879.eurprd06.prod.outlook.com (2603:10a6:20b:2c::24) by AM6PR06MB4899.eurprd06.prod.outlook.com (2603:10a6:20b:5e::28) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2979.34; Sun, 10 May 2020 11:59:57 +0000 Received: from AM6PR06MB5879.eurprd06.prod.outlook.com ([fe80::6427:d0c5:a0f3:68b1]) by AM6PR06MB5879.eurprd06.prod.outlook.com ([fe80::6427:d0c5:a0f3:68b1%4]) with mapi id 15.20.2979.033; Sun, 10 May 2020 11:59:57 +0000 From: Thorsten Altenkirch To: Thomas Streicher , Jon Sterling CC: =?utf-8?B?IkpveWFsLCBBbmRyw6ki?= , "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrn+BFzsbNwSEEa9XfXV/1cG1qibOgWAgAAyGYCAAAS1AIAATROA///484CAAI5iAIAAJIIAgABlowCAAFujgIAAIkaAgAADnYCAAHDSgIAA8f+AgAC+d4CAAHxwAIAAL1GAgAAahQCAABNRAIAAUYqAgAAMlACAAGY1gIAAQEIA Date: Sun, 10 May 2020 11:59:57 +0000 Message-ID: <2B1AB8DA-9331-4F48-AA8F-F0BAB2BCBC41@nottingham.ac.uk> References: <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F5693@Pli.gst.uqam.ca> <20200510090957.GA24125@mathematik.tu-darmstadt.de> In-Reply-To: <20200510090957.GA24125@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/16.36.20041900 authentication-results: mathematik.tu-darmstadt.de; dkim=none (message not signed) header.d=none;mathematik.tu-darmstadt.de; dmarc=none action=none header.from=exmail.nottingham.ac.uk; x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: d7a78456-8253-4b5f-efee-08d7f4d9a8ef x-ms-traffictypediagnostic: AM6PR06MB4899: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-forefront-prvs: 039975700A x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: mnSPmRFQtlqEH9/faLp4W2R4jqwmbRy33IpGft21ORBmE04nU5qwHSmZveeG5K/ltSlT59RsOjL/V/0r4D7wZCkE+D2Y1MzHUSm2G1+KYvvlJBEVvs5i56fZ/KrMVes77tr10V8wayf7n2dOCTLXx1Lt/IRchTA944T8qU6TSZAhAp3RdmNbvwdPYu3HUYKTYRcR5lnUM/vG1aT7gb7BWLbfL6wxNQ92DR0xxmUaBrbRJI80cxIaUcKdUyPClZUQ/3RNPEQMAUWYvaIY05iuluRDz/+ELbA2aMPOlLK/yEXYI8cvRYwLdFVmMwPbM54uQm0xyJ24zGDHmHjZfy2Wp4b+qh4fnMOHYkw3cfI5IIlLM6gmT5Wg6UauIyoKP79jHuITTlNBeym5x1VRCvfWEZhBCjVDp5tNoFHhca8CCmuN20lU2d7VIiI4FcnKmRSjea5xamsUHqdx4ZzzLEc7mmGS2uDT8J5WR8nWhMF5t27QCRb/okf05PyYRzNTXpL605IlKQgS4c0GV85HAOMcyCM1nanEXj+DxSMAE+VQTFHOoI+Juif1B3IYGrc5Vb1+tso5TUmqlRVSAruPnH4PBbcQdPXzG+Lkj/LlUsOZ8FA= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AM6PR06MB5879.eurprd06.prod.outlook.com;PTR:;CAT:NONE;SFTY:;SFS:(346002)(366004)(396003)(376002)(136003)(39860400002)(33430700001)(36756003)(5660300002)(186003)(26005)(316002)(786003)(6506007)(110136005)(54906003)(66446008)(66556008)(66476007)(66946007)(76116006)(91956017)(64756008)(86362001)(55236004)(9686003)(6512007)(6486002)(2906002)(966005)(4326008)(478600001)(8936002)(71200400001)(8676002)(33656002)(33440700001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: Jes2GzDM8tlNRbIFbg6lp82AHPrNa8MagSQtQ5L91/biGIebqhrmf82cNJvl6thkW2HLlOsmG5AhSjTDePi0h0mB0dLImdxl2+mxlbgN+m/Z/MrPelmiKKh1gZ7u9uMIICS+iUOGj10alNJ322pIpUqOqbWI6VpuHZm7ysAreUVPIKZujRbsSMF3EMk353VGiPDm67Hbx+lTuMeeKQgVAezbLQlAhaZw9DBEC2eejchfEyCNOnpAqhocm3tMYJJXE37aBABAsZ/tEwjVPANF0PijRD5KRBtRTuXyFG01EUWDaocNfqYynT46SobJKCpLMazWfLakgiQe90mxNObadKfKqx9VfJfCNruHZzuXtqu4ZFtLOApqre5ZySERtvEJHXE9D2t6dtrwVNFaypt3IaIzoLnn4nYpTYejWGy89Jqvk1EJbc2/McWWdYQw/bi/PiYLFKX8XMokDLauWwaOGrCPDRvkSLGFDuWhscXxNP8= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <31B3283783877147...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: d7a78456-8253-4b5f-efee-08d7f4d9a8ef X-MS-Exchange-CrossTenant-originalarrivaltime: 10 May 2020 11:59:57.3942 (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: vG8NM/UfCwGXoHlUMyhXhAoIStr1Fjh9t+2JmEL7o3L2hQz9XTGVEne1smyg3XEkxQe075B0vdhtjP3j6ZLWv0Z/NVkGqjdedg5ymP+YL6TBpT1aipUF1AcAf3Xdxg/U X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB4899 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 RGVhciBUaG9tYXMsDQoNCiAgICBJIG1vc3RseSBhZ3JlZSB3aXRoIHdoYXQgSm9uIHNhaWQuIEkg YWxzbyB0aGluayB0aGF0IGludGVuc2lvbmFsIHR5cGUNCiAgICB0aGVvcnkgd2l0aGluIGFuIGV4 dGVuc2lvbmFsIHR5cGUgdGhlb3J5IChpdCBpcyAyIGxldmVscyBhbmQgbm90IDMpIGlzDQogICAg YW4gYXR0cmFjdGl2ZSBzeXN0ZW0gZm9yIGN1YmljYWwgdHlwZSB0aGVvcnkuDQoNClRoYXQgc2Vl bXMgdG8gYmUgcHV0dGluZyB0aGUgY2FydCBiZWZvcmUgdGhlIGhvcnNlLiBIb1RUIGlzIHRoZSB0 aGVvcnkgSSB3YW50IHRvIHdvcmsgaW4sIHRoZSBzdHJpY3QgbGF5ZXIgaXMgb25seSB0aGVyZSB0 byBkbyBzb21lIGludGVybmFsaXplZCBtZXRhdGhlb3J5Lg0KDQogICAgSW4gdGhlIHNpbXBsaWNp YWwgY2FzZSB0aGlzIGlzIGEgYml0IG1vcmUgcHJvYmxlbWF0aWMgc2luY2UgdGhlDQogICAgZmls bGluZyBjb25kaXRpb25zIGZvciBLYW4gY29tcGxleGVzIGludm9sdmUgY2xhc3NpY2FsIGV4aXN0 ZW50aWFsDQogICAgcXVhbnRpZmljYXRpb24gYW5kIGFzIHNob3duIGJ5IFRoaWVycnkgZXQuYWwu IHRoaXMgaXMgaW1wb3J0YW50IQ0KDQpJIHRoaW5rIHdlIGhhdmUgdHdvIGRpc2N1c3Npb25zIGhl cmU6IG9uZSBpcyBhYm91dCBzaW1wbGljaWFsIHNldHMgd2hpY2ggaXMgYWJvdXQgdGhlIHJlZHVj dGlvbiBvZiBIb1RUIHRvIHNldCBsZXZlbCBzdHJ1Y3R1cmVzIGFuZCB0aGUgb3RoZXIgaXMgYWJv dXQgKHNlbWktKXNpbXBsaWNpYWwgdHlwZXMgd2hpY2ggaXMgYWJvdXQgbW9kZWxsaW5nIGhpZ2hl ciBzdHJ1Y3R1cmVzIHdpdGhpbiBIb1RULg0KDQpUaGUgY2xhc3NpY2FsIGFzc3VtcHRpb25zIGlu IHRoZSBmaWxsaW5nIGNvbmRpdGlvbnMgZm9yIEthbiBjb21wbGV4ZXMgY2FuIGJlIGF2b2lkZWQg YXMgd2FzIHNob3duIGJ5IEdhbWJpbm8gYW5kIFNhdHRsZXI6DQpodHRwczovL2FyeGl2Lm9yZy9h YnMvMTUxMC4wMDY2OQ0Kd2hvIGRldmVsb3AgYSB0aGVvcnkgb2YgdW5pZm9ybSBmaWJyYXRpb25z IHRoYXQgY2FwdHVyZXMgYm90aCBjdWJpY2FsIGFuZCBzaW1wbGljaWFsIHNldHMuIFRoaXMgbWVh bnMgd2UgY2FuIG1vZGVsIFBpLXR5cGVzIHVzaW5nIHVuaWZvcm0gc2ltcGxpY2lhbCBzZXRzLiBI b3dldmVyLCBpdCBpcyBub3QgY2xlYXIgaG93IHRvIGludGVycHJldCBhIHVuaXZhbGVudCB1bml2 ZXJzZSBpbiB1bmlmb3JtIHNpbXBsaWNpYWwgc2V0cy4gSXQgaXMgcG9zc2libGUgdG8gZG8gdGhp cyBpbiB1bmlmb3JtIGN1YmljYWwgc2V0cyBkdWUgdG8gdGhlIGZhY3QgdGhhdCB0aGUgaW50ZXJ2 YWwgaXMgYSB0aW55IG9iamVjdC4NCg0KICAgIFRoYXQgdGhlIGV4dGVuc2lvbmFsIGxldmVsIGlz IGp1c3QgZm9ybXVsYXRlZCB1c2luZyBKIGFuZCBLIGlzIGENCiAgICBwb3NzaWJpbGl0eS4gSXQg aGFzIHRvIGJlIHNlZW4gaW4gcHJhY3RpY2UgaG93IGZhciBpdCBnb2VzLg0KDQpZb3UgbmVlZCBL IG9uIHRoZSBzdHJpY3QgbGV2ZWwsIGJlY2F1c2UgdGhhdCBpcyBleGFjdGx5IHRoZSBwb2ludCB0 aGF0IHlvdSBkb27igJl0IG5lZWQgdG8gY2FyZSBhYm91dCBjb2hlcmVuY2VzIGFueW1vcmUuIEJ0 dywgSSB0aGluayBjYWxsaW5nIGl0ICJleHRlbnNpb25hbCBsZXZlbCIgaXMgYSBtaXNub21lciBi ZWNhdXNlIGFjdHVhbGx5IHRoZSBmaWJyYW50IGxheWVyIGlzIG1vcmUgZXh0ZW5zaW9uYWwgdGhh biB0aGUgc3RyaWN0IG9uZSBiZWNhdXNlIGl0IGlzIHVuaXZhbGVudC4gDQoNClNvIGZvciBleGFt cGxlIGlmIHlvdSBkZWZpbmUgc2VtaS1zaW1wbGljaWFsIHR5cGVzIGluIGEgMi1sZXZlbCB0eXBl IHRoZW9yeSBpdCBpcyBlc3NlbnRpYWwgdGhhdCB5b3UgaGF2ZSBLLg0KDQpDaGVlcnMsDQpUaG9y c3Rlbg0KDQoKCgpUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2htZW50IGFyZSBpbnRlbmRlZCBz b2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUKYW5kIG1heSBjb250YWluIGNvbmZpZGVudGlhbCBpbmZv cm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcwptZXNzYWdlIGluIGVycm9yLCBwbGVh c2UgY29udGFjdCB0aGUgc2VuZGVyIGFuZCBkZWxldGUgdGhlIGVtYWlsIGFuZAphdHRhY2htZW50 LiAKCkFueSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQgYnkgdGhlIGF1dGhvciBvZiB0aGlz IGVtYWlsIGRvIG5vdApuZWNlc3NhcmlseSByZWZsZWN0IHRoZSB2aWV3cyBvZiB0aGUgVW5pdmVy c2l0eSBvZiBOb3R0aW5naGFtLiBFbWFpbApjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJz aXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCAKd2hlcmUgcGVybWl0dGVkIGJ5IGxh dy4KCgoKCg==