From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:4d07:: with SMTP id o7mr15132543wmh.59.1588591042791; Mon, 04 May 2020 04:17:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:bb42:: with SMTP id l63ls174192wmf.0.experimental-gmail; Mon, 04 May 2020 04:17:20 -0700 (PDT) X-Received: by 2002:a7b:c417:: with SMTP id k23mr14631954wmi.147.1588591040415; Mon, 04 May 2020 04:17:20 -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 71si1272509wmb.1.2020.05.04.04.17.20 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 04:17:20 -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 14EA02B7C72_EAFF9C0B for ; Mon, 4 May 2020 11:17:20 +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 C489230AA3E_EAFF9BFF for ; Mon, 4 May 2020 11:17:19 +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 1jVZ67-0002ku-8N; Mon, 04 May 2020 12:17:19 +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 12:17:19 +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 12:17:18 +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 12:17:18 +0100 Received: from EUR04-HE1-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 12:17:18 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=UFY15gi3Lgo6HsK3D385ecBoeAo3oHlS9HNxWbjF93RKda0YAb37GjqCiXsiIIr9gMFPQRyxyu0GwaiO8odFNA6GEOUUYnUUOuY/rzT8IuO4HbFumw7EATCZNJahk2FZ+ExABF30Us5RWLyYYypjI8iSd38txROzg2Ay1mGIhK0VwY2NwKeglqMJ6nzEXaDB1Mfg3tHV/p0JttBiYVihoxtgQi9yNtt+nRekUt7E9baYiXmeY9c44D1HK1tSYPEl33q2l3Id25SgAmeSM83qYLxGaX+UA4+6ynqMmW1Abeg8ppktAYC92Qbzrb+uGb1tvXq1xPCCtQdAY5dZKkam8w== 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=AbPWeWrp6Mq6d7W99E/AkbDOb7gL4YhhfuhD6dwDRBs=; b=FOOnvOsisUGSL1uU9Z5QHanYXHA/DsT7HWjBd94H4j2sQDDH9vlvb5sSXR8puE4btTBPsKP+/R7/wCDGCM5AoAqexkymjBl5/bLqCP1CAhnlfeu6rVLPqC24EQAAI33NbyVWkua73h9cmu2fiiv0/RQuHIvAK0VbCFMp7qf7oD74cn60I25vxGJoIMk8DALFUvdpb7JbXEy1k+vM4vPIV5gCcpABnB0PXL+8Y7qa2eUgp3AUmfmFGr0tn/gLRiXBsZ3ojFqqoXb+sX4Q0E9ZWDgtFpMDOXApCxLkDP2mVHq+DkAC7/Wkb/pFw/euT3/aa/jqDPAbewNsfcRy81B6FQ== 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 AM6PR06MB4567.eurprd06.prod.outlook.com (2603:10a6:20b:63::17) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2958.27; Mon, 4 May 2020 11:17:17 +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 11:17:17 +0000 From: Thorsten Altenkirch To: "stre...@mathematik.tu-darmstadt.de" CC: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiXwjoAgAAVvQA= Date: Mon, 4 May 2020 11:17:17 +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: 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: 8c7c84be-458e-440c-5276-08d7f01cb4bd x-ms-traffictypediagnostic: AM6PR06MB4567: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8882; x-forefront-prvs: 03932714EB x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: r9cH/Qkwa9sDX2dE5c/51z28rJbqbUxI2f+Uvjpf7Z2oDDmd21UBXDA8qApx8YnBkpHSEzWl3YruFEyUnINDP+TYlqHsOeOm7eu9zteW9Tyt1wx32TRgC3hsxYn3oSp6Z2w9+acjwrMl68Pe8oeswGRNbQKrhWuDbeOaZEZRg9p/vtlKeDTJqSSKSPdgJyBSus3ppxbyqb9sSHExyT3lMxcmpf5PWS1OIOqSLbhJV5rb2LnH11CXGUriX5REKinQtEZRDb/gmTKFlDZWF+csDOtTLnUKfnKqx4jVYPXAHu7ebb5gSZDqDmG6l5bx4lSpgZ4FXmXPSe3t/j1XX/nB638pz/6Ir0fPrJJvxv2f1BuqUrqDxYvR28qmBFuMCRSh63yXW030GKJuVGBnIcVK+BTMRINpDTPrNfsjwzd2/DtuvSHgZcy+/YhadW05SlJ4 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)(39860400002)(136003)(376002)(396003)(366004)(478600001)(6486002)(5660300002)(786003)(8936002)(316002)(6916009)(9686003)(33656002)(6512007)(66946007)(76116006)(91956017)(2906002)(4326008)(71200400001)(8676002)(55236004)(53546011)(6506007)(86362001)(186003)(26005)(66476007)(66556008)(64756008)(66446008)(36756003);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: GUxeU8XTalD5cmL7pNUboG7mERlTC6O3RXZbLIva441ZqQswu7yQ7/tuZs1patV/mZMtc+8XhFzvKMcxfmiuJeLejwDVdoIpnW4aiV/lIB4/Yu2rc09azA8MR+/uR53GPZ8x6O3j4mMOPdmBRaZxjhLHXGO1jEWu0cQT07yDs2V4x9FeQWC74nBx7TUv6zcjnON1AMaTW5FOwstf3vXYthfFZFGDnJIAU+miWkPzugkIFoXq9Xxuep8bp6l2NvO89uLaHywodkrfswqT3X2rbzcEY0wrmQv8IKiFAOackYc94z2k1ZR0vGuM2+XTf8F8Uhv1Jiycfs4FWuWCtaTRFFauFjx9FsBQgduzBxHKtf5IT+Ub3c5Nb8rcqkdwoWvp0i5vYi1N+ESzWWyVq2Y+b8dH5xx3oHUoFhiTY654rnraFdfZiE0qjwyGmLYOfL+MAhA7XsnaHN6fKGAz2IASVoDzT9e2oqDO5fwbp0iRnoxlvjS5eoJQsDA6WNhPdGZ5H+po9+Nq+6/7ZDZ3PTBAFVxaKKxtMeQHO+rcsjF5/SjUhQgUHFE4bCyKwFAt82gi5PKbrauM/R0iR8SeWbv6et23n5OT+AgBYrGqOSKjR8I+uEP6ZeRLQON+cx1D+qNroD0L6143PVzVgj+yMBBKtV3VULkeTzJsJf5M5aKlu3oSrvDNavu91KbLD9r/WryOsAGT7ydNz4VV9MBNlVjaLKFUtE1qbZ98Fo4qQASsgcUolkf+eMO4XYZacPjVTAKzALE0gxlo6DB/iZLJ3zJ5zbFM1J+kOuq8PUI10WpU2Sg= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <1CB04E1C7728AF40...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 8c7c84be-458e-440c-5276-08d7f01cb4bd X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 11:17:17.7032 (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: kfYNhHilxPz1LRz95Y4BexkBEMMDdiUwuOEO0WxCLH0O4rCZlKGIVIFxm6dfxzLPSEUrtmu5AzPKuG7M/RhstQupb9gOcujKYOcpXc1hB3Yxz7g/nj69qId1oh9kdOj2 X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB4567 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 T24gMDQvMDUvMjAyMCwgMTI6MDAsICJzdHJlLi4uQG1hdGhlbWF0aWsudHUtZGFybXN0YWR0LmRl IiA8c3RyZS4uLkBtYXRoZW1hdGlrLnR1LWRhcm1zdGFkdC5kZT4gd3JvdGU6DQoNCiAgICA+IEkg YW0ganVzdCByZWFkaW5nIGEgcGFwZXIgd2hpY2ggdXNlcyB0aGUgd29yZCDDouKCrMWTSWRlbnRp ZmljYXRpb27DouKCrMKdIGluc3RlYWQNCiAgICA+IG9mIGVxdWFsaXR5LiBJIHRoaW5rIHRoaXMg aGFzIGJlZW4gcHJvcG9zZWQgYnkgQm9iIEhhcnBlci4gQ2FuIGFueWJvZHkNCiAgICA+IGVubGln aHRlbiBtZSB3aGF0IGlzIHRoZSBkaWZmZXJlbmNlIGJldHdlZW4gaWRlbnRpZmljYXRpb25zIGFu ZCBlcXVhbGl0eT8NCiAgICA+IE1heWJlIHRoZXJlIGlzIGFuIGlkZW50aWZpY2F0aW9uIGJldHdl ZW4gdGhlbSBidXQgdGhleSBhcmUgbm90IGVxdWFsPyBBcmUNCiAgICA+IHRoZSByZWFsIG51bWJl cnMgMC45OTnDouKCrMKmIGlkZW50aWZpZWQgb3IgYXJlIHRoZXkgZXF1YWw/DQoNCiAgICBZb3Ug bWF5IGlkZW50aWZ5IHRoaW5ncyB3aGljaCBhcmUgbm90IGVxdWFsLg0KDQpIZW5jZSBteSBxdWVz dGlvbiB3ZXRoZXIgMC45OTkuLi4gYW5kIDEgYXJlIGVxdWFsIG9yIGlkZW50aWZpZWQuIA0KDQpN eSB1bmRlcnN0YW5kaW5nIGlzIHRoYXQgMC45OTkuLi4gYW5kIDEgYXMgcmVhbCBudW1iZXJzIGFy ZSBlcXVhbC4gVGhhdCBpcyB3aGF0IHdlIG1lYW4gYnkgZXF1YWxpdHkgaW4gTWF0aGVtYXRpY3Mu IFRoZSBkaWZmZXJlbmNlIHdoaWNoIGlzIGludHJvZHVjZWQgaGVyZSBpcyBpbnRlbnNpb25hbCBh bmQgZG9lc24ndCBtYWtlIGFueSBzZW5zZS4gV2UgbWF5IGV2ZW4gYXNrIHdoZXRoZXIgMysxIGFu ZCA0IGFyZSBpZGVudGlmaWVkIG9yIGVxdWFsPw0KDQogICBTbyAnJ2lkZW50aWZ5Jycgc2VlbXMg dG8gbWVhbg0KICAgIGNvbnNpZGVyIGFzIGVxdWFsLg0KICAgIEluIGEgc2Vuc2UgdGhpcyBpcyB2 ZXJ5IGRlc2NyaXB0aXZlIGZvciB3aGF0IGlzIGdvaW5nIG9uIGluIEhvVFQgd2hlcmUgb25lDQog ICAgbmV2ZXIgcGVyZm9ybXMgcXVvdGllbnRzIGJ1dCByYXRoZXIgd2lkZW5zIGVxdWl2YWxlbmNl IHJlbGF0aW9ucy4NCg0KSSBkb24ndCB1bmRlcnN0YW5kIHRoaXMuIFN1cmVseSB3ZSBxdW90aWVu dCBpbiBIb1RUIGV2ZW4gdGhvdWdoIHRoZSBub3Rpb24gb2YgYSBISVQgb3IgZXZlbiBhIFFJVCAo aS5lLiBhIHNldCBsZXZlbCBISVQpIGFyZSBtb3JlIGdlbmVyYWwgdGhhbiBvcmRpbmFyeSBzZXQt cXVvdGllbnRzLg0KDQogICAgVGhpcyBpcyByZWFsbHkgZGlmZmVyZW50IGluIHRoZSByZXNwZWN0 aXZlIHRvcG9zIG1vZGVscyBhcyBlZyBzaW1wbGljaWFsDQogICAgc2V0cyBvciBhbHJlYWR5IHRo ZSB0b3BvcyBvZiByZWZsZXhpdmUgZ3JhcGhzIGFzIGV4ZW1wbGlmaWVkIGJ5IE4uIEtyYXVzJ3MN CiAgICBwdXp6bGluZyBjb3VudGVyZXhhbXBsZS4NCg0KV2hhdCBwdXp6bGluZyBjb3VudGVyZXhh bXBsZSBpcyB0aGlzPw0KDQpUaG9yc3Rlbg0KDQrvu79PbiAwNC8wNS8yMDIwLCAxMjowMCwgInN0 cmUuLi5AbWF0aGVtYXRpay50dS1kYXJtc3RhZHQuZGUiIDxzdHJlLi4uQG1hdGhlbWF0aWsudHUt ZGFybXN0YWR0LmRlPiB3cm90ZToNCg0KICAgID4gSSBhbSBqdXN0IHJlYWRpbmcgYSBwYXBlciB3 aGljaCB1c2VzIHRoZSB3b3JkIMOi4oKsxZNJZGVudGlmaWNhdGlvbsOi4oKswp0gaW5zdGVhZA0K ICAgID4gb2YgZXF1YWxpdHkuIEkgdGhpbmsgdGhpcyBoYXMgYmVlbiBwcm9wb3NlZCBieSBCb2Ig SGFycGVyLiBDYW4gYW55Ym9keQ0KICAgID4gZW5saWdodGVuIG1lIHdoYXQgaXMgdGhlIGRpZmZl cmVuY2UgYmV0d2VlbiBpZGVudGlmaWNhdGlvbnMgYW5kIGVxdWFsaXR5Pw0KICAgID4gTWF5YmUg dGhlcmUgaXMgYW4gaWRlbnRpZmljYXRpb24gYmV0d2VlbiB0aGVtIGJ1dCB0aGV5IGFyZSBub3Qg ZXF1YWw/IEFyZQ0KICAgID4gdGhlIHJlYWwgbnVtYmVycyAwLjk5OcOi4oKswqYgaWRlbnRpZmll ZCBvciBhcmUgdGhleSBlcXVhbD8NCg0KICAgIFlvdSBtYXkgaWRlbnRpZnkgdGhpbmdzIHdoaWNo IGFyZSBub3QgZXF1YWwuIFNvICcnaWRlbnRpZnknJyBzZWVtcyB0byBtZWFuDQogICAgY29uc2lk ZXIgYXMgZXF1YWwuDQogICAgSW4gYSBzZW5zZSB0aGlzIGlzIHZlcnkgZGVzY3JpcHRpdmUgZm9y IHdoYXQgaXMgZ29pbmcgb24gaW4gSG9UVCB3aGVyZSBvbmUNCiAgICBuZXZlciBwZXJmb3JtcyBx dW90aWVudHMgYnV0IHJhdGhlciB3aWRlbnMgZXF1aXZhbGVuY2UgcmVsYXRpb25zLg0KICAgIFRo aXMgaXMgcmVhbGx5IGRpZmZlcmVudCBpbiB0aGUgcmVzcGVjdGl2ZSB0b3BvcyBtb2RlbHMgYXMg ZWcgc2ltcGxpY2lhbA0KICAgIHNldHMgb3IgYWxyZWFkeSB0aGUgdG9wb3Mgb2YgcmVmbGV4aXZl IGdyYXBocyBhcyBleGVtcGxpZmllZCBieSBOLiBLcmF1cydzDQogICAgcHV6emxpbmcgY291bnRl cmV4YW1wbGUuDQoNCiAgICBUaG9tYXMNCg0KDQoKCgpUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRh Y2htZW50IGFyZSBpbnRlbmRlZCBzb2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUKYW5kIG1heSBjb250 YWluIGNvbmZpZGVudGlhbCBpbmZvcm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcwpt ZXNzYWdlIGluIGVycm9yLCBwbGVhc2UgY29udGFjdCB0aGUgc2VuZGVyIGFuZCBkZWxldGUgdGhl IGVtYWlsIGFuZAphdHRhY2htZW50LiAKCkFueSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQg YnkgdGhlIGF1dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdApuZWNlc3NhcmlseSByZWZsZWN0IHRo ZSB2aWV3cyBvZiB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLiBFbWFpbApjb21tdW5pY2F0 aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCAK d2hlcmUgcGVybWl0dGVkIGJ5IGxhdy4KCgoKCg==