From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a50:a5c8:: with SMTP id b8-v6mr9697135edc.1.1525520155071; Sat, 05 May 2018 04:35:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:ba87:: with SMTP id x7-v6ls6676084ede.6.gmail; Sat, 05 May 2018 04:35:54 -0700 (PDT) X-Received: by 2002:a50:90fd:: with SMTP id d58-v6mr9704026eda.12.1525520153988; Sat, 05 May 2018 04:35:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525520153; cv=none; d=google.com; s=arc-20160816; b=FdKcuXYCeLCx5j47oRkDn3YE5YX2Xu4ZFlcdSebhySOo+OLDp29zNTRJ7UYwKbcZN6 K8cp5SbXk5C7DLvNIr8WDsVC/wdViUpEH53b7TJmOzTz8t9cnFqe0A2Zj10hWNmh/axa zIx/84QDJa+mdEOy2Z6RAhTaxbqiImtLzyHk2pBKZFIHv2SDEa3aekZW+06tqSPl0dVE /2A46YlqtuBW3Svrb2fOnufzFwA+BIbF9i0/xDvKTtnWFAdxpBiXVX8KaiiJYOZV9/Gr B+KU272HIo0s0rUQ/eSazUjGYKIDhhCAIiGuty1Tuf5dUn1ZV3jRpSCMnmfs9CCqPvOh hKOw== 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=37dwJcUCtldTh9n0ztdf7VtGot7EDj+MopFK4ue4m8I=; b=kQU6nGcQ31euLBfApUvt6jw9jZwe0tl5TSNt/rBQOPNPnGpPpUJD8YF0zTp20Om53o l9/CwrpOBkPbu/OEcJ7lE8ryank0ja3+0WBi/0Q6X9UX/CPd/2dYmTooUqKJZ5bUlhll Lq2OoQuT5BZYbHJ2SmOjbwqtRzYt5pmoWD7iIt97khrA2Su9IPiMfX3eUhYiPU56s9D+ F8ICPKTcgVBE45NkJhDlU2x59556EuAa1ECbLCzAOUocGP9DpWA+mBAUTnt25agoAa64 3/7t4qwIf0wBzNj99Nut3jr8Q0RwKL0b6BhL5QqJBeBPDqKPfzbru1g+/lvQP9gsPWHC 7ujw== 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 v28-v6si100988edd.1.2018.05.05.04.35.53 for ; Sat, 05 May 2018 04:35:53 -0700 (PDT) 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 9D8622DF5DE_AED9719B for ; Sat, 5 May 2018 11:35:53 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 5029030AEA6_AED9719F for ; Sat, 5 May 2018 11:35:53 +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 1fEvTk-0003YQ-Or; Sat, 05 May 2018 12:35:53 +0100 Received: from EUR01-DB5-obe.outbound.protection.outlook.com (213.199.154.183) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Sat, 5 May 2018 12:35:46 +0100 Received: from DB6PR0601MB2037.eurprd06.prod.outlook.com (10.168.56.142) by DB6PR0601MB2392.eurprd06.prod.outlook.com (10.169.213.23) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.735.16; Sat, 5 May 2018 11:35:51 +0000 Received: from DB6PR0601MB2037.eurprd06.prod.outlook.com ([fe80::10e3:47c2:5cdf:ea16]) by DB6PR0601MB2037.eurprd06.prod.outlook.com ([fe80::10e3:47c2:5cdf:ea16%13]) with mapi id 15.20.0735.016; Sat, 5 May 2018 11:35:51 +0000 From: Thorsten Altenkirch To: Michael Shulman , =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= CC: Homotopy Type Theory Subject: Re: [HoTT] Bishop's work on type theory Thread-Topic: [HoTT] Bishop's work on type theory Thread-Index: AQHT4+skxcm/AzBp+EuTV9bH7fGsN6QgHcMAgAACEQCAAAJQgIAAAPwAgAACJwCAAGWfgIAAiFOA Date: Sat, 5 May 2018 11:35:51 +0000 Message-ID: References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> <385f5d47-0656-4a4d-b24c-c2abeab629e7@googlegroups.com> In-Reply-To: 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: [86.28.226.182] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB6PR0601MB2392;7:UJZ7AY/AHOrLOD2DT83L3+XKfQ0JBVDSLELSSuYujrEOAeo4Z+FK9DdcLz+ChOSTo0w540sIwDsYHQlSGuzG2q0d4inHDQT15qkzoFW2Fb0NEg+2tAHgGvYCjdftR1TIemBPNP4m/ZWlaM8sQgBYgcXHi3UvTYfURg/FuMjyJskoCqsBvooH4/Xsd9si4WDu0rhSosKi7Mm+FQsCNmFcJHAPoizt3QQbe7M9w6sTpRzc6AP3IPYvDZQgk3rUR6r9 x-ms-exchange-antispam-srfa-diagnostics: SOS; x-microsoft-antispam: UriScan:(215639381216008);BCL:0;PCL:0;RULEID:(7020095)(4652020)(8989080)(5600026)(4534165)(7168020)(4627221)(201703031133081)(201702281549075)(8990040)(2017052603328)(7167020)(7153060)(7193020);SRVR:DB6PR0601MB2392; x-ms-traffictypediagnostic: DB6PR0601MB2392: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(215639381216008)(131327999870524); x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(8121501046)(5005006)(93006095)(93001095)(10201501046)(3231254)(944501410)(52105095)(3002001)(6041310)(20161123560045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123562045)(20161123558120)(20161123564045)(6072148)(201708071742011);SRVR:DB6PR0601MB2392;BCL:0;PCL:0;RULEID:;SRVR:DB6PR0601MB2392; x-forefront-prvs: 0663390E1B x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(396003)(366004)(39380400002)(39850400004)(346002)(199004)(189003)(6506007)(6436002)(26005)(2906002)(6512007)(93886005)(110136005)(316002)(3280700002)(186003)(86362001)(97736004)(7736002)(3660700001)(5660300001)(786003)(55236004)(53936002)(102836004)(305945005)(6486002)(478600001)(2171002)(53546011)(81156014)(2900100001)(68736007)(486006)(476003)(8676002)(14454004)(39060400002)(5250100002)(81166006)(25786009)(106356001)(66066001)(8936002)(4326008)(105586002)(6246003)(99286004)(76176011)(58126008)(6116002)(3846002)(229853002)(11346002)(74482002)(446003)(2616005)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB6PR0601MB2392;H:DB6PR0601MB2037.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: P0t1f9QTy1oBruz11/MX/zRLUFEZd2b2KUBLPC04qMSVXIF/taPLF6SOHvKGjmGji37yVWbi78+SHPGq+vJ/49tenKRjR1otzIQQVYQ59AJCsr5qRCkycVsRq9ied/PfzPcaNJyCeTv30TGXkWzXMdbyAB2fBQqk4iNQY74hgniXwSKOgr5sjPpam1ANV5iY spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Office365-Filtering-Correlation-Id: da6d8e3d-a768-44f6-730a-08d5b27c5aeb X-MS-Exchange-CrossTenant-Network-Message-Id: da6d8e3d-a768-44f6-730a-08d5b27c5aeb X-MS-Exchange-CrossTenant-originalarrivaltime: 05 May 2018 11:35:51.2611 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB6PR0601MB2392 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 DQoNCk9uIDA1LzA1LzIwMTgsIDA1OjI3LCAiaG9tb3RvcHl0Li4uQGdvb2dsZWdyb3Vwcy5jb20g b24gYmVoYWxmIG9mDQpNaWNoYWVsIFNodWxtYW4iIDxob21vdG9weXQuLi5AZ29vZ2xlZ3JvdXBz LmNvbSBvbiBiZWhhbGYgb2YNCnNodS4uLkBzYW5kaWVnby5lZHU+IHdyb3RlOg0KDQo+My4gSGUg aW5jbHVkZXMgdGhlIGF4aW9tIG9mIGNob2ljZSAocDEyKSBmb3JtdWxhdGVkIGluIHRlcm1zIG9m IGhpcw0KPihwcm9vZi1pcnJlbGV2YW50KSBwcm9wb3NpdGlvbnMsIGFzIHdlbGwgYXMgd2hhdCBz ZWVtcyB0byBiZSBhIEhpbGJlcnQNCj5jaG9pY2Ugb3BlcmF0b3IgKHRob3VnaCBpdCdzIG5vdCBj bGVhciB0byBtZSB3aGV0aGVyIHRoaXMgYXBwbGllcyBpbg0KPm9wZW4gY29udGV4dHMgb3Igbm90 KS4gIFNpbmNlIGhlIGhhcyBwb3dlcmNsYXNzZXMgd2l0aCBwcm9wb3NpdGlvbmFsDQo+ZXh0ZW5z aW9uYWxpdHksIEkgdGhpbmsgdGhpcyBtZWFucyB0aGF0IERpYWNvbmVzY3UncyBhcmd1bWVudCBw cm92ZXMNCj5MRU0sIHdoaWNoIGhlIG9idmlvdXNseSB3b3VsZG4ndCB3YW50LiAgSXQncyBoYXJk ZXIgZm9yIG1lIHRvIGd1ZXNzDQo+aG93IHRoaXMgc2hvdWxkIGJlIGZpeGVkLCBzaW5jZSB3aXRo b3V0IHNvbWUga2luZCBvZiBBQywgc2V0b2lkcyBkb24ndA0KPnNhdGlzZnkgdGhlIHByaW5jaXBs ZSBvZiB1bmlxdWUgY2hvaWNlLg0KDQpXaHkgbm90PyBJZiB3ZSBpZGVudGlmeSBwcm9wb3NpdGlv bnMgd2l0aCBzZXRvaWRzIHRoYXQgYXJlIGludGVybmFsbHkNCnByb3Bvc2l0aW9ucyAoYWxsIGVs ZW1lbnRzIGFyZSBlcXVhbCkgYW5kIGlkZW50aWZ5IHByb3Bvc2l0aW9ucyB1cHRvDQpsb2dpY2Fs IGVxdWFsaXR5IHdlIGdldCB1bmlxdWUgY2hvaWNlLg0KDQpXaGF0IGRvIEkgbWlzcyBoZXJlPw0K VGhvcnN0ZW4NCg0KDQo+DQoNCgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJl IGludGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlk ZW50aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4g ZXJyb3IsIHBsZWFzZSBjb250YWN0IHRoZSBzZW5kZXIgYW5kIGRlbGV0ZSB0aGUgZW1haWwgYW5k CmF0dGFjaG1lbnQuIAoKQW55IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieSB0aGUgYXV0 aG9yIG9mIHRoaXMgZW1haWwgZG8gbm90Cm5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9m IHRoZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uIEVtYWlsCmNvbW11bmljYXRpb25zIHdpdGgg dGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkIAp3aGVyZSBwZXJt aXR0ZWQgYnkgbGF3LgoKCgoK