From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:906:3709:: with SMTP id d9mr15784443ejc.94.1588607877654; Mon, 04 May 2020 08:57:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:6b89:: with SMTP id l9ls6579213ejr.6.gmail; Mon, 04 May 2020 08:57:56 -0700 (PDT) X-Received: by 2002:a17:906:3da:: with SMTP id c26mr15765842eja.290.1588607875927; Mon, 04 May 2020 08:57:55 -0700 (PDT) Return-Path: Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTPS id i2si628001edn.2.2020.05.04.08.57.55 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 08:57:55 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; 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.124 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 8A2213C3FA4_EB03B83B for ; Mon, 4 May 2020 15:57:55 +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 uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 476CB3C3F4A_EB03B83F for ; Mon, 4 May 2020 15:57:55 +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 1jVdTe-0003ee-P1 for homotopyt...@googlegroups.com; Mon, 04 May 2020 16:57:55 +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 16:57:54 +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 16:57:54 +0100 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.1531.3 via Frontend Transport; Mon, 4 May 2020 16:57:54 +0100 Received: from EUR05-AM6-obe.outbound.protection.outlook.com (128.243.226.54) 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 16:57:54 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=NgD9P3FmOrpvcGMeB4tOKL1jyHSH4qCA60mx8XTV6yL+c0pt7jAo0WUCoC9H3jpyEWhdDGtXQUPcHpsEZyLbIxQL67djAOa8PjvXy0m0mkEG/E4y5Amaushrk4kOjkAKmx22kOLHPJEwk8DsRSeGXzm+GyIYHxkucD/2hpsNZ7VnJrEqJa51cziCeiLCrULaT8j7246N1Bjxr9vgSiecAYJVyK0TpbE+JzBvd1AGi4SVRj2jQC7Yd9jmkwosQ73eidUI64ZRNMECSluc1CGIO4XqdoTenZOsSPufk6UkwBQfEyAH9vFUvFNG1wNDCQn8O/sMpCT7J+wVBacHn7gjOA== 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=4G9FeCj/qCuuqmejHrzare+CsP7uYt+VZW1xYj3TOqU=; b=IP2EWBdcM+RAqBIgALwmIteWsyouwoqiHVwecQba7mf/lP5rh9gCZyyef4IMBa4eBQLf+5D8I/eBQPjSjKHwSaOKNRyEQDlqRPbIH4A5BIjIasktVmXNeeuaNgcJ7phCY9xfYpy/cuM+7oFZ7XGY/12syGlx2uRiJoFXpnmmWbz4gb8t7ElUxl2OdpcAVY/ULK/C2yQoeVkidVL48puPStjCUdxRgcjL2/P/dLoCIV26HpRWtoSbKvQ+gAsIRqXu6tnCRWQHrVLOTkAYjfOT947zOmrTnj9w5ZImllIu95t+ysJD60qBybz7PQRh+GR4KlHQqnBzMvla3he35ciA1A== 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 AM6PR06MB6198.eurprd06.prod.outlook.com (2603:10a6:20b:ff::26) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.29; Mon, 4 May 2020 15:57:53 +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 15:57:53 +0000 From: Thorsten Altenkirch To: nicolai.kraus , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiX6KSAgAAZu8SAABAZAIAAE+UA Date: Mon, 4 May 2020 15:57:53 +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: 7b8c8acd-62b9-4a83-1ef4-08d7f043e75e x-ms-traffictypediagnostic: AM6PR06MB6198:|AM6PR06MB6198: x-ld-processed: 67bda7ee-fd80-41ef-ac91-358418290a1e,ExtAddr x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 03932714EB x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: AxGdjQAacVNRVroTJcLtH6FfsyGyecX+ofZSId2uuezoySwdflK8K6qGTQVmtSW0ff7RUhk0MexJS6uXDEbcZgNkQ5RSs1UKeeEqnjFe7+wmLMKAvFqlaOO0kBpfhjTtWFKEx5nagrecFnrZdNIFZQEV3Eryr1sgwosPgnMkeyVtDz7d2ugfQtjvv0j5vTTtJfbK3qO6U8cTe3TPWRcAFez4vk+68uAJj7ghfBzxq1yrmLv9CDnhqTIQkicj4gK3DvFKxsTD60T2pP0RJ/fMSFTg1HQ4Cwy6g+XTdvsgVj25TE2A/y2rJ9kCn/XjVOgTIV6W2JEr54sfSIPu1F1sF0FfT+Wl5nW3Qck5pDgSeY/z/w9Jt4q4AgOiFt89acUnuMPLqk6cjz3EUJRmbQKn5sK4VLh5OKOIqwymfapsIJ3aOHf9b+uL/gS5OPChPfeBrGnyrQ6SsJa7welZtkE9I7xGDAp+kOHSfEuc28l2LQqP1Bq0E5pzEU+kkpVDEhVp6LOQYb0NGWOgBkd3/3O/zw== 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)(396003)(366004)(346002)(136003)(39860400002)(186003)(86362001)(71200400001)(66574012)(66946007)(66446008)(64756008)(66556008)(66476007)(91956017)(76116006)(316002)(786003)(2906002)(110136005)(5660300002)(6512007)(9686003)(478600001)(55236004)(53546011)(966005)(6506007)(6486002)(26005)(36756003)(8676002)(8936002)(33656002);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: MOeT1zuSrw6yLxk40ywz3KBwZGErZD1SeciAh/2ime4MUhkXHXq6jv/uT8NiAV5kO8pUKdWFoN0ErYVCoTdR7FE0dwooV7/K4Ugdd9fvc7QYtzepXOHuk/1L/T9299qVoiPc0Jrp4pyEjWeSUoUHwPcXlmbm0qHFO18zuTgr6R+2Lzr3FMpyAz15rxT1CREiHKd0wFxseCPjO2n41sxvXiFTLqEcSs3PjR8N7yaeI5Yq70dp0/HzrKe4a4ngd5VIk0+JPQo8VnZMW7aKEyGIn6VnufDpL5Aj2g93yGwn380lKWxQTSvU0M47VMO6zzCb2uxeGv71qXPcELLpMG7/C7R2W+drN81UzS8c2TZuIiZ18ty5Elw9jrWuyB3vKP13F2KJSNg5iXGFgeM05pOwPXQ6X7MktBpK5FfDNnltKrsCEh87V/1xrXi6StE+0WW8kISc4BFDpg5GgEQIIItizVzwrLARERm31sJysjMcEdNNBl9x0IH27ZPneGr3Gkc0VRdimSjCT4kJsPninxKBhOOdyeN+X1jXCzyG3TdGT5msuv+1xOWl/kBIUOBtOn4MjhpusJ0KRuLOXETtPIys6lV0X9q3NLkhw/3lgZJ7GfzJxo8Cf8SYomF2kkvp4iaaZCD09z1ua2pjSb0uvogSmEuQeLIDIi0PodflYJXXq7JwuINr2HFi7+s63qm2rgSrM9ZkbIYE5E04z5gKsn1Wv4VSWiP8M/7Bs55ExYHZB3+hzGaZ/nExH4OICZ5L9yQe0Lf3h3VrJl3Bt0nJVMGZeSTUhp+O0Z7zMySoW8UM03c= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <4414CA6D8136F245...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 7b8c8acd-62b9-4a83-1ef4-08d7f043e75e X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 15:57:53.0855 (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: bTHaVIVT4guk5E6QTz7K70T64BE7WYhvbnd6V2f8UrPdmzBbzZDe01ZYw+21l7Wls+vvIEFDmo4mcDc3LQiWqiZTh1C1m3/HipYNhqgyzpP/rHkmEuEMyKF+yf6GXFt/ X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB6198 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 T2ssIEkgYXBvbG9naXplIGRpc2N1c3Npb25zIG9uIG5hbWVzIGFuZCBzeW50YXggYXJlIGF0IHRo ZSBzYW1lIHRpbWUgdmVyeSBhdHRyYWN0aXZlIGFuZCBhcmUgYWxzbyBzY29mZmVkIGF0IGJlY2F1 c2UgdGhleSBzZWVtIG5vdCB0byBoYXZlIG11Y2ggY29udGVudC4gDQoNCkkgYW0gcXVpdGUgaGFw cHkgd2l0aCBNaWtlJ3MgZXhwbGFuYXRpb24gdG8gdXNlIHRoZSB3b3JkICJpZGVudGlmaWNhdGlv bnMiIGZvciBpbmhhYml0YW50cyBvZiBlcXVhbGl0eSB0eXBlcy4gIlBhdGhzIiBvciAiZXF1YWxp dHkgcHJvb2ZzIiBvciAiZXZpZGVuY2UgZm9yIGVxdWFsaXR5IiBhcmUgYWxzbyBnb29kIGFsdGVy bmF0aXZlcy4NCg0KSG93ZXZlciwgSSBwcmVmZXIgdG8gdXNlIHRoZSB3b3JkICJlcXVhbGl0eSIg ZXZlbiBlcXVhbGl0eSBpcyBub3QgcHJvcG9zaXRpb25hbC4gVHdvIG1hdGhlbWF0aWNhbCBvYmpl Y3RzIHdoaWNoIHNoYXJlIGFsbCBwcm9wZXJ0aWVzIHdlIGNhbiB0YWxrIGFib3V0IHNob3VsZCBi ZSBjb25zaWRlcmVkIGVxdWFsIGV2ZW4gaWYgdGhlcmUgaXMgbW9yZSB0aGFuIG9uZSByZWFzb24g LyBwcm9vZiAvIGlkZW50aWZpY2F0aW9uIHRoYXQgdGhpcyBpcyB0aGUgY2FzZS4gTW9yZW92ZXIs IHRoZXJlIGlzIG5vIG90aGVyICJlcXVhbGl0eSIgd2UgY2FuIHRhbGsgYWJvdXQgaW4gVHlwZSBU aGVvcnkuDQoNClRob3JzdGVuDQoNCu+7v09uIDA0LzA1LzIwMjAsIDE2OjQ3LCAiaG9tb3RvcHl0 Li4uQGdvb2dsZWdyb3Vwcy5jb20gb24gYmVoYWxmIG9mIE5pY29sYWkgS3JhdXMiIDxob21vdG9w eXQuLi5AZ29vZ2xlZ3JvdXBzLmNvbSBvbiBiZWhhbGYgb2Ygbmljb2xhLi4uQGdtYWlsLmNvbT4g d3JvdGU6DQoNCiAgICBGb3Igd2hhdCBpdCdzIHdvcnRoLCAiaWRlbnRpZmljYXRpb24iIGlzIG11 Y2ggY2xvc2VyIHRvIFBlciBNYXJ0aW4tTMO2ZidzIA0KICAgIG9yaWdpbmFsIHRlcm1pbm9sb2d5 ICgiaWRlbnRpdHkgdHlwZSIpIHRoYW4gImVxdWFsaXR5IiBvciAicGF0aCIgYXJlLg0KICAgIE5p Y29sYWkNCg0KICAgIE9uIDA0LzA1LzIwMjAgMTU6NDgsIFN0ZWZhbiBNb25uaWVyIHdyb3RlOg0K ICAgID4+IEkgZG9uJ3QgdGhpbmsgdXNpbmcgImlkZW50aWZpY2F0aW9uIiBuZWNlc3NhcmlseSBp bXBsaWVzIGFueQ0KICAgID4+IGRpZmZlcmVuY2UgYmV0d2VlbiAiaWRlbnRpZmljYXRpb24iIGFu ZCAiZXF1YWxpdHkiLiAgSSBkb24ndCB0aGluayBvZg0KICAgID4+IGl0IHRoYXQgd2F5LiAgRm9y IG1lIHRoZSBwb2ludCBpcyBqdXN0IHRvIGhhdmUgYSB3b3JkIHRoYXQgcmVmZXJzIHRvDQogICAg Pj4gYW4gKmVsZW1lbnQqIG9mIGFuIGlkZW50aXR5IHR5cGUuICBDYWxsaW5nIGl0ICJhbiBlcXVh bGl0eSIgY2FuIGhhdmUNCiAgICA+PiB0aGUgd3JvbmcgY29ubm90YXRpb24gYmVjYXVzZSBjbGFz c2ljYWxseSwgYW4gZXF1YWxpdHkgaXMganVzdCBhDQogICAgPj4gcHJvcG9zaXRpb24gKG9yIGEg dHJ1ZSBwcm9wb3NpdGlvbiksIHdoZXJlYXMgYW4gZWxlbWVudCBvZiBhbiBpZGVudGl0eQ0KICAg ID4+IHR5cGUgY2FycmllcyBpbmZvcm1hdGlvbi4gIENhbGxpbmcgaXQgImFuIGlkZW50aWZpY2F0 aW9uIiBzdWdnZXN0cw0KICAgID4+IGV4YWN0bHkgdGhlIGluZm9ybWF0aW9uIHRoYXQgaXQgY2Fy cmllczogYSB3YXkgb2YgaWRlbnRpZnlpbmcgdHdvDQogICAgPj4gdGhpbmdzLg0KICAgID4gSSB0 aG91Z2h0IHRoYXQncyB3aGF0ICJwYXRoIiB3YXMgZm9yPw0KICAgID4NCiAgICA+DQogICAgPiAg ICAgICAgICBTdGVmYW4gIndobyByZWFsbHkgZG9lc24ndCBrbm93IHdoYXQgaGUncyB0YWxraW5n IGFib3V0Ig0KICAgID4NCg0KICAgIC0tIA0KICAgIFlvdSByZWNlaXZlZCB0aGlzIG1lc3NhZ2Ug YmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQgdG8gdGhlIEdvb2dsZSBHcm91cHMgIkhvbW90b3B5 IFR5cGUgVGhlb3J5IiBncm91cC4NCiAgICBUbyB1bnN1YnNjcmliZSBmcm9tIHRoaXMgZ3JvdXAg YW5kIHN0b3AgcmVjZWl2aW5nIGVtYWlscyBmcm9tIGl0LCBzZW5kIGFuIGVtYWlsIHRvIEhvbW90 b3B5VC4uLkBnb29nbGVncm91cHMuY29tLg0KICAgIFRvIHZpZXcgdGhpcyBkaXNjdXNzaW9uIG9u IHRoZSB3ZWIgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL21zZ2lkL0hvbW90b3B5 VHlwZVRoZW9yeS9iMWI1NTRiMS0xYzcwLTBiZDYtNWMwOS1jZDVmMGYyZTQ4ZjklNDBnbWFpbC5j b20uDQoNCgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNv bGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9y bWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFz ZSBjb250YWN0IHRoZSBzZW5kZXIgYW5kIGRlbGV0ZSB0aGUgZW1haWwgYW5kCmF0dGFjaG1lbnQu IAoKQW55IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieSB0aGUgYXV0aG9yIG9mIHRoaXMg ZW1haWwgZG8gbm90Cm5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRoZSBVbml2ZXJz aXR5IG9mIE5vdHRpbmdoYW0uIEVtYWlsCmNvbW11bmljYXRpb25zIHdpdGggdGhlIFVuaXZlcnNp dHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkIAp3aGVyZSBwZXJtaXR0ZWQgYnkgbGF3 LgoKCgoK