From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a5d:62c7:: with SMTP id o7mr14567358wrv.212.1589138442812; Sun, 10 May 2020 12:20:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:db47:: with SMTP id f7ls5959391wrj.8.gmail; Sun, 10 May 2020 12:20:41 -0700 (PDT) X-Received: by 2002:adf:ed82:: with SMTP id c2mr15458798wro.255.1589138441187; Sun, 10 May 2020 12:20:41 -0700 (PDT) Return-Path: Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id u16si906832wmd.2.2020.05.10.12.20.41 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sun, 10 May 2020 12:20:41 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; 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.129 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id D3E5D2B5654_EB85408B for ; Sun, 10 May 2020 19:20:40 +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 uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 773402B5648_EB85408F for ; Sun, 10 May 2020 19:20:40 +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 1jXrV9-0002JT-Rt; Sun, 10 May 2020 20:20:40 +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 20:20:39 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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 20:20:39 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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 20:20:39 +0100 Received: from EUR03-DB5-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 20:20:39 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=bFHC5G16poIPXvrZDa718UHOlAf3322IhDVz248uHIzAmaaR7YWjD1UKfHm+r11ZDFGVfyHe91pvfXY0c/oMW3oH7NWTEa+V1QIvFVtfNIMKWrQGmSQK/dt9m5JUidQabg/ezC/Owc4zEAyFfI4zkAFEudylM0eAF13bNoESLSDz7c0wxj4KPmJ3cc0BIdYpt4nmP4AvAmITt/ULTimtYUtpNnwIMrw1AM760xrkxDzRXzpZW/H0Iu9vXTtqPtkQ4jQVSWnH3KuzdU4a/4f+nVKaonRRql+aF2sRJr+hZXCwPQo8l0G2nY6zu20bOrED2kqD8LFRzLJ+XO2Q0WzYVw== 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=Y+ONLFr7CjwV1inGgTUlHWaIfg/hnlEwwMQ9k7rkEVs=; b=dMndvWgLjySV7jyyfnSgg3eFJjx4eO5YfyKIMWI7AL0iJ7jjl0W8QGUQALNA9meqWsGlHqmWqRH5bdcdcEopBzt8gRlKUc47hqD1ipDbbUeXvIRDZLlh3DH6XtpFdIdL+zwbCkxtTAAaRXzRvrlXVeIlv83FiWFfnQLcqvP/CRPkBsXVZiI5Lnok88e7LCvXUHihNC7mOeNFeQywBo0ONe6BcnZfrVj0ctcibPG3XD7Psg6o7h18WCpiDGEXiXpwpwEplvUEGpRdEdAlY+IlE1EkcAV6jia9AkD3g4kDYZUo3Aq+vBQA1xcJvYe0OxYPH5oDCOvo9TsgGj3iAaonxQ== 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 AM6PR06MB6184.eurprd06.prod.outlook.com (2603:10a6:20b:fc::27) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2979.27; Sun, 10 May 2020 19:20:38 +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 19:20:38 +0000 From: Thorsten Altenkirch To: Michael Shulman CC: Jon Sterling , "'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+d4CAAHxwAIAAL1GAgAAahQCAABNRAIABAL6AgAAVJICAAGnTgA== Date: Sun, 10 May 2020 19:20:38 +0000 Message-ID: <579A6ED1-65D0-4A71-88A6-66191A70F6A2@nottingham.ac.uk> References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <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> <154D1B4B-6881-4269-8BA1-1CE8EBB0BE0D@nottingham.ac.uk> In-Reply-To: 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: sandiego.edu; dkim=none (message not signed) header.d=none;sandiego.edu; 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: 47b1c119-f51d-4a93-f501-08d7f517390a x-ms-traffictypediagnostic: AM6PR06MB6184: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:4714; x-forefront-prvs: 039975700A x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: RnE1/PIQURZCj9XdjEQcKa6v9gLyX4ptW1Efoh8H5FjbIz7W3Y9ZImTSQjY6X+groEWIii+SX9KSETpVoahNs59aVomDNwt7x6yV/MX/TDwsJakr+m9lhSK2LSDWfzuM+ebaoAdwfKq3+8zhYQdnZIzywIBIX8uChzCT18Jexqnl7a9HXgnk75BSVmq2KN7/8+v/qkW5k/i7rlaoA5H3O7z5D8Hs8GZW2wDoYubI86WMAbWWSUqwBxIyJAmbZxsD+gT5CQHSFZG/3LxVkKQsF1bSwAtdmkI45aTIvaJ0l42WBWYxPogP0Uuohy7eH869iEMfBmD1qCdUVF6ofhNVh8lNNN4PPp1PNFskScD4iXQfAkUzTHMlrkvyC1xZP3Ae5L4+1WBMg5tTlg/0sSEVuSDrNDKGKZ4XLnFEixBT2otiiKk1WDca0J5hcVLEs1u8Bp2xHAI6vbwgXQSYzwe389PtCkbNvNGuV0V9+N15WT2q8eHQEIb+i1JBl0INv7wrK3h8jEBqJqzJOdrmLTq/XA== 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)(39860400002)(136003)(376002)(33430700001)(5660300002)(53546011)(55236004)(6506007)(6512007)(6486002)(76116006)(36756003)(33440700001)(66446008)(33656002)(91956017)(66946007)(66556008)(66476007)(64756008)(26005)(478600001)(4326008)(8936002)(9686003)(6916009)(186003)(54906003)(2906002)(71200400001)(786003)(316002)(86362001)(8676002);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: pssWGGjlJPXRPsC6YW6vlhkp2d+eQx6QPgT411rw3SwkPQmfCBXputCRIxNo1Dsq/ByX6PAyxBzSS7iy2fNJy/aeiPZ5J4aUHSUo0p7pOH3/W23Lyr8v894+rJHkOA/XmXTIXOhAQvBDg8Je+qkMU7vdxeWHteSLXpPXfqN1Yea7QeahYeo7gs8ArRCNJXyqlIF8jlA7OkEUpSVhrx3O3ijeBGn0rpZqtBYSq6toQlzVfbvNpICZmhWn5J8zzFmlVqxQxO06PYBqnlXg6n4v+C3PHX/qpE2I8rnujLwCjZ29nIf7FK5kfFvyXh2goiHWLXovPw7Crw3+aqM8ov/yYBVJLqh4xNuxalMfxOLw4CwBAT/Ke5uEvSoPXI23hOqxSLbm+LnhicpSJnyIgHSZaD5dqZPfKw8R3kexI0bUrTQgW+12nbwyJMv7RS2s7Dg+SUmdX2PlBUSbIg4uSeBs65chs+lMa2/zNL01JSWYf9E= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <54A0005186D5DC44...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 47b1c119-f51d-4a93-f501-08d7f517390a X-MS-Exchange-CrossTenant-originalarrivaltime: 10 May 2020 19:20:38.5567 (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: c888+qd0NpJJBB/JxEYwOayGlfIPIr0y1qgh/oVo98pAlL+xwuKmpiBF1WOpUCMbc5CDKp8Pl/H0MLnTrNg5nj6/SceQjCoxTWwXKIflpFhe6kFtjp9qbmNJH3+/bMiB X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB6184 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 DQoNCu+7v09uIDEwLzA1LzIwMjAsIDE1OjA2LCAiTWljaGFlbCBTaHVsbWFuIiA8c2h1Li4uQHNh bmRpZWdvLmVkdT4gd3JvdGU6DQoNCiAgICBPbiBTdW4sIE1heSAxMCwgMjAyMCBhdCA0OjQ2IEFN IFRob3JzdGVuIEFsdGVua2lyY2gNCiAgICA8VGhvcnN0ZW4uLi4uQG5vdHRpbmdoYW0uYWMudWs+ IHdyb3RlOg0KICAgID4gRGVmaW5pbmcgc2ltcGxpY2lhbCB0eXBlcyBpc24ndCBlbnRpcmVseSBz dHJhaWdodGZvcndhcmQgKGFzIHlvdSBrbm93IEkgc3VwcG9zZSksIGJlY2F1c2UgRGVsdGEgaXMg bm90IGRpcmVjdGVkLiBXZSBjYW4gZG8gc2VtaS1zaW1wbGljaWFsIHR5cGVzIGFzIGEgUmVlZHkg bGltaXQsIGkuZS4gYW4gaW5maW5pdGUgU2lnbWEgdHlwZQ0KDQogICAgV2UgY2FuIGNlcnRhaW5s eSAqdGFsayogYWJvdXQgc2ltcGxpY2lhbCB0eXBlcyBpbiAyTFRUIGFzIGV4b2Z1bmN0b3JzDQog ICAgZnJvbSB0aGUgZXhvY2F0ZWdvcnkgRGVsdGEgdG8gdGhlIGV4b2NhdGVnb3J5IFR5cGUuICBJ IGFzc3VtZSB0aGUNCiAgICBwb2ludCB5b3UncmUgbWFraW5nIGlzIHRoYXQgd2UgZG9uJ3QgaGF2 ZSBhIChmaWJyYW50KSAqdHlwZSBvZioNCiAgICBzaW1wbGljaWFsIHR5cGVzLCB3aGVyZWFzIHdl IGRvIGhhdmUgYSBmaWJyYW50IHR5cGUgb2Ygc2VtaXNpbXBsaWNpYWwNCiAgICB0eXBlcyAodW5k ZXIgYXBwcm9wcmlhdGUgYXhpb21zKT8NCg0KWWVzLCBieSB0YWxraW5nIGFib3V0IEkgbWVhbnQg d2l0aGluIEhvVFQuIEkgbWVhbiB3ZSB3YW50IHRvIHVuZGVyc3RhbmQgdGhlbSBhcyBzdHJ1Y3R1 cmVzIG5vdCBqdXN0IGFzIHNvbWUgc2V0LWxldmVsIGVuY29kaW5nLiANCg0KQWxzbyBJIGZpbmQg dGhlIEthbi1jb25kaXRpb24gbW9yZSBuYXR1cmFsIGluIEhvVFQgYmVjYXVzZSB3ZSBqdXN0IG5l ZWQgdG8gc3RhdGUgYW4gZXF1aXZhbGVuY2UuIE9uIHRoZSBsZXZlbCBvZiBzZXQtbGV2ZWwgTWF0 aGVtYXRpY3Mgd2UgZWl0aGVyIGhpZGUgdGhlIHdpdG5lc3Mgb3Igd2UgbmVlZCB0byBpbnRyb2R1 Y2UgdW5pZm9ybWl0eSBjb25kaXRpb25zLiANCg0KSSBhbHNvIGRvbid0IHRoaW5rIGl0IGlzIGFu IGlzc3VlIHRoYXQgRGVsdGEgaXMgbm90IGRpcmVjdCBiZWNhdXNlIERlbHRhIGlzIGJhc2VkIG9u IHRoZSBoYWNrIHRvIGJ1aWxkIGlkZW50aXRpZXMgaW50byB0aGUgZnJhbWV3b3JrIGJ1dCBvYnRh aW4gY29tcG9zaXRpb24gdmlhIHRoZSBLYW4gY29uZGl0aW9uLiBIZW5jZSBJIHRoaW5rIHdlIHNo b3VsZCByZXByZXNlbnQgaWRlbnRpdGllcyBpbiB0aGUgc2FtZSB3YXkgYXMgY29tcG9zaXRpb24u DQoNCiAgICA+IFlvdSBuZWVkIHNvbWUgZXh0cmEgcHJpbmNpcGxlcywgZS5nLiB0aGF0IHN0cmlj dCBOYXQgaXMgZmlicmFudCBvciBtYXliZSBiZXR0ZXIgdGhhdCBjZXJ0YWluIGNvaW5kdWN0aXZl IHR5cGVzIGV4aXN0Lg0KDQogICAgUGVyc29uYWxseSwgSSB0aGluayB0aGUgYmVzdCBheGlvbSB0 byB1c2UgaGVyZSBpcyB0aGF0IGV4by1OYXQgaXMNCiAgICAqY29maWJyYW50KiwgaS5lLiBQaS10 eXBlcyB3aXRoIGRvbWFpbiBleG8tTmF0IHByZXNlcnZlIGZpYnJhbmN5LiAgV2UNCiAgICBkb24n dCBrbm93IGhvdyB0byBtb2RlbCAiZXhvLU5hdCBpcyBmaWJyYW50IiBpbiBhbGwgaGlnaGVyIHRv cG9zZXMsDQogICAgYnV0IGl0J3MgZWFzeSB0byBpbnRlcnByZXQgImV4by1OYXQgaXMgY29maWJy YW50IiBpbiBzdWNoIG1vZGVscywNCiAgICBzaW5jZSBQaS10eXBlcyB3aXRoIGRvbWFpbiBleG8t TmF0IGFyZSBqdXN0IGV4dGVybmFsbHktaW5maW5pdGUNCiAgICBwcm9kdWN0cy4NCg0KCgoKVGhp cyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUg YWRkcmVzc2VlCmFuZCBtYXkgY29udGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlv dSBoYXZlIHJlY2VpdmVkIHRoaXMKbWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIGNvbnRhY3QgdGhl IHNlbmRlciBhbmQgZGVsZXRlIHRoZSBlbWFpbCBhbmQKYXR0YWNobWVudC4gCgpBbnkgdmlld3Mg b3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QK bmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGlu Z2hhbS4gRW1haWwKY29tbXVuaWNhdGlvbnMgd2l0aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5n aGFtIG1heSBiZSBtb25pdG9yZWQgCndoZXJlIHBlcm1pdHRlZCBieSBsYXcuCgoKCgo=