From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.170.136 with SMTP id t130mr100698wme.28.1513002212752; Mon, 11 Dec 2017 06:23:32 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.138.198 with SMTP id m189ls1631551wmd.4.canary-gmail; Mon, 11 Dec 2017 06:23:31 -0800 (PST) X-Received: by 10.28.63.83 with SMTP id m80mr128293wma.10.1513002211196; Mon, 11 Dec 2017 06:23:31 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513002211; cv=none; d=google.com; s=arc-20160816; b=nYfr4KU0h0R9NkgyN/C8tXa9e4OHEyn+ZZ27s50MA8wX/trGfpJ+KC5Gz4Zc6RQL/+ cqTcbDrj7r7/VUhp959MYexNJlOJbzI015fXkh9d3HnHf4xp6Sb07N7aMN7q6WEorX1Z /gc2m6ERvPAtdXFo9NU5fpd243uMqLHdqJlxtgyytmsIcaSD88pL6unokvwvlir+WPKV P9cmasLvHXa1rJzk0FCVgvPauKZ7PAR6xI193ennt6x6YGahzQE3jsc+9fFJQuTimqyr MaM5WQqwsMwxOmEu3jRDkCfQI5KLm/eB470gDP8fLzziq0Cmar5Wpnj3TbcSvIJOIDxV kM5A== 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 :spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from :arc-authentication-results; bh=t3XUYKgrumcvS7G7r8BpYNeAMs4qPBpezvJFhvu8ylE=; b=fjYnyk3IPICKHrFFoRcPs0cq6CvVw0VWArXc95hc24Q0Z3GoE8OQOsGtM0pHTDtoKk PPsgamnoE+KmqGvkbCyf/5z8hLUYWiAQL662hZSEhQVcYzHWaRWLq9MhdJnc4aVL08OP 3fekk5iFsiRkKm0lHWg/0X0VouMUy4BfwxSMkcyoVwPIdKcPc2fc15TDQuA+f8Ufp4b/ kodih9BPaBkcDYq4fbcusk5/qx64hu1crIXIhw1a18Q7v2lYyalrO0OZO1VQAmCr51z/ afNfqxbEa2JW+koKVwRwct9SJoftTC1eVkOVe5NWxj3dEafX+30vRZ2hLiBiPwFMqG5l vE6w== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Return-Path: Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTP id e80si964978wmi.2.2017.12.11.06.23.31 for ; Mon, 11 Dec 2017 06:23:31 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 97B2A7804DF_A2E94E2B for ; Mon, 11 Dec 2017 14:23:30 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 5A91D7677EB_A2E94E2F for ; Mon, 11 Dec 2017 14:23:30 +0000 (GMT) Received: from uiwexhub03.is.nottingham.ac.uk ([128.243.15.146] helo=UIWEXHUB03.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1:AES128-SHA:128) (Exim 4.85) (envelope-from ) id 1eOOzS-0006zc-CO; Mon, 11 Dec 2017 14:23:30 +0000 Received: from EUR02-AM5-obe.outbound.protection.outlook.com (213.199.180.148) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Mon, 11 Dec 2017 14:23:29 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) by DB5PR06MB1718.eurprd06.prod.outlook.com (10.165.213.16) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.302.9; Mon, 11 Dec 2017 14:23:28 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::51a3:6727:473b:460e]) by DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::51a3:6727:473b:460e%14]) with mapi id 15.20.0302.013; Mon, 11 Dec 2017 14:23:28 +0000 From: Thorsten Altenkirch To: Kristina Sojakova , Homotopy Type Theory Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Thread-Topic: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? Thread-Index: AQHTcje6ntODVCgsJUW7bijhlNm7RaM+MsiA Date: Mon, 11 Dec 2017 14:23:28 +0000 Message-ID: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> In-Reply-To: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/f.21.0.170409 authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1718;6:rC7BGDnazr/5AHJN+DTaNDdvVt5FoMKNOgx074gHyLDKMVri8ksuEf+RuUhpcd6dBqLiokxykXQFNnAbM1wxBOUkJB5xF5SiSUVpQ1Lgxvm2UMRaLMFzha4hA250r5eKmXaYumuIWuJ9dvlGe1GvDEvyIdYlooz7AXUJSK20jORDT09oSfKMe6UWCWuM0jyhBnknP1VHpLgn402UN9W+Zf/lnYXhoI+f1vG6cQ6z6F4+bD0N9CdGGExvpnLjcRDINdDaz3afWHcxFR8XYClCJZ0eYZXbgs/8tSWSJP8WOGtTdhbJrNZDRzqTBWX07j56eZcnXXq/zfdhQxryKLBQYGdrleDb+mMM59sHfNd6db0=;5:lkhQbnuTXryeEUUKMUeKc6BDVfUwvM4jlct1MMEzct5r8ktrGGTsJyHk8nwGTK6nQ9V0C4Z6o3mdmhdrlz2Ocj5UvHyNXYK4C9/JPDNT1nbdnVniKcw7/mDId7XRhJDBPM5JqoXxuTDGPdOf9fyfFp2AqAQDTh7gH6B35w8tvO4=;24:k898yYFhol/MK5msQffnu/h5IupHXDFr+rjoJOgBqgXZZoZ9KeSWd5L8vQe34zMO9+qWOg4w110Ixi7YtHjloovmdFBt+69HFUadIhgSRCI=;7:8MW2ki4jw/Ck+BV2tDz/moJPx3ScVoo/z33j4ZdQK+5IYFT3tJyL/8SEibLXKkXweZrdMGRPfzZ7YgWC7lQFw91x9ER3akhAMeNimDSU+glTtw31LPHaoCZjNweZ5akwpaFaEnkHW1gN5T4uRK3HOsnwphnWcziG6Je+/UQ8II+kTpztdK/IxDUAoc5g5XOcqbKMNpKnCxxAeBEEwXBilAxXe73VawB7ct+E6EjoRPh3PSg6YB+haMY5jJZ1heOW x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 04fc3abc-af73-4042-fac2-08d540a2bfb6 x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(5600026)(4604075)(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(2017052603307);SRVR:DB5PR06MB1718; x-ms-traffictypediagnostic: DB5PR06MB1718: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(211936372134217)(155532106045638); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(8121501046)(5005006)(10201501046)(93006095)(93001095)(3231022)(920507027)(3002001)(6041248)(20161123560025)(20161123562025)(20161123564025)(20161123558100)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123555025)(6072148)(201708071742011);SRVR:DB5PR06MB1718;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1718; x-forefront-prvs: 0518EEFB48 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(346002)(366004)(24454002)(51874003)(189003)(199004)(42882006)(2950100002)(966005)(39060400002)(53546010)(786003)(316002)(25786009)(8676002)(33656002)(81166006)(81156014)(86362001)(99286004)(76176011)(8936002)(53936002)(110136005)(6306002)(3280700002)(5250100002)(106356001)(68736007)(83506002)(6246003)(229853002)(5660300001)(2900100001)(58126008)(6512007)(97736004)(66066001)(2906002)(478600001)(3660700001)(14454004)(83716003)(3846002)(102836003)(82746002)(74482002)(6436002)(305945005)(6486002)(6506006)(6116002)(34040400001)(7736002)(105586002)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1718;H:DB5PR06MB1717.eurprd06.prod.outlook.com;FPR:;SPF:None;PTR:InfoNoRecords;MX:1;A:1;LANG:en; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <2BB93D88D9246847...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 04fc3abc-af73-4042-fac2-08d540a2bfb6 X-MS-Exchange-CrossTenant-originalarrivaltime: 11 Dec 2017 14:23:28.7644 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR06MB1718 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: -0.0 (/) SGkgS3Jpc3RpbmEsDQoNCkkgZ3Vlc3MgeW91IGFyZSBub3QgYXNzdW1pbmcgUHJvcDpTZXQgYmVj YXVzZSB0aGF0IHdvdWxkIGJlIFN5c3RlbSBVIGFuZCBoZW5jZSBpbmNvbnNpc3RlbnQuDQoNCkJ5 IHByb29mLWlycmVsZXZhbmNlIEkgYXNzdW1lIHRoYXQgeW91IG1lYW4gdGhhdCBhbnkgdHdvIGlu aGFiaXRhbnRzIG9mIGEgcHJvcG9zaXRpb24gYXJlIGRlZmluaXRpb25hbGx5IGVxdWFsLiBUaGlz IGFzc3VtcHRpb24gaXMgaW5jb25zaXN0ZW50IHdpdGggaXQgYmVpbmcgYSB0b3BzIHNpbmNlIGlu IGFueSBUb3BvcyB5b3UgZ2V0IHByb3Bvc2l0aW9uYWwgZXh0ZW5zaW9uYWxpdHksIHRoYXQgaXMg UCxRIDogUHJvcCwgKFAgPC0+IFEpIDwtPiAoUCA9IFEpLCB3aGljaCBpcyBpbmRlZWQgYW4gaW5z dGFuY2Ugb2YgdW5pdmFsZW5jZS4gDQoNCkl0IHNob3VsZCBiZSBwb3NzaWJsZSB0byB1c2UgYSBy ZWFsaXphYmlsaXR5IHNlbWFudGljcyBsaWtlIG9tZWdhLXNldHMgb3IgTGFtYmRhLXNldHMgdG8g bW9kZWwgdGhlIGltcHJlZGljYXRpdmUgdGhlb3J5IGFuZCBpZGVudGlmeSB0aGUgcHJvcG9zaXRp b25zIHdpdGggUEVScyB0aGF0IGFyZSBqdXN0IHN1YnNldHMuIA0KDQpDaGVlcnMsDQpUaG9yc3Rl biANCg0KDQpPbiAxMS8xMi8yMDE3LCAwNDoyMiwgImhvbW90b3B5dC4uLkBnb29nbGVncm91cHMu Y29tIG9uIGJlaGFsZiBvZiBLcmlzdGluYSBTb2pha292YSIgPGhvbW90b3B5dC4uLkBnb29nbGVn cm91cHMuY29tIG9uIGJlaGFsZiBvZiBzb2pha292YS4uLkBnbWFpbC5jb20+IHdyb3RlOg0KDQog ICAgRGVhciBhbGwsDQogICAgDQogICAgSSBhc2tlZCB0aGlzIHF1ZXN0aW9uIGxhc3QgeWVhciBv biB0aGUgY29xLWNsdWIgbWFpbGluZyBsaXN0IGJ1dCBkaWQgbm90IA0KICAgIHJlY2VpdmUgYSBj b25jbHVzaXZlIGFuc3dlciBzbyBJIGFtIHRyeWluZyBoZXJlIG5vdy4gSXMgdGhlIHRoZW9yeSB3 aXRoIA0KICAgIGEgcHJvb2YtcmVsZXZhbnQgaW1wcmVkaWNhdGl2ZSB1bml2ZXJzZSBTZXQsIHBy b29mLWlycmVsZXZhbnQgDQogICAgaW1wcmVkaWNhdGl2ZSB1bml2ZXJzZSBQcm9wLCBhbmQgZnVu Y3Rpb24gZXh0ZW5zaW9uYWxpdHkgKGtub3duIHRvIGJlKSANCiAgICBjb25zaXN0ZW50PyBJdCBp cyBrbm93biB0aGF0IHRoZSBwcm9vZi1pcnJlbGV2YW5jZSBvZiBQcm9wIG1ha2VzIHRoZSBJZCAN CiAgICB0eXBlIGJlaGF2ZSBkaWZmZXJlbnRseSB1c3VhbCBhbmQgaW4gcGFydGljdWxhciwgbWFr ZXMgdGhlIHRoZW9yeSANCiAgICBpbmNvbXBhdGlibGUgd2l0aCB1bml2YWxlbmNlLCBzbyBpdCBp cyBub3QganVzdCBhIG1hdHRlciBvZiB0YWNraW5nIG9uIA0KICAgIGFuIGludGVycHJldGF0aW9u IGZvciBQcm9wLg0KICAgIA0KICAgIFRoYW5rcyBpbiBhZHZhbmNlIGZvciBhbnkgaW5zaWdodCwN CiAgICANCiAgICBLcmlzdGluYQ0KICAgIA0KICAgIC0tIA0KICAgIFlvdSByZWNlaXZlZCB0aGlz IG1lc3NhZ2UgYmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQgdG8gdGhlIEdvb2dsZSBHcm91cHMg IkhvbW90b3B5IFR5cGUgVGhlb3J5IiBncm91cC4NCiAgICBUbyB1bnN1YnNjcmliZSBmcm9tIHRo aXMgZ3JvdXAgYW5kIHN0b3AgcmVjZWl2aW5nIGVtYWlscyBmcm9tIGl0LCBzZW5kIGFuIGVtYWls IHRvIEhvbW90b3B5VHlwZVRoZS4uLkBnb29nbGVncm91cHMuY29tLg0KICAgIEZvciBtb3JlIG9w dGlvbnMsIHZpc2l0IGh0dHBzOi8vZ3JvdXBzLmdvb2dsZS5jb20vZC9vcHRvdXQuDQogICAgDQoN CgoKCgpUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2htZW50IGFyZSBpbnRlbmRlZCBzb2xlbHkg Zm9yIHRoZSBhZGRyZXNzZWUKYW5kIG1heSBjb250YWluIGNvbmZpZGVudGlhbCBpbmZvcm1hdGlv bi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcwptZXNzYWdlIGluIGVycm9yLCBwbGVhc2Ugc2Vu ZCBpdCBiYWNrIHRvIG1lLCBhbmQgaW1tZWRpYXRlbHkgZGVsZXRlIGl0LiAKClBsZWFzZSBkbyBu b3QgdXNlLCBjb3B5IG9yIGRpc2Nsb3NlIHRoZSBpbmZvcm1hdGlvbiBjb250YWluZWQgaW4gdGhp cwptZXNzYWdlIG9yIGluIGFueSBhdHRhY2htZW50LiAgQW55IHZpZXdzIG9yIG9waW5pb25zIGV4 cHJlc3NlZCBieSB0aGUKYXV0aG9yIG9mIHRoaXMgZW1haWwgZG8gbm90IG5lY2Vzc2FyaWx5IHJl ZmxlY3QgdGhlIHZpZXdzIG9mIHRoZQpVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uCgpUaGlzIG1l c3NhZ2UgaGFzIGJlZW4gY2hlY2tlZCBmb3IgdmlydXNlcyBidXQgdGhlIGNvbnRlbnRzIG9mIGFu CmF0dGFjaG1lbnQgbWF5IHN0aWxsIGNvbnRhaW4gc29mdHdhcmUgdmlydXNlcyB3aGljaCBjb3Vs ZCBkYW1hZ2UgeW91cgpjb21wdXRlciBzeXN0ZW0sIHlvdSBhcmUgYWR2aXNlZCB0byBwZXJmb3Jt IHlvdXIgb3duIGNoZWNrcy4gRW1haWwKY29tbXVuaWNhdGlvbnMgd2l0aCB0aGUgVW5pdmVyc2l0 eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgYXMKcGVybWl0dGVkIGJ5IFVLIGxlZ2lz bGF0aW9uLgoK