From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a2e:96c2:: with SMTP id d2mr11090778ljj.214.1588609026522; Mon, 04 May 2020 09:17:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:8155:: with SMTP id t21ls2787692ljg.5.gmail; Mon, 04 May 2020 09:17:05 -0700 (PDT) X-Received: by 2002:a2e:9456:: with SMTP id o22mr10815176ljh.94.1588609024961; Mon, 04 May 2020 09:17:04 -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 q24si812113ljg.4.2020.05.04.09.17.04 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 09:17:04 -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 387676D158E_EB04000B for ; Mon, 4 May 2020 16:17:04 +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 92F8B724348_EB03FFFF for ; Mon, 4 May 2020 16:17:03 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp3.nottingham.ac.uk with esmtp (Exim 4.85) (envelope-from ) id 1jVdmA-0007wE-VD; Mon, 04 May 2020 17:17:03 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.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.1531.3; Mon, 4 May 2020 17:17:02 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.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_GCM_SHA256) id 15.1.1531.3; Mon, 4 May 2020 17:17:02 +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; Mon, 4 May 2020 17:17:02 +0100 Received: from EUR05-AM6-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; Mon, 4 May 2020 17:17:02 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=HgBSQ9J6kxDw62XvJysIcR8tsjVM4sdHZ5W3AXbUGrQyZNEBBG3THhPaHsnDzp3RI8FsN5Mi92fL8Yt1933DNquKs0NqKg1nW74dPOmwELCqRuEdDuSBMkTmDa1uaclcbODGGPX3hWVOOpMn4pzYWm4po6KY4BPTyNt3RhoojTlZqOawzJ6Oe7D5brGKnIJedMcmxDtc4Z0ERoci6h81NYmsvK/ZZTD3M8exNkO1FHXOKR0Qf6EeGIkUashKvtDplS+GWxvUBQJLcaz0mbX2idbZqqrnxqu2JZtmFBaFE7NHrDQ4g7kV+TrRGLXPd1UN66Y8wHascbpxlSrZxSNEnQ== 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=cw4d5nyqi9esrOuehiAQPrTGPx+QTW4PDBXy50ihokg=; b=f7syjmUj+5LICHYxGl/T24VE7CwZ1SmVFiUAhTT3dSBI4RK93nGKfRI7JtN1FGsWQ2v4B1Z6MS4YXoCin7fI/3FKrLoymKpruE3bjU9K5AcyWMG6QcrjJrHZB0TZ8mqAMpbL9F3zSbIGAoyGudU7NE0nE5ysY4iD15RXSlp5zb+9nZgU0zqbvJ4q+9PhbhspggjFX3Mn7XE2A+VhTcPGXnelV+Xc2DYjkNBcTy1Ose1nrocAgzqmSM8gKZsW1CTbYDKOAFB2dZA15DyzDGQgFCRaWKbMQ0mIJu1CRgx1xtkG4lKg9UXmf4sI6OrxwIblT1tGOCEX+E8aT5obqJvMAA== 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 AM6PR06MB5687.eurprd06.prod.outlook.com (2603:10a6:20b:98::20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.19; Mon, 4 May 2020 16:17:00 +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.2958.030; Mon, 4 May 2020 16:17:00 +0000 From: Thorsten Altenkirch To: Steve Awodey , Michael Shulman CC: Stefan Monnier , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiX6KSAgAAZu8SAABPDgIAAAj4AgAATVIA= Date: Mon, 4 May 2020 16:17:00 +0000 Message-ID: References: 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: gmail.com; dkim=none (message not signed) header.d=none;gmail.com; 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: 718b55a0-042f-4ef3-6e8d-08d7f0469348 x-ms-traffictypediagnostic: AM6PR06MB5687: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:7219; x-forefront-prvs: 03932714EB x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: /IyNuRzyr29ClGjIAOeaDSJzhgOaiLesW0jemRlIUQRGr7GcmIUJMdLIqdgQt/b6wuGPQOayG+BBYd1hF+F3V3ouheY1iWFZ8mzE1JqT3IZDkCzvoG9DMQ/ctf/USOGHBBu6zVst91lSqMDBwUjpAQtiAjOw8iN7fNoN7YpD87UEtpvlInXt9Ff38/et0RN0JiK1F5j8HXzWmxQ5UYXfrPOus3XYfu0FIfDQgWgXE26i2aGQFP/qY5Rr8HelbUsaU7L2zPDYoEYvXb5LV0BuGfY6KAEenCJbm0bH1CSv/8FJg6w1qrh7pClhY2PxjfLhIyR0JSa4jHU1udZmBLtgrj8JSMy8hh4yg7rHhIdeTdC6TV4OXTBK2nyLKZyapO605S51O+f/Xo5otOiutFRp0HshNPhqFvPS/dvej8SUGAepN8REKogj9jcs1PKxY6HHn3xsvJIYEpQULqvAc4RbpnNH/qasaCaaySQ8WPCYw20A1oqt+UsryLcaPeOgEh1JGptFl00d8awyBGNPMq51Wg== 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:(366004)(396003)(39860400002)(136003)(346002)(376002)(86362001)(76116006)(2906002)(6486002)(66556008)(9686003)(66476007)(55236004)(66946007)(6512007)(186003)(6506007)(26005)(5660300002)(64756008)(66446008)(33656002)(53546011)(478600001)(966005)(91956017)(54906003)(8936002)(110136005)(4326008)(36756003)(316002)(8676002)(71200400001)(786003);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: fkfl9q63Hcfb7jtA5ydgfXWF77mlYcJzcCUIpTxTpunpZU8n0pxlxTIsPhq2z0S3LBLEJyFouOtYQqCzJ3kygzy1eWikDTIq9tNcQw5eS1ikSW6GESUz69rPqFwHptLJrwg1EgogmgBxJHgZ+5ScYM/RI/Rwi7972FDlT5E7P/6HfP8U9F84kF8a8ohEoE1PiqhBJ2PNSm6wHfOkuzU1Ju6d+/H+ZUcGGIgdunmWcR5V+PMmyyxCyEpcP7efDYCLqkW5p4TeNAf9UqIh5lEaEQDcZjw2hfMIydgfXrd2dWuAsEvOPCeVcKON7huyp/33yHysqvkrOGl3WttPdZTznFH+yQnKfCQQSHzG7Ra8gcjiHCVtq+G7lWqwOnRNwMeWudUkqfuG8Rj63jY4T7/9rh4WjZ1rt2JYIH1JyN/JEO92hcLmuwoAFUDHwin2R209yEFId+QPVPRbPdCLK+GWcI9qbF8QZwS34NkNUdYjzBNgTCLpZsMe7koAI39yIB9ZaLL0kXEcEDNiVGOEVgsPLEJ4VuRsG2eqUnfTMI6F/thaByn0ix9lP2WUE1jDPCzlMAxVqmVmlw0Tc/dpa1AMtcP/3kbPLE5V//nuTxNdZEthE7F+5nzeEwwI1op8jDDv3PG0gmcFN9L2UjsXl+hq+nLM1NysacNIBxTeiwL6Wqy6uHysGesufeG9HKU/CH3LO7nLfLBd/PdoM1SiBudeC6+vlJx1wHjZLFwYOlBbs2PCsGrBiAB+QMLdIBWSH3p5ukvO6nTxuMwT05FQitUpt8BrNp1A+amb8lBoZmaJ7pc= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <1F421AD44A8F6A43...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 718b55a0-042f-4ef3-6e8d-08d7f0469348 X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 16:17:00.4609 (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: QDwNBQzoIvW8ui1CLnKXye//0hCSMhlTtY/xWx1/SjOo1vKCYoVR2Kp8QyM5j5Nwfdt+eZG5PGwhlbG07BalBddswSEKFSe9jeuF6R4kO62dptNRz1PMYIg0IYQ0pAAk X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB5687 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 DQogICAgSeKAmW0gYWZyYWlkIHRoYXQgc29tZW9uZSBtYXkgaGF2ZSBoYWNrZWQgVGhvcnN0ZW7i gJlzIGVtYWlsIGFjY291bnQuIFRoZSByZWFsIFRob3JzdGVuIHdlbnQgdGhyb3VnaCBhbGwgdGhp cyB3aXRoIHVzIG1hbnkgeWVhcnMgYWdvLiANCiAgICA6IC0gKQ0KDQpPbmUgb2Ygb3VyIGRvZ3Mg Z2FpbmVkIGFjY2VzcyB0byBteSBsYXB0b3AgLSBzb3JyeS4gVGhlc2UgYW5pbWFscyBjYW4gYmUg dmVyeSBhd2t3YXJkLg0KDQpIb3dldmVyLCBldmVuIHRoZSByZWFsIFRob3JzdGVuIGhhZCBhIGZy aWVuZGx5IGFyZ3VtZW50IHdpdGggQW5kcmUgSm95YWwgd2hlbiB3ZSB3ZXJlIHdyaXRpbmcgdGhl IGJvb2sgYWJvdXQgd2hldGhlciB0byB1c2UgPSBmb3IgdGhlIGVxdWFsaXR5IHR5cGUuIA0KDQpU aG9yc3Rlbg0KDQrvu79PbiAwNC8wNS8yMDIwLCAxNzowOCwgIlN0ZXZlIEF3b2RleSIgPHN0ZXZl Li4uQGdtYWlsLmNvbT4gd3JvdGU6DQoNCiAgICBJ4oCZbSBhZnJhaWQgdGhhdCBzb21lb25lIG1h eSBoYXZlIGhhY2tlZCBUaG9yc3RlbuKAmXMgZW1haWwgYWNjb3VudC4gVGhlIHJlYWwgVGhvcnN0 ZW4gd2VudCB0aHJvdWdoIGFsbCB0aGlzIHdpdGggdXMgbWFueSB5ZWFycyBhZ28uIA0KICAgIDog LSApDQoNCg0KICAgID4gT24gTWF5IDQsIDIwMjAsIGF0IDEyOjAwLCBNaWNoYWVsIFNodWxtYW4g PHNodS4uLkBzYW5kaWVnby5lZHU+IHdyb3RlOg0KICAgID4gDQogICAgPiBUaGUgd29yZCAicGF0 aCIgaXMgY2xvc2VseSB0aWVkIHRvIHRoZSBob21vdG9weSBpbnRlcnByZXRhdGlvbiwgYW5kIHRv DQogICAgPiB0aGUgY2xhc3NpY2FsIHBlcnNwZWN0aXZlIG9mIG9vLWdyb3Vwb2lkcyBwcmVzZW50 ZWQgdmlhIHRvcG9sb2dpY2FsDQogICAgPiBzcGFjZXMsIHdoaWNoIGhhcyB2YXJpb3VzIHByb2Js ZW1zLiAgVGhpcyBpcyBwYXJ0aWN1bGFybHkgYW4gaXNzdWUgaW4NCiAgICA+IGNvaGVzaXZlIHR5 cGUgdGhlb3J5LCB3aGVyZSB0aGVyZSBpcyBhIHNlcGFyYXRlICJwb2ludC1zZXQgbGV2ZWwiDQog ICAgPiBub3Rpb24gb2YgcGF0aCB0aGF0IGl0IGlzIGltcG9ydGFudCB0byBkaXN0aW5ndWlzaCBm cm9tDQogICAgPiBpZGVudGlmaWNhdGlvbnMuDQogICAgPiANCiAgICA+PiBPbiBNb24sIE1heSA0 LCAyMDIwIGF0IDc6NDggQU0gU3RlZmFuIE1vbm5pZXIgPG1vbi4uLkBpcm8udW1vbnRyZWFsLmNh PiB3cm90ZToNCiAgICA+PiANCiAgICA+Pj4gSSBkb24ndCB0aGluayB1c2luZyAiaWRlbnRpZmlj YXRpb24iIG5lY2Vzc2FyaWx5IGltcGxpZXMgYW55DQogICAgPj4+IGRpZmZlcmVuY2UgYmV0d2Vl biAiaWRlbnRpZmljYXRpb24iIGFuZCAiZXF1YWxpdHkiLiAgSSBkb24ndCB0aGluayBvZg0KICAg ID4+PiBpdCB0aGF0IHdheS4gIEZvciBtZSB0aGUgcG9pbnQgaXMganVzdCB0byBoYXZlIGEgd29y ZCB0aGF0IHJlZmVycyB0bw0KICAgID4+PiBhbiAqZWxlbWVudCogb2YgYW4gaWRlbnRpdHkgdHlw ZS4gIENhbGxpbmcgaXQgImFuIGVxdWFsaXR5IiBjYW4gaGF2ZQ0KICAgID4+PiB0aGUgd3Jvbmcg Y29ubm90YXRpb24gYmVjYXVzZSBjbGFzc2ljYWxseSwgYW4gZXF1YWxpdHkgaXMganVzdCBhDQog ICAgPj4+IHByb3Bvc2l0aW9uIChvciBhIHRydWUgcHJvcG9zaXRpb24pLCB3aGVyZWFzIGFuIGVs ZW1lbnQgb2YgYW4gaWRlbnRpdHkNCiAgICA+Pj4gdHlwZSBjYXJyaWVzIGluZm9ybWF0aW9uLiAg Q2FsbGluZyBpdCAiYW4gaWRlbnRpZmljYXRpb24iIHN1Z2dlc3RzDQogICAgPj4+IGV4YWN0bHkg dGhlIGluZm9ybWF0aW9uIHRoYXQgaXQgY2FycmllczogYSB3YXkgb2YgaWRlbnRpZnlpbmcgdHdv DQogICAgPj4+IHRoaW5ncy4NCiAgICA+PiANCiAgICA+PiBJIHRob3VnaHQgdGhhdCdzIHdoYXQg InBhdGgiIHdhcyBmb3I/DQogICAgPj4gDQogICAgPj4gDQogICAgPj4gICAgICAgIFN0ZWZhbiAi d2hvIHJlYWxseSBkb2Vzbid0IGtub3cgd2hhdCBoZSdzIHRhbGtpbmcgYWJvdXQiDQogICAgPj4g DQogICAgPiANCiAgICA+IC0tIA0KICAgID4gWW91IHJlY2VpdmVkIHRoaXMgbWVzc2FnZSBiZWNh dXNlIHlvdSBhcmUgc3Vic2NyaWJlZCB0byB0aGUgR29vZ2xlIEdyb3VwcyAiSG9tb3RvcHkgVHlw ZSBUaGVvcnkiIGdyb3VwLg0KICAgID4gVG8gdW5zdWJzY3JpYmUgZnJvbSB0aGlzIGdyb3VwIGFu ZCBzdG9wIHJlY2VpdmluZyBlbWFpbHMgZnJvbSBpdCwgc2VuZCBhbiBlbWFpbCB0byBIb21vdG9w eVQuLi5AZ29vZ2xlZ3JvdXBzLmNvbS4NCiAgICA+IFRvIHZpZXcgdGhpcyBkaXNjdXNzaW9uIG9u IHRoZSB3ZWIgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL21zZ2lkL0hvbW90b3B5 VHlwZVRoZW9yeS9DQU92aXZReF8yVGluUkhCcm1PQVpGbm1GcDhWVlEteU1jUHZ0S0Z0WC1kOXdH c0QlMkIyUSU0MG1haWwuZ21haWwuY29tLg0KDQoKCgpUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRh Y2htZW50IGFyZSBpbnRlbmRlZCBzb2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUKYW5kIG1heSBjb250 YWluIGNvbmZpZGVudGlhbCBpbmZvcm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcwpt ZXNzYWdlIGluIGVycm9yLCBwbGVhc2UgY29udGFjdCB0aGUgc2VuZGVyIGFuZCBkZWxldGUgdGhl IGVtYWlsIGFuZAphdHRhY2htZW50LiAKCkFueSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQg YnkgdGhlIGF1dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdApuZWNlc3NhcmlseSByZWZsZWN0IHRo ZSB2aWV3cyBvZiB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLiBFbWFpbApjb21tdW5pY2F0 aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCAK d2hlcmUgcGVybWl0dGVkIGJ5IGxhdy4KCgoKCg==