From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.126.197 with SMTP id z188mr643719wmc.14.1513768623136; Wed, 20 Dec 2017 03:17:03 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.223.201.147 with SMTP id f19ls6634398wrh.12.gmail; Wed, 20 Dec 2017 03:17:02 -0800 (PST) X-Received: by 10.28.189.85 with SMTP id n82mr644444wmf.23.1513768622139; Wed, 20 Dec 2017 03:17:02 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513768622; cv=none; d=google.com; s=arc-20160816; b=dqosdKCWdpv7Ja7kQCr84o0+0S5d69OE1xURP/EXnueWnnUw1LzHYl+GChRAQekjGc luHRhNeF+JLbCh4KclUQ++Pjies9C+eMkzrmetzoBLpbftxsggvV2QrP2czslCxH34Eo Lb8PovT5etVwC0fjkiGS5o3RokzrBz5j23kXMavkpAeFUvJ3AcIIOrklMkpy/lrufP3u fqJaLOdtl3LQT0sugTgMe/qVonXi8lTHh7yA3wyR6QBrcPWt7uEacZqXMEov4+wRPgb6 gXapCWefvuPEDu9lRuRdpL90O+iHqlP7tDuiXpX7vR1FZM4gcimI6TARmqImfl0Xqp4E Y5TQ== 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=zaFOsNXIJrMHASDmAMlh2TKX+8NDViEEw8PnstPWVOk=; b=s4+Sg7eZHOtp3mbVUFUVssJJR78gkNGLtbOw6o520J0zaQgcH7tlDx4pPdOURlfo2d pu0P5vYBm5gNzy7ASmxGNqjqUWIhQkSKbQwKAQqAwmj5NdZx6IJTRNhdFwrY1P9HAE7X GrgbRaHTjpfxcqWkNY67zgf0xulBY1J5DF1A+99PhH5L5otcZmsdQb+or2y/kX+LXRzD 1nsIHy6dunlYRCGq96oHtgtBoCMEcH51U7k4pAaCPtS27Vv9OF688Dde9b1bzqSEhv17 TvRPnuJFuuC0vZgo0SjnWthgL4zSRdh2/ukOkyOkYtyltpaVAsdTJmTLN+zC3t52JUGy +JuQ== 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 a14si372548wmg.0.2017.12.20.03.17.02 for ; Wed, 20 Dec 2017 03:17:02 -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 C59DF835547_A3A46ADB for ; Wed, 20 Dec 2017 11:17:01 +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 87A297C77C2_A3A46ADF for ; Wed, 20 Dec 2017 11:17:01 +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 1eRcMv-0000rL-Bh; Wed, 20 Dec 2017 11:17:01 +0000 Received: from EUR01-HE1-obe.outbound.protection.outlook.com (213.199.154.215) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Wed, 20 Dec 2017 11:17:01 +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; Wed, 20 Dec 2017 11:16:59 +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; Wed, 20 Dec 2017 11:16:59 +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+AgAABlgCAATRTAIAABH8A Date: Wed, 20 Dec 2017 11:16:59 +0000 Message-ID: <5B8F4A6C-DD7C-4A14-812C-4AEA35C41BEA@exmail.nottingham.ac.uk> References: <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> <20171220110052.GC8054@mathematik.tu-darmstadt.de> In-Reply-To: <20171220110052.GC8054@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/f.15.1.160411 x-originating-ip: [82.31.58.108] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1720;6:Tb2WgmrRpGspU7OV1AoGp49XC/wRMWW95lnJzqIUyUOB6penIKxCD77Kul4ynN+IL7wRBG6EUZMDDtpcnDCtSISfsUqrw7hE6AOQ6NOUsXS2vNAWrB2qq7Pa1YIJLujvlSgazEESoYuExRuhT6fWwvPYBYMaYQm2S2FfE7WYNc4YOJ8NoYG7JiOoeaPZrsdqcWvD6dgq+wxK53NkJvAcMgfXf3dhRGd/L+0xi9gD4+zjJvg8fxqApS0n49+SRE6Z6lMFEhiRouIT+cN+x2TqqLjSCnvPbsE4vL7SHaCuytXBII5CCgOzOjQJ9jMCoBxI1ZKpGlaDq0ucI8SpoIZb3YPexiWeRYSwZ9BEglR1EOM=;5:DHVgryYRGs1WlUK7uj0UibUhU7fBxjh1KlUQ00XOMa0oI+JQxr0/rFFEi47ZmaO3KkNoBoJEL/EY+UEoLkJ2UgNTU1ruRDY3RpFCOOhnmvl94+qR57ig8dskPhmUbpHnoHOVQW9G7cGvHObzc1ovcyY9wJ6Cdut81cGiVvOavVc=;24:FsvcCfHRV9unwCKbu1/x3XNiWEArg7e7VG5dIdm4dYy3cS1/ckjQ8d1oi3vBd9sK3FQqIJ8PS4/bHQatpYYKdt6wPsuK9IkrQuDuwdi2YRU=;7:hO9BTmR3PG6MTW00AUgwLpPDb6JHIdoDCbFmaQ/3GKpcGlpowgXAGvIS3zUOY6i8Iihmq5gBGnCDBBGct5o9tTWEXD0rONvhWH3sQbO8zGsClBL4zho2sj2gT4ybEUWK85cYNCoV8TCS9TksuKSWS82WuXvE1AAAkqSWorX61cxFWZGI4G0ZeZN3G9nUAzqlxMpaQArq3sNcPC+8SFQrswnU4rCkiElpuomD2/uHZyZUJsayRmeeYZFSf1/9ueMw x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 1290e495-10a5-461e-9df9-08d5479b3019 x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(5600026)(4604075)(2017052603307)(7153060);SRVR:DB5PR06MB1720; x-ms-traffictypediagnostic: DB5PR06MB1720: authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(131327999870524); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040470)(2401047)(5005006)(8121501046)(93006095)(93001095)(3231023)(10201501046)(3002001)(6041268)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123558120)(20161123562045)(20161123564045)(20161123560045)(6072148)(201708071742011);SRVR:DB5PR06MB1720;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1720; x-forefront-prvs: 0527DFA348 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(39380400002)(39860400002)(346002)(376002)(396003)(199004)(189003)(3846002)(59450400001)(6116002)(68736007)(6486002)(83716003)(76176011)(83506002)(8936002)(99286004)(102836003)(14454004)(6512007)(229853002)(478600001)(2900100001)(86362001)(2906002)(3280700002)(82746002)(3660700001)(105586002)(74482002)(5250100002)(25786009)(106356001)(316002)(786003)(8676002)(7736002)(4326008)(53936002)(81166006)(81156014)(66066001)(305945005)(6246003)(6916009)(2950100002)(42882006)(5660300001)(93886005)(6506007)(58126008)(54906003)(6436002)(97736004)(33656002)(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) spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 1290e495-10a5-461e-9df9-08d5479b3019 X-MS-Exchange-CrossTenant-originalarrivaltime: 20 Dec 2017 11:16:59.4343 (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 (/) SGkgVGhvbWFzLA0KDQp3ZSBoYXZlIGFscmVhZHkgZXN0YWJsaXNoZWQgdGhhdCBteSBhcmd1bWVu dCB3YXMgaW5jb3JyZWN0IChmb3IgdGhlIHJlYXNvbnMgeW91IHN0YXRlKSBhbmQgSSB3YXMgbWlz aW5mb3JtZWQgYWJvdXQgdGhlIGJlaGF2aW91ciBvZiBMZWFuLiANCg0KDQoNCj4NCj5Bbm90aGVy IGdhcCBpbiBUaG9yc3RlbidzIGFyZ3VtZW50IGlzIHRoZSBmb2xsb3dpbmcuIFRob3VnaCBTaW5n bGUoYSkgYW5kDQo+U2luZ2xlKGEnKSBhcmUgaXNvbW9ycGhpYyBpbiBvcmRlciB0byBjb25jbHVk ZSB0aGF0IHRoZXkgYXJlIHByb3Bvc2l0aW9uYWxseQ0KPmVxdWFsIHRoZXkgd291bGQgaGF2ZSB0 byBiZSBlbGVtZW50cyBvZiBhIHVuaXZhbGVudCB1bml2ZXJzZSBCVVQgSSBkb24ndCBzZWUNCj53 aGVyZSBzdWNoIGEgdW5pdmVyc2Ugc2hvdWxkIGNvbWUgZnJvbSBpbiB0aGUgZ2VuZXJhbCB0b3Bv cyBjYXNlIQ0KDQpJIGRvbuKAmXQgdW5kZXJzdGFuZCB0aGlzIHBvaW50LiBJbiBhIHR5cGUgdGhl b3JldGljIGltcGxlbWVudGF0aW9uIG9mIGEgdG9wb3MgU2luZ2xlKGEpIGFuZCBTaW5nbGUoYeKA mSkgd291bGQgYmUgcHJvcG9zaXRpb25hbGx5IGVxdWFsIGR1ZSB0byBwcm9wb3NpdGlvbmFsIGV4 dGVuc2lvbmFsaXR5LiBUaGUgb25seSBhZGRpdGlvbmFsIGFzc3VtcHRpb24gSSBuZWVkIHRvIG1h a2UgaXMgdGhhdCB0aGUgdW5pdmVyc2Ugb2YgcHJvcG9zaXRpb24gaXMgc3RyaWN0LCBlLmcuIHdl IGhhdmUgdGhhdCBFbChBIC0+IEIpIGlzIGRlZmluaXRpb25hbGx5IGVxdWFsIHRvICBFTChBKSAt PiBFbChCKS4gVGhpcyBzZWVtcyB0byBiZSBxdWl0ZSBuYXR1cmFsIGZyb20gdGhlIHBvaW50IG9m IHR5cGUgdGhlb3J5IHdoZXJlIHVuaXZlcnNlcyBhcmUgdXN1YWxseSBzdHJpY3QgYW5kIG1vcmVv dmVyIHRoaXMgaXMgdHJ1ZSBpbiBhbnkgdW5pdmFsZW50IGNhdGVnb3J5IGdpdmluZyByaXNlIHRv IGEgdG9wb3MuIA0KDQpUaG9yc3Rlbg0KCgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1l bnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4g Y29uZmlkZW50aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3Nh Z2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5kIGl0IGJhY2sgdG8gbWUsIGFuZCBpbW1lZGlhdGVseSBk ZWxldGUgaXQuIAoKUGxlYXNlIGRvIG5vdCB1c2UsIGNvcHkgb3IgZGlzY2xvc2UgdGhlIGluZm9y bWF0aW9uIGNvbnRhaW5lZCBpbiB0aGlzCm1lc3NhZ2Ugb3IgaW4gYW55IGF0dGFjaG1lbnQuICBB bnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZQphdXRob3Igb2YgdGhpcyBlbWFp bCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2YgdGhlClVuaXZlcnNpdHkg b2YgTm90dGluZ2hhbS4KClRoaXMgbWVzc2FnZSBoYXMgYmVlbiBjaGVja2VkIGZvciB2aXJ1c2Vz IGJ1dCB0aGUgY29udGVudHMgb2YgYW4KYXR0YWNobWVudCBtYXkgc3RpbGwgY29udGFpbiBzb2Z0 d2FyZSB2aXJ1c2VzIHdoaWNoIGNvdWxkIGRhbWFnZSB5b3VyCmNvbXB1dGVyIHN5c3RlbSwgeW91 IGFyZSBhZHZpc2VkIHRvIHBlcmZvcm0geW91ciBvd24gY2hlY2tzLiBFbWFpbApjb21tdW5pY2F0 aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5IGJlIG1vbml0b3JlZCBh cwpwZXJtaXR0ZWQgYnkgVUsgbGVnaXNsYXRpb24uCgo=