From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.211.79 with SMTP id k76mr743231lfg.1.1516833659854; Wed, 24 Jan 2018 14:40:59 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.67.66 with SMTP id m2ls1203055lfj.1.gmail; Wed, 24 Jan 2018 14:40:58 -0800 (PST) X-Received: by 10.25.81.154 with SMTP id g26mr732330lfl.15.1516833658481; Wed, 24 Jan 2018 14:40:58 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1516833658; cv=none; d=google.com; s=arc-20160816; b=vcBv4dykybSxHwhS36ZeYNmSfygjEqmr9r3e6cSH+xtKOlCRtTasJJUoTacWGJhhXY 5r7b0MeSQ9vmDDOx5Irc+lMWKVqoqouAB9j1VFEIMUUe/z31irJoUjYmKCv6UNIKsC9T sx7gY0SZS8R40qRH7qVkbngkyfnCIrc/lLdUau1w+RwQOAsf6JzLWEY8ThgiOmHD0kKl d2b20n/YkNzRm6gIp356/HxRHr3Ydw1g14XNJM89zZd7174VWg9U76TcNzb7DfZiqj9N GhaCR59ONcXwIyqUX7gfPI8lS/qrmlOstlXCvfKVvxmT9TRFPhyLKx/EUVef9GnfRmKQ caYw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:spamdiagnosticmetadata:spamdiagnosticoutput :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:dkim-signature :arc-authentication-results; bh=QOTdxNcZVC/xLlS00XgOC2YIMAbvWtbCnXzieyRsVjU=; b=euTTOvxtv7F6iwupkkwKnLPJ83JtMSsdPPbrlRwAfuXDbc3sh5dSZFkUbxAgpSicAZ PIVD42vYsKGiSJgwrgm5XMzd8vQsh9aMY/Z2xB1AJPyQJULMUewnmP2wqkGqWTg3HNrP 1ZMR6KBUWtc7QtVnf+TwVMX6m9+Pa6Ldn+1JGl4G2N5ahcOobFugJYsXiYJHW7EN2vDs 7gXv1njkvBe1+KqukGg929ovBmI+9iDKXr9FXCJlkTCgdadtsuu1oeXEWNSyoQV6s6Db Z5yCFZtEHL3UD479W7zTs6YwoAy5C0J+ycY8K1XMygoW0QKlJ74lUACN9J+T6OoVuV6s ZK0w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@leeds365.onmicrosoft.com header.s=selector1-leeds-ac-uk header.b=2ZUXhGsi; spf=pass (google.com: domain of n.ga...@leeds.ac.uk designates 129.11.77.151 as permitted sender) smtp.mailfrom=N.Ga...@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk Return-Path: Received: from mhost02h.leeds.ac.uk (mhost02h.leeds.ac.uk. [129.11.77.151]) by gmr-mx.google.com with ESMTPS id y16si118634lje.2.2018.01.24.14.40.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 24 Jan 2018 14:40:57 -0800 (PST) Received-SPF: pass (google.com: domain of n.ga...@leeds.ac.uk designates 129.11.77.151 as permitted sender) client-ip=129.11.77.151; Authentication-Results: gmr-mx.google.com; dkim=pass head...@leeds365.onmicrosoft.com header.s=selector1-leeds-ac-uk header.b=2ZUXhGsi; spf=pass (google.com: domain of n.ga...@leeds.ac.uk designates 129.11.77.151 as permitted sender) smtp.mailfrom=N.Ga...@leeds.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=leeds.ac.uk Received: from APOLLO2.ds.leeds.ac.uk (apollo2.leeds.ac.uk [129.11.5.5]) by mhost02h.leeds.ac.uk (8.14.4/8.14.4) with ESMTP id w0OMes0J020581 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Wed, 24 Jan 2018 22:40:55 GMT Received: from APOLLO8.ds.leeds.ac.uk (129.11.6.119) by APOLLO2.ds.leeds.ac.uk (129.11.5.5) with Microsoft SMTP Server (TLS) id 8.3.245.1; Wed, 24 Jan 2018 22:40:54 +0000 Received: from EUR01-DB5-obe.outbound.protection.outlook.com (213.199.154.176) by outlook.leeds.ac.uk (129.11.6.119) with Microsoft SMTP Server (TLS) id 14.3.195.1; Wed, 24 Jan 2018 22:40:54 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=leeds365.onmicrosoft.com; s=selector1-leeds-ac-uk; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version; bh=QOTdxNcZVC/xLlS00XgOC2YIMAbvWtbCnXzieyRsVjU=; b=2ZUXhGsiKk05VFzf7OEB2A3bRDsnp99XHuF/UTIyQQg47EoSyYQoKim0aV1Kj/M11aY09NlFYWHLJ0YjI7SYq4sJ8ILoagElSmJgbMivcBQwnjfgwVMa+p7cNgFvCUUo9yVEBmHoy3lMKjVEvHMQc4hfDOoWIPQLZrA4v7+Uiew= Received: from DB5PR0301MB1959.eurprd03.prod.outlook.com (10.167.227.19) by DB5PR0301MB1957.eurprd03.prod.outlook.com (10.167.227.17) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.428.17; Wed, 24 Jan 2018 22:40:46 +0000 Received: from DB5PR0301MB1959.eurprd03.prod.outlook.com ([fe80::e08d:a2c8:4ead:dbae]) by DB5PR0301MB1959.eurprd03.prod.outlook.com ([fe80::e08d:a2c8:4ead:dbae%14]) with mapi id 15.20.0428.024; Wed, 24 Jan 2018 22:40:46 +0000 From: Nicola Gambino To: Homotopy Type Theory , "escardo...@gmail.com" Subject: Re: [HoTT] Re: Coquand's list of open problems Thread-Topic: [HoTT] Re: Coquand's list of open problems Thread-Index: AQHTlWPL/WyYdo54hkqwUCkHGEb80qODnfcA Date: Wed, 24 Jan 2018 22:40:46 +0000 Message-ID: References: <17bbe329-b471-490c-b11d-31c50f1334f1@googlegroups.com> In-Reply-To: <17bbe329-b471-490c-b11d-31c50f1334f1@googlegroups.com> Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3445.5.20) authentication-results: spf=none (sender IP is ) smtp.mailfrom=N.Ga...@leeds.ac.uk; x-originating-ip: [95.150.150.71] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR0301MB1957;7:TYBKvpRQ5+uUZXW3kjN31k7DEs1STA5E5CKS0VIT0w60ZXwFBZlA3aaCpuxtUrufvjU25Hn09BP81wL8FjKgwcSDoaHOsBZMUqD0l+EmDjVpBHqxVuwIYoJCi9TR0I30VRqBeB3Oql/+CV0vLxnYKsFK9L5somgcgnsL52fz++MRNBBdz5fGcPnbXXfedI9yxlm81AnOYUQV8hf0zQwVCl9EogUZ9AeB1Ju55JThpyYgaUC3DhoTqbkY3wFbI+Yx x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 5748bffc-012f-4be9-a475-08d5637b82c6 x-microsoft-antispam: UriScan:(232050936154180);BCL:0;PCL:0;RULEID:(7020095)(4652020)(8989060)(4534165)(4627221)(201703031133081)(201702281549075)(8990040)(5600026)(4604075)(3008032)(2017052603307)(7153060)(7193020);SRVR:DB5PR0301MB1957; x-ms-traffictypediagnostic: DB5PR0301MB1957: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(232050936154180)(85827821059158); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040501)(2401047)(5005006)(8121501046)(3231023)(2400081)(944501161)(93006095)(93001095)(10201501046)(3002001)(6041288)(20161123560045)(20161123562045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123564045)(20161123558120)(6072148)(201708071742011);SRVR:DB5PR0301MB1957;BCL:0;PCL:0;RULEID:;SRVR:DB5PR0301MB1957; x-forefront-prvs: 056297E276 x-forefront-antispam-report: SFV:NSPM;SFS:(10009020)(366004)(346002)(396003)(39380400002)(376002)(39860400002)(199004)(189003)(86362001)(82746002)(53546011)(76176011)(102836004)(7736002)(3660700001)(786003)(110136005)(6506007)(97736004)(36756003)(316002)(54896002)(606006)(26005)(2950100002)(5660300001)(2900100001)(42882006)(74482002)(106356001)(33656002)(14454004)(3280700002)(2501003)(413944005)(5250100002)(966005)(478600001)(72206003)(6436002)(25786009)(83716003)(66066001)(6116002)(3846002)(99286004)(6486002)(68736007)(6306002)(6512007)(53936002)(81166006)(81156014)(50226002)(39060400002)(236005)(8936002)(8676002)(105586002)(229853002)(6246003)(186003)(57306001)(2906002);DIR:OUT;SFP:1101;SCL:1;SRVR:DB5PR0301MB1957;H:DB5PR0301MB1959.eurprd03.prod.outlook.com;FPR:;SPF:None;PTR:InfoNoRecords;A:1;MX:1;LANG:en; received-spf: None (protection.outlook.com: leeds.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: WYEhQMGfdR0AEVkmHHYJPtIdOjqOQEP7HWP0eebYdgLy7uvE8N2DBrgQc5m/0Ii6OhEvAA1KWoM2yU6FWg104g== spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: multipart/alternative; boundary="_000_ADD5404883CE422B99ED80F8406E29DCleedsacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 5748bffc-012f-4be9-a475-08d5637b82c6 X-MS-Exchange-CrossTenant-originalarrivaltime: 24 Jan 2018 22:40:46.8664 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: bdeaeda8-c81d-45ce-863e-5232a535b7cb X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR0301MB1957 X-OriginatorOrg: leeds.ac.uk X-UOL-RateLimit: userRateLimit[a:n.g...@leeds.ac.uk,c:0.1719118382251172,l:500.0] --_000_ADD5404883CE422B99ED80F8406E29DCleedsacuk_ Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: base64 RGVhciBNYXJ0aW4sDQoNCk9uIDI0IEphbiAyMDE4LCBhdCAyMjozNiwgTWFydMOtbiBIw7Z0emVs IEVzY2FyZMOzIDxlc2NhcmRvLi4uQGdtYWlsLmNvbTxtYWlsdG86ZXNjYXJkby4uLkBnbWFpbC5j b20+PiB3cm90ZToNCg0KU28gb25lIHZhZ3VlIHF1ZXN0aW9uIGlzIGhvdyBtdWNoIG9uZSBjYW4g ZG8gKndpdGhvdXQqIHByb3Bvc2l0aW9uYWwgcmVzaXppbmcgYW5kIGxpdmluZyB3aXRoIHRoZSBm YWN0IHRoYXQgdW5pdmVyc2UgbGV2ZWxzIG1heSBnbyB1cCBhbmQgZG93biBpbiBjb25zdHJ1Y3Rp b25zIHN1Y2ggYXMgdGhlIGFib3ZlLiAoQSB2YWd1ZSBhbnN3ZXIgaXMgImEgbG90IiwgZnJvbSBt eSBvd24gZXhwZXJpZW5jZSBvZiBmb3JtYWxpemluZyB0aGluZ3MuKQ0KDQpBIG1vcmUgcHJlY2lz ZSBxdWVzdGlvbiBpcyB0aGF0IGlmIHdlIGhhdmUgYSBtb25hZCAidXAgdG8gdW5pdmVyc2UganVn Z2xpbmciIChzdWNoIGFzIHRoZSBhYm92ZSksIHdoYXQga2luZCBvZiB1bml2ZXJzYWwgcHJvcGVy dHkgInVwIHRvIHVuaXZlcnNlIGp1Z2dsaW5nIiBkb2VzIGl0IGNvcnJlc3BvbmQgdG8uDQoNCllv dSBtYXkgaGF2ZSBhIGxvb2sgYXQgcmVsYXRpdmUgbW9uYWRzIChBbHRlbmtpcmNoIGV0IGFsKSBh bmQgcmVsYXRpdmUgcHNldWRvbW9uYWRzIChGaW9yZSwgR2FtYmlubywgSHlsYW5kLCBXaW5za2Vs KS4gV2UgY29uc2lkZXJlZCB0aGUgcHJlc2hlYWYgY29uc3RydWN0aW9uIHRoYXQgdGFrZXMgYSBz bWFsbCBjYXRlZ29yeSB0byBhIGxvY2FsbHkgc21hbGwgb25lIChhbmQgaGVuY2UganVtcHMgdXAg YSB1bml2ZXJzZSkgYXMgYSByZWxhdGl2ZSBwc2V1ZG9tb25hZC4gSGVyZSwg4oCccHNldWRv4oCd IHJlZmVycyB0byBjb2hlcmVuY2UgaXNzdWVzLCB3aGljaCBJIGFtIG5vdCBzdXJlIGFyaXNlIGlu IHR5cGUgdGhlb3J5Lg0KDQpCZXN0IHdpc2hlcywNCk5pY29sYQ0KDQpEciBOaWNvbGEgR2FtYmlu bw0KU2Nob29sIG9mIE1hdGhlbWF0aWNzLCBVbml2ZXJzaXR5IG9mIExlZWRzDQpXZWI6IGh0dHA6 Ly93d3cxLm1hdGhzLmxlZWRzLmFjLnVrL35wbXRuZy8NCg0K --_000_ADD5404883CE422B99ED80F8406E29DCleedsacuk_ Content-Type: text/html; charset="utf-8" Content-ID: Content-Transfer-Encoding: base64 PGh0bWw+DQo8aGVhZD4NCjxtZXRhIGh0dHAtZXF1aXY9IkNvbnRlbnQtVHlwZSIgY29udGVudD0i dGV4dC9odG1sOyBjaGFyc2V0PXV0Zi04Ij4NCjwvaGVhZD4NCjxib2R5IHN0eWxlPSJ3b3JkLXdy YXA6IGJyZWFrLXdvcmQ7IC13ZWJraXQtbmJzcC1tb2RlOiBzcGFjZTsgbGluZS1icmVhazogYWZ0 ZXItd2hpdGUtc3BhY2U7IiBjbGFzcz0iIj4NCkRlYXIgTWFydGluLCZuYnNwOzxiciBjbGFzcz0i Ij4NCjxkaXY+PGJyIGNsYXNzPSIiPg0KPGJsb2NrcXVvdGUgdHlwZT0iY2l0ZSIgY2xhc3M9IiI+ DQo8ZGl2IGNsYXNzPSIiPk9uIDI0IEphbiAyMDE4LCBhdCAyMjozNiwgTWFydMOtbiBIw7Z0emVs IEVzY2FyZMOzICZsdDs8YSBocmVmPSJtYWlsdG86ZXNjYXJkby4uLkBnbWFpbC5jb20iIGNsYXNz PSIiPmVzY2FyZG8uLi5AZ21haWwuY29tPC9hPiZndDsgd3JvdGU6PC9kaXY+DQo8YnIgY2xhc3M9 IkFwcGxlLWludGVyY2hhbmdlLW5ld2xpbmUiPg0KPGRpdiBjbGFzcz0iIj4NCjxkaXYgc3R5bGU9 ImZvbnQtZmFtaWx5OiBIZWx2ZXRpY2E7IGZvbnQtc2l6ZTogMTRweDsgZm9udC1zdHlsZTogbm9y bWFsOyBmb250LXZhcmlhbnQtY2Fwczogbm9ybWFsOyBmb250LXdlaWdodDogbm9ybWFsOyBsZXR0 ZXItc3BhY2luZzogbm9ybWFsOyB0ZXh0LWFsaWduOiBzdGFydDsgdGV4dC1pbmRlbnQ6IDBweDsg dGV4dC10cmFuc2Zvcm06IG5vbmU7IHdoaXRlLXNwYWNlOiBub3JtYWw7IHdvcmQtc3BhY2luZzog MHB4OyAtd2Via2l0LXRleHQtc3Ryb2tlLXdpZHRoOiAwcHg7IiBjbGFzcz0iIj4NClNvIG9uZSB2 YWd1ZSBxdWVzdGlvbiBpcyBob3cgbXVjaCBvbmUgY2FuIGRvICp3aXRob3V0KiBwcm9wb3NpdGlv bmFsIHJlc2l6aW5nIGFuZCBsaXZpbmcgd2l0aCB0aGUgZmFjdCB0aGF0IHVuaXZlcnNlIGxldmVs cyBtYXkgZ28gdXAgYW5kIGRvd24gaW4gY29uc3RydWN0aW9ucyBzdWNoIGFzIHRoZSBhYm92ZS4g KEEgdmFndWUgYW5zd2VyIGlzICZxdW90O2EgbG90JnF1b3Q7LCBmcm9tIG15IG93biBleHBlcmll bmNlIG9mIGZvcm1hbGl6aW5nIHRoaW5ncy4pJm5ic3A7PC9kaXY+DQo8ZGl2IHN0eWxlPSJmb250 LWZhbWlseTogSGVsdmV0aWNhOyBmb250LXNpemU6IDE0cHg7IGZvbnQtc3R5bGU6IG5vcm1hbDsg Zm9udC12YXJpYW50LWNhcHM6IG5vcm1hbDsgZm9udC13ZWlnaHQ6IG5vcm1hbDsgbGV0dGVyLXNw YWNpbmc6IG5vcm1hbDsgdGV4dC1hbGlnbjogc3RhcnQ7IHRleHQtaW5kZW50OiAwcHg7IHRleHQt dHJhbnNmb3JtOiBub25lOyB3aGl0ZS1zcGFjZTogbm9ybWFsOyB3b3JkLXNwYWNpbmc6IDBweDsg LXdlYmtpdC10ZXh0LXN0cm9rZS13aWR0aDogMHB4OyIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+ DQo8L2Rpdj4NCjxkaXYgc3R5bGU9ImZvbnQtZmFtaWx5OiBIZWx2ZXRpY2E7IGZvbnQtc2l6ZTog MTRweDsgZm9udC1zdHlsZTogbm9ybWFsOyBmb250LXZhcmlhbnQtY2Fwczogbm9ybWFsOyBmb250 LXdlaWdodDogbm9ybWFsOyBsZXR0ZXItc3BhY2luZzogbm9ybWFsOyB0ZXh0LWFsaWduOiBzdGFy dDsgdGV4dC1pbmRlbnQ6IDBweDsgdGV4dC10cmFuc2Zvcm06IG5vbmU7IHdoaXRlLXNwYWNlOiBu b3JtYWw7IHdvcmQtc3BhY2luZzogMHB4OyAtd2Via2l0LXRleHQtc3Ryb2tlLXdpZHRoOiAwcHg7 IiBjbGFzcz0iIj4NCkEgbW9yZSBwcmVjaXNlIHF1ZXN0aW9uIGlzIHRoYXQgaWYgd2UgaGF2ZSBh IG1vbmFkICZxdW90O3VwIHRvIHVuaXZlcnNlIGp1Z2dsaW5nJnF1b3Q7IChzdWNoIGFzIHRoZSBh Ym92ZSksIHdoYXQga2luZCBvZiB1bml2ZXJzYWwgcHJvcGVydHkgJnF1b3Q7dXAgdG8gdW5pdmVy c2UganVnZ2xpbmcmcXVvdDsgZG9lcyBpdCBjb3JyZXNwb25kIHRvLiZuYnNwOzwvZGl2Pg0KPC9k aXY+DQo8L2Jsb2NrcXVvdGU+DQo8L2Rpdj4NCjxkaXY+DQo8ZGl2PjxiciBjbGFzcz0iIj4NCjwv ZGl2Pg0KPGRpdj5Zb3UgbWF5IGhhdmUgYSBsb29rIGF0IHJlbGF0aXZlIG1vbmFkcyAoQWx0ZW5r aXJjaCBldCBhbCkgYW5kIHJlbGF0aXZlIHBzZXVkb21vbmFkcyAoRmlvcmUsIEdhbWJpbm8sIEh5 bGFuZCwgV2luc2tlbCkuIFdlIGNvbnNpZGVyZWQgdGhlIHByZXNoZWFmIGNvbnN0cnVjdGlvbiB0 aGF0IHRha2VzIGEgc21hbGwgY2F0ZWdvcnkgdG8gYSBsb2NhbGx5IHNtYWxsIG9uZSAoYW5kIGhl bmNlIGp1bXBzIHVwIGEgdW5pdmVyc2UpIGFzIGEgcmVsYXRpdmUNCiBwc2V1ZG9tb25hZC4gSGVy ZSwg4oCccHNldWRv4oCdIHJlZmVycyB0byBjb2hlcmVuY2UgaXNzdWVzLCB3aGljaCBJIGFtIG5v dCBzdXJlIGFyaXNlIGluIHR5cGUgdGhlb3J5LjwvZGl2Pg0KPGRpdj48YnIgY2xhc3M9IiI+DQo8 L2Rpdj4NCjxkaXY+QmVzdCB3aXNoZXMsPC9kaXY+DQo8ZGl2Pk5pY29sYTwvZGl2Pg0KPC9kaXY+ DQo8YnIgY2xhc3M9IiI+DQo8ZGl2IGNsYXNzPSIiPkRyIE5pY29sYSBHYW1iaW5vPGJyIGNsYXNz PSIiPg0KU2Nob29sIG9mIE1hdGhlbWF0aWNzLCBVbml2ZXJzaXR5IG9mJm5ic3A7TGVlZHM8YnIg Y2xhc3M9IiI+DQpXZWI6Jm5ic3A7PGEgaHJlZj0iaHR0cDovL3d3dzEubWF0aHMubGVlZHMuYWMu dWsvfnBtdG5nLyIgY2xhc3M9IiI+aHR0cDovL3d3dzEubWF0aHMubGVlZHMuYWMudWsvfnBtdG5n LzwvYT4NCjwvZGl2Pg0KPGJyIGNsYXNzPSIiPg0KPC9ib2R5Pg0KPC9odG1sPg0K --_000_ADD5404883CE422B99ED80F8406E29DCleedsacuk_--