From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:e9cf:: with SMTP id l15mr115037wrn.166.1588593866792; Mon, 04 May 2020 05:04:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7ec2:: with SMTP id z185ls17960985wmc.1.canary-gmail; Mon, 04 May 2020 05:04:25 -0700 (PDT) X-Received: by 2002:a7b:cf25:: with SMTP id m5mr15423703wmg.65.1588593865223; Mon, 04 May 2020 05:04:25 -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 q17si538663wmg.1.2020.05.04.05.04.25 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 05:04:25 -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 EC8686D13DA_EB004C8B for ; Mon, 4 May 2020 12:04:24 +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 uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id A0F02724A99_EB004C8F for ; Mon, 4 May 2020 12:04:24 +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 1jVZpe-0008MG-EP for homotopyt...@googlegroups.com; Mon, 04 May 2020 13:04:24 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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:04:22 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) 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:04:22 +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 13:04:22 +0100 Received: from EUR04-DB3-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:04:21 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=S75KdOcAZRJfvdR3IBNDbI1+OFnm+oRnlZ24UMOFrvnEICu8+H4+bEKpROJciEL65/ASkBGnP6R/1PVGG4M/lh0Zmo8MOmFScyuS5A4Gg9G+JX9sKmEDz7TQwceArVOTSgN3PNLtmdEpmRIBVuJQU3w0sZUaj0okbQX9Istuw5MvnroMuWADjkY5mybYr+O4F2hIIuJ4fXXxc5hHy/+mkPdpUlhmdcSaKA3wA/M/GhzK5QZBiRCMhJNeKNXAkxf+zH1zT74RU4oZQe/8HoGlY4STIWKXA12UB17v/UBlgVYC1//3lxZc+TOLjkfqjObwdp8lWw1OwhqLUJjprIAFcQ== 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=eRahVSfE9HASGJJnJ9Xs2NNumuZZufGvaE57havaYRs=; b=j49sheHDjpuY5+pX8BLJHp0T+rkuIh/wByQ6aYKPv7h/kHpH2yPehzI6w93sroqf0G0UypRa+9WpNMBzNvHaE4v8t8VKGegXQ0P5PphQnvSXIyfIX0JFZTarRkVRcZL9oouQbx+Bpsponm5P/5g28ufxn6d3sa42xhmyYMhyFpHTWm3fLosnPdiJogxJSp5zFw5unE21Bgm2Kbh0ovAcakNoBMSTjdZjp76sGanN1k6kOz/DxXCr8nhdiFMCYCYfbl4+Uj1F8+2UzMgmTZ8fuPawzym4OsZNM1gs9GnlzQwLCj/dZ37kX3PYVfoafb1piwcmoFr4M4TkOoW+SXaslw== 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 AM6PR06MB4470.eurprd06.prod.outlook.com (2603:10a6:20b:9::10) 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 12:04:20 +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:04:20 +0000 From: Thorsten Altenkirch To: nicolai.kraus , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIfdkjXqlf/k7YUmG/+lTb1bxCKiXwjoAgAAVvQD///ZFgIAAFt8A Date: Mon, 4 May 2020 12:04:20 +0000 Message-ID: <2538F5D2-B963-4695-B5F3-610C0FCEC4B4@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: 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: 400ed569-90c2-4393-057c-08d7f0234730 x-ms-traffictypediagnostic: AM6PR06MB4470:|AM6PR06MB4470: x-ld-processed: 67bda7ee-fd80-41ef-ac91-358418290a1e,ExtAddr x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:6430; x-forefront-prvs: 03932714EB x-ms-exchange-senderadcheck: 1 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: b6kNLUdY3LmuzXbZJJOF5kNubksyEfzdobC3yCp6x1aOUpFiC35s+67JxRHZEJyJJfr7slUxquKjPw8riB1oirc934aJPZDvZ5kbDvbV28WDvLzgsSeU1c3Co9l3d+waJo08xWyS8BuPJtDL93aeJi7c3MOsztnPGMOeY4RzkoGHQhsoLAYUKWqDHdeN/QqDBtax4wV2aqRRuJLycdxVhU7f1KUtox/gELh7spN3q45dMZm5C0NiAJmQFd5cSQ/AurI9+1tP7RlDkLNfw8KMUInjHEe/x/PUjcYP6i4Q+Bt1ytSe779j59ZRoOZc27EgPKbIfCm4B/MwNWNTjFQlyyIIZieWQOvf0x7tp0PBz3oODpGB9JhEg/81ZsQbNndBXyANxe9/4X2xTStyf1L/7PtiO7fE1o+IILyvjROwuHeAEgclXx6LHKiwW5qjIwCxoHrIZkND/5h1MHqyiSb1SSPm1nsbeMVztZ7vY3tf1bYoaD5DXAxjuDfZDVtsdaehk+dtlXl4iUs4yRfN5+3qZA== 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)(366004)(396003)(376002)(136003)(39860400002)(53546011)(71200400001)(8936002)(5660300002)(2906002)(8676002)(86362001)(36756003)(26005)(64756008)(66556008)(66446008)(33656002)(9686003)(478600001)(6512007)(6506007)(66574012)(55236004)(966005)(186003)(786003)(316002)(110136005)(6486002)(66476007)(66946007)(91956017)(76116006);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata: C+I9p1ky5Xl4r3QLk086pkTNvHxSZbW+Wiq8sscsSd+81Efdow0JixvjGgL9NUtAJQ21y+gMKWU/V0rB+RDpffQQiLCNd3y9Cdyht++xIQ6Vhtz2Nhkk7KRWDLNQQ/DdZ1EFU+iwRAIrToNxPwryqHL/ZRUurRADZxIjCGq87oz3gO9RXjaeTqRXzK8RtlG9oDpognSIfr4XmD44LJRjo3O5MvME21DkBOwxzCD8gEvc4IzUcy4+twL7xV9cHgIKRX2vxOO39UP6aI3ZRa/qC8/OI3gzaTAQ9Lb88mnJcp7BddsTijtUBXTJ449eEjU8WltW9yyBV1espktsY3+zyQMmkdYLSoHVoS+zIiPDmydcRqj6cAFu/dQjOgA6QIDlxIoSuFqbVe8HvQwrExHfGI1hFYgA3EsHXF8Qdukwn615Akcj9qaSYqqA4WhQlZpGt5mI236MjL1/kXkKPOOIHXz6EY0ddgiZp3limXb5g6DCNXuLGTsnj32QlXWLFiIGHoCe/b/4eZlDqoTg335jOZ6Cxw3DgN5wk2ayycnzqdBbBgp59m1c1yeXru2hTLUWp2aQcoGbAwcxYk4y7b+inC9jCRRVra4lukNmceiMpHOPwL6uAdD2bcdKp4o+EaTSAcyzh39xTMJEq9lwvBzSLSRy3CW5bHRp61XEIRGaa8ObI/VoaJnlVSxKOoVSHZm7mvFnowQgE2CCP4iIb1i3O816YZ1DCPCTUR5ZLXMLryISBQ/YfkWoU40TY2N+NCAlAKutf9GKDtlH+Ps4LElBQtF2JAa2esHL3ZKxkI4tO8E= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="utf-8" Content-ID: <02594452D97C2F47...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 400ed569-90c2-4393-057c-08d7f0234730 X-MS-Exchange-CrossTenant-originalarrivaltime: 04 May 2020 12:04:20.3636 (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: hUW3GeN2ZCE6KxvmnhOHEzWV70Wz5jUNzm9zQngkqY12QgEsD+TuxIYozatK9kvph6yRpb12FC48lW69YIea9ItayQa8aNIQllBrLHrcaMnB3rFn7wqJd7iv8rMpxYYS X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM6PR06MB4470 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 SSBhbHdheXMgdGhvdWdodCB0aGF0IHRoZSAibWFnaWMgdHJpY2siIHdvdWxkIGp1c3QgY2F1c2Ug Y29uZnVzaW9uLiANCg0KSXQgaXMgaW1wb3J0YW50IHRvIGRpc3Rpbmd1aXNoIHdoZXRoZXIgd2Ug dGFsayBhYm91dCBNYXRoZW1hdGljcyBvciB3aGV0aGVyIHdlIGRvIE1hdGhlbWF0aWNzLiBUaGUg bWFnaWMgdHJpY2sgZXhhbXBsZSB3b3JrcyBiZWNhdXNlIHdlIGNvbmZ1c2UgdGhlIHR3by4gTXlz dCByZWR1Y2VzIHRvIHRoZSBzZWNyZXQgYnV0IG1hdGhlbWF0aWNhbGx5IHRoZXJlIGlzIG5vIGlu dmVyc2UuIFdoYXQgbWF0dGVycyBpcyB0aGUgbGF0dGVyLg0KDQpUaG9yc3Rlbg0KDQoNCu+7v09u IDA0LzA1LzIwMjAsIDEyOjQyLCAiTmljb2xhaSBLcmF1cyIgPG5pY29sYS4uLkBnbWFpbC5jb20+ IHdyb3RlOg0KDQogICAgT24gMDQvMDUvMjAyMCAxMjoxNywgVGhvcnN0ZW4gQWx0ZW5raXJjaCB3 cm90ZToNCiAgICA+ICAgICAgVGhpcyBpcyByZWFsbHkgZGlmZmVyZW50IGluIHRoZSByZXNwZWN0 aXZlIHRvcG9zIG1vZGVscyBhcyBlZyBzaW1wbGljaWFsDQogICAgPiAgICAgIHNldHMgb3IgYWxy ZWFkeSB0aGUgdG9wb3Mgb2YgcmVmbGV4aXZlIGdyYXBocyBhcyBleGVtcGxpZmllZCBieSBOLiBL cmF1cydzDQogICAgPiAgICAgIHB1enpsaW5nIGNvdW50ZXJleGFtcGxlLg0KICAgID4NCiAgICA+ IFdoYXQgcHV6emxpbmcgY291bnRlcmV4YW1wbGUgaXMgdGhpcz8NCg0KICAgIFRob21hcyB3YXMg cmVmZXJyaW5nIHRvOg0KICAgIGh0dHBzOi8vaG9tb3RvcHl0eXBldGhlb3J5Lm9yZy8yMDEzLzEw LzI4Lw0KDQogICAgWW91IG1heSBhbHNvIGhhdmUgc2VlbiBpdCBpbiBteSB0aGVzaXMgb3IgdGhl IHBhcGVyICJOb3Rpb25zIG9mIA0KICAgIEFub255bW91cyBFeGlzdGVuY2UgaW4gTWFydGluLUzD tmYgVHlwZSBUaGVvcnkiLiA6KQ0KICAgIE5pY29sYWkNCg0KDQogICAgLS0gDQogICAgWW91IHJl Y2VpdmVkIHRoaXMgbWVzc2FnZSBiZWNhdXNlIHlvdSBhcmUgc3Vic2NyaWJlZCB0byB0aGUgR29v Z2xlIEdyb3VwcyAiSG9tb3RvcHkgVHlwZSBUaGVvcnkiIGdyb3VwLg0KICAgIFRvIHVuc3Vic2Ny aWJlIGZyb20gdGhpcyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNl bmQgYW4gZW1haWwgdG8gSG9tb3RvcHlULi4uQGdvb2dsZWdyb3Vwcy5jb20uDQogICAgVG8gdmll dyB0aGlzIGRpc2N1c3Npb24gb24gdGhlIHdlYiB2aXNpdCBodHRwczovL2dyb3Vwcy5nb29nbGUu Y29tL2QvbXNnaWQvSG9tb3RvcHlUeXBlVGhlb3J5L2EyNTA0NTgyLWE3ZjUtNmJjYi1lYmM2LTE3 YWU4NjllYmFhOCU0MGdtYWlsLmNvbS4NCg0KCgoKVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0YWNo bWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2VlCmFuZCBtYXkgY29udGFp biBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJlY2VpdmVkIHRoaXMKbWVz c2FnZSBpbiBlcnJvciwgcGxlYXNlIGNvbnRhY3QgdGhlIHNlbmRlciBhbmQgZGVsZXRlIHRoZSBl bWFpbCBhbmQKYXR0YWNobWVudC4gCgpBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5 IHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QKbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUg dmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4gRW1haWwKY29tbXVuaWNhdGlv bnMgd2l0aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgCndo ZXJlIHBlcm1pdHRlZCBieSBsYXcuCgoKCgo=