From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.222.8 with SMTP id v8mr122906lfg.22.1513694652619; Tue, 19 Dec 2017 06:44:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.101.66 with SMTP id z63ls2403220ljb.7.gmail; Tue, 19 Dec 2017 06:44:10 -0800 (PST) X-Received: by 10.46.2.155 with SMTP id y27mr272352lje.18.1513694650902; Tue, 19 Dec 2017 06:44:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513694650; cv=none; d=google.com; s=arc-20160816; b=o+QIrHxt8a8nRI+MFyJE59TMog1vo+r5Tegrug/X+f2eN/3+PbJZlKJYV2o4awdrJt lx/hslfbTSxj3/HCIfZ39lWSLssvUFFX82PsktHmRDHNd/3c3kL4nrbkOZ2xdnvF/suM 482EZjkfc2XXfvYwH+OmtNimOooqJ6BWsE2jqUb7kDkfRPJ+RlnrUQYNG4F1dhuV6z+h biIvPArkxxbccP8U9bsjJOTlFzyYTWGNDor1Ea9aTwZ6uj9zdKqEwKMPO2E9BvUj00VC tu0ItApEEhjVyHl2KRgr6y6WT+5huvOiY7AJXYqllqYTp89qQzc3lZe5sFOWrvxt/4pK 6b1Q== 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=/x+A4UZDGz419Uf1lVAmX+7xSCb+iVeNtNMEBMnsmI4=; b=PBgUIcvZLpHjVfXb1KIV97bar7P7bizUR9O5XbJEXu+/4V2rzNTIykvRqbqMfyYHM2 75XxU63CxHithlyv66T/e3XJ7TiRXm6hIlvn0YHuT9dUWx8qZbdD7ea8/Zp4yKEuwutm 0qAmrHAnKJdyTnMaUZxi9g51iMM4n0AsYq2ytLl0cF1Ex9NUsh7aMIF4DSxlugldkiA7 kW6UTD19LEd5jTYhtqC2wIhJbxPmJ7m8dBQtkSO6qxX5SKuwyb/vehSf0U09K2jq9wvn gh3oGWjt0YuBANRU5CcNCEunw0KzRd70GoKmCTMK6lifjGrvsFmgsHKsJse8v6UjZ26K Wuxw== 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 j25si381780lfh.0.2017.12.19.06.44.10 for ; Tue, 19 Dec 2017 06:44:10 -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 52B6683563A_A3925BAB for ; Tue, 19 Dec 2017 14:44:10 +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 A3BCF7C4B08_A3925B9F for ; Tue, 19 Dec 2017 14:44:09 +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 1eRJ7p-0005qH-6N; Tue, 19 Dec 2017 14:44:09 +0000 Received: from EUR01-HE1-obe.outbound.protection.outlook.com (213.199.154.216) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Tue, 19 Dec 2017 14:44:09 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) by DB5PR06MB1720.eurprd06.prod.outlook.com (10.165.213.18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.323.15; Tue, 19 Dec 2017 14:44:07 +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.0323.018; Tue, 19 Dec 2017 14:44:07 +0000 From: Thorsten Altenkirch To: Andrej Bauer , 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+MsiAgAFNJACAAA1dAIAAEHaAgAAFP4CABQTogIACmu0AgAAacoCAABWzgIABlfMAgAGLLYCAACi3gIAADmUA Date: Tue, 19 Dec 2017 14:44:07 +0000 Message-ID: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <20171215170011.GA22027@mathematik.tu-darmstadt.de> <20171217102151.GA16619@mathematik.tu-darmstadt.de> <20171218115228.GB29410@mathematik.tu-darmstadt.de> <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> In-Reply-To: Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/f.21.0.170409 x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1720;6:QoFF/3qtLWu1+h5edLeZIyYDR+3eIblTEQa6SHB/fmGgr2ugyYSICUh9TLXpWFgo1CQE5WZti4xo9nq6abx7sUN0zzPo/2gWle1LRMxr2cHLm2wMObQ/dknqcyXjP2wJizbOW6xFHt6RBDTQ+KKFgCOhxw6bTQDQoqbI/VZinDYw2pgnvpQFXSxJ1peErAfzlrAqU8x/SOr/JBse7WyAWHFEJHOAPHq21QYwhp1Vzbl6Zt1n9A67jtdUKPeo32aay1Q7YGJqTPFcXlAYSCyLlAR9SwKLL4N//npq9m237Oo7h0W5t5Tpmr+ahuqgNCrYkQHfMwY0sVqpMxxRsn7u1P9FA7VaXBRw9qcdPXtYuA4=;5:69HgasGSwOv9bUU6Zhb5MpyabNxUF4IsWCzSO71ytuxDLSxp/+xfFNUCDoGOViKJdri8uo9XFiminPqmVU83EYHwKAiG3hDYntPZvwhy7IgKL9Cxw9rb99922k6N6zv7tzRcrirLd8uynyvEURVIto/+NVro5922rkImiRYrEOQ=;24:qsVjR3XhNDcPKJHfdEJvL4bkKexiUaZTbzbJdrqjU9zDCaT6evYKV7PyNv8QT8KHDNvzrwTcDVh/8Y8zOZ7CEbSfrrjMwMIX6k7fWtCpjo4=;7:3HEqItD6xFs3aamv85wo/Gu0Wq/u3MP7DKyYomZWRo7oXHcAOdxL9BvfQNCkaXBF5LphhWMoyQ4DKYtL8CyMykNzr6OBmxB4oqNQLcwbSzBCMM56jwcVpUWpAqR8suPbN402/3Wr2zXKB9tCu+y8j1lyv18dgfePPre7SawnmQ7a7iYvBblIqalYBz/p7H7ZT4mxPfVt22/gZp5J+nfd0Uf+nQilJ55q5rypYatqkatPppcRjo6GmaHYN49G6tFe x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 00136e2f-6aa5-4d38-6472-08d546eef541 x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(5600026)(4604075)(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(2017052603307);SRVR:DB5PR06MB1720; x-ms-traffictypediagnostic: DB5PR06MB1720: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(211936372134217); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(5005006)(8121501046)(10201501046)(3002001)(3231023)(920507027)(93006095)(93001095)(6041248)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123560025)(20161123562025)(20161123558100)(20161123564025)(20161123555025)(6072148)(201708071742011);SRVR:DB5PR06MB1720;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1720; x-forefront-prvs: 052670E5A4 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(396003)(346002)(366004)(39860400002)(24454002)(199004)(189003)(83506002)(478600001)(6506007)(53546011)(66066001)(82746002)(3280700002)(6306002)(2906002)(58126008)(229853002)(6512007)(786003)(316002)(8676002)(966005)(110136005)(83716003)(6436002)(3660700001)(86362001)(97736004)(8936002)(81156014)(6486002)(6246003)(6116002)(102836003)(74482002)(34040400001)(305945005)(105586002)(2950100002)(25786009)(2900100001)(7736002)(33656002)(42882006)(93886005)(3846002)(81166006)(5250100002)(99286004)(76176011)(14454004)(5660300001)(53936002)(106356001)(68736007)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1720;H:DB5PR06MB1717.eurprd06.prod.outlook.com;FPR:;SPF:None;PTR:InfoNoRecords;A:1;MX:1;LANG:en; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <8377F326B0F13A4F...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 00136e2f-6aa5-4d38-6472-08d546eef541 X-MS-Exchange-CrossTenant-originalarrivaltime: 19 Dec 2017 14:44:07.3188 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR06MB1720 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: -0.0 (/) VGhhbmsgeW91LCBBbmRyZWouDQoNCkluZGVlZCwgd2hpbGUgaW4gdXN1YWwgVHlwZSBUaGVvcnkg YSB1bml2ZXJzZSAoVSwgRWwpIHdpdGggYSB1bml0IHR5cGUgaXMgcHJlc2VudGVkIGFzDQoNCglv bmUgOiBVDQoJRWwgb25lID09IDENCg0KKHdoZXJlID09IGlzIGRlZmluaXRpb25hbCBlcXVhbGl0 eSkgc2VtYW50aWNhbGx5IHdlIG9ubHkgaGF2ZQ0KDQoJzrEgOiBFbCBvbmUgfiAxDQoNCih3aGVy ZSB+IGlzIGlzb21vcnBoaXNtKS4NCg0KSSB3YXMganVzdCBhcHBseWluZyB0aGUgc2FtZSBhYnVz ZSBvZiBsYW5ndWFnZSB0byAgzqksIHRoYXQgaXMgdGhlcmUgaXMNCg0KCeKAnFNpbmdsZShhKeKA nSA6IM6pDQoJRWwgKOKAnFNpbmdsZShhKeKAnSkgPT0gU2luZ2xlKGEpDQoNCldoZXJlIEkgc2hv dWxkIGhhdmUgc2FpZDoNCg0KCc6yIDogIEVsICjigJxTaW5nbGUoYSnigJ0pIH4gU2luZ2xlKGEp DQoNCkhvd2V2ZXIsIGlmIHRoZSBjYXRlZ29yeSBpbiBxdWVzdGlvbiBpcyB1bml2YWxlbnQgdGhl biBpc29tb3JwaGljIG9iamVjdHMgYXJlIGVxdWFsIGFuZCB0aGUgYWJ1c2Ugb2YgbGFuZ3VhZ2Ug aXMganVzdGlmaWVkLiANCg0KVGhvcnN0ZW4NCg0KT24gMTkvMTIvMjAxNywgMTM6NTIsICJob21v dG9weXQuLi5AZ29vZ2xlZ3JvdXBzLmNvbSBvbiBiZWhhbGYgb2YgQW5kcmVqIEJhdWVyIiA8aG9t b3RvcHl0Li4uQGdvb2dsZWdyb3Vwcy5jb20gb24gYmVoYWxmIG9mIGFuZHJlai4uLkBhbmRyZWou Y29tPiB3cm90ZToNCg0KICAgID4gSSBkb27igJl0IHVuZGVyc3RhbmQgdGhpczogSFByb3BzIGFy ZSBzdWJvYmplY3RzIG9mIDEgaGVuY2UgdGhleSBnZXQgY2xhc3NpZmllZCBhcyBwcm9wb3NpdGlv bnMuIEhlbmNlIHRoZXJlIGlzIGFuIGVsZW1lbnQgb2YgT21lZ2EgY29ycmVzcG9uZGluZyB0byBT aWdsZShhKS4NCiAgICANCiAgICBJIGJlbGVpdmUgYSBsb3Qgb2YgdGhlIGNvbmZ1c2lvbiBpbiB0 aGlzIGRpc2N1c3Npb24gd291bGQgZ28gYXdheSBpZg0KICAgIHdlIHRyYW5zbGF0ZWQgc29tZSBv ZiB3aGF0IFRob21hcyBpcyBzYXlpbmcgaW50byBhIG1vcmUgc3ludGFjdGljDQogICAgc2V0dXAu IFdlIGhhdmUgdG8gYmUgYSBiaXQgY2FyZWZ1bCBhYm91dCB3aGF0ICJjb3JyZXNwb25kcyB0byIg bWVhbnMuDQogICAgDQogICAgVG8gc2F5IHRoYXQgIM6pICBjbGFzc2lmaWVzIHRydXRoIHZhbHVl cywgb3IgaC1wcm9wb3NpdGlvbnMsIG1lYW5zIHRoYXQ6DQogICAgDQogICAgMS4gVGhlcmUgaXMg YSB0eXBlIM6pLg0KICAgIA0KICAgIDIuIFRoZXJlIGlzIGEgdHlwZSBmYW1pbHkgRWwocCkgaW5k ZXhlZCBieSBwIDogzqkuDQogICAgDQogICAgMy4gRm9yIGV2ZXJ5IHAgOiDOqSB0aGUgdHlwZSBF bChwKSBpcyBhbiBoLXByb3AgKHRoZXJlJ3MgYSB0ZXJtIHdpdG5lc3NpbmcgdGhpcykuDQogICAg DQogICAgNC4gRm9yIGV2ZXJ5IGgtcHJvcCBQIC0tIHdoaWNoIGlzIGEgdHlwZSwgbm90IGFuIGVs ZW1lbnQgb2YgzqkhIC0tDQogICAgdGhlcmUgaXMgcCA6IM6pIHN1Y2ggdGhhdCBQIGlzIGVxdWl2 YWxlbnQgdG8gRWwocCkuIChBZ2FpbiB3ZSBuZWVkIGENCiAgICB0ZXJtIHdpdG5lc3NpbmcgdGhl IGVxdWl2YWxlbmNlLikNCiAgICANCiAgICBOb3csIGl0IG1heSBoYXBwZW4gdGhhdCBoLXByb3Bz IFAgYW5kIFEgYXJlIGJvdGggZXF1aXZhbGVudCB0byBFbChyKQ0KICAgIGV2ZW4gdGhvdWdoIHRo ZXkgYXJlIG5vdCBlcXVhbC4NCiAgICANCiAgICBGdXJ0aGVybW9yZSwgdGhlcmUgY2FuIGJlIGNs YXNzLW1hbnkgc3Vib2JqZWN0cyBvZiAxIGluIGEgdG9wb3MsIGZvcg0KICAgIGluc3RhbmNlIGlu IHNldHMgdGhlcmUgYXJlIGNsYXNzLW1hbnkgc2luZ2xldG9ucy4gT2YgY291cnNlLCBhIHdob2xl DQogICAgbG90IG9mIHRoZW0gd2lsbCBiZSBpc29tb3JwaGljIGFuZCB2ZXJ5IG1hbnkgImNvcnJl c3BvbmQgdG8iIHRoZQ0KICAgIGVsZW1lbnQg4oqkIDogzqkuIEJ1dCBhdCBsZWFzdCBvbiB0aGlz IG1haWxpbmcgbGlzdCB3ZSdyZSBub3QgaW4gdGhlDQogICAgYnVzaW5lc3Mgb2Ygc3dlZXBpbmcg aXNvbW9ycGhpc21zIHVuZGVyIHRoZSBydWcuDQogICAgDQogICAgV2l0aCBraW5kIHJlZ2FyZHMs DQogICAgDQogICAgQW5kcmVqDQogICAgDQogICAgLS0gDQogICAgWW91IHJlY2VpdmVkIHRoaXMg bWVzc2FnZSBiZWNhdXNlIHlvdSBhcmUgc3Vic2NyaWJlZCB0byB0aGUgR29vZ2xlIEdyb3VwcyAi SG9tb3RvcHkgVHlwZSBUaGVvcnkiIGdyb3VwLg0KICAgIFRvIHVuc3Vic2NyaWJlIGZyb20gdGhp cyBncm91cCBhbmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNlbmQgYW4gZW1haWwg dG8gSG9tb3RvcHlUeXBlVGhlLi4uQGdvb2dsZWdyb3Vwcy5jb20uDQogICAgRm9yIG1vcmUgb3B0 aW9ucywgdmlzaXQgaHR0cHM6Ly9ncm91cHMuZ29vZ2xlLmNvbS9kL29wdG91dC4NCiAgICANCg0K CgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVseSBm b3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9u LiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5k IGl0IGJhY2sgdG8gbWUsIGFuZCBpbW1lZGlhdGVseSBkZWxldGUgaXQuIAoKUGxlYXNlIGRvIG5v dCB1c2UsIGNvcHkgb3IgZGlzY2xvc2UgdGhlIGluZm9ybWF0aW9uIGNvbnRhaW5lZCBpbiB0aGlz Cm1lc3NhZ2Ugb3IgaW4gYW55IGF0dGFjaG1lbnQuICBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhw cmVzc2VkIGJ5IHRoZQphdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVm bGVjdCB0aGUgdmlld3Mgb2YgdGhlClVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4KClRoaXMgbWVz c2FnZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1c2VzIGJ1dCB0aGUgY29udGVudHMgb2YgYW4K YXR0YWNobWVudCBtYXkgc3RpbGwgY29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNoIGNvdWxk IGRhbWFnZSB5b3VyCmNvbXB1dGVyIHN5c3RlbSwgeW91IGFyZSBhZHZpc2VkIHRvIHBlcmZvcm0g eW91ciBvd24gY2hlY2tzLiBFbWFpbApjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5 IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCBhcwpwZXJtaXR0ZWQgYnkgVUsgbGVnaXNs YXRpb24uCgo=