From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:2358:: with SMTP id j85-v6mr369477wmj.4.1529004945505; Thu, 14 Jun 2018 12:35:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:9ecf:: with SMTP id h198-v6ls1943834wme.6.gmail; Thu, 14 Jun 2018 12:35:44 -0700 (PDT) X-Received: by 2002:a1c:4c9:: with SMTP id 192-v6mr343057wme.8.1529004944298; Thu, 14 Jun 2018 12:35:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1529004944; cv=none; d=google.com; s=arc-20160816; b=yABXx5FsNBmbkW0ogQdBWijDU80nudT/k/JY9FFd4O4J6mxH50B+no9LfT/bu6wGia FNquzEcdEZe8lhQllt+75tF6WWIY9AYDmh5H1GL6tV7db+U8VWksr+d9MP0yC87bn5Am ddXznBlEhosHz/D57n9tDaA53XftbbAmBlLt+VyrpHBWlh6t+ZiU+Hf0UW7ha0EH2o1z tc+LHmz503GIykG7ajgHQQtlHq1hCmq7kqUYMMD4kcnkSfsr9ENq/l87fBZDwnGDp4jq +ARybGZqTdNpgFQMikBgWWKJuqF3CRLZH5l+465O6uLdWf3Ml6iQsY/VzN03Rpf+t0M5 67Fw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:arc-authentication-results; bh=aeQ5QEYeN/cKuLgRfhm9+aN2d1m5qz4CGTEDMkAInXA=; b=CL2k/T1gwMzG3CbHJq/Y5iMxEVsc/TcMXCMlH7r0OTqNAI9vU1liSZ2TCiGvQyaEAa cGTaKUI67erc7oYFvlOXkdYPSNrukM5fDwl+8C4VCyA8KsmxlcdZZqIlZ/HRDl+Hywzf uJ94EKwi7XqsKHyIkpn3TIQvyBtzNns6xXmJsAB0CGW7PggN9L4ntd/D32u2+qJJH4Rx +AsZwmeyd62GmrNO9jzrwdVoXkxokeQn8vs+3pCkHS80L44aelqjWdJP0AJ5yc/OuFmy KtVd+y/GRJCDsbRZsTKVBETo/8M8Q5pRMbeSVoxiYy1aimeZRi6zAi9rElyzlScxPwrc BZ1A== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.133 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) smtp.mailfrom=Thierry...@cse.gu.se Return-Path: Received: from targaryen.ita.chalmers.se (targaryen.ita.chalmers.se. [129.16.226.133]) by gmr-mx.google.com with ESMTPS id x21-v6si103550wmh.3.2018.06.14.12.35.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 14 Jun 2018 12:35:44 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.133 is neither permitted nor denied by best guess record for domain of thierry...@cse.gu.se) client-ip=129.16.226.133; Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.133 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 targaryen.ita.chalmers.se (129.16.226.133) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1415.2; Thu, 14 Jun 2018 21:35:43 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.1415.007; Thu, 14 Jun 2018 21:35:43 +0200 From: Thierry Coquand To: Richard Williamson CC: Homotopy Theory Subject: Re: [HoTT] Quillen model structure, PS Thread-Topic: [HoTT] Quillen model structure, PS Thread-Index: AQHUBBbi5vjGkQVLxUK/PUCIDcPT2A== Date: Thu, 14 Jun 2018 19:35:43 +0000 Message-ID: <87AA5F45-E3E9-4F1C-B104-82D41A6B8573@chalmers.se> References: <20180614183959.GA1401@richard.richard> In-Reply-To: <20180614183959.GA1401@richard.richard> Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: text/plain; charset="utf-8" Content-ID: <7B06FF0D55CCE546...@chalmers.se> Content-Transfer-Encoding: base64 MIME-Version: 1.0 DQogIEkgd3JvdGUNCg0K4oCU4oCU4oCU4oCU4oCU4oCUDQoNCmlmIHdlIGxpbWl0IG91cnNlbHZl cyB0byB0aGUgY2FzZSB3aGVyZSB0aGUgYmFzZSBjYXRlZ29yeSBpcyB0aGUgTGF3dmVyZSB0aGVv cnkgb2YNCmRpc3RyaWJ1dGl2ZSBsYXR0aWNlcywgb3IgZGUgTW9yZ2FuIGFsZ2VicmEsIG9yIEJv b2xlYW4gYWxnZWJyYSBhbmQgd2UgdGFrZSB0aGUgZmlicmF0aW9ucw0KYXMgZGVmaW5lZCBwYWdl IDEzLCB3ZSBnZXQgdGhlIHNhbWUgbm90aW9uIGFzIENpc2luc2tpIC1uYWl2ZS0gZmlicmF0aW9u cy4NCg0K4oCU4oCU4oCU4oCU4oCU4oCUDQoNCiBJIHNob3VsZCBoYXZlIGFkZGVkIHRoYXQgdGhp cyBpcyBub3QgY29tcGxldGVseSB0cml2aWFsOiBpdCBhbW91bnRzIHRvIHRoZSBmYWN0IHRoYXQg dG8gDQpoYXZlIHRoZSAtdW5pZm9ybS0gcmlnaHQgbGlmdGluZyBmaWxsaW5nIHByb3BlcnR5IHcu ci50LiBhbnkgb3BlbiBib3ggaW5jbHVzaW9uDQoNCiBBIHggSUkgXGN1cCBCIHggYiAgICAtPiAg ICAgQiAgeCBJSSAgICAgICAgICAgICB3aGVyZSBCIGlzIC1yZXByZXNlbnRhYmxlLSwgQSAtPiBC IG1vbm8NCg0KKHdoZXJlIHdlIGhhdmUgYSBjaG9pY2Ugb2YgbGlmdGluZyB0aGF0IGFyZSBuYXR1 cmFsIHcuci50LiBtYXAgQuKAmSAtPiBCIGJldHdlZW4NCnJlcHJlc2VudGFibGVzKQ0KDQppcyAt ZXF1aXZhbGVudC0gdG8gaGF2aW5nIHRoZSAobm9uIG5lY2Vzc2FyaWx5IHVuaWZvcm0pIHJpZ2h0 IGxpZnRpbmcgcHJvcGVydHkgDQp3LnIudC4gLWFueS0gb3BlbiBib3ggaW5jbHVzaW9uDQoNCiBB IHggSUkgXGN1cCBCIHggYiAgICAtPiAgICAgQiAgeCBJSSAgICAgICAgICAgICBCIGFyYml0cmFy eSwgQSAtPiBCIG1vbm8NCg0KDQoNCiAgVGhlIHNhbWUgaG9sZHMgKGFuZCBpcyBlaXRoZXIgdG8g Y2hlY2spIGZvciB0cml2aWFsIGZpYnJhdGlvbnM6IHRvIGhhdmUgdGhlIHVuaWZvcm0NCnJpZ2h0 IGxpZnRpbmcgcHJvcGVydHkgdy5yLnQuIEEgLT4gQiBtb25vLCBCIHJlcHJlc2VudGFibGUgaXMg ZXF1aXZhbGVudCB0byBoYXZpbmcNCnRoZSByaWdodCBsaWZ0aW5nIHByb3BlcnR5IHcuci50LiBh biBhcmJpdHJhcnkgbW9uby4NCg0KIEJlc3QgcmVnYXJkcywNCiBUaGllcnJ5DQoNCg0KDQo+IE9u IDE0IEp1biAyMDE4LCBhdCAyMDozOSwgUmljaGFyZCBXaWxsaWFtc29uIDxyd2lsbGkuLi5AZ21h aWwuY29tPiB3cm90ZToNCj4gDQo+IERlYXIgVGhpZXJyeSwNCj4gDQo+IEZvcmdpdmUgbWUgZm9y IG5vdCBxdWl0ZSBoYXZpbmcgYW4gb3ZlcnZpZXcgb2YgZXhhY3RseSB3aGF0IGhhcw0KPiBiZWVu IGRvbmUuIE15IGludGVyZXN0IGhlcmUgaXMgaW4gaG93IHRoZSBtb2RlbCBzdHJ1Y3R1cmUgeW91 DQo+IGhhdmUgY29uc3RydWN0ZWQgY29tcGFyZXMgd2l0aCBDaXNpbnNraSdzIHdvcmsuIEZvciBl eGFtcGxlLCBJDQo+IHdvdWxkIGV4cGVjdCB0aGF0IHRoZSBjYXRlZ29yeSBvZiBjYXJ0ZXNpYW4g Y3ViaWNhbCBzZXRzIGlzIGENCj4gdGVzdCBjYXRlZ29yeS4gSW5kZWVkLCBJIHdvdWxkIGV4cGVj dCB0aGF0IG1vcmUgb3IgbGVzcyBleGFjdGx5DQo+IHRoZSBzYW1lIHRlY2huaXF1ZSBhcyBpbiA4 LjQgb2YgTGVzIHByw6lmYWlzY2VhdXggY29tbWUgLi4uIGdvZXMNCj4gdGhyb3VnaCB0byBwcm92 ZSB0aGlzLiBBbmQgSSB3b3VsZCBleHBlY3QgdGhhdCBvbmUgY2FuIHB1dCBhDQo+IG1vZGVsIHN0 cnVjdHVyZSBvbiBpbiB0aGUgc2FtZSB3YXkuDQo+IA0KPiBOb3csIEkgYmVsaWV2ZSBJIHNhdyBp biBzb21lIHNsaWRlcyB0aGF0IHRoYXQgeW91ciBtb2RlbA0KPiBzdHJ1Y3R1cmUgY29pbmNpZGVz IHdpdGggdGhlIENpc2luc2tpIG9uZS4gQnV0IHRoaXMgZG9lcyBub3Qgc2VlbQ0KPiBjb21wYXRp YmxlIHdpdGggbXkgZXhwZWN0YXRpb25zIGFib3ZlLCBiZWNhdXNlIHRoZW4gaXQgaXMNCj4gY2Vy dGFpbmx5IFF1aWxsZW4gZXF1aXZhbGVudCB0byB0aGUgU2VycmUgbW9kZWwgc3RydWN0dXJlIG9u DQo+IHRvcG9sb2dpY2FsIHNwYWNlcyAob3Igd2hhdGV2ZXIpLg0KPiANCj4gVGh1cyBteSBxdWVz dGlvbnM6DQo+IA0KPiAxKSBIYXZlIEkgbWlzaW50ZXJwcmV0ZWQgdGhlIHNsaWRlcyBvciBzb21l IG90aGVyIGFzcGVjdCBvZiB5b3VyDQo+IHdvcms/DQo+IA0KPiAyKSBJZiBub3QsIHdoZXJlIGV4 YWN0bHkgZG8gQ2lzaW5za2kncyB0ZWNobmlxdWVzIGZhaWw/DQo+IA0KPiBCZXN0IHdpc2hlcywN Cj4gUmljaGFyZA0KDQo=