From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.235.87 with SMTP id j84mr172155lfh.13.1508064166704; Sun, 15 Oct 2017 03:42:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.46.21.76 with SMTP id 12ls76664ljv.2.gmail; Sun, 15 Oct 2017 03:42:45 -0700 (PDT) X-Received: by 10.46.23.70 with SMTP id l67mr208232lje.11.1508064165086; Sun, 15 Oct 2017 03:42:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1508064165; cv=none; d=google.com; s=arc-20160816; b=eRtFt2dMpXjuxUmTkwlBIB5+9AVlqCa9gbZVA5jYzMsOUi0XxDfnz7WhXXc+Wn0HmJ a7WRW6fvpTL1vmhuNX7YLWAP0sDBmUW5xxDPbvlgzomTrynImn/8UiI56i/3r/HGd7U4 hoTpbr5mmL6mkwzshMB45ADzg8tKSs+CKisiOKoLlJHhwk6EbFPKtYTycRZAfDABbaP1 eE1lgcnPr1e3tmYkVw06ds42sbHgYKxBv6XstQNZd//rvLfwEgOzVIRddNH920oDy/yz o9Wq8c4CijTNvlLxXg1fV4e5tqVvv8tfWaAguFm5g4vAsjvhQNVfVsa65RWWXGbw6izq 3e2Q== 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=DI9YXoFhErqqvbApCRnIMztDDmizjvUkJrHNZJgfHrg=; b=f5I+cjsNY5hZqr/oGUTRc9HfOZk4+K3/u92g2erWVpp4CxWKkd66lwLHq7jPQT/hA5 EZXFx2zj5sLBrDNkGjqBNE0VCGL+hCFrY4VTdnPH+LVQTKXWDRp7CbOLOn6AtbMlI+ir CV62pD8JA6zUouqhaNkkHP2de/rmDfeiqJKvMRHhPJLOFQP4CgTWoafcIJMaECf1fNGG jX3K9xkQ3EYDJN3qLlFyu/9GwbtLOKEoz5KzV6f8KumT+um8+ulyMqjMkSscqyldaodl Or+snK/9RwwsR8nlKkIgQgeagZ8B+jMj5b7rY7zqs3W2480euEC//G+N7V3Edp8vFeJd dTnQ== 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 j65si256918lje.3.2017.10.15.03.42.44 for ; Sun, 15 Oct 2017 03:42:44 -0700 (PDT) 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 58EC43D5816_9E33BA4B for ; Sun, 15 Oct 2017 10:42:44 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id B2CE0690244_9E33BA3F for ; Sun, 15 Oct 2017 10:42:43 +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 1e3gNX-0007SM-6g; Sun, 15 Oct 2017 11:42:43 +0100 Received: from EUR03-AM5-obe.outbound.protection.outlook.com (213.199.154.113) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.351.0; Sun, 15 Oct 2017 11:42:42 +0100 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.77.7; Sun, 15 Oct 2017 10:42:42 +0000 Received: from DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::38e6:ba6f:5e58:86c9]) by DB5PR06MB1717.eurprd06.prod.outlook.com ([fe80::38e6:ba6f:5e58:86c9%14]) with mapi id 15.20.0077.022; Sun, 15 Oct 2017 10:42:42 +0000 From: Thorsten Altenkirch To: Andrej Bauer , Homotopy Type Theory CC: Univalent Mathematics Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Topic: [HoTT] A small observation on cumulativity and the failure of initiality Thread-Index: AQHTQ4n+2jeUen/lsUyeJmmKJObyUKLhbFIAgAACMQCAAZiMgIAAEeaAgAG1U4A= Date: Sun, 15 Oct 2017 10:42:41 +0000 Message-ID: References: <20171013081056.GB18718@mathematik.tu-darmstadt.de> 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 x-originating-ip: [82.31.58.108] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;DB5PR06MB1720;6:osjH5/s8+EZ4AhCZD/HrIml3fYvQT5VGFOAx4GVQi+LDKCzGRtlM4yVWQAR9BKdtj7UZe/l+x5VcrIJ3nW+LQ6vbH4NHAJn7FKAhbo/peOC83l6SADKcbk9BHBWdN9s6G4BS1BC4f9rVcZt05k3df5sEcZOr7mYI623SFK5p77DFESxwIu80IFvgolsVC4Tuqrubm6sKNgLU6Fpdo6TBlCcnDs+hjuoIZaj6ktENZp80wfolegHx9OTFWMdxx6YHlalpqXwSMT7sabSTtrezYEMQPJpUKaVnFwEqaIwGpepVCTZ66P/WPCiJsAm0G12R134FLvwdLP792cAcPCe3lA==;5:M24C4uusmN4iS/xCNsjRSbFvPgtlQWeHEeclEQxf6qr/oyYeINMP5ohc++zS71pg3ZI9xW+jI9VSj0T6VSsTOQOMS9b9yRZ8E9wHlsJR1eoTSTzX2C2PQ/mfuefpoWmO1ZUCmbp/V6VDlRNp3mX7eqC+JoJjglF7O2jNwVHbaMc=;24:67IYw1G/KAM70dkpXGqusKE0IpfmlyYgQdLT4Zz0t00SGUfsjI1nJvHhJtGfwV5TUehsQ7JVzbfJmy87Tn+8VNUa8czuT6031E2gIID5To0=;7:9VlWi/wgKWdEeaEVuEE6kmRtmtO2wbXeGSiuumCLke3s9VuoGR1NW4Glr9Bw21IYqRXkbzBsMgV4cK1fSIgzJpD5zjs0R37zUvik5hpirgx1n3kHqBXR+Q0AysiPlZgrd5cYoNPMagUYQk4oMc9GMMIwP1Q66PfUJeH052w7TT0a1q8kmLGZL8MWUQJ/LmvbB8e+jdKWeqUkFpkU6fEmiA6AFNwVi5gy2ee/NuAXm/M= x-ms-exchange-antispam-srfa-diagnostics: SSOS; x-ms-office365-filtering-correlation-id: 2410c10a-aa80-41ca-5dc2-08d513b97676 x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(22001)(2017030254152)(2017052603199)(201703131423075)(201703031133081)(201702281549075);SRVR:DB5PR06MB1720; x-ms-traffictypediagnostic: DB5PR06MB1720: x-exchange-antispam-report-test: UriScan:(215639381216008)(228788266533470)(211936372134217)(17755550239193); x-microsoft-antispam-prvs: x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(100000700101)(100105000095)(100000701101)(100105300095)(100000702101)(100105100095)(6040450)(2401047)(5005006)(8121501046)(93006095)(93001095)(3002001)(100000703101)(100105400095)(10201501046)(920507026)(6041248)(20161123562025)(20161123564025)(201703131423075)(201702281529075)(201702281528075)(201703061421075)(201703061406153)(20161123558100)(20161123555025)(20161123560025)(6072148)(201708071742011)(100000704101)(100105200095)(100000705101)(100105500095);SRVR:DB5PR06MB1720;BCL:0;PCL:0;RULEID:(100000800101)(100110000095)(100000801101)(100110300095)(100000802101)(100110100095)(100000803101)(100110400095)(100000804101)(100110200095)(100000805101)(100110500095);SRVR:DB5PR06MB1720; x-forefront-prvs: 046164D5C4 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(6009001)(346002)(376002)(24454002)(189002)(199003)(7736002)(99286003)(305945005)(2900100001)(8936002)(34040400001)(53936002)(5660300001)(6512007)(6306002)(786003)(316002)(68736007)(478600001)(83506001)(3660700001)(74482002)(3846002)(6246003)(8676002)(81166006)(58126008)(81156014)(110136005)(966005)(86362001)(189998001)(5250100002)(14454004)(2906002)(229853002)(66066001)(93886005)(6116002)(102836003)(6486002)(53546010)(3280700002)(6436002)(50986999)(25786009)(42882006)(2950100002)(101416001)(76176999)(4326008)(54356999)(97736004)(106356001)(6506006)(105586002)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:DB5PR06MB1720;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) authentication-results: spf=none (sender IP is ) smtp.mailfrom=psz...@exmail.nottingham.ac.uk; spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <16861C1D55DFF746...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Exchange-CrossTenant-originalarrivaltime: 15 Oct 2017 10:42:41.8576 (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 (/) T24gMTQvMTAvMjAxNywgMTA6MzcsICJob21vdG9weXQuLi5AZ29vZ2xlZ3JvdXBzLmNvbSBvbiBi ZWhhbGYgb2YNCkFuZHJlaiBCYXVlciIgPGhvbW90b3B5dC4uLkBnb29nbGVncm91cHMuY29tIG9u IGJlaGFsZiBvZg0KYW5kcmVqLi4uQGFuZHJlai5jb20+IHdyb3RlOg0KDQo+PiBJbiBvdXIgcmVj ZW50IHdvcmsgb24gaW50cmluc2ljDQo+PiBzeW50YXggb2YgVHlwZSBUaGVvcnkgd2UgcHJlc2Vu dCBhIHR5cGVkIHN5bnRheCB0aGF0IG5ldmVyIHJlZmVycyB0bw0KPj4gcHJldGVybXMuIEluIHRo aXMgZnJhbWV3b3JrIHRoZW9yaWVzIHdpdGggY29lcmNpb25zIGNhbm5vdCBiZSBleHByZXNzZWQN Cj4+IGFuZCB0aGUgc3ludGF4IGlzIHRoZSBpbml0aWFsIGFsZ2VicmEgb2YgdGhlIGNvcnJlc3Bv bmRpbmcgbm90aW9uIG9mDQo+PiBhbGdlYnJhcy4NCj4NCj5UaGlzIGlzIHF1aXRlIGNvb2wsIGJ1 dCBJJ2QganVzdCBsaWtlIHRvIHBvaW50IG91dCB0aGF0IHRoZXJlIGFyZQ0KPmxldmVscyBvZiBh YnN0cmFjdGlvbiwgc29tZSBvZiB3aGljaCBjYW5ub3QgYmUgaWdub3JlZC4NCj4NCj5BdCBhIHZl cnkgYmFuYWwgbGV2ZWwsIHdlIG5lZWQgdG8ga25vdyBob3cgdG8gY29udmVydCBjb25jcmV0ZSBz eW50YXgNCj5pbnRvIGFic3RyYWN0IHN5bnRheC4NCj4NCj5BdCBhIHNsaWdodGx5IGxlc3MgYmFu YWwgbGV2ZWwsIHdlIGhhdmUgdG8gYWRtaXQgdGhhdCBwcmV0ZXJtcw0KPihleHByZXNzZWQgYXMg YWJzdHJhY3Qgc3ludGF4KSBhcmUgdW5hdm9pZGFibGUuIEFuIGltcG9ydGFudCBhc3BlY3Qgb2YN Cj50eXBlIHRoZW9yeSByZXZvbHZlcyBhcm91bmQgbWFraW5nIHN1cmUgdGhhdCB0aGUgdGhpbmcg d3JpdHRlbiBkb3duDQo+bWFrZXMgc2Vuc2UuIFRoZSAidGhpbmcgd3JpdHRlbiBkb3duIiBpcyBh IHByZXRlcm0gKHNvbWV0aGluZyB0aGF0DQo+c3Vydml2ZWQgcGFyc2luZyBidXQgaGFzIHlldCB0 byBiZSB0eXBlIGNoZWNrZWQpLg0KDQpJbmRlZWQsIGJ1dCBpdCBpc24ndCBldmVuIHByZXRlcm1z IGJ1dCBzdHJpbmdzIHdlIHJlYWxseSBzZWUgKG9yIGJpdHM/KS4NClRoZSB0aGVvcmVtIHRoYXQg YmV0YS1yZWR1Y3Rpb24gcHJlc2VydmVzIG1hdGNoaW5nIGJyYWNrZXRzIGlzICBtaXhpbmcNCmxl dmVscyBvZiBhYnN0cmFjdGlvbiBpbiBiYWQgd2F5LiBBcyB3ZSBhcmUgaGFwcHkgdG8gcmVhc29u IGFib3V0IHRlcm1zIGFzDQp0cmVlcyBrbm93aW5nIHRoYXQgd2UgY2FuIHBhcnNlIHN0cmluZ3Mg aW50byB0cmVlcywgd2Ugc2hvdWxkIHRoaW5rIGFib3V0DQppbnRyaW5zaWMgdGVybXMgKHdoYXQg VGhvbWFzIGNhbGxzICJkZXJpdmF0aW9ucyIpIGtub3dpbmcgdGhhdCBieSB0eXBlDQpjaGVja2lu ZyBhbmQgc2NvcGUgY2hlY2tpbmcgd2UgY2FuIGNvbnZlcnQgdHJlZXMgaW50byBkZXJpdmF0aW9u cy4NCkFzc2lnbmluZyBtZWFuaW5nIHRvIHB1cmVseSBzeW50YWN0aWMgZW50aXRpZXMgaXMgYSBj b25mdXNpbmcgbGV2ZWxzIG9mDQphYnN0cmFjdGlvbnMgaW4gdGhlIHNhbWUgd2F5IGFzIHRoZSBt YXRjaGluZyBicmFja2V0cyB0aGVvcmVtLg0KDQo+DQo+VGhlcmUgaXMgYWxzbyB0aGUgcXVlc3Rp b24gb2YgYnJlYWtpbmcgdGhlIHZpY2lvdXMgY2lyY2xlOiB3ZSBleHByZXNzDQo+dHlwZSB0aGVv cnkgaW5zaWRlIHR5cGUgdGhlb3J5LCBidXQgd2hlcmUgZGlkIHRoZSBvcmlnaW5hbCB0eXBlIHRo ZW9yeQ0KPmNvbWUgZnJvbT8gSSB0aGluayBpdCBpcyBxdWl0ZSByZWFzb25hYmxlIHRvIHRha2Ug dGhlIHBvc3NpdGlvbiB0aGF0DQo+dHlwZSB0aGVvcnkgaXMgcHJpbWl0aXZlLCBidXQgaXQgaXMg YWxzbyBlcXVhbGx5IHJlYXNvbmFibGUgdG8gdGFrZQ0KPnRoZSBwb3NpdGlvbiB0aGF0IG9uZSBz aG91bGQgYW5hbHlzZSBob3cgdHlwZSB0aGVvcnkgYXJpc2VzIGZyb20gYQ0KPm1vcmUgY29uY3Jl dGUgc2V0dXAsIGZvciBpbnN0YW5jZSwgdGhlcmUgaXMgc29tZSB2YWx1ZSBpbiBrbm93aW5nIHRo YXQNCj50aGUgc3ludGFjdGljIG1vZGVscyBiYXNlZCBvbiBjb25jcmV0ZSBzeW50YXggYXJlIGlu aXRpYWwgZm9yIHR5cGUNCj50aGVvcnkuDQoNClRoZSBvcmlnaW5hbCB0eXBlIHRoZW9yeSBpcyBp biBvdXIgbWluZCBhbmQgd2UgbWF5IHVzZSBlbmdsaXNoIG9yIGFueQ0Kb3RoZXIgbmF0dXJhbCBs YW5ndWFnZSB0byBleHByZXNzIGl0IGFuZCB0aGVuIHdlIHdhbnQgdG8gYmUgbW9yZSBwcmVjaXNl DQphbmQgdXNlIHRoZSB0eXBlIHRoZW9yeSBpbiBvdXIgbWluZHMgdG8gZXhwbGFpbiB0aGUgdHlw ZSB0aGVvcnkgd2UNCmltcGxlbWVudCwgd2hpY2ggdGhlbiBpbiB0dXJuIGNhbiBiZSBpbXBsZW1l bnRlZC4gTm8gdmljaW91cyBjaXJjbGUuDQoNClRob3JzdGVuDQoNCg0KPg0KPldpdGgga2luZCBy ZWdhcmRzLA0KPg0KPkFuZHJlag0KPg0KPi0tIA0KPllvdSByZWNlaXZlZCB0aGlzIG1lc3NhZ2Ug YmVjYXVzZSB5b3UgYXJlIHN1YnNjcmliZWQgdG8gdGhlIEdvb2dsZSBHcm91cHMNCj4iSG9tb3Rv cHkgVHlwZSBUaGVvcnkiIGdyb3VwLg0KPlRvIHVuc3Vic2NyaWJlIGZyb20gdGhpcyBncm91cCBh bmQgc3RvcCByZWNlaXZpbmcgZW1haWxzIGZyb20gaXQsIHNlbmQgYW4NCj5lbWFpbCB0byBIb21v dG9weVR5cGVUaGUuLi5AZ29vZ2xlZ3JvdXBzLmNvbS4NCj5Gb3IgbW9yZSBvcHRpb25zLCB2aXNp dCBodHRwczovL2dyb3Vwcy5nb29nbGUuY29tL2Qvb3B0b3V0Lg0KDQoKCgoKVGhpcyBtZXNzYWdl IGFuZCBhbnkgYXR0YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2Vl CmFuZCBtYXkgY29udGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJl Y2VpdmVkIHRoaXMKbWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIHNlbmQgaXQgYmFjayB0byBtZSwg YW5kIGltbWVkaWF0ZWx5IGRlbGV0ZSBpdC4gCgpQbGVhc2UgZG8gbm90IHVzZSwgY29weSBvciBk aXNjbG9zZSB0aGUgaW5mb3JtYXRpb24gY29udGFpbmVkIGluIHRoaXMKbWVzc2FnZSBvciBpbiBh bnkgYXR0YWNobWVudC4gIEFueSB2aWV3cyBvciBvcGluaW9ucyBleHByZXNzZWQgYnkgdGhlCmF1 dGhvciBvZiB0aGlzIGVtYWlsIGRvIG5vdCBuZWNlc3NhcmlseSByZWZsZWN0IHRoZSB2aWV3cyBv ZiB0aGUKVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtLgoKVGhpcyBtZXNzYWdlIGhhcyBiZWVuIGNo ZWNrZWQgZm9yIHZpcnVzZXMgYnV0IHRoZSBjb250ZW50cyBvZiBhbgphdHRhY2htZW50IG1heSBz dGlsbCBjb250YWluIHNvZnR3YXJlIHZpcnVzZXMgd2hpY2ggY291bGQgZGFtYWdlIHlvdXIKY29t cHV0ZXIgc3lzdGVtLCB5b3UgYXJlIGFkdmlzZWQgdG8gcGVyZm9ybSB5b3VyIG93biBjaGVja3Mu IEVtYWlsCmNvbW11bmljYXRpb25zIHdpdGggdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbSBt YXkgYmUgbW9uaXRvcmVkIGFzCnBlcm1pdHRlZCBieSBVSyBsZWdpc2xhdGlvbi4KCg==