From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.170.70 with SMTP id t67mr243709lfe.8.1513701447182; Tue, 19 Dec 2017 08:37:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.215.94 with SMTP id o91ls518328lfg.13.gmail; Tue, 19 Dec 2017 08:37:25 -0800 (PST) X-Received: by 10.25.77.8 with SMTP id a8mr243694lfb.16.1513701445139; Tue, 19 Dec 2017 08:37:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513701445; cv=none; d=google.com; s=arc-20160816; b=w0uPdlsKl9KJWSJ/LAweeMgyLUedzOOR0eQ1mLwpXUviUqwPPS6yly8+baMF0ptEvx rbjqiXRpO/jClRfPoQ7mpXiXjLeTAvzbw3GCOdDdqa86Yx/8e5027Sl9a1+AExFphJ5G ocimgtiLL/MhZtE4dGGNveSjUyTo70jUsy+m8eiyaFD/sZyuX7tBtzaDahX5EAiTpayK 7BC/emQyP/8cEk0KJugOhwGJJJhorsmz/osWb/1fZ0bGrg9G8a39BrwGsOrUus+nLKHI LFs8KErME9M6jggNRO570PUMGzLt20cEB2as9yKH2jwFMw9wJpaQkCIemSwLTfXPMaeg bptA== 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=4UvwZjKZgBEhlVdwEpmcOuKQStcWTOlXk1Sy4xnT9Hc=; b=jC2JB8J72fTQ4MsR6Th+k6/kRcJgATPK+icndvq6otDMOUAIUhz11zEfZcPsPxv97y UEiEGzIXTrDOfszIhsNj1MmiSuMve9BMvUAosEysJj0jh3A9BEV7meDeBeSoVAzE0yEJ hvV8WqGfH1Uu7AAG4dFuWToIAUCC1vkHXkQrJqjPPjIgg9h56ctGwZgbSWTXUJA5sGjn Nsm199McyXrK+uBCdShiIBC2MyDzIPQKiLrRB39bWGNx444q41DGJYV/xcBDfneK2eZO 4P4fwGzpMUanEWA423UPufIReMj/ydbhkjNbketpRradIkpfir5vQbI6p1zI3ZHHpxSh thbA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Return-Path: Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTP id q77si1257169lfi.1.2017.12.19.08.37.24 for ; Tue, 19 Dec 2017 08:37:24 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten....@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten....@nottingham.ac.uk Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 0035A44F029_A394044B for ; Tue, 19 Dec 2017 16:37:24 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 7328239DC37_A394043F for ; Tue, 19 Dec 2017 16:37:23 +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 1eRKtP-0002nX-46; Tue, 19 Dec 2017 16:37:23 +0000 Received: from EUR01-HE1-obe.outbound.protection.outlook.com (213.199.154.210) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Tue, 19 Dec 2017 16:37:23 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) by DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) 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 16:37:21 +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 16:37:21 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: 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+MsiAgAFNJACAAA1dAIAAEHaAgAAFP4CABQTogIACmu0AgAAacoCAABWzgIABlfMAgAGLLYCAACi3gIAADmUAgAANMACAAAreAIAABf+AgAABlgA= Date: Tue, 19 Dec 2017 16:37:21 +0000 Message-ID: References: <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> <20171219153118.GA9218@mathematik.tu-darmstadt.de> <20171219163139.GB13875@mathematik.tu-darmstadt.de> In-Reply-To: <20171219163139.GB13875@mathematik.tu-darmstadt.de> 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;DB5PR06MB1717;6:RR5zu7Lf9zk9qzmnVOHveoAtP79YIJHh3IGTOpB+l6WgUJTXH6nYzmglM6YYGnhaPRBKh/Ji0HNPBkyB1ey9UAyRJWHffuiUtEzb1gFft8K92O7NLo8xOq7cU9zQsy24715fvxCa3ppYvLynwIbQfnBJ2Vr984GiJFBEz2b4xZHS6my5OGClDW8rtD9zZr99c1iUIWjD3/nRe7YF8G28sfQONcIH9HgNDPFHArPAMPtWcduq3YIbh9bHDIDJKOntFCm9Ac0wokPvA5bNO9J3Gq1ghkD8XMsHjmuoGpZ+LQeAeJmuTTlZDAjhgcV9H4g5thBzwM4uqAyUHfvvZLrrkzgDvtqkXfHnPtinFfn7hQA=;5:WeVWI4V8+Cx4nkNiZ7pSlz3zYA7+gmVXQPdsKEhwCDqibx7jPnBRFkcqL/D+6j0dzk85ePgIY9yQhMZtzRTQ9qT6Jcf2ZJb0SCNM/J1hKCFpAdWZycNxs7MnhsyC6K2pG/305TNCZ8OC2sHtmh7udY9EyOCFnxKRz2e7pFy17jU=;24:EkSvjX0vOFGYmGaxdlTJuit7WEctsL2FTW+7Uy0WpwC1OCqodGUPEGjvzBU6SWm7GcmZZWtDzo1XuDf8MVqF7oFzSwFW+S5g3Vg3ON/ZYHI=;7:1qJytvgts5H2k7Ov1om5syU2DEvJOC44GVph/qy9iSD4YmyghGHjtvYmX4/JObXSx8Qc+FUspW0cE0hSX1xN+cfBu2ZS4SyIdhrqfYtoBAOttCwC8UcB1RHYK8LfJ7yStkVnnHijEiH0DVP7ChRECw8YHRFO3lxGZ4p8yJVhH4yDgEQytcMif83GidLeYu1fejwZmu4OxoHsJD8MhcjRtiRIVVj0BKDZh1uPPO3lXM0iOavSJ7OZqhYPrxbujlwX x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 49efa557-62c5-4c93-19c9-08d546fec6df x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(5600026)(4604075)(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(2017052603307);SRVR:DB5PR06MB1717; x-ms-traffictypediagnostic: DB5PR06MB1717: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:; x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040450)(2401047)(5005006)(8121501046)(3002001)(10201501046)(3231023)(93006095)(93001095)(6041248)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123560025)(20161123562025)(20161123555025)(20161123558100)(20161123564025)(6072148)(201708071742011);SRVR:DB5PR06MB1717;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1717; x-forefront-prvs: 052670E5A4 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(376002)(39860400002)(346002)(396003)(24454002)(189003)(199004)(93886005)(76176011)(53936002)(25786009)(478600001)(229853002)(86362001)(105586002)(68736007)(106356001)(14454004)(6486002)(316002)(6512007)(82746002)(6436002)(4326008)(54906003)(6246003)(58126008)(8676002)(2950100002)(81166006)(7736002)(83506002)(81156014)(99286004)(786003)(6116002)(3846002)(6506007)(2900100001)(3660700001)(305945005)(53546011)(8936002)(5250100002)(102836003)(3280700002)(33656002)(97736004)(42882006)(83716003)(5660300001)(2906002)(74482002)(6916009)(66066001)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1717;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: <06BA7A1E3BD0B548...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 49efa557-62c5-4c93-19c9-08d546fec6df X-MS-Exchange-CrossTenant-originalarrivaltime: 19 Dec 2017 16:37:21.3690 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR06MB1717 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: -0.0 (/) SSB0aGluayB0aGVyZSBpcyBhIHRyYWRlIG9mZjogeW91IGNhbiBiZSBkZXN0cnVjdGl2ZSBhbmQg dXNlIGNob2ljZSBidXQgc3RpY2sgdG8gc2V0cyBvciB5b3UgYXJlIGNvbnN0cnVjdGl2ZSBhbmQg dXNlIEhvVFQuIEJ1dCBoYXZpbmcgbm8gY2hvaWNlIGFuZCB1c2luZyBzZXRzIGlzIHNhZC4gDQoN ClQuDQoNCk9uIDE5LzEyLzIwMTcsIDE2OjMxLCAiVGhvbWFzIFN0cmVpY2hlciIgPHN0cmUuLi5A bWF0aGVtYXRpay50dS1kYXJtc3RhZHQuZGU+IHdyb3RlOg0KDQogICAgPiBBaCwgeW91IHN1ZmZl ciBmcm9tIHVzaW5nIHNldCB0aGVvcnkgYXMgYSBtZXRhIGxhbmd1YWdlLiAoDQogICAgPiANCiAg ICA+IFRoZXJlIGFyZSBsb3RzIGlmIHVuaXZhbGVudCBjYXRlZ29yaWVzLiBJbiBIb1RULg0KICAg IA0KICAgIFRoYXQgY2xlYXJzIGl0IHVwIQ0KICAgIA0KICAgIFRob21hcw0KICAgIA0KICAgIFBT ICBJIGFtIG5vdCBmaXhlZCB0byBzZXQgdGhlb3J5LiBDb3VsZCBhcyB3ZWxsIGJlIGEgc3VmZmll bnRseSBzdHJvbmcNCiAgICBleHRlbnNpb25hbCB0eXBlIHRoZW9yeS4gQnV0LCBvZiBjb3Vyc2Us IHNldCB0aGVvcnkgaXMgZmluZSBmb3IgbWUgYXMNCiAgICBhIG1ldGFsYW5ndWFnZS4NCiAgICAN Cg0KCgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVs eSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0 aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBz ZW5kIGl0IGJhY2sgdG8gbWUsIGFuZCBpbW1lZGlhdGVseSBkZWxldGUgaXQuIAoKUGxlYXNlIGRv IG5vdCB1c2UsIGNvcHkgb3IgZGlzY2xvc2UgdGhlIGluZm9ybWF0aW9uIGNvbnRhaW5lZCBpbiB0 aGlzCm1lc3NhZ2Ugb3IgaW4gYW55IGF0dGFjaG1lbnQuICBBbnkgdmlld3Mgb3Igb3BpbmlvbnMg ZXhwcmVzc2VkIGJ5IHRoZQphdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkg cmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhlClVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4KClRoaXMg bWVzc2FnZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1c2VzIGJ1dCB0aGUgY29udGVudHMgb2Yg YW4KYXR0YWNobWVudCBtYXkgc3RpbGwgY29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNoIGNv dWxkIGRhbWFnZSB5b3VyCmNvbXB1dGVyIHN5c3RlbSwgeW91IGFyZSBhZHZpc2VkIHRvIHBlcmZv cm0geW91ciBvd24gY2hlY2tzLiBFbWFpbApjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJz aXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCBhcwpwZXJtaXR0ZWQgYnkgVUsgbGVn aXNsYXRpb24uCgo=