From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6512:2025:: with SMTP id s5mr11722879lfs.121.1588601851635; Mon, 04 May 2020 07:17:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:5456:: with SMTP id d22ls2173657lfn.6.gmail; Mon, 04 May 2020 07:17:29 -0700 (PDT) X-Received: by 2002:a19:6448:: with SMTP id b8mr11660556lfj.18.1588601849631; Mon, 04 May 2020 07:17:29 -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 f1si885712lfm.1.2020.05.04.07.17.29 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 07:17:29 -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 BF6A42B7BDA_EB023F8B for ; Mon, 4 May 2020 14:17:28 +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 75F313647A1_EB023F8F for ; Mon, 4 May 2020 14:17:28 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp4.nottingham.ac.uk with esmtp (Exim 4.85) (envelope-from ) id 1jVbuR-0003c1-Qj; Mon, 04 May 2020 15:17:28 +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 15:17:27 +0100 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.1531.3; Mon, 4 May 2020 15:17:27 +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; Mon, 4 May 2020 15:17:27 +0100 Received: from EUR05-DB8-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 15:17:24 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=TCk78xmWnb45V4YXL/i8RUASOvjaQfaPxV9AQw430l8AWSygoO07gYGhJ95tLABwaspKDQuhi9Wu5Joe/JrKpavrvOTz9seyDK9KGMoIApkWlm5Gz9WeD+Z87K2pJVk4i7EJaGw230OIoO/7+7/W12+vOC6e0tG9ON5XaEedB7Gb2X5ri8V+m2/mMzC/B58j8jFNWR9liyn+FATIu086bQSV18X3X24q6S8dCf/KWp7U1HLkk7fZZX6QozoIjbq4FYwZU6I29zL8gOavmXhCPlmy5cx3kjDMyMy5URyURbF5K4pr0ArD/iuoQa9eCFytD6BnxYNyXUpRyAhN0zO7OQ== 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=qIdRaxv9rutzQ8P4iTsmvzustBT6ts+iUVVzHd5vSV8=; b=MPmBVSzC9g7d31WwXnu8fcH5838pogf28vJGS/HQODKbcbLlK8E62kNc1EicRTi0FdA5yI6YWrkMaTiKN31Hrg1TKObHWiunnYx4PdJzaw0Kef3R1DGUUUV2LxssaexX+pWvLuJuzRN2PGsnCmz59g88dtloNts3HcGiS5S8v4Q+cnEoLH7Fc20f6v+Zc1uC0gQjqRvO1IZsrZlIk1HMgLGHKlArrMzjuDrNNUMG+86azv9aoMC4ZZyqq/dPWdueMAa9irTBAKEszhveEmRzXWdRnEBdpAQvIKtOSuD126pPoGbaKJDA5UiOLiiAwrn3SqlikUsHTA7zV1rtNYG8fQ== 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 AM6PR06MB5944.eurprd06.prod.outlook.com (2603:10a6:20b:2a::30) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.20; Mon, 4 May 2020 14:17:24 +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 14:17:24 +0000 From: Thorsten Altenkirch To: Michael Shulman CC: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiX6KSAgAAhpoA= Date: Mon, 4 May 2020 14:17:23 +0000 Message-ID: <7A5CCED7-4FFC-43EE-AD3C-699899C19520@nottingham.ac.uk> 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: 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: 0438dbfe-9d90-4452-3e6d-08d7f035ddd8 x-ms-traffictypediagnostic: AM6PR06MB5944: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8273; x-forefront-prvs: 03932714EB x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: v5P3nlCoF6d1z6AGtDxFhTEDcuCTlCy481q7EKhZJRj/rlxcM3D1hQKTOWHQOkUcVkM+8WRpXS0HMSyH/oV/rw8X5+xHSC580lIpwdzWeT06L7yILIyjz4todUeZDgxahQPfxZRAUFD65uD90UqhN0K7lVpg4xQ2yf7ccQYC0IJonIUFYe1MadH7vUpvhapDdOpcsf/pGFXCp6v70ehb+1mQR3ZZ0YaTbIPZlCeRrH6WCPBn7DSEtcqIylD8oyb4cvwdCS7GQsKgky8knS4yMMixtw8oG0AMBXPqDZj7oq+5kwLk9Zrf7edC9ZuOPR45zoxdGtwcFzdEIkMRmxmU2wwjTFYyBlMzK0baeShaI22WzBTEEeI2sf263GH0Ona7sei0seR8wuPEwcqBdWXdTNro0ryoIxTASxVdCH2qLQJeyDYiLkRWt93zxLSt5k4qu/p0Wjbhlta04NcLuQvmNOnMv96uKhojUrvtxRQQDcqJaOiLR5xsYNHX8icxeZTRA/nh6yinJEwIpBivty+JJw== 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:(376002)(39860400002)(136003)(396003)(366004)(346002)(26005)(6512007)(786003)(316002)(33656002)(186003)(64756008)(66446008)(66556008)(2906002)(6486002)(86362001)(6916009)(9686003)(4326008)(966005)(478600001)(8676002)(8936002)(71200400001)(6506007)(53546011)(55236004)(5660300002)(66946007)(91956017)(76116006)(66476007)(36756003);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: JcD/VuEIduwW4mryLENiZOUXe9OEkYdx4Gyb+w2PmC3RM1mGcyuXHjN8OwOVyTfXbknfFlFxNzA2XWIMzbtkQ6sAijqHT0XEqxIh5leBDVTfGPfsI1tOFniCBhzlatAaagBsd2bAD+S4221W2fK3noBc9BrNShecDJcb2Zq6FlH0bOw/cndGObkWCzn82rtrrFM6b2xJgmaQR1FLgcwZA6LqTXo5ZXy7j9wbpKbdY1rhYP3kF3DdWHE+GxnDLzk4cPdleMDAFXal0pa6KvNB4UpDBdkzoPmn9FD8rZqScoCJjNQ001faupbgml7f4dhLbwAU3lmq3LVaqCZBgJbiU+cc6Z1ar2ZeUMaQ+msUErE3xyLUxlUS0a81A25iTrx84GyKjwxPo2BEMMAMpXDtlvkbsAyulVQU8a7yLNzKHujndw2T6EqJrkdttH+MmO8e0rfJh+W99KuTu1G5B5LiPKrwbf7w/9vCo5v/Opm1wg0KPOi+qMzUvpdRuVMqPyVGTQ30Pbhf6mzlwIV6IpOqUwyC5TSRhnCb6k3Q24QpZ0ihrw1JFOF3TjOtW0G3Ge/tc3qaGS3ZTXVSS906Y9eAbUZ3w/iqCHg5/LmKXmxVqQIjR3i/xwLkCOM8NdamSd2O4VgFWX7nE4MGMaU44W1vDlUEyWto7MK8JWQlRb9t+jSsqTxSJFIeBVPddorlrzm6JGOaoih62PgnOuYlnkabDCnHX5cWYcwRyCbzWHQ/zk1pFkrAjig6KdjhkEtCZvK7PX9KtG9YIKgt3VRAaT4827Pp5uxJbqG0ZCWvzdV9kNc= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <4759AF9A7BA5DF4E...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 0438dbfe-9d90-4452-3e6d-08d7f035ddd8 X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 14:17:24.0804 (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: L7DGIKqY9SF1MOi/vgnn6wE/zloC2A4hpGGTuYoicaSiTb1U+XgqIfJnsxaUWayNvCpGH+acupY290xwm/Y7R8vVfea/40hwuasW6E6vSyiL50M7bhqntGRGlW8pe+BA X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB5944 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 VGhpcyBzZWVtcyByZWFzb25hYmxlLiBJIHVzdWFsbHkgc2F5ICJlcXVhbGl0eSBwcm9vZnMiIGJ1 dCB0aGUgd29yZCBwcm9vZiBhbHNvIGhhcyBvdGhlciBjb25vdGF0aW9ucy4gQWxzbyB3aGF0IGlz IGFuIGVsZW1lbnQgb2YgMyA8PSA0LCBpZiBub3QgYSBwcm9vZiBvciBldmlkZW5jZT8gTWF5YmUg aXQgaXMgYSBpbmlkZW50aWZpY2F0aW9uPyBfXw0KDQpUaG9yc3Rlbg0KDQrvu79PbiAwNC8wNS8y MDIwLCAxNDoxNywgIk1pY2hhZWwgU2h1bG1hbiIgPHNodS4uLkBzYW5kaWVnby5lZHU+IHdyb3Rl Og0KDQogICAgSSBkb24ndCB0aGluayB1c2luZyAiaWRlbnRpZmljYXRpb24iIG5lY2Vzc2FyaWx5 IGltcGxpZXMgYW55DQogICAgZGlmZmVyZW5jZSBiZXR3ZWVuICJpZGVudGlmaWNhdGlvbiIgYW5k ICJlcXVhbGl0eSIuICBJIGRvbid0IHRoaW5rIG9mDQogICAgaXQgdGhhdCB3YXkuICBGb3IgbWUg dGhlIHBvaW50IGlzIGp1c3QgdG8gaGF2ZSBhIHdvcmQgdGhhdCByZWZlcnMgdG8NCiAgICBhbiAq ZWxlbWVudCogb2YgYW4gaWRlbnRpdHkgdHlwZS4gIENhbGxpbmcgaXQgImFuIGVxdWFsaXR5IiBj YW4gaGF2ZQ0KICAgIHRoZSB3cm9uZyBjb25ub3RhdGlvbiBiZWNhdXNlIGNsYXNzaWNhbGx5LCBh biBlcXVhbGl0eSBpcyBqdXN0IGENCiAgICBwcm9wb3NpdGlvbiAob3IgYSB0cnVlIHByb3Bvc2l0 aW9uKSwgd2hlcmVhcyBhbiBlbGVtZW50IG9mIGFuIGlkZW50aXR5DQogICAgdHlwZSBjYXJyaWVz IGluZm9ybWF0aW9uLiAgQ2FsbGluZyBpdCAiYW4gaWRlbnRpZmljYXRpb24iIHN1Z2dlc3RzDQog ICAgZXhhY3RseSB0aGUgaW5mb3JtYXRpb24gdGhhdCBpdCBjYXJyaWVzOiBhIHdheSBvZiBpZGVu dGlmeWluZyB0d28NCiAgICB0aGluZ3MuDQoNCiAgICBPbiBNb24sIE1heSA0LCAyMDIwIGF0IDI6 MzUgQU0gVGhvcnN0ZW4gQWx0ZW5raXJjaA0KICAgIDxUaG9yc3Rlbi4uLi5Abm90dGluZ2hhbS5h Yy51az4gd3JvdGU6DQogICAgPg0KICAgID4gSSBhbSBqdXN0IHJlYWRpbmcgYSBwYXBlciB3aGlj aCB1c2VzIHRoZSB3b3JkIOKAnElkZW50aWZpY2F0aW9u4oCdIGluc3RlYWQgb2YgZXF1YWxpdHku IEkgdGhpbmsgdGhpcyBoYXMgYmVlbiBwcm9wb3NlZCBieSBCb2IgSGFycGVyLiBDYW4gYW55Ym9k eSBlbmxpZ2h0ZW4gbWUgd2hhdCBpcyB0aGUgZGlmZmVyZW5jZSBiZXR3ZWVuIGlkZW50aWZpY2F0 aW9ucyBhbmQgZXF1YWxpdHk/IE1heWJlIHRoZXJlIGlzIGFuIGlkZW50aWZpY2F0aW9uIGJldHdl ZW4gdGhlbSBidXQgdGhleSBhcmUgbm90IGVxdWFsPyBBcmUgdGhlIHJlYWwgbnVtYmVycyAwLjk5 OeKApiBpZGVudGlmaWVkIG9yIGFyZSB0aGV5IGVxdWFsPw0KICAgID4NCiAgICA+DQogICAgPg0K ICAgID4gVGhvcnN0ZW4NCiAgICA+DQogICAgPiBUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2ht ZW50IGFyZSBpbnRlbmRlZCBzb2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUNCiAgICA+IGFuZCBtYXkg Y29udGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJlY2VpdmVkIHRo aXMNCiAgICA+IG1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBjb250YWN0IHRoZSBzZW5kZXIgYW5k IGRlbGV0ZSB0aGUgZW1haWwgYW5kDQogICAgPiBhdHRhY2htZW50Lg0KICAgID4NCiAgICA+IEFu eSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQgYnkgdGhlIGF1dGhvciBvZiB0aGlzIGVtYWls IGRvIG5vdA0KICAgID4gbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhlIFVuaXZl cnNpdHkgb2YgTm90dGluZ2hhbS4gRW1haWwNCiAgICA+IGNvbW11bmljYXRpb25zIHdpdGggdGhl IFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkDQogICAgPiB3aGVyZSBw ZXJtaXR0ZWQgYnkgbGF3Lg0KICAgID4NCiAgICA+DQogICAgPg0KICAgID4gLS0NCiAgICA+IFlv dSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQgdG8gdGhl IEdvb2dsZSBHcm91cHMgIkhvbW90b3B5IFR5cGUgVGhlb3J5IiBncm91cC4NCiAgICA+IFRvIHVu c3Vic2NyaWJlIGZyb20gdGhpcyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20g aXQsIHNlbmQgYW4gZW1haWwgdG8gSG9tb3RvcHlULi4uQGdvb2dsZWdyb3Vwcy5jb20uDQogICAg PiBUbyB2aWV3IHRoaXMgZGlzY3Vzc2lvbiBvbiB0aGUgd2ViIHZpc2l0IGh0dHBzOi8vZ3JvdXBz Lmdvb2dsZS5jb20vZC9tc2dpZC9Ib21vdG9weVR5cGVUaGVvcnkvQkJDMEI4RjMtQUIxNi00MTk2 LUI5QjktQjFCMzAzMUIyRDdEJTQwbm90dGluZ2hhbS5hYy51ay4NCg0KCgoKVGhpcyBtZXNzYWdl IGFuZCBhbnkgYXR0YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2Vl CmFuZCBtYXkgY29udGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJl Y2VpdmVkIHRoaXMKbWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIGNvbnRhY3QgdGhlIHNlbmRlciBh bmQgZGVsZXRlIHRoZSBlbWFpbCBhbmQKYXR0YWNobWVudC4gCgpBbnkgdmlld3Mgb3Igb3Bpbmlv bnMgZXhwcmVzc2VkIGJ5IHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QKbmVjZXNzYXJp bHkgcmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4gRW1h aWwKY29tbXVuaWNhdGlvbnMgd2l0aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBi ZSBtb25pdG9yZWQgCndoZXJlIHBlcm1pdHRlZCBieSBsYXcuCgoKCgo=