From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.18.148 with SMTP id 20mr40736lfs.44.1513500450335; Sun, 17 Dec 2017 00:47:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.5.3 with SMTP id 3ls1594306ljf.13.gmail; Sun, 17 Dec 2017 00:47:28 -0800 (PST) X-Received: by 10.46.19.1 with SMTP id 1mr1131194ljt.15.1513500448573; Sun, 17 Dec 2017 00:47:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513500448; cv=none; d=google.com; s=arc-20160816; b=U1dJkxNhbOV+b9oEWfLzy5zIgEZOCC86Qxe5IkxQe+guT5Y4NdtzKzJZ7QUYT/gNIY DjoO+JzPppRq8IG2xd8BQGZ8lpNozPfO3MzJG0iOTlwMMXN0rnvxIxT80XwmW5Bop+wz UaHSESgoMxOikv4mmIIFfyivgoiqJ0axUjUAx8IBHJaIpiQ3GuSFM3LblmupjLWwQGMS r7UkwaJnCBq7RdB0gOjLl8ZNku17i+oFM87FQ0qKevJMK0QlV+pzrPQ4BtfeCcBOnx8q TEPpP8DHZigFX0OYv2F3aYZzoYD9hVw1AaBsA0QbOIx+qxZwZLlbxVmM09pEKbVtFMHU mALA== 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=/JJMq5PktzB0SuvRCsg93LykYeofaS0Dsfd6Jvhu50c=; b=n39fHjJrmOgVlG89Pdl+p+MAZuH5RPD4wLf2XlqXbMlksGFTobEZ0ODj6SbQCBInqV 6hOXdkGg4gtk5NEbvTL2+QmJGWpiJpLHGrVnAfOFPy1mBcW/XZ7LApcd9XIfR69bbC+I rEZDg31KntywYHZq8A7XtgheNCFHiRRGpGLrNd30CmalHPsF/RgXRy4C1pBtd1ktI61W /4ulDo7v3DSlA0Gk6+Kl1dA2ngaSqhmGkBwdPRmNLfuP/g6II8LCB5sXvQbkAUkO4M5w V9kkNmu2Uq31Du1c5DX0YZABaLW3/gshIb10rktDKrK7kEFeJmhGxrodJ5hcOol64Qh3 whiA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Return-Path: Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTP id h89si302479lfb.3.2017.12.17.00.47.28 for ; Sun, 17 Dec 2017 00:47:28 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id C766C3C32B0_A362F1FB for ; Sun, 17 Dec 2017 08:47:27 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 7EB9F3C3273_A362F1FF for ; Sun, 17 Dec 2017 08:47:27 +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 1eQUbX-0000RY-59; Sun, 17 Dec 2017 08:47:27 +0000 Received: from EUR01-VE1-obe.outbound.protection.outlook.com (213.199.154.246) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Sun, 17 Dec 2017 08:47:27 +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 08:47:25 +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 08:47:25 +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+MsiAgAFNJACAAA1dAIAAEHaAgAAFP4CABQTogIACmu0A Date: Sun, 17 Dec 2017 08:47:25 +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> In-Reply-To: <20171215170011.GA22027@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:k9RlkaxCSSHC4GhOWtMQaSBtjCoMeVoZoFsuOlFgFXgojK5VcP4Zb5X7ylAxT/nRbocBPDZvPpILgjQ5PsggDSYqRyTvrCNndw1noK5Tn7Iqo+yRiSk86xH7Eq1Dc5U5E4nJ0iQANNd7mdCr7znulnFSrSeQhc6V0A2IfBCnmCxrwF1rfXepnfCTCP7Mm57Qt8sEOtfGynABCdEJM7KxDH2fPU3YpxeZfxNKrDj5AKb7Xhu0/Ydv/nK8CVQX99vCYPY2YdQ9wtvgrCa0QH5pYhwpPDql5oaj2VVfT8Wu+mxnRr4mdi+S1SnX53a0/QIGFBcKkhDvZW9GpIQ2Jcwlp6/kYgUJok0phSieMW7segU=;5:aWnJVOvHbivJ7ZLRfSl9/t1a+bbNMJe5BG24t6sLF868iKX8o/kXC8jk5SXMsYdJK40jS8bwRZfJvYiBz+9EOyR/KoCKBboe3/FUE1GcQZCIfXEwg7cGP1IVHl6Kf37xe9koqS1fGvkQlHN9+uHOyah8ynlIGvqWSf2NmtKoQ5Q=;24:awQTFqQ3GoJnhqa3L9kh6bRiowdW95GdH5gJtlQMGo1rXmY5qBgtiPjqjwpK7ygPl29BpQMEhcIiiThJUfESAXIGFwNReMooy0wttGOvaow=;7:K1Q6UDCvpykI+vY3EcuNDpQvMGmb/VVETMoyHemTqyXrxRZDhkMuWDvXM914BLaMBq86t6kBfcf93RttjfiZOEm1WOjNcaw7zSJtWv6p9Covy9SfP9oMs1Eo81+lKa1rgijPDpaXu2cRzUj17mIQfGCzUV0zf5kGVbNcLooov2X+TAKiVtNf92OwRWvOSzsRawHYNd6sUBzCCAPQ/3pHhHC6bEu7eLy7bghKZFB2h0fQbtSBpfnu5SjMMKpwcper x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: e39a643f-bef4-4d2c-9a5d-08d5452acbf8 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); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(8121501046)(5005006)(93006095)(93001095)(3002001)(10201501046)(3231023)(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)(346002)(39850400004)(376002)(396003)(366004)(24454002)(199004)(189003)(6512007)(25786009)(6486002)(229853002)(6436002)(53936002)(39060400002)(6246003)(2900100001)(4326008)(478600001)(5250100002)(105586002)(106356001)(66066001)(7736002)(305945005)(5660300001)(6916009)(42882006)(2950100002)(86362001)(8936002)(8676002)(81166006)(81156014)(68736007)(2906002)(76176011)(786003)(316002)(99286004)(102836003)(14454004)(83506002)(3846002)(6116002)(3660700001)(54906003)(97736004)(6506007)(59450400001)(53546011)(93886005)(3280700002)(74482002)(58126008)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1718;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) spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <2677E0BED679FA43...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: e39a643f-bef4-4d2c-9a5d-08d5452acbf8 X-MS-Exchange-CrossTenant-originalarrivaltime: 17 Dec 2017 08:47:25.4709 (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 (/) DQoNCk9uIDE1LzEyLzIwMTcsIDE3OjAwLCAiaG9tb3RvcHl0Li4uQGdvb2dsZWdyb3Vwcy5jb20g b24gYmVoYWxmIG9mDQpUaG9tYXMgU3RyZWljaGVyIiA8aG9tb3RvcHl0Li4uQGdvb2dsZWdyb3Vw cy5jb20gb24gYmVoYWxmIG9mDQpzdHJlLi4uQG1hdGhlbWF0aWsudHUtZGFybXN0YWR0LmRlPiB3 cm90ZToNCg0KPk1vcmVvdmVyLCB0b3Bvc2VzIHdpbGwgbm90IHZhbGlkYXRlIHVuaXZhbGVuY2Uu IEFzIHBvaW50ZWQgb3V0IHRvIG1lDQo+YnkgTWFydGluIEVzY2FyZG8geW91IGNhbid0IGV2ZW4g Zm9ybXVsYXRlIGl0IGJlY2F1c2UgaW4gYXJiaXRyYXJ5DQo+dG9wb3NlcyB5b3UgZG9uJ3QgaGF2 ZSB1bml2ZXJzZSAobm90IHRvIHNwZWFrIG9mIHVuaXZhbGVudCBvbmVzKS4NCg0KSSB3YXMgb25s eSB0YWxraW5nIGFib3V0IHRoZSBzcGVjaWFsIGNhc2Ugb2YgKC0xKS11bml2YWxlbmNlIG9yDQpw cm9wb3NpdGlvbmFsIGV4dGVuc2lvbmFsaXR5IHRoYXQgaXMgZm9yIFAsUSA6IFByb3ANCg0KKFAg PC0+IFEpIC0+IChQID0gUSkNCg0KVGhvcnN0ZW4NCj4NCg0KCgoKClRoaXMgbWVzc2FnZSBhbmQg YW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQg bWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZl ZCB0aGlzCm1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5kIGl0IGJhY2sgdG8gbWUsIGFuZCBp bW1lZGlhdGVseSBkZWxldGUgaXQuIAoKUGxlYXNlIGRvIG5vdCB1c2UsIGNvcHkgb3IgZGlzY2xv c2UgdGhlIGluZm9ybWF0aW9uIGNvbnRhaW5lZCBpbiB0aGlzCm1lc3NhZ2Ugb3IgaW4gYW55IGF0 dGFjaG1lbnQuICBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZQphdXRob3Ig b2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhl ClVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4KClRoaXMgbWVzc2FnZSBoYXMgYmVlbiBjaGVja2Vk IGZvciB2aXJ1c2VzIGJ1dCB0aGUgY29udGVudHMgb2YgYW4KYXR0YWNobWVudCBtYXkgc3RpbGwg Y29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNoIGNvdWxkIGRhbWFnZSB5b3VyCmNvbXB1dGVy IHN5c3RlbSwgeW91IGFyZSBhZHZpc2VkIHRvIHBlcmZvcm0geW91ciBvd24gY2hlY2tzLiBFbWFp bApjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJl IG1vbml0b3JlZCBhcwpwZXJtaXR0ZWQgYnkgVUsgbGVnaXNsYXRpb24uCgo=