From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.89.6 with SMTP id n6mr586725lfb.8.1466075301618; Thu, 16 Jun 2016 04:08:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.132.129 with SMTP id g123ls427451wmd.9.gmail; Thu, 16 Jun 2016 04:08:21 -0700 (PDT) X-Received: by 10.194.156.200 with SMTP id wg8mr577953wjb.7.1466075300962; Thu, 16 Jun 2016 04:08:20 -0700 (PDT) Return-Path: Received: from mhost02h.leeds.ac.uk (mhost02h.leeds.ac.uk. [129.11.77.151]) by gmr-mx.google.com with ESMTPS id x203si518225wme.0.2016.06.16.04.08.20 for (version=TLS1_2 cipher=AES128-GCM-SHA256 bits=128/128); Thu, 16 Jun 2016 04:08:20 -0700 (PDT) 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; 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 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 u5GB8HAe009904 (version=TLSv1/SSLv3 cipher=AES256-SHA bits=256 verify=NOT); Thu, 16 Jun 2016 12:08:19 +0100 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; Thu, 16 Jun 2016 12:08:18 +0100 Received: from emea01-db3-obe.outbound.protection.outlook.com (213.199.154.79) by outlook.leeds.ac.uk (129.11.6.119) with Microsoft SMTP Server (TLS) id 14.3.195.1; Thu, 16 Jun 2016 12:08:18 +0100 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=w1UhDeK2JsreL95Ocbd7cgB/L2MT2Z/226cUn+UzJbM=; b=alngOtsNHIFlxkEEQX5IYMpuT47TxtyZpDOXZgD1ouVEAzy8MWCEh/LrYl4hImtMiLhhVqDkx+283frdpAFw7PGkmCYZuvVO5c/w2dBlZ7mOlpb/b1HJ7tzM1MkNzXKRufo8Y6ieJd5XcLYyhdSRGM1hWpLhI/neFOC22dvQ/jk= Received: from DB5PR03MB1544.eurprd03.prod.outlook.com (10.164.179.18) by DB5PR03MB1543.eurprd03.prod.outlook.com (10.164.179.17) with Microsoft SMTP Server (TLS) id 15.1.523.12; Thu, 16 Jun 2016 11:08:17 +0000 Received: from DB5PR03MB1544.eurprd03.prod.outlook.com ([10.164.179.18]) by DB5PR03MB1544.eurprd03.prod.outlook.com ([10.164.179.18]) with mapi id 15.01.0523.011; Thu, 16 Jun 2016 11:08:17 +0000 From: Nicola Gambino To: Homotopy Type Theory CC: Andrej Bauer Subject: Re: [HoTT] Is synthetic the right word? Thread-Topic: [HoTT] Is synthetic the right word? Thread-Index: AQHRxzNv5vmZbAAUyUurEwfAh6y5C5/r5PoAgAALi4A= Date: Thu, 16 Jun 2016 11:08:17 +0000 Message-ID: <938A64FB-A458-48ED-8C15-4DA72C9715BB@leeds.ac.uk> References: In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3112) authentication-results: spf=none (sender IP is ) smtp.mailfrom=N.Ga...@leeds.ac.uk; x-ms-exchange-messagesentrepresentingtype: 1 x-originating-ip: [95.150.149.200] x-ms-office365-filtering-correlation-id: 92a1dbe4-bcea-4f4d-67eb-08d395d684e3 x-microsoft-exchange-diagnostics: 1;DB5PR03MB1543;6:3ViK3Aq8wMgpmPNj3Ix4kcAglUTczr3nPSZUwBo99kKt/gJBZBN/v+RJnQ2xS2SrnYIO5BWVE8cbHxxEiDZ1mEUFFvCAKIOaFr6rCMXT19nVpJdq4CWzV5+davlHfQfKPpKm44eCrNPQmXiY4uC8ZPzlxPnhs+wnn6doHB4YI9UU4eFzBhh0BAVJpvWI3zQOUPp2N9b+pFGWqtc2QHFEoMA532nRQrhBeOAR3Xzrup9+DhhMuxK0aD1BOSpVYT9xqO+IoSsYBpqVcvuNNET4OFnhdu10DFXwQk1M3h2/eME=;5:FYLRfcnZDOobanYlqw2xQ8wP5G2WGk1/qnSoVZOoDy2K0djFVChwAnnqJPsPg+RwNmNdcJAPmXEAo/sSRPy+7menOjHP05e+qjFaFiV9YGEmUYjxaG1as2sVJbxeJ0/m+lJdtNF4patQNMoHW/T5LA==;24:Fp2tBrV7XLcT0a1AXoeo0Oy+rEGMBdVCEVaJge2agWEV58XPcgT+Be9BzuJBOHJXEOZ2q2jneHw5MrNVg133MAvAu5u/dHmp9N1jQ3WggXg=;7:RUj7sfIRKQdDSdzHWu3W1mN1Nt0ku6MAWxCbtRuq0foRySFgEajfYfmUm47W1Zvd7ujihtlaD6QAnS6scYi8meiNwsA94PfAX1f6nIisz1OgS7xKcs9yLTbiZN5x/h03akW/BIV4IMjY6bX2wUSsfaOYAAKvp44lqeDHtVIJf39G3ROSHF/eTfaYnuAhKl4THM+sDJFdXbCIiva411cI3w== x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:;SRVR:DB5PR03MB1543; x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(228788266533470)(211936372134217); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(601004)(2401047)(5005006)(8121501046)(3002001)(10201501046);SRVR:DB5PR03MB1543;BCL:0;PCL:0;RULEID:;SRVR:DB5PR03MB1543; x-forefront-prvs: 09752BC779 x-forefront-antispam-report: SFV:NSPM;SFS:(10009020)(6009001)(7916002)(199003)(51444003)(252514010)(24454002)(71364002)(189002)(10400500002)(5008740100001)(82746002)(3660700001)(11100500001)(19580405001)(122556002)(19580395003)(87936001)(5004730100002)(189998001)(3280700002)(86362001)(110136002)(4326007)(2900100001)(2906002)(92566002)(66066001)(101416001)(586003)(8936002)(5002640100001)(106116001)(2950100001)(81166006)(106356001)(81156014)(76176999)(8676002)(50986999)(50226002)(57306001)(105586002)(68736007)(36756003)(77096005)(97736004)(33656002)(6116002)(74482002)(83716003)(15975445007)(102836003)(3846002)(104396002);DIR:OUT;SFP:1101;SCL:1;SRVR:DB5PR03MB1543;H:DB5PR03MB1544.eurprd03.prod.outlook.com;FPR:;SPF:None;PTR:InfoNoRecords;A:1;MX:1;CAT:NONE;LANG:en;CAT:NONE; received-spf: None (protection.outlook.com: leeds.ac.uk does not designate permitted sender hosts) spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <3F1F0135AAD86547...@eurprd03.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Jun 2016 11:08:17.3867 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: bdeaeda8-c81d-45ce-863e-5232a535b7cb X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR03MB1543 X-OriginatorOrg: leeds.ac.uk X-UOL-RateLimit: userRateLimit[a:n.g...@leeds.ac.uk,c:2.2615100966850616,l:500.0] RGVhciBhbGwsDQoNCkkgZG8gbm90IHRoaW5rIHRoYXQgdGhlIHdvcmQg4oCcc3ludGhldGlj4oCd IGluIHRoZXNlIGNvbnRleHRzIGlzIGludGVuZGVkIHRvIG1lYW4g4oCcYXJ0aWZpY2lhbOKAnS4N Cg0KSW5zdGVhZCwgSSB0aGluayB0aGF0IGl0IGlzIHVzZWQgdG8gZGVub3RlIHRoZSByZXN1bHQg b2YgYSBzeW50aGVzaXMuIFRoaXMgaXMgdGhlIHNhbWUgd2F5IGluIHdoaWNoIOKAnHN5bnRoZXRp Y+KAnSBpcyB1c2VkIGluIHRoZSBleHByZXNzaW9uIOKAnHN5bnRoZXRpYyBnZW9tZXRyeeKAnSwg YXMgb3Bwb3NlZCB0byAiYW5hbHl0aWMgZ2VvbWV0cnnigJ0uIEluIGFuYWx5dGljIGdlb21ldHJ5 LCB3ZSB1c2UgY29vcmRpbmF0ZXMgdG8gZGVmaW5lIHBvaW50cywgbGluZXMsIGV0Yy4uLCB3aGls ZSBpbiBzeW50aGV0aWMgZ2VvbWV0cnkgdGhlc2Ugbm90aW9ucyBhcmUgdGFrZW4gYXMgcHJpbWl0 aXZlLiBUaGUgdHdvIHdheXMgb2YgZG9pbmcgZ2VvbWV0cnkgYXJlIHJlbGF0ZWQgcHJlY2lzZWx5 LiANCg0KVGhlcmUgaXMgYSBjbGVhciBzaW1pbGFyaXR5IHdpdGggdGhlIHNpdHVhdGlvbiBpbiBo b21vdG9weSB0aGVvcnkuIENsYXNzaWNhbCBob21vdG9weSB0aGVvcnksIGluIHdoaWNoIHRvcG9s b2dpY2FsIHNwYWNlcyBhcmUgZGVmaW5lZCB2aWEgdGhlaXIgcG9pbnRzIGFuZCBvcGVuIHNldHMs IGlzIHRoZSBhbmFsb2d1ZSBvZiBhbmFseXRpYyBnZW9tZXRyeS4gSG9tb3RvcHkgdGhlb3J5IGRv bmUgaW4gbW9kZWwgY2F0ZWdvcmllcyBvciBpbiB0eXBlIHRoZW9yeSBpcyB0aGUgYW5hbG9ndWUg b2Ygc3ludGhldGljIGdlb21ldHJ5LCBhbmQgdGhlcmVmb3JlIGl0IGlzIG5vdCB1bnJlYXNvbmFi bGUgdG8gY2FsbCBpdCBzeW50aGV0aWMgaG9tb3RvcHkgdGhlb3J5LiBBbiBhbHRlcm5hdGl2ZSB3 b3VsZCBiZSB0byBjYWxsIGl0IOKAnGF4aW9tYXRpYyBob21vdG9weSB0aGVvcnkiDQoNCkluIGVp dGhlciBjYXNlLCBJIHRoaW5rIHRoYXQgYWRkaW5nIOKAnHN5bnRoZXRpY+KAnSBvciDigJxheGlv bWF0aWPigJ0gdG8g4oCcaG9tb3RvcHkgdGhlb3J54oCdIGlzIG5vdCBpbnRlbmRlZCB0byBzdWdn ZXN0IGEgZGlmZmVyZW50IHN1YmplY3QsIGJ1dCByYXRoZXIgYSBkaWZmZXJlbnQgd2F5IG9mIGRv aW5nIHRoaW5ncy4gDQoNCkJlc3Qgd2lzaGVzLA0KTmljb2xhDQoNCg0KPiBPbiAxNiBKdW4gMjAx NiwgYXQgMTE6MjcsIEFuZHJlaiBCYXVlciA8YW5kcmVqLi4uQGFuZHJlai5jb20+IHdyb3RlOg0K PiANCj4gVmFyaW91cyBzdWJqZWN0cyBoYXZlIGJlZW4gY2FsbGVkIHN5bnRoZXRpYywgYW5kIGlu IGV2ZXJ5IGNhc2UgSSBhbQ0KPiBhd2FyZSBvZiB0aGUgc3ViamVjdCBkZXZlbG9wcyBhIGJyYW5j aCBvZiBtYXRoZW1hdGljcyBpbiAodGhlIGludGVybmFsDQo+IGxhbmd1YWdlIG9mKSBhIHRvcG9z IHRoYXQgaXMgcGFydGljdWxhcmx5IHN1aXRhYmxlIGZvciB0aGUgdG9waWMgYXQNCj4gaGFuZC4g VGh1cyB3ZSBoYXZlIGhhZCBTeW50aGV0aWMgRGlmZmVyZW50aWFsIEdlb21ldHJ5LCBTeW50aGV0 aWMNCj4gRG9tYWluIFRoZW9yeSwgU3ludGhldGljIFRvcG9sb2d5IGFuZCBTeW50aGV0aWMgQ29t cHV0YWJpbGl0eS4NCj4gDQo+IFRoZSB3b3JkICJzeW50aGV0aWMiIGhlcmUgcmVmZXJzIHRvIHRo ZSBmYWN0IHRoYXQgd2UgY3JlYXRlIGFuDQo+IGFydGlmaWNpYWwsIG9yIHN5bnRoZXRpYywgd29y bGQgb2YgbWF0aGVtYXRpY3Mgc3VpdGFibGUgZm9yIGRvaW5nDQo+IHdoYXRldmVyIGl0IGlzIHdl IGFyZSBkb2luZy4gRm9yIGluc3RhbmNlLCB0aGUgZWZmZWN0aXZlIHRvcG9zIGlzDQo+IHN1aXRh YmxlIGZvciBkb2luZyBjb21wdXRhYmlsaXR5LiBJZiBJIGFtIHdyb25nIGFib3V0IHRoaXMgcGFy dGljdWxhcg0KPiBwb2ludCwgSSB3b3VsZCBsaWtlIHRvIGhlYXIgd2h5IFN5bnRoZXRpYyBEaWZm ZXJlbnRpYWwgR2VvbWV0cnkgd2FzDQo+IG9yaWdpbmFsbHkgc28gY2FsbGVkLg0KPiANCj4gVGhl IHdvcmQgInN5bnRoZXRpYyIgZG9lcyBub3QgcmVmZXIgdG8gdGhlcmUgYmVpbmcgYSBjb21wbGV0 ZWx5IG5ldw0KPiB0aGluZyB0aGF0IGlzIGRpZmZlcmVudCBmcm9tIHdoYXQgaGFzIGJlZW4gZG9u ZSBzbyBmYXIuIEluIHRoZSBhYm92ZQ0KPiBleGFtcGxlcyB0aGVyZSBpcyBhbHdheXMgYSBjbGVh ciBjb25uZWN0aW9uIHRvIHRoZSB0cmFkaXRpb25hbCB3YXlzLA0KPiB3aXRoIHN1aXRhYmxlIHRy YW5zZmVyIHRoZW9yZW1zIGd1YXJhbnRlZWluZyB0aGF0IHRoZSBzeW50aGV0aWMgd29ybGQNCj4g aXMgbm90IGp1c3QgYSBoYWxsdWNpbmF0aW9uLg0KPiANCj4gSW4gbGluZSB3aXRoIHRoZSBlc3Rh Ymxpc2hlZCB0ZXJtaW5vbG9neSwgc3VjaCBhcyBpdCBtYXkgYmUsIFN5bnRoZXRpYw0KPiBIb21v dG9weSBUaGVvcnkgd291bGQgYmUgaG9tb3RvcHkgdGhlb3J5IGRldmVsb3BlZCBpbiAodGhlIGlu dGVybmFsDQo+IGxhbmd1YWdlIG9mKSBhIHRvcG9zLCBvciBvdGhlciBzdWl0YWJsZSBzdHJ1Y3R1 cmUsIHRoYXQgaXMNCj4gcGFydGljdWxhcmx5IHN1aXRhYmxlIGZvciBkb2luZyBob21vdG9weSB0 aGVvcnkuIE9uZSBtYXkgcHV0IGEgdmFyeWluZw0KPiBhbW91bnRzIG9mIGVtcGhhc2lzIG9uIHRo ZSBpbnRlcm5hbCBsYW5ndWFnZSBvciB0aGUgbW9kZWxzLCBhY2NvcmRpbmcNCj4gdG8gdGFzdGUu IFdoYXQgSSB0aGluayB3ZSBhcmUgbGFja2luZyBhdCB0aGUgbW9tZW50IGlzIGEgY2xlYXIgd2F5 IG9mDQo+IHRyYW5zZmVyaW5nIHJlc3VsdHMgaW4gc3ludGhldGljIGhvbW90b3B5IHRoZW9yeSBi YWNrIHRvIGEgdHJhZGl0aW9uYWwNCj4gc2V0dXAuIFRoZSBleHBsYW5hdGlvbiB3aGljaCBzYXlz ICJpbnRlcnByZXRldCBpbiBLYW4gc2ltcGxpY2lhbCBzZXRzDQo+IGFuZCBhcHBseSB0aGUgZ2Vv bWV0cmljIHJlYWxpemF0aW9uIiBkb2VzIG5vdCBzZWVtIHRvIGJlIGdvb2QgZW5vdWdoLA0KPiBv ciBhdCBsZWFzdCBpdCBzaG91bGQgYmUgbWFkZSBtYXRoZW1hdGljYWxseSBwcmVjaXNlLiBQZXJo YXBzIHRoZSB3ZQ0KPiBzaG91bGQganVzdCBmb3JnZXQgYWJvdXQgdG9wb2xvZ3kgYW5kIHVzZSBz aW1wbGljaWFsIHNldHMgYXMgdGhlDQo+IG5hdHVyYWwgdHJhZGl0aW9uYWwgc2V0dXAgZm9yIGRv aW5nIGhvbW90b3B5IHRoZW9yeT8NCj4gDQo+IFdlIGV2ZW4gaGF2ZSBTeW50aGV0aWMgQ29tYmlu YXRvcmljcywgYWx0aG91Z2ggaXRzIGF1dGhvciBwcmVmZXJzIHRvDQo+IGFkb3B0IHRlcm1pbm9s b2d5IGZyb20gYmlvbG9neSBhbmQgYW50aHJvcG9sb2d5IDotKQ0KPiANCj4gV2l0aCBraW5kIHJl Z2FyZHMsDQo+IA0KPiBBbmRyZWoNCj4gDQo+IC0tIA0KPiBZb3UgcmVjZWl2ZWQgdGhpcyBtZXNz YWdlIGJlY2F1c2UgeW91IGFyZSBzdWJzY3JpYmVkIHRvIHRoZSBHb29nbGUgR3JvdXBzICJIb21v dG9weSBUeXBlIFRoZW9yeSIgZ3JvdXAuDQo+IFRvIHVuc3Vic2NyaWJlIGZyb20gdGhpcyBncm91 cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNlbmQgYW4gZW1haWwgdG8gSG9t b3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb20uDQo+IEZvciBtb3JlIG9wdGlvbnMsIHZp c2l0IGh0dHBzOi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQuDQoNCj09PQ0KRHIgTmljb2xh IEdhbWJpbm8NClNjaG9vbCBvZiBNYXRoZW1hdGljcw0KVW5pdmVyc2l0eSBvZiBMZWVkcw0KRS1t YWlsOiBuLmdhLi4uQGxlZWRzLmFjLnVrDQoNCg0KDQoNCg==