From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a50:a7e4:: with SMTP id i91mr13802785edc.381.1588594329630; Mon, 04 May 2020 05:12:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:d1da:: with SMTP id bs26ls6138137ejb.10.gmail; Mon, 04 May 2020 05:12:07 -0700 (PDT) X-Received: by 2002:a17:906:d143:: with SMTP id br3mr14739122ejb.348.1588594327752; Mon, 04 May 2020 05:12:07 -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 a3si585599edn.1.2020.05.04.05.12.07 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 05:12:07 -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 3ECBA3C3A89_EB00697B for ; Mon, 4 May 2020 12:12:07 +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 uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id CC6EB3C3A70_EB00696F for ; Mon, 4 May 2020 12:12:06 +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 1jVZx8-0007Ao-4m; Mon, 04 May 2020 13:12:06 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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 13:12:05 +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 13:12:05 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.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_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Mon, 4 May 2020 13:12:05 +0100 Received: from EUR01-VE1-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 13:12:05 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=HT3H5ky0eAZ09vj5R4gayWY5qZqrnh8Jm7o7K5H/ReqQ++e5N6ezLRuTtVkEWeiqXMWT46v/YHZ6AX3JDBU1I4mGTcxWa58IkqtTEa7JXkvwDAd4m17ixpPQoHqKveV8joFa6i0Q4soN4Aui0f0DQER/YEYKzo0/e5QoHrMhUZDRFNUg/RacG9ELDk++Xz22mDB+/dUZMwOQN6dlxOtSgN3iuxEyBW6uccNhjtUP983pmNW8N+0mZrmtEVebbcsWsuJV6QBct3eZPUoLMLAg9BcrVcPwD+scurVK7DbhMESvYfQqzqG07wdMzHdZh+SwrHtvmHR6MWTmzzEi5kHEjw== 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=UVwz6uc2+7OsVqQfqxUsvylvL5DuzlCA4caWrsOE3h4=; b=mH9zEl+vmPJyuXoKZWD5uBXmBsY9ttqkSQz21XN2AL9dEt7vQSMKYIECUwsPSCC8g6XAItLniAipIu7LlYP1+ik+9/tL9//yi7lPpUT6Mr88vP+SznWwIE/7DYsi5xFGmffQrQhoK6BxEYqfpXGwehG0vTBHS0JmRagJ3XJzHYebL+0GIujODHvUurFCPLoK5WMrx0LLHbWSx0g23jPwfxhPdtC4lf/qE78eNyNk0dJA2vfCz1No+zXmGRDsNQxpM2ZHaoZScZA1BrFahyLJAYy6UR1+ATv4cZBQXmdiUzMJXYSVuJ55O/H3ekV3PmBQZUaRvDNcskVl0dkLOJ2sQw== 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 AM6PR06MB4520.eurprd06.prod.outlook.com (2603:10a6:20b:3c::17) 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 12:12:04 +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 12:12:04 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiXwjoAgAAVvQD///zyAIAAElyA Date: Mon, 4 May 2020 12:12:04 +0000 Message-ID: <31C5A7B0-8512-4ABD-8DAA-EF3A1FA0EEFF@nottingham.ac.uk> References: <20200504120620.GA14623@mathematik.tu-darmstadt.de> In-Reply-To: <20200504120620.GA14623@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: e2ff0c39-f3ed-437d-d1e8-08d7f0245bcb x-ms-traffictypediagnostic: AM6PR06MB4520: 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: Q06DtFmwqMfsZjTbnGrflXTqLNG/8jhAoMO/HLYIEtbfQFZYG128HQ2zZ8pdlaAMYVA+AZhevt+CxLejqe8MYzWse/EivuqkoTUPnNCxB9kryLq6eGUoVmEIL/iqQOC18VExtFGVHc3VfspAAZzNIUs4kxEhQWJiEQsrweE/YF6/AcyGkY2ltRDJxBOmCE4cOtDQvvLvb+3M2aK/AtDPxbhwUmG3j3nY+sWeR7HyqsLE3ECWZqo6scd1zJBmd5NCRsoVb5a6oZnmFvekJZJAt/SwNSIt4KLdLgF2wsTffJ3uCEuWi2N+pBgaIpbNKQYIwcD4SQRaerA9C5FqFP/9YWsvq9SzSpPXpi8T7rEvk3ayeeHUY5jt1rdoYTvsfIR10oBwq5/Z7n5nSKMqOKca8CbmWG1FMWOwmYQSH0pUwT+ZZwB6g2ncs9mqqkGpkogAzJ1t8vY8L6+tZhFBVW8wjLOnTEAwT8ikJMLolhrytlwCNalr4xvCNVkmCepxWtY3We2+gIiZBb9YZGDzx2hE/w== 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)(346002)(396003)(376002)(39860400002)(136003)(76116006)(91956017)(66946007)(8936002)(5660300002)(66446008)(83080400001)(66476007)(66556008)(64756008)(6506007)(55236004)(86362001)(8676002)(2906002)(36756003)(33656002)(6512007)(9686003)(966005)(478600001)(71200400001)(26005)(786003)(6486002)(316002)(186003)(4326008)(6916009);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: C1c6GTKGpLcj4J1QJZsQyHQC0Gc+ds7Q2PHyHgQjTi6/HJNW/+fX7CSnFpCoAfEjUkn6RXpGRbwTPbYCNKBZrRhzZKmVUMNC178ld45042WPDCCp0CzkBvilH+L+tYA/Z81s9z6DLyOmowBLlkVoTy8M5kmZpglSHQYer+Zz2ZEHZx9SQgveKsffuZeuxqKpJKp390JwY21T0TwEEL+hTh+dbok5eqEG9DPJfm8HbM8+kHAgav9H3Rx8x6XxPkhKqbLuhEbY95O99nkwkgPoiwu/ys6sRcBd887KF49wM6eNX7a5nDufdmqIsl2JHIJiLWpoj/mHifM+vjxhkt1WkRYyvaw5sT0EWqeODLJnd7d/byecGQ5RxOewiAuEpzQLD1n4szvUURJc0+mHvEPgEEh6CH0J3d5b7fgofAWJl5aAQy/hmXRcbcaWd3QATHB7k/okcfkzEhbys+RmBpOmnHy9vOCZxUGVob3xwP9KZglmfdVlfAHADP4367Vn2oIVYHgVtIlrBagJ1I16Ss7CmKq2ITdT5Qih685GEnxyHtU8jwPbb6dBNEmdtN8fbtIAC/gpXSNhjoEJyXd6ICMWZAMaufKLWRWY05+c4xwRjL3BjT+WTk9sTH5eHCAjHXBvdVkLLyqu4hKuQaKQrV7oSruY/0q/i588CLwSE0NyPyUklbC/PXpR4kP1JxBXcm/LOLdgML719wpfDMI/TBAdDbEdEldQDQnxC/uS+JitWlwgVbmMeue7rMNVVdC7Ju2qwqULHi+KCjt1tN1KVzaRZjmBBrAsLzLaAlfjxJ3u+YE= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <33CDC6F71854224C...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: e2ff0c39-f3ed-437d-d1e8-08d7f0245bcb X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 12:12:04.4768 (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: ZiC5llksED7BIjAe4PgFL1TrDvrByoE/BP5Nv7/hjoUaWcXwuY8+aPQggz14XXpMb1lGm2ptFNGDtuVRfTv5Lmj3LFF5nGp7emm4bj7RTfLDe0PwCq4LBkZHoREIVKEr X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB4520 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 SGkgVGhvbWFzDQoNCkJ1dCBJIGFtIG5vdCAiaW50ZXJwcmV0aW5nIEhvVFQgaW4gU1NldCIuIEkg YW0ganVzdCB3b3JraW5nIGluIEhvVFQuIFlvdSBhcmUgZG9pbmcgTWV0YW1hdGhlbWF0aWNzLCBJ IGFtIGp1c3QgdGFsa2luZyBhYm91dCBNYXRoZW1hdGljcy4NCg0KU3VyZSB3aGVuIHlvdSBjb25z aWRlciBtb2RlbHMgb2YgeW91ciB0aGVvcnkgeW91IGNhbiBzYXkgdGhhdCBjZXJ0YWluIGVxdWFs aXRpZXMgYXJlIGp1c3QgbWV0YXRoZW9yZXRpYyBlcXVhbGl0aWVzIGFuZCBvdGhlcnMgYXJlIG5v bi10cml2aWFsIGVxdWFsaXRpZXMuIA0KDQpEbyB5b3UgdGhpbmsgb2YgYSBtb2RlbCBvZiBzZXQg dGhlb3J5IHdoZW4geW91IGRvIHNldCB0aGVvcnk/DQoNCkNoZWVycywNClRob3JzdGVuDQoNCu+7 v09uIDA0LzA1LzIwMjAsIDEzOjA2LCAiVGhvbWFzIFN0cmVpY2hlciIgPHN0cmUuLi5AbWF0aGVt YXRpay50dS1kYXJtc3RhZHQuZGU+IHdyb3RlOg0KDQogICAgSGkgVGhvcnN0ZW4sDQoNCiAgICA+ ICAgICBUaGlzIGlzIHJlYWxseSBkaWZmZXJlbnQgaW4gdGhlIHJlc3BlY3RpdmUgdG9wb3MgbW9k ZWxzIGFzIGVnIHNpbXBsaWNpYWwNCiAgICA+ICAgICBzZXRzIG9yIGFscmVhZHkgdGhlIHRvcG9z IG9mIHJlZmxleGl2ZSBncmFwaHMgYXMgZXhlbXBsaWZpZWQgYnkgTi4gS3JhdXMncw0KICAgID4g ICAgIHB1enpsaW5nIGNvdW50ZXJleGFtcGxlLg0KICAgID4gDQogICAgPiBXaGF0IHB1enpsaW5n IGNvdW50ZXJleGFtcGxlIGlzIHRoaXM/DQoNCiAgICBJIGxlYXJudCBpdCBmcm9tIE5pY29sYWkg d2hlbiBoZSBnYXZlIGEgbGl0dGxlIHRhbGsgYXQgQ1NMIDIwMTcgd2hlbg0KICAgIGdpdmVuIGEg cHJpemUgZm9yIGhpcyB0aGVzaXMuDQogICAgVGhlIGNvdW50ZXJleGFtcGxlIG9yIHJhdGhlciBt eSBhcHByZWNpYXRpb24gb2YgaXQgSSBoYXZlIG1hZGUgYSBsaXR0bGUgbm90ZQ0KICAgIG9uIHdo aWNoIEkgaGF2ZSBwdXQgZm9yIGNvbnZlbmllbmNlIGF0DQogICAgaHR0cHM6Ly93d3cubWF0aGVt YXRpay50dS1kYXJtc3RhZHQuZGUvfnN0cmVpY2hlci9rcmF1cy5wZGYNCg0KICAgIFRoZSBwb2lu dCBpcyB0aGF0IGludGVycHJldGluZyBIb1RUIGluIHNTZXQgaXMgdmVyeSBkaWZmZXJlbnQgZnJv bSB0aGUNCiAgICB0cmFkaXRpb25hbCBpbnRlcnByZXRhdGlvbiBvZiBsb2dpYyBpbiBzU2V0LiBU aGUgc2FtZSBoYXBwZW5zIGFscmVhZHkNCiAgICB0aGUgdG9wb3Mgb2YgcmVmbGV4aXZlIGdyYXBo cy4gUHJvcG9zaXRpb25zIGFyZSBjb25uZWN0ZWQgcmVmbGV4aXZlDQogICAgZ3JhcGhzIGFuZCB0 aGVlIGFyZSB2ZXJ5IG1hbiBub25pc29tb3JwaGljIHN1Y2ggZ3V5cyBidXQgSG9UVA0KICAgIGlk ZW50aWZpZXMgdGhlbSBhbGwuDQoNCiAgICBCdXQgdGhpcyBoYXMgbm90aGluZyB0byBkbyB3aXRo IEhvVFQgcGVyIHNlLiBGb3IgZXhhbXBsZSB5b3UgY2FuDQogICAgaW50ZXJwcmV0IEhPTCBpbiBh c3NlbWJsaWVzIGluIHR3byB2ZXJ5IGRpZmZlcmVudCB3YXlzIG9uY2UgYGEgbGENCiAgICB0b3Bv cyAocHJvb2YgaXJyZWxldmFudCkgYW5kIG9uY2UgYGEgbGEgIG1vZGVsIG9mIFRUIChwcm9vZiBy ZWxldmFudCkuDQoNCiAgICBJbiBtYXRoZW1hdGljcyBlcXVhbGl0eSBpcyBhIHZlcnkgcmVsYXRp dmUgbm90aW9uLiBCdXQgb25lIG1heSBwZXJmb3JtDQogICAgcXVvdGllbnRzIHRvIHJlY29uY2ls ZSB0aGVtLi4uDQoNCiAgICBUaG9tYXMNCg0KCgoKVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNo bWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2VlCmFuZCBtYXkgY29udGFp biBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJlY2VpdmVkIHRoaXMKbWVz c2FnZSBpbiBlcnJvciwgcGxlYXNlIGNvbnRhY3QgdGhlIHNlbmRlciBhbmQgZGVsZXRlIHRoZSBl bWFpbCBhbmQKYXR0YWNobWVudC4gCgpBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5 IHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QKbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUg dmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4gRW1haWwKY29tbXVuaWNhdGlv bnMgd2l0aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgCndo ZXJlIHBlcm1pdHRlZCBieSBsYXcuCgoKCgo=