From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.67.70 with SMTP id m6mr1103694lfj.21.1488050386629; Sat, 25 Feb 2017 11:19:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.167.201 with SMTP id q192ls642153lfe.35.gmail; Sat, 25 Feb 2017 11:19:45 -0800 (PST) X-Received: by 10.46.8.74 with SMTP id g10mr915359ljd.1.1488050385068; Sat, 25 Feb 2017 11:19:45 -0800 (PST) Return-Path: Received: from tyrell.ita.chalmers.se (tyrell.ita.chalmers.se. [129.16.226.132]) by gmr-mx.google.com with ESMTPS id y19si436543wmd.0.2017.02.25.11.19.44 (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sat, 25 Feb 2017 11:19:44 -0800 (PST) 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; Sat, 25 Feb 2017 20:19:43 +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; Sat, 25 Feb 2017 20:19:43 +0100 From: Thierry Coquand To: "univalent-...@googlegroups.com" CC: homotopytypetheory Subject: Re: [HoTT] about the HTS Thread-Topic: [HoTT] about the HTS Thread-Index: AQHSjePTXjyUspl4WUiKTqinTtS8xaF6CauA Date: Sat, 25 Feb 2017 19:19:43 +0000 Message-ID: <12C1D5CB-D95A-4EC1-B5F9-C67F92685529@chalmers.se> References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> In-Reply-To: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> 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_12C1D5CBD95A4EC1B5F9C67F92685529chalmersse_" MIME-Version: 1.0 --_000_12C1D5CBD95A4EC1B5F9C67F92685529chalmersse_ Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: base64 IEhlcmUgaXMgbm90ZSA8aHR0cDovL3d3dy5jc2UuY2hhbG1lcnMuc2UvfmNvcXVhbmQvYmlzaG9w LnBkZj4gd2hpY2ggc2hvdWxkIGJlIGNvbm5lY3RlZCB0byB0aGlzIG1lc3NhZ2UuIEl0IGNvbnRh aW5zIGZpcnN0IGEgc2VsZiBjb250YWluZWQNCnByZXNlbnRhdGlvbiBvZiB0aGUgY3ViaWNhbCBz ZXQgbW9kZWwsIGFuZCB0aGVuIGEgbm90aW9uIG9mIOKAnEJpc2hvcCBzZXTigJ0gd2hpY2ggY29y cmVzcG9uZHMNCnRvIHRoZSBmYWN0IHRoYXQgYW55IHR3byBwYXRocyBiZXR3ZWVuIHRoZSBzYW1l IGVuZCBwb2ludHMgYXJlIC1qdWRnbWVudGFsbHktIGVxdWFsLg0KT25lIGRlZmluZXMgYSBzdWJw cmVzaGVhZiBvZiB0aGUgdW5pdmVyc2Ugd2hpY2ggY2xhc3NpZmllcyB0aGVzZSBzZXRzLCBhbmQg IG9uZSBub3RpY2VzDQp0aGF0IHRoaXMgbm90aW9uIGlzIGNsb3NlZCBieSB0aGUgS2FuIGZpbGxp bmcgb3BlcmF0aW9uIG9mIHRoZSB1bml2ZXJzZSAoYmVjYXVzZSB0aGlzIGlzIGRlZmluZWQNCmlu IHRlcm0gb2YgZ2x1ZWluZywgYW5kIHRoaXMgbm90aW9uIGlzIGNsb3NlZCBieSB0aGUgZ2x1ZWlu ZyBvcGVyYXRpb24pLCBhbmQgaGVuY2UgaXQgaXMgZmlicmFudA0KKGFuZCB1bml2YWxlbnQpLg0K DQogSWYgdGhpcyBpcyBjb3JyZWN0LCBvbmUgZXhwZWN0cyBhIGNvcnJlc3BvbmRpbmcgdHlwZSBz eXN0ZW0gd2l0aCBkZWNpZGFibGUgdHlwZS1jaGVja2luZywgYW5kDQpjb25uZWN0aW9ucyB3aXRo IHdoYXQgaGFzDQpiZWVuIGRvbmUgaW4gb2JzZXJ2YXRpb25hbCB0eXBlIHRoZW9yeSAoYW5kIGl0 IHdpbGwgYmUgaW50ZXJlc3RpbmcgdG8gc2VlIGlmIHRoaXMgY2FuIGFsc28gYmUgY29ubmVjdGVk DQp0byB0aGUgbW9yZSByZWNlbnQgd29yayBvZiBUaG9yc3RlbiBldCBhbC4pIHdoaWxlIHN0YXlp bmcgaW4gYSB1bml2YWxlbnQgdGhlb3J5Lg0KIFRoaWVycnkNCg0KDQpPbiAyMyBGZWIgMjAxNywg YXQgMTU6NDcsIFZsYWRpbWlyIFZvZXZvZHNreSA8dmxhZC4uLkBpYXMuZWR1PG1haWx0bzp2bGFk Li4uQGlhcy5lZHU+PiB3cm90ZToNCg0KSnVzdCBhIHRob3VnaHTigKYgQ2FuIHdlIGRldmlzZSBh IHZlcnNpb24gb2YgdGhlIEhUUyB3aGVyZSBleGFjdCBlcXVhbGl0eSB0eXBlcyBhcmUgbm90IGF2 YWlsYWJsZSBmb3IgdGhlIHVuaXZlcnNlcyBzdWNoIHRoYXQsIGV2ZW4gd2l0aCB0aGUgZXhhY3Qg ZXF1YWxpdHksIEhUUyB3b3VsZCByZW1haW4gYSB1bml2YWxlbnQgdGhlb3J5Lg0KDQpNYXliZSBv bmx5IHNvbWUgdHlwZXMgc2hvdWxkIGJlIGVxdWlwcGVkIHdpdGggdGhlIGV4YWN0IGVxdWFsaXR5 IGFuZCB0aGlzIHNob3VsZCBiZSBhIHNwZWNpYWwgcXVhbGl0eSBvZiB0eXBlcy4NCg0KVmxhZGlt aXIuDQoNClBTIElmIHRoZXJlIGFyZSBoaWdoZXIgaW5kdWN0aXZlIHR5cGVzIHRoZW4gdGhlIGV4 YWN0IGVxdWFsaXR5IHNob3VsZCBub3QgYmUgYXZhaWxhYmxlIGZvciB0aGVtIGVpdGhlci4NCg0K LS0NCllvdSByZWNlaXZlZCB0aGlzIG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQg dG8gdGhlIEdvb2dsZSBHcm91cHMgIkhvbW90b3B5IFR5cGUgVGhlb3J5IiBncm91cC4NClRvIHVu c3Vic2NyaWJlIGZyb20gdGhpcyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20g aXQsIHNlbmQgYW4gZW1haWwgdG8gSG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb208 bWFpbHRvOkhvbW90b3B5VHlwZVRoZS4uLkBnb29nbGVncm91cHMuY29tPi4NCkZvciBtb3JlIG9w dGlvbnMsIHZpc2l0IGh0dHBzOi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQuDQoNCg== --_000_12C1D5CBD95A4EC1B5F9C67F92685529chalmersse_ Content-Type: text/html; charset="utf-8" Content-ID: <694900E708C16843...@chalmers.se> Content-Transfer-Encoding: base64 PGh0bWw+DQo8aGVhZD4NCjxtZXRhIGh0dHAtZXF1aXY9IkNvbnRlbnQtVHlwZSIgY29udGVudD0i dGV4dC9odG1sOyBjaGFyc2V0PXV0Zi04Ij4NCjwvaGVhZD4NCjxib2R5IHN0eWxlPSJ3b3JkLXdy YXA6IGJyZWFrLXdvcmQ7IC13ZWJraXQtbmJzcC1tb2RlOiBzcGFjZTsgLXdlYmtpdC1saW5lLWJy ZWFrOiBhZnRlci13aGl0ZS1zcGFjZTsiIGNsYXNzPSIiPg0KPGRpdiBjbGFzcz0iIj4mbmJzcDtI ZXJlIGlzJm5ic3A7PGEgaHJlZj0iaHR0cDovL3d3dy5jc2UuY2hhbG1lcnMuc2UvfmNvcXVhbmQv YmlzaG9wLnBkZiIgY2xhc3M9IiI+bm90ZSZuYnNwOzwvYT53aGljaCBzaG91bGQgYmUgY29ubmVj dGVkIHRvIHRoaXMgbWVzc2FnZS4gSXQgY29udGFpbnMgZmlyc3QgYSBzZWxmIGNvbnRhaW5lZDwv ZGl2Pg0KPGRpdiBjbGFzcz0iIj5wcmVzZW50YXRpb24gb2YgdGhlIGN1YmljYWwgc2V0IG1vZGVs LCBhbmQgdGhlbiBhIG5vdGlvbiBvZiDigJxCaXNob3Agc2V04oCdIHdoaWNoIGNvcnJlc3BvbmRz PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPnRvIHRoZSBmYWN0IHRoYXQgYW55IHR3byBwYXRocyBiZXR3 ZWVuIHRoZSBzYW1lIGVuZCBwb2ludHMgYXJlIC1qdWRnbWVudGFsbHktIGVxdWFsLjwvZGl2Pg0K PGRpdiBjbGFzcz0iIj5PbmUgZGVmaW5lcyBhIHN1YnByZXNoZWFmIG9mIHRoZSB1bml2ZXJzZSB3 aGljaCBjbGFzc2lmaWVzIHRoZXNlIHNldHMsIGFuZCAmbmJzcDtvbmUgbm90aWNlczwvZGl2Pg0K PGRpdiBjbGFzcz0iIj50aGF0IHRoaXMgbm90aW9uIGlzIGNsb3NlZCBieSB0aGUgS2FuIGZpbGxp bmcgb3BlcmF0aW9uIG9mIHRoZSB1bml2ZXJzZSAoYmVjYXVzZSB0aGlzIGlzIGRlZmluZWQ8L2Rp dj4NCjxkaXYgY2xhc3M9IiI+aW4gdGVybSBvZiBnbHVlaW5nLCBhbmQgdGhpcyBub3Rpb24gaXMg Y2xvc2VkIGJ5IHRoZSBnbHVlaW5nIG9wZXJhdGlvbiksIGFuZCBoZW5jZSBpdCBpcyBmaWJyYW50 PC9kaXY+DQo8ZGl2IGNsYXNzPSIiPihhbmQgdW5pdmFsZW50KS48L2Rpdj4NCjxkaXYgY2xhc3M9 IiI+PGJyIGNsYXNzPSIiPg0KPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPiZuYnNwO0lmIHRoaXMgaXMg Y29ycmVjdCwgb25lIGV4cGVjdHMgYSBjb3JyZXNwb25kaW5nIHR5cGUgc3lzdGVtIHdpdGggZGVj aWRhYmxlIHR5cGUtY2hlY2tpbmcsIGFuZCZuYnNwOzwvZGl2Pg0KPGRpdiBjbGFzcz0iIj5jb25u ZWN0aW9ucyB3aXRoIHdoYXQgaGFzPC9kaXY+DQo8ZGl2IGNsYXNzPSIiPmJlZW4gZG9uZSBpbiBv YnNlcnZhdGlvbmFsIHR5cGUgdGhlb3J5IChhbmQgaXQgd2lsbCBiZSBpbnRlcmVzdGluZyB0byBz ZWUgaWYgdGhpcyBjYW4gYWxzbyBiZSBjb25uZWN0ZWQ8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+dG8g dGhlIG1vcmUgcmVjZW50IHdvcmsgb2YgVGhvcnN0ZW4gZXQgYWwuKSB3aGlsZSBzdGF5aW5nIGlu IGEgdW5pdmFsZW50IHRoZW9yeS48L2Rpdj4NCjxkaXYgY2xhc3M9IiI+Jm5ic3A7VGhpZXJyeTwv ZGl2Pg0KPGRpdiBjbGFzcz0iIj48YnIgY2xhc3M9IiI+DQo8L2Rpdj4NCjxkaXYgY2xhc3M9IiI+ PGJyIGNsYXNzPSIiPg0KPC9kaXY+DQo8ZGl2Pg0KPGJsb2NrcXVvdGUgdHlwZT0iY2l0ZSIgY2xh c3M9IiI+DQo8ZGl2IGNsYXNzPSIiPk9uIDIzIEZlYiAyMDE3LCBhdCAxNTo0NywgVmxhZGltaXIg Vm9ldm9kc2t5ICZsdDs8YSBocmVmPSJtYWlsdG86dmxhZC4uLkBpYXMuZWR1IiBjbGFzcz0iIj52 bGFkLi4uQGlhcy5lZHU8L2E+Jmd0OyB3cm90ZTo8L2Rpdj4NCjxiciBjbGFzcz0iQXBwbGUtaW50 ZXJjaGFuZ2UtbmV3bGluZSI+DQo8ZGl2IGNsYXNzPSIiPkp1c3QgYSB0aG91Z2h04oCmIENhbiB3 ZSBkZXZpc2UgYSB2ZXJzaW9uIG9mIHRoZSBIVFMgd2hlcmUgZXhhY3QgZXF1YWxpdHkgdHlwZXMg YXJlIG5vdCBhdmFpbGFibGUgZm9yIHRoZSB1bml2ZXJzZXMgc3VjaCB0aGF0LCBldmVuIHdpdGgg dGhlIGV4YWN0IGVxdWFsaXR5LCBIVFMgd291bGQgcmVtYWluIGEgdW5pdmFsZW50IHRoZW9yeS48 YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+DQpNYXliZSBvbmx5IHNvbWUgdHlwZXMgc2hvdWxk IGJlIGVxdWlwcGVkIHdpdGggdGhlIGV4YWN0IGVxdWFsaXR5IGFuZCB0aGlzIHNob3VsZCBiZSBh IHNwZWNpYWwgcXVhbGl0eSBvZiB0eXBlcy48YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+DQpW bGFkaW1pci48YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+DQpQUyBJZiB0aGVyZSBhcmUgaGln aGVyIGluZHVjdGl2ZSB0eXBlcyB0aGVuIHRoZSBleGFjdCBlcXVhbGl0eSBzaG91bGQgbm90IGJl IGF2YWlsYWJsZSBmb3IgdGhlbSBlaXRoZXIuDQo8YnIgY2xhc3M9IiI+DQo8YnIgY2xhc3M9IiI+ DQotLSA8YnIgY2xhc3M9IiI+DQpZb3UgcmVjZWl2ZWQgdGhpcyBtZXNzYWdlIGJlY2F1c2UgeW91 IGFyZSBzdWJzY3JpYmVkIHRvIHRoZSBHb29nbGUgR3JvdXBzICZxdW90O0hvbW90b3B5IFR5cGUg VGhlb3J5JnF1b3Q7IGdyb3VwLjxiciBjbGFzcz0iIj4NClRvIHVuc3Vic2NyaWJlIGZyb20gdGhp cyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNlbmQgYW4gZW1haWwg dG8NCjxhIGhyZWY9Im1haWx0bzpIb21vdG9weVR5cGVUaGVvcnkmIzQzO3Vuc3UuLi5AZ29vZ2xl Z3JvdXBzLmNvbSIgY2xhc3M9IiI+SG9tb3RvcHlUeXBlVGhlb3J5JiM0Mzt1bnN1Li4uQGdvb2ds ZWdyb3Vwcy5jb208L2E+LjxiciBjbGFzcz0iIj4NCkZvciBtb3JlIG9wdGlvbnMsIHZpc2l0IDxh IGhyZWY9Imh0dHBzOi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQiIGNsYXNzPSIiPmh0dHBz Oi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQ8L2E+LjxiciBjbGFzcz0iIj4NCjwvZGl2Pg0K PC9ibG9ja3F1b3RlPg0KPC9kaXY+DQo8YnIgY2xhc3M9IiI+DQo8L2JvZHk+DQo8L2h0bWw+DQo= --_000_12C1D5CBD95A4EC1B5F9C67F92685529chalmersse_--