From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.166.204 with SMTP id p195mr1209622wme.29.1513510786830; Sun, 17 Dec 2017 03:39:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.209.78 with SMTP id i75ls2454940wmg.0.gmail; Sun, 17 Dec 2017 03:39:45 -0800 (PST) X-Received: by 10.223.153.202 with SMTP id y68mr1517703wrb.17.1513510785533; Sun, 17 Dec 2017 03:39:45 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513510785; cv=none; d=google.com; s=arc-20160816; b=AWEd4henljw1RaPRAyqUd/gF3erGGF++18oU31J1hoseIYMhU+AAtFLUhAtVD/P/Lz 5fcyL/wPRHbLU7HuuL5ciYI9wbWTRvQG290uAFMRD+jmilABWfdYvZ4ST4owWWsr2Zd6 1LTP5S5BQJA7o2eCS/6D3Fl8n3cCCmKYTl4fNtH/gLOwbJF6YHyvKD92FTvgfLhw6/bQ jCEU5No26iRCUi7X/TK8kdiRK5qjBm6sHh2a3coLmUp+bz9Nb86O89fzgyTVPksviJQ4 bAg9vSLRJLKffVMvqusL9fDM6u5y+ysN8P+KaJPNEUviulrBlE7o7bl8o3KDC2UnZ/Wg iBaA== 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:cc:to:from :arc-authentication-results; bh=AEgdMyNZ5Y5XQMVO5hXWeoECJ5dvoaPI4iUrXO3vTC0=; b=PXjF32RJUjjezVTPpjqDaTgyRCyn0jYAcVMEKvyCfIJb5RT4aXmdITQNLe3IzLmz8V cHziig+6kX3YVyiqtFep4Sz6y7CVts0tuB3G0ODJk8N+nc6AZyS2Wvmk0jmxP8HIbdzq 6PVx9Y4/gZz4Sx+cQ9oIOgdRqjyvvjbIivZBBHo1ZE90+UX551eoJNvbv82jWqMu+TZb cVvX6eSDpRk9xiNvD6vgHOGA2qd67cbz3kUNBPak++KMjlt+SStwy8WRFwVqwCV87Dfe hKHO9+Ve/mDDUhZIBDiRh7fly/5baYYKe8Cw29mUGsrw1FbUDMicV3IG/+52vRXxJ62n WMrg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Return-Path: Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTP id m4si1293157wrm.4.2017.12.17.03.39.45 for ; Sun, 17 Dec 2017 03:39:45 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 3F85041C344_A365781B for ; Sun, 17 Dec 2017 11:39:45 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 00ACA31A02D_A365781F for ; Sun, 17 Dec 2017 11:39:45 +0000 (GMT) Received: from uiwexhub03.is.nottingham.ac.uk ([128.243.15.146] helo=UIWEXHUB03.ad.nottingham.ac.uk) by smtp4.nottingham.ac.uk with esmtps (TLSv1:AES128-SHA:128) (Exim 4.85) (envelope-from ) id 1eQXIE-0007qm-Pf; Sun, 17 Dec 2017 11:39:44 +0000 Received: from EUR01-DB5-obe.outbound.protection.outlook.com (213.199.154.177) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Sun, 17 Dec 2017 11:39:42 +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.323.15; Sun, 17 Dec 2017 11:39:41 +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; Sun, 17 Dec 2017 11:39:41 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: Andrea Vezzosi , 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+MsiAgAFNJACAAA1dAIAAEHaAgAAFP4CABQTogIACmu0AgAAacoCAABWzgA== Date: Sun, 17 Dec 2017 11:39:41 +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> In-Reply-To: <20171217102151.GA16619@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/14.5.7.151005 authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; x-originating-ip: [82.31.58.108] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1718;6:IjutCAf30E3ea5g1Y/WLZ5H9kgwfvNf3Ptj/NzHaP4GorI3PYRUZqyqkf299FeA3JkCnmS+TrK/m5QTZMOvanXqeWdsItNiqZ9k9oGIZr0lIX0X62gNuiBe5L85iEi/NpIMiLYG0MxysYzG0GjvP/TWraVxdE2eMEDeNCLBlxAcT7b/EIKGZrjxaG9HZqhr6EAeQRZie1tGEEwx4yiMBxMURP1SEgxHP22xTa7e4UQ9ODIJDpVzBQXkm2p4wn0V6HLW6Y2BGPweGp1gna5nmPCLnIbHxqin3c3Bs1lrC/1mz3eMfx63x096UosWkisuGzfSLW7QN7ho4bMZBV1QDkTBDeTV96XrrUh1EUCpobak=;5:8mB/KY2OsO5B/l4ekpyseAVHiehwu+mPz9oGQjstddAWElMROtlCTajA6iY181wYQpnN3reW76EXbIplcTizyHLc5BrfUVfkfZkpO87FTr7jNHo3l78QxD7iKfogepMZa37S4MB+VneQc4w0wMT/LXCfvnbcYyyhaDqs8gumqGw=;24:4xcSj32UyNYvDgjvFMKM+CevXer9Wz7IeiyqkUIZ8KzeyipvOEDBgpUqXfpSwOVF7RT4pLdKsFoji3uKaatP3Y2gdccwz2prUIu5TdZibrc=;7:b6K/Wg/dmvh9Vnyg8U3l+Z1NAAysX/3Uz2qg5vtQNY3jqy2r51KSRPKK6WsSjKoTz7h97iy6g8NOBc5KdpftuX0QT+qgJejjw5hlOEF7Bgee3lBOOaEnSQUuf0BvbVDiFsP9kZo+TW7qMu2wOPW9eW9bMzwyye1HKMqfw52ZYvhMj51JgGDX0wczSYQ4xU+tb44P7IpQk1y9/DQNMQUpGeyCPx+8lxKDOSu/c4OTRU8qJGUQTuiGQb8lTgI1wdgG x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 3622b2d6-ed34-4a6d-a74c-08d54542dc94 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:; x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(8121501046)(5005006)(93006095)(93001095)(3002001)(3231023)(10201501046)(6041248)(20161123555025)(20161123560025)(20161123564025)(20161123562025)(20161123558100)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(6072148)(201708071742011);SRVR:DB5PR06MB1718;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1718; x-forefront-prvs: 05245CA661 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39850400004)(366004)(346002)(396003)(376002)(189003)(199004)(24454002)(8676002)(8936002)(81166006)(68736007)(81156014)(2906002)(6506007)(305945005)(6916009)(42882006)(2950100002)(5660300001)(86362001)(97736004)(54906003)(3280700002)(74482002)(58126008)(59450400001)(53546011)(93886005)(102836003)(316002)(99286004)(14454004)(76176011)(786003)(3660700001)(83506002)(3846002)(6116002)(53936002)(6436002)(4326008)(2900100001)(6246003)(25786009)(229853002)(6486002)(6512007)(7736002)(106356001)(66066001)(478600001)(105586002)(5250100002)(39060400002)(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: <8AB435032FA4E044...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 3622b2d6-ed34-4a6d-a74c-08d54542dc94 X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Dec 2017 11:39:41.2274 (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 (/) T24gMTcvMTIvMjAxNywgMTA6MjEsICJUaG9tYXMgU3RyZWljaGVyIg0KPHN0cmUuLi5AbWF0aGVt YXRpay50dS1kYXJtc3RhZHQuZGU+IHdyb3RlOg0KDQo+PiA+TW9yZW92ZXIsIHRvcG9zZXMgd2ls bCBub3QgdmFsaWRhdGUgdW5pdmFsZW5jZS4gQXMgcG9pbnRlZCBvdXQgdG8gbWUNCj4+ID5ieSBN YXJ0aW4gRXNjYXJkbyB5b3UgY2FuJ3QgZXZlbiBmb3JtdWxhdGUgaXQgYmVjYXVzZSBpbiBhcmJp dHJhcnkNCj4+ID50b3Bvc2VzIHlvdSBkb24ndCBoYXZlIHVuaXZlcnNlIChub3QgdG8gc3BlYWsg b2YgdW5pdmFsZW50IG9uZXMpLg0KPj4gDQo+PiBJIHdhcyBvbmx5IHRhbGtpbmcgYWJvdXQgdGhl IHNwZWNpYWwgY2FzZSBvZiAoLTEpLXVuaXZhbGVuY2Ugb3INCj4+IHByb3Bvc2l0aW9uYWwgZXh0 ZW5zaW9uYWxpdHkgdGhhdCBpcyBmb3IgUCxRIDogUHJvcA0KPj4gDQo+PiAoUCA8LT4gUSkgLT4g KFAgPSBRKQ0KPg0KPlRoaXMgd291bGQgYmUgb2sgYnV0IHlvdSBhc3N1bWUgYWxzbyB0aGF0IFNp bmdsZShUcnVlKSBhbmQNCj5TaW5nbGUoZmFsc2UpIGFyZSBwcm9wb3NpdGlvbnMgYnV0IHRoZXkg YXJlIGp1c3QgYm90aCBJU09NT1JQSElDIHRvIDENCj5pbiBPbWVnYSA9IFByb3AuIFRoYXQncyB3 aGVyZSB5b3UgYXBwbHkgVUEgZm9yIChzdWIpc2luZ2xldG9ucw0KPlVOQ09OU0NJT1VTTFkuDQoN Ckkgd2Fzbid0IGRlZmVuZGluZyB0aGUgaW5jb25zaXN0ZW5jeSBkZXJpdmF0aW9uIEkgcG9zdGVk IGVhcmxpZXIsIGFzIE1pa2UNCnBvaW50ZWQgb3V0IGl0LCBpdCBpZ25vcmVzIHR5cGUgYW5ub3Rh dGlvbnMuDQoNCkhvd2V2ZXIsIEkgZG9uJ3QgdW5kZXJzdGFuZCB5b3VyIHBvaW50LiBTdXJlbHkg VUEgZm9yIHN1YnNpbmdsZXRvbnMgaXMNCmV4YWN0bHkgcHJvcG9zaXRpb25hbCBleHRlbnNpb25h bGl0eS4NCg0KPlRoZSBpbmNvbnNpc3RlbmN5IHByb29mIHlvdSBoYXZlIGdpdmVuIGlzIGEgc2xp Z2h0bHkgZGlzdG9ydGVkIHZlcnNpb24NCj5vZiB0aGUgZm9sbG93aW5nIHJpZGljdWxvdXMgYXJn dW1lbnQ6IHthfSBhbmQge2J9IGFyZSBpc29tb3JwaGljIHRodXMNCj5lcXVhbCBmb3Igd2hpY2gg cmVhc29uIGEgPSBiLg0KDQpJbmRlZWQsIGJ1dCB3ZSBhcmUgbm90IGluIHNldCB0aGVvcnkuIElu IHNldCBsZXZlbCBIb1RUIFNpbmdsZShUcnVlKSA9DQpTaW5nbGUoRmFsc2UpIGJ1dCBUcnVlICE9 IEZhbHNlLg0KDQpXaGVuZXZlciB3ZSBjYW4gcHJvdmUgdGhhdCBhIHR5cGUgaXMgQSBwcm9wb3Np dGlvbmFsLCB0aGF0IGlzIGFsbA0KeCx5OkEueD15IGl0IGlzIGEgc3Vic2luZ2xldG9uIGFuZCB3 ZSBjYW4gY29uc3RydWN0IGEgY29ycmVzcG9uZGluZw0KZWxlbWVudCBvZiBQcm9wIChha2EgT21l Z2EpLiBIZW5jZSBhIHRvcG9zIGNvcnJlc3BvbmRzIHRvIHNldC1sZXZlbCBIb1RUDQooaWdub3Jp bmcgcHJlZGljYXRpdml0eSBpc3N1ZXMgZm9yIHRoZSBtb21lbnQpLg0KDQpJbiBhIGxhbmd1YWdl IGxpa2UgTGVhbiB3aXRoIGEgc3RhdGljIHVuaXZlcnNlIG9mIHByb3Bvc2l0aW9ucyB0aGlzIGlz IG5vdA0KdGhlIGNhc2UuIE9ubHkgY2VydGFpbiBzdWJzaW5nbGV0b25zIGdldCBjbGFzc2lmaWVk LiBJIGRvbid0IHJlYWxseQ0KdW5kZXJzdGFuZCB0aGUgcmVsYXRpb24gYnV0IGl0IHNlZW1zIHRo YXQgeW91IGdldCBhIHF1YXNpdG9wb3MuIEFuZCBpbmRlZWQNCmluIHRoaXMgbGFuZ3VhZ2UgeW91 IGRvbid0IGhhdmUgdW5pcXVlIGNob2ljZSAod2hpY2ggd2FzIHRoZSBjYXVzZSBvZiBteQ0KY29u ZnVzaW9uKS4gDQoNClRoZSBpc3N1ZSB3YXMgdGhpczogaW4gYSB0eXBlIHRoZW9yeSB3aXRoIGEg c3RhdGljIHVuaXZlcnNlIG9mDQpwcm9wb3NpdGlvbnMgeW91IGNhbiBhZGQgZGVmaW5pdGlvbmFs IHByb29mLWlycmVsZXZhbmNlLCB0aGF0IGlzIGFueSB0d28NCnByb29mcyBvZiBhIHByb3Bvc2l0 aW9uIGFyZSBkZWZpbml0aW9uYWxseSBlcXVhbC4gVGhlIGRlcml2YXRpb24gSSBwb3N0ZWQNCmVh cmxpZXIgc2VlbWVkIHRvIGltcGx5IHRoYXQgeW91IGNhbm5vdCBoYXZlIGRlZmluaXRpb25hbA0K cHJvb2YtaXJyZWxldmFuY2UgYW5kIGEgYmUgaW4gYSB0b3Bvcy4gTHVja2lseSB0aGlzIHR1cm5z IG91dCB0byBiZQ0KaW5jb3JyZWN0IGFuZCBpdCBpcyBqdXN0IGR1ZSB0byB0aGUgd2F5IHByb29m IGlycmVsZXZhbmNlIGlzIGltcGxlbWVudGVkDQppbiBMZWFuICh3aGljaCBpcyBqdXN0IHdyb25n IGltaG8pLg0KDQoNCgoKCgpUaGlzIG1lc3NhZ2UgYW5kIGFueSBhdHRhY2htZW50IGFyZSBpbnRl bmRlZCBzb2xlbHkgZm9yIHRoZSBhZGRyZXNzZWUKYW5kIG1heSBjb250YWluIGNvbmZpZGVudGlh bCBpbmZvcm1hdGlvbi4gSWYgeW91IGhhdmUgcmVjZWl2ZWQgdGhpcwptZXNzYWdlIGluIGVycm9y LCBwbGVhc2Ugc2VuZCBpdCBiYWNrIHRvIG1lLCBhbmQgaW1tZWRpYXRlbHkgZGVsZXRlIGl0LiAK ClBsZWFzZSBkbyBub3QgdXNlLCBjb3B5IG9yIGRpc2Nsb3NlIHRoZSBpbmZvcm1hdGlvbiBjb250 YWluZWQgaW4gdGhpcwptZXNzYWdlIG9yIGluIGFueSBhdHRhY2htZW50LiAgQW55IHZpZXdzIG9y IG9waW5pb25zIGV4cHJlc3NlZCBieSB0aGUKYXV0aG9yIG9mIHRoaXMgZW1haWwgZG8gbm90IG5l Y2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRoZQpVbml2ZXJzaXR5IG9mIE5vdHRpbmdo YW0uCgpUaGlzIG1lc3NhZ2UgaGFzIGJlZW4gY2hlY2tlZCBmb3IgdmlydXNlcyBidXQgdGhlIGNv bnRlbnRzIG9mIGFuCmF0dGFjaG1lbnQgbWF5IHN0aWxsIGNvbnRhaW4gc29mdHdhcmUgdmlydXNl cyB3aGljaCBjb3VsZCBkYW1hZ2UgeW91cgpjb21wdXRlciBzeXN0ZW0sIHlvdSBhcmUgYWR2aXNl ZCB0byBwZXJmb3JtIHlvdXIgb3duIGNoZWNrcy4gRW1haWwKY29tbXVuaWNhdGlvbnMgd2l0aCB0 aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQgYXMKcGVybWl0dGVk IGJ5IFVLIGxlZ2lzbGF0aW9uLgoK