From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.72.71 with SMTP id v68mr5418242lfa.9.1490201388804; Wed, 22 Mar 2017 09:49:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.202.1 with SMTP id a1ls209880lfg.41.gmail; Wed, 22 Mar 2017 09:49:46 -0700 (PDT) X-Received: by 10.25.72.71 with SMTP id v68mr5418091lfa.9.1490201386826; Wed, 22 Mar 2017 09:49:46 -0700 (PDT) Return-Path: Received: from tyrell.ita.chalmers.se (tyrell.ita.chalmers.se. [129.16.226.132]) by gmr-mx.google.com with ESMTPS id 82si290130wmg.3.2017.03.22.09.49.46 (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Wed, 22 Mar 2017 09:49:46 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.132; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.132 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Received: from tyrell.ita.chalmers.se (129.16.226.132) by tyrell.ita.chalmers.se (129.16.226.132) with Microsoft SMTP Server (TLS) id 15.1.396.30; Wed, 22 Mar 2017 17:49:45 +0100 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.0396.037; Wed, 22 Mar 2017 17:49:45 +0100 From: Thierry Coquand To: Matt Oliveri CC: Homotopy Type Theory , "univalent-...@googlegroups.com" Subject: Re: [HoTT] about the HTS Thread-Topic: [HoTT] about the HTS Thread-Index: AQHSoyxPD+H/oI0ecESb6K8fiaRrgQ== Date: Wed, 22 Mar 2017 16:49:45 +0000 Message-ID: References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com> In-Reply-To: <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-exchange-messagesentrepresentingtype: 1 x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_D688CD8B5DDE4CA684DE478A8E23890Cchalmersse_" MIME-Version: 1.0 --_000_D688CD8B5DDE4CA684DE478A8E23890Cchalmersse_ Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: base64 DQpJZiBteSBub3RlIHdhcyBjb3JyZWN0LCBpdCBkZXNjcmliZXMgaW4gdGhlIGN1YmljYWwgc2V0 IG1vZGVsIHR3byB1bml2YWxlbnQgdW5pdmVyc2VzDQooc3VicHJlc2hlYWYgb2YgdGhlIGZpcnN0 IHVuaXZlcnNlKSAgdGhhdCBzYXRpc2Z5DQoNCiAoMSkgICBpZiAgIEEgOiBzU2V0ICAgIGFuZCAg IHAgOiBQYXRoIEEgYSBiICAgdGhlbiAgIGEgPSBiIDogQSAgYW5kIHAgaXMgdGhlIGNvbnN0YW50 IHBhdGggYQ0KKGVxdWFsaXR5IHJlZmxlY3Rpb24gcnVsZSkNCg0KICgyKSAgIGlmIEEgOiBiU2V0 IGFuZCBwIGFuZCBxIG9mIHR5cGUgUGF0aCBBIGEgYiAgIHRoZW4gcCA9IHEgOiBQYXRoIEEgYSBi DQooanVkZ2VtZW50YWwgZm9ybSBvZiBVSVApDQoNCiBNYXliZSAoMSkgb3IgKDIpIGNvdWxkIGJl IHVzZWQgaW5zdGVhZCBvZiBIVFMgKGFuZCB3ZSB3b3VsZCByZW1haW4gaW4gYW4gdW5pdmFsZW50 DQp0aGVvcnksIHdoZXJlIGFsbCB0eXBlcyBhcmUgZmlicmFudCkNCg0KIEZvciB0ZXN0aW5nIHRo aXMsIG9uZSBxdWVzdGlvbiBpczogIGNhbiB3ZSBkZWZpbmUgc2VtaS1zaW1wbGljaWFsIHR5cGVz IGluICgxKT8gaW4gKDIpPw0KDQogQmVzdCByZWdhcmRzLA0KIFRoaWVycnkNCg0KDQoNCk9uIDIw IE1hciAyMDE3LCBhdCAxNjoxMiwgTWF0dCBPbGl2ZXJpIDxhdG0uLi5AZ21haWwuY29tPG1haWx0 bzphdG0uLi5AZ21haWwuY29tPj4gd3JvdGU6DQoNClNvIHRoZSBhbnN3ZXIgd2FzIHllcywgcmln aHQ/IFByb2JsZW0gc29sdmVkPw0KDQpPbiBUaHVyc2RheSwgRmVicnVhcnkgMjMsIDIwMTcgYXQg OTo0Nzo1NyBBTSBVVEMtNSwgdiB2IHdyb3RlOg0KSnVzdCBhIHRob3VnaHTigKYgQ2FuIHdlIGRl dmlzZSBhIHZlcnNpb24gb2YgdGhlIEhUUyB3aGVyZSBleGFjdCBlcXVhbGl0eSB0eXBlcyBhcmUg bm90IGF2YWlsYWJsZSBmb3IgdGhlIHVuaXZlcnNlcyBzdWNoIHRoYXQsIGV2ZW4gd2l0aCB0aGUg ZXhhY3QgZXF1YWxpdHksIEhUUyB3b3VsZCByZW1haW4gYSB1bml2YWxlbnQgdGhlb3J5Lg0KDQpN YXliZSBvbmx5IHNvbWUgdHlwZXMgc2hvdWxkIGJlIGVxdWlwcGVkIHdpdGggdGhlIGV4YWN0IGVx dWFsaXR5IGFuZCB0aGlzIHNob3VsZCBiZSBhIHNwZWNpYWwgcXVhbGl0eSBvZiB0eXBlcy4NCg0K VmxhZGltaXIuDQoNClBTIElmIHRoZXJlIGFyZSBoaWdoZXIgaW5kdWN0aXZlIHR5cGVzIHRoZW4g dGhlIGV4YWN0IGVxdWFsaXR5IHNob3VsZCBub3QgYmUgYXZhaWxhYmxlIGZvciB0aGVtIGVpdGhl ci4NCg0KLS0NCllvdSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1YnNj cmliZWQgdG8gdGhlIEdvb2dsZSBHcm91cHMgIkhvbW90b3B5IFR5cGUgVGhlb3J5IiBncm91cC4N ClRvIHVuc3Vic2NyaWJlIGZyb20gdGhpcyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxz IGZyb20gaXQsIHNlbmQgYW4gZW1haWwgdG8gSG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vw cy5jb208bWFpbHRvOkhvbW90b3B5VHlwZVRoZS4uLkBnb29nbGVncm91cHMuY29tPi4NCkZvciBt b3JlIG9wdGlvbnMsIHZpc2l0IGh0dHBzOi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQuDQoN Cg== --_000_D688CD8B5DDE4CA684DE478A8E23890Cchalmersse_ Content-Type: text/html; charset="utf-8" Content-ID: <87D8519D95CA3744...@chalmers.se> Content-Transfer-Encoding: base64 PGh0bWw+DQo8aGVhZD4NCjxtZXRhIGh0dHAtZXF1aXY9IkNvbnRlbnQtVHlwZSIgY29udGVudD0i dGV4dC9odG1sOyBjaGFyc2V0PXV0Zi04Ij4NCjwvaGVhZD4NCjxib2R5IHN0eWxlPSJ3b3JkLXdy YXA6IGJyZWFrLXdvcmQ7IC13ZWJraXQtbmJzcC1tb2RlOiBzcGFjZTsgLXdlYmtpdC1saW5lLWJy ZWFrOiBhZnRlci13aGl0ZS1zcGFjZTsiIGNsYXNzPSIiPg0KPGRpdiBjbGFzcz0iIj48YnIgY2xh c3M9IiI+DQo8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+SWYgbXkgbm90ZSB3YXMgY29ycmVjdCwgaXQg ZGVzY3JpYmVzIGluIHRoZSBjdWJpY2FsIHNldCBtb2RlbCB0d28gdW5pdmFsZW50IHVuaXZlcnNl czwvZGl2Pg0KPGRpdiBjbGFzcz0iIj4oc3VicHJlc2hlYWYgb2YgdGhlIGZpcnN0IHVuaXZlcnNl KSAmbmJzcDt0aGF0IHNhdGlzZnk8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+PGJyIGNsYXNzPSIiPg0K PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPiZuYnNwOygxKSAmbmJzcDsgaWYgJm5ic3A7IEEgOiBzU2V0 ICZuYnNwOyAmbmJzcDthbmQgJm5ic3A7IHAgOiBQYXRoIEEgYSBiICZuYnNwOyB0aGVuICZuYnNw OyBhID0gYiA6IEEgJm5ic3A7YW5kIHAgaXMgdGhlIGNvbnN0YW50IHBhdGggYTwvZGl2Pg0KPGRp diBjbGFzcz0iIj4oZXF1YWxpdHkgcmVmbGVjdGlvbiBydWxlKTwvZGl2Pg0KPGRpdiBjbGFzcz0i Ij48YnIgY2xhc3M9IiI+DQo8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+Jm5ic3A7KDIpICZuYnNwOyBp ZiBBIDogYlNldCBhbmQgcCBhbmQgcSBvZiB0eXBlIFBhdGggQSBhIGIgJm5ic3A7IHRoZW4gcCA9 IHEgOiBQYXRoIEEgYSBiPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPihqdWRnZW1lbnRhbCBmb3JtIG9m IFVJUCk8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+PGJyIGNsYXNzPSIiPg0KPC9kaXY+DQo8ZGl2IGNs YXNzPSIiPiZuYnNwO01heWJlICgxKSBvciAoMikgY291bGQgYmUgdXNlZCBpbnN0ZWFkIG9mIEhU UyAoYW5kIHdlIHdvdWxkIHJlbWFpbiBpbiBhbiB1bml2YWxlbnQ8L2Rpdj4NCjxkaXYgY2xhc3M9 IiI+dGhlb3J5LCB3aGVyZSBhbGwgdHlwZXMgYXJlIGZpYnJhbnQpPC9kaXY+DQo8ZGl2IGNsYXNz PSIiPjxiciBjbGFzcz0iIj4NCjwvZGl2Pg0KPGRpdiBjbGFzcz0iIj4mbmJzcDtGb3IgdGVzdGlu ZyB0aGlzLCBvbmUgcXVlc3Rpb24gaXM6ICZuYnNwO2NhbiB3ZSBkZWZpbmUgc2VtaS1zaW1wbGlj aWFsIHR5cGVzIGluICgxKT8gaW4gKDIpPzwvZGl2Pg0KPGRpdiBjbGFzcz0iIj48YnIgY2xhc3M9 IiI+DQo8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+Jm5ic3A7QmVzdCByZWdhcmRzLDwvZGl2Pg0KPGRp diBjbGFzcz0iIj4mbmJzcDtUaGllcnJ5PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPjxiciBjbGFzcz0i Ij4NCjwvZGl2Pg0KPGRpdiBjbGFzcz0iIj48YnIgY2xhc3M9IiI+DQo8L2Rpdj4NCjxiciBjbGFz cz0iIj4NCjxkaXY+DQo8YmxvY2txdW90ZSB0eXBlPSJjaXRlIiBjbGFzcz0iIj4NCjxkaXYgY2xh c3M9IiI+T24gMjAgTWFyIDIwMTcsIGF0IDE2OjEyLCBNYXR0IE9saXZlcmkgJmx0OzxhIGhyZWY9 Im1haWx0bzphdG0uLi5AZ21haWwuY29tIiBjbGFzcz0iIj5hdG0uLi5AZ21haWwuY29tPC9hPiZn dDsgd3JvdGU6PC9kaXY+DQo8YnIgY2xhc3M9IkFwcGxlLWludGVyY2hhbmdlLW5ld2xpbmUiPg0K PGRpdiBjbGFzcz0iIj4NCjxkaXYgZGlyPSJsdHIiIGNsYXNzPSIiPlNvIHRoZSBhbnN3ZXIgd2Fz IHllcywgcmlnaHQ/IFByb2JsZW0gc29sdmVkPzxiciBjbGFzcz0iIj4NCjxiciBjbGFzcz0iIj4N Ck9uIFRodXJzZGF5LCBGZWJydWFyeSAyMywgMjAxNyBhdCA5OjQ3OjU3IEFNIFVUQy01LCB2IHYg d3JvdGU6DQo8YmxvY2txdW90ZSBjbGFzcz0iZ21haWxfcXVvdGUiIHN0eWxlPSJtYXJnaW46IDA7 bWFyZ2luLWxlZnQ6IDAuOGV4O2JvcmRlci1sZWZ0OiAxcHggI2NjYyBzb2xpZDtwYWRkaW5nLWxl ZnQ6IDFleDsiPg0KSnVzdCBhIHRob3VnaHTigKYgQ2FuIHdlIGRldmlzZSBhIHZlcnNpb24gb2Yg dGhlIEhUUyB3aGVyZSBleGFjdCBlcXVhbGl0eSB0eXBlcyBhcmUgbm90IGF2YWlsYWJsZSBmb3Ig dGhlIHVuaXZlcnNlcyBzdWNoIHRoYXQsIGV2ZW4gd2l0aCB0aGUgZXhhY3QgZXF1YWxpdHksIEhU UyB3b3VsZCByZW1haW4gYSB1bml2YWxlbnQgdGhlb3J5Lg0KPGJyIGNsYXNzPSIiPg0KPGJyIGNs YXNzPSIiPg0KTWF5YmUgb25seSBzb21lIHR5cGVzIHNob3VsZCBiZSBlcXVpcHBlZCB3aXRoIHRo ZSBleGFjdCBlcXVhbGl0eSBhbmQgdGhpcyBzaG91bGQgYmUgYSBzcGVjaWFsIHF1YWxpdHkgb2Yg dHlwZXMuDQo8YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+DQpWbGFkaW1pci4gPGJyIGNsYXNz PSIiPg0KPGJyIGNsYXNzPSIiPg0KUFMgSWYgdGhlcmUgYXJlIGhpZ2hlciBpbmR1Y3RpdmUgdHlw ZXMgdGhlbiB0aGUgZXhhY3QgZXF1YWxpdHkgc2hvdWxkIG5vdCBiZSBhdmFpbGFibGUgZm9yIHRo ZW0gZWl0aGVyLjxiciBjbGFzcz0iIj4NCjwvYmxvY2txdW90ZT4NCjwvZGl2Pg0KPGRpdiBjbGFz cz0iIj48YnIgY2xhc3M9IndlYmtpdC1ibG9jay1wbGFjZWhvbGRlciI+DQo8L2Rpdj4NCi0tIDxi ciBjbGFzcz0iIj4NCllvdSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1 YnNjcmliZWQgdG8gdGhlIEdvb2dsZSBHcm91cHMgJnF1b3Q7SG9tb3RvcHkgVHlwZSBUaGVvcnkm cXVvdDsgZ3JvdXAuPGJyIGNsYXNzPSIiPg0KVG8gdW5zdWJzY3JpYmUgZnJvbSB0aGlzIGdyb3Vw IGFuZCBzdG9wIHJlY2VpdmluZyBlbWFpbHMgZnJvbSBpdCwgc2VuZCBhbiBlbWFpbCB0bw0KPGEg aHJlZj0ibWFpbHRvOkhvbW90b3B5VHlwZVRoZW9yeSYjNDM7dW5zdS4uLkBnb29nbGVncm91cHMu Y29tIiBjbGFzcz0iIj5Ib21vdG9weVR5cGVUaGVvcnkmIzQzO3Vuc3UuLi5AZ29vZ2xlZ3JvdXBz LmNvbTwvYT4uPGJyIGNsYXNzPSIiPg0KRm9yIG1vcmUgb3B0aW9ucywgdmlzaXQgPGEgaHJlZj0i aHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL29wdG91dCIgY2xhc3M9IiI+aHR0cHM6Ly9ncm91 cHMuZ29vZ2xlLmNvbS9kL29wdG91dDwvYT4uPGJyIGNsYXNzPSIiPg0KPC9kaXY+DQo8L2Jsb2Nr cXVvdGU+DQo8L2Rpdj4NCjxiciBjbGFzcz0iIj4NCjwvYm9keT4NCjwvaHRtbD4NCg== --_000_D688CD8B5DDE4CA684DE478A8E23890Cchalmersse_--