From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.80.142.245 with SMTP id x50mr323459edx.0.1513699819402; Tue, 19 Dec 2017 08:10:19 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.80.241.28 with SMTP id w28ls6736049edl.0.gmail; Tue, 19 Dec 2017 08:10:17 -0800 (PST) X-Received: by 10.80.151.161 with SMTP id e30mr327000edb.4.1513699817963; Tue, 19 Dec 2017 08:10:17 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1513699817; cv=none; d=google.com; s=arc-20160816; b=PdjjWYDQ1BC9Yuu9PCOlTnH7mhCtzdFg9EyN1J6+10HW75UngrK/OW+IpiyPjxKRp+ bYoF3aYn6EqN68m0GTmK4Br+HBMMbJmtyzKWD9+YnvWg/T7qWAP52RYrnPtHhE3P3chm uKeqATJUGRsVXuiw5pyT/7lfB4/eP882ZFB13xTTnvM2tnlC4XZuuiv4Z74jlXEK7jN5 9ApPnWwpMgY/lDlwcLvokXtaB5BZNOFleOzCZa76uJBBQ+72UN/EHu6+pmxcE/au/WC+ 2W+g2SD1R37q80OZUndz8kc+/qUDX+GMAl8fB3PJOJrTpINNAsksaM3d+mz8gpIkE4vc vrUA== 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=DUSs9m7SwGUXmX4au7udW9bH6soy2t8LyhdM6syR+g4=; b=W7tpc6HG9M3XtbeM7ilsgAB81RgQyXEHEzMvUeUpTLcWldDyoj8hxwzIzkQ/c18bB1 xwsqzjpxAFTm4pNtRwssa7WLtcmecL3sbDryj/st5kIiaqOKRVKmt1paMbHamVGwRzMU jlTElQ3ghrbI8VqLVgdwphNbbpI7ncreXUYqFeiMnVk9opZuduzS+DjGHAp1wcCrR7nZ qF2nQpsiiqti/Ydy+kX/IU3lNvhCBs9O+3HfQOfgJ3+p/8mP8zP/mTjfPblpST2jRXKx EQVFMhjCQ7xAdI36suhdLTsGOi/ZHITNKU/fnUmRXntghmsXmTRCqgP0r1ZZZ+O13ZOL 6MLg== 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 h45si1227205eda.2.2017.12.19.08.10.17 for ; Tue, 19 Dec 2017 08:10:17 -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 9F03341C18F_A3939E9B for ; Tue, 19 Dec 2017 16:10:17 +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 6FAF131FAA9_A3939E9F for ; Tue, 19 Dec 2017 16:10:17 +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 1eRKT8-0008G9-Vd; Tue, 19 Dec 2017 16:10:17 +0000 Received: from EUR02-HE1-obe.outbound.protection.outlook.com (213.199.180.175) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Tue, 19 Dec 2017 16:10:15 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com (10.165.213.15) by DB5PR06MB1719.eurprd06.prod.outlook.com (10.165.213.17) 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:10:13 +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:10:13 +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+MsiAgAFNJACAAA1dAIAAEHaAgAAFP4CABQTogIACmu0AgAAacoCAABWzgIABlfMAgAGLLYCAACi3gIAADmUAgAANMACAAAreAA== Date: Tue, 19 Dec 2017 16:10:13 +0000 Message-ID: References: <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> <20171219153118.GA9218@mathematik.tu-darmstadt.de> In-Reply-To: <20171219153118.GA9218@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;DB5PR06MB1719;6:rRAiRBx9driAYpsekYX+poI1YU6pwQ69D7NO85qJdoW0ju4mIIIPdXWArQt4R87l5u5UUMxpelpoV3yObPczJLb8KLSDFOMCcdClBzYuLBuQnnt6IAAAhKIBcmNqwyegNdNTky3SuLkkRUUnKWHO47C1cUEjIiOV1zjBJAEP994t7wfk7GLjpQMueGhIa1tsyyGoen1LxS9JM/LcOkUnrqiML62m06gsXbMIy+PjlvNrFkYlFHQFN1noWjxWai1zyU+4dM4HQrOHuHBdV8V5pTLfvlOWceI5FjbDcaL7ZDwjKP8umRHC6oN2QcLndP2iAHA0UJTPIU8vKiefFTqzo+BjMA6t1wuDqAeN4md8iVk=;5:1vT3nsDGVh/R6Gqofl9/6DBAcJYjVhyHWZAI94okmjoP3SL7r2dIfR6XBCF+WW2DFowoUQAsSDN7MaehpE8WzIxgqXF4QPpqZMLbDDEvNqY9Bd/NlQckEPjiyN2rdWrjiXmfB4ODABHci3hXnltMBlbKMoYZE94GGfBU3W6Z5Lg=;24:7AA7BcgyU8/qVGKWPs77OJrIKpBlq3zFvtrj9tWe9WAx9htSdQM7fzLvDSOX5Avut6X03dHuNyR3xxD8M9QIipKfd3aIrCCY+M8m1IAP3aQ=;7:iwi3XNboQu31O+1ySCCg60aKzMTdBcS36Vz3RDyJifX0N9KY8LDS304DWGw1EzR9L8Td98j5vzvnwW+PrD2IokjuSmiKFT6KEs2Y5aqCnephzZ2DoAv9Q8ACI2iHtg1AsETnst2+pxVahBZDDu9DxsMS6BTsBIIvZBGPVAh1zqYdEEwLrPnBGfecUFRDyJ21Ap01oGEAEImLCMyAgO5b23cZLvK4zyXETUpf9F2Z2vxXhl5I4v2YS6huKdz/zEKX x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: a2796002-b449-4257-1b1e-08d546fafc68 x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(5600026)(4604075)(4534020)(4602075)(4627115)(201703031133081)(201702281549075)(2017052603307);SRVR:DB5PR06MB1719; x-ms-traffictypediagnostic: DB5PR06MB1719: 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)(10201501046)(93006095)(93001095)(3231023)(3002001)(6041248)(20161123562025)(20161123555025)(20161123564025)(20161123560025)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123558100)(6072148)(201708071742011);SRVR:DB5PR06MB1719;BCL:0;PCL:0;RULEID:(100000803101)(100110400095);SRVR:DB5PR06MB1719; x-forefront-prvs: 052670E5A4 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(39860400002)(396003)(366004)(376002)(346002)(189003)(199004)(24454002)(8676002)(93886005)(76176011)(14454004)(81166006)(478600001)(68736007)(42882006)(316002)(7736002)(786003)(2950100002)(74482002)(33656002)(105586002)(5660300001)(81156014)(83716003)(305945005)(2906002)(58126008)(6916009)(25786009)(97736004)(54906003)(8936002)(4326008)(106356001)(3660700001)(6116002)(102836003)(6486002)(5250100002)(229853002)(53936002)(2900100001)(99286004)(6246003)(86362001)(82746002)(6512007)(6506007)(66066001)(3280700002)(53546011)(6436002)(3846002)(83506002)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1719;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: <2BFAB27AC3B6594D...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: a2796002-b449-4257-1b1e-08d546fafc68 X-MS-Exchange-CrossTenant-originalarrivaltime: 19 Dec 2017 16:10:13.1992 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB5PR06MB1719 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: -0.0 (/) QWgsIHlvdSBzdWZmZXIgZnJvbSB1c2luZyBzZXQgdGhlb3J5IGFzIGEgbWV0YSBsYW5ndWFnZS4g KA0KDQpUaGVyZSBhcmUgbG90cyBpZiB1bml2YWxlbnQgY2F0ZWdvcmllcy4gSW4gSG9UVC4NCg0K VGhvcnN0ZW4NCg0KT24gMTkvMTIvMjAxNywgMTU6MzEsICJob21vdG9weXQuLi5AZ29vZ2xlZ3Jv dXBzLmNvbSBvbiBiZWhhbGYgb2YgVGhvbWFzIFN0cmVpY2hlciIgPGhvbW90b3B5dC4uLkBnb29n bGVncm91cHMuY29tIG9uIGJlaGFsZiBvZiBzdHJlLi4uQG1hdGhlbWF0aWsudHUtZGFybXN0YWR0 LmRlPiB3cm90ZToNCg0KICAgIEkgYW0gYWZyYWlkIHRoZXJlIHdhbnQgZXhpc3QgdG9vIG1hbnkg dW5pdmFsZW50IGNhdGVnb3JpZXMuIFRoZXkgYWxsDQogICAgd291bGQgYmUgcmlnaWQgd2hpY2gg aXMgdmVyeSBpbmNvbnN0cnVjdGl2ZS4NCiAgICANCiAgICANCg0KCgoKClRoaXMgbWVzc2FnZSBh bmQgYW55IGF0dGFjaG1lbnQgYXJlIGludGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQph bmQgbWF5IGNvbnRhaW4gY29uZmlkZW50aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNl aXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJyb3IsIHBsZWFzZSBzZW5kIGl0IGJhY2sgdG8gbWUsIGFu ZCBpbW1lZGlhdGVseSBkZWxldGUgaXQuIAoKUGxlYXNlIGRvIG5vdCB1c2UsIGNvcHkgb3IgZGlz Y2xvc2UgdGhlIGluZm9ybWF0aW9uIGNvbnRhaW5lZCBpbiB0aGlzCm1lc3NhZ2Ugb3IgaW4gYW55 IGF0dGFjaG1lbnQuICBBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2VkIGJ5IHRoZQphdXRo b3Igb2YgdGhpcyBlbWFpbCBkbyBub3QgbmVjZXNzYXJpbHkgcmVmbGVjdCB0aGUgdmlld3Mgb2Yg dGhlClVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4KClRoaXMgbWVzc2FnZSBoYXMgYmVlbiBjaGVj a2VkIGZvciB2aXJ1c2VzIGJ1dCB0aGUgY29udGVudHMgb2YgYW4KYXR0YWNobWVudCBtYXkgc3Rp bGwgY29udGFpbiBzb2Z0d2FyZSB2aXJ1c2VzIHdoaWNoIGNvdWxkIGRhbWFnZSB5b3VyCmNvbXB1 dGVyIHN5c3RlbSwgeW91IGFyZSBhZHZpc2VkIHRvIHBlcmZvcm0geW91ciBvd24gY2hlY2tzLiBF bWFpbApjb21tdW5pY2F0aW9ucyB3aXRoIHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0gbWF5 IGJlIG1vbml0b3JlZCBhcwpwZXJtaXR0ZWQgYnkgVUsgbGVnaXNsYXRpb24uCgo=