From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:a11b:: with SMTP id o27-v6mr162639wro.11.1527673061352; Wed, 30 May 2018 02:37:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:a00a:: with SMTP id j10-v6ls6466372wme.6.gmail; Wed, 30 May 2018 02:37:40 -0700 (PDT) X-Received: by 2002:a1c:f50e:: with SMTP id t14-v6mr106830wmh.27.1527673060518; Wed, 30 May 2018 02:37:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527673060; cv=none; d=google.com; s=arc-20160816; b=Gq2PHrbJVOUpmvn+qci6ancAdyYXP0wuSmQaTHN466/P8t2iqXFZfvaFQrTcdITwcg AeYAWLkyZDI2xkQOpf2FtDKmBuwIjzB3MG4uQMERBcRK0WI8E0LLOEzBexoy/2paLbLy J/JV4opxjIAMfgxXfLHzjOx1PzNh2z3ngwjp0zwHSr/XaBm+fb6mx2HBNi95YVkvdzoU uHSzOkWRoPaWbtAhtWKtaL57hj1l9nIYNM4kK2z2bRklqZ+TuS89Sn01bpOofeF2/tBp Pw16L9acgwc58GRHb6vsE86YF1FYK4EfAa+djTuhV3lHg8rE1/FFNYcSdVBavYuBtlIL IXEA== 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=WNqbMnikYlmw4M86LDIq/1UKSopGRvMqW+Ucios2IfA=; b=WoA4YMn8ZxGpHGQn0ayJo2qGN8oRq2rsmJI/G3KhFJZGzdo0EXDDp+qYWic1WdtwaF OBBrZJbs7tLwdqIpulSpPeRF8g7kEIppFI3t0lD5n/7ilaLhTRIlUtVXKRiopxlUVLF5 oTvMyG7OdL+11CMashhLFvbsfiqUomC87mS9cRsZBP79pCgnOsiYMx9/YLXLAXC2TeZd mkM1208E9Z03GK6UJdQIEHyiGg5z4wi9rHa8fojv7/kJYXKO52whiCIoDjBKHAARNRf0 no+ITrJtawhnyqc4JSONZC+U1vYqalPKpBulHA5syAAueK9hQ9Y29goxPZRF05f4eSk/ G4Yg== 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 x3-v6si244997wrn.0.2018.05.30.02.37.40 for ; Wed, 30 May 2018 02:37:40 -0700 (PDT) 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 276606D0F51_B0E70E4B for ; Wed, 30 May 2018 09:37:40 +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 D1435242826_B0E70E3F for ; Wed, 30 May 2018 09:37:39 +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 1fNxY3-0004Cd-Hn; Wed, 30 May 2018 10:37:39 +0100 Received: from EUR02-HE1-obe.outbound.protection.outlook.com (213.199.180.182) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.389.1; Wed, 30 May 2018 10:37:39 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4333.eurprd06.prod.outlook.com (20.177.57.10) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384) id 15.20.820.11; Wed, 30 May 2018 09:37:37 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::f1f5:ad90:65d9:391c]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::f1f5:ad90:65d9:391c%13]) with mapi id 15.20.0797.018; Wed, 30 May 2018 09:37:37 +0000 From: Thorsten Altenkirch To: Thomas Streicher , Michael Shulman CC: "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Re: Where is the problem with initiality? Thread-Topic: [HoTT] Re: Where is the problem with initiality? Thread-Index: AQHT9tTcHLLfpdPhZECSp3WbPXTJiqRGfjeAgABT6ICAATLCgIAAESOA Date: Wed, 30 May 2018 09:37:37 +0000 Message-ID: <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> In-Reply-To: <20180530093331.GA28365@mathematik.tu-darmstadt.de> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.a.0.180210 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;VI1PR06MB4333;7:ZZpJtqGLSOS39ZXSCetzEIOSjwg+sWmZM1B3RugTUm/uF56tkpiulwce3MsTsw4iyGtMlONoKYWDg3FTweDswojI2+Z3wYlLHr71D5ORGYT+KqCIwshtNi3l6rAXTXrVSOaNw+G6gv2jVcyhyrVXe1MAnu43JR5qYFqAH2KJ/zn4XJQgowfzfrv17MO2cIWxcG7XlJmHJZoA7gbBMMSpFa0AtrBfNEm0Mb1D5Kc5zrCDCEAiMhYMMHRPbq7AFTgh x-ms-exchange-antispam-srfa-diagnostics: SOS; x-microsoft-antispam: UriScan:;BCL:0;PCL:0;RULEID:(7020095)(4652020)(8989080)(5600026)(4534165)(4627221)(201703031133081)(201702281549075)(8990040)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB4333; x-ms-traffictypediagnostic: VI1PR06MB4333: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(788757137089); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(10201501046)(93006095)(93001095)(3231254)(944501410)(52105095)(3002001)(149027)(150027)(6041310)(20161123560045)(20161123564045)(20161123558120)(20161123562045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(6072148)(201708071742011)(7699016);SRVR:VI1PR06MB4333;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB4333; x-forefront-prvs: 0688BF9B46 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(366004)(376002)(346002)(39380400002)(39860400002)(189003)(199004)(446003)(2616005)(6436002)(11346002)(8676002)(476003)(14454004)(25786009)(5250100002)(4326008)(53936002)(6246003)(2171002)(316002)(786003)(58126008)(110136005)(97736004)(93886005)(81166006)(81156014)(6512007)(305945005)(8936002)(7736002)(33656002)(486006)(82746002)(74482002)(2906002)(3280700002)(3660700001)(5660300001)(6486002)(66066001)(478600001)(3846002)(6116002)(106356001)(105586002)(2900100001)(229853002)(83716003)(99286004)(102836004)(53546011)(26005)(68736007)(86362001)(186003)(76176011)(6506007)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4333;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-microsoft-antispam-message-info: 6YGWW18FsgozhA0RwYY8S+S4gO9UKKISz4JSjLIugkbDS4v1EVOfhmpl8aajere9rElN013pldwZJCO7UYUptkdtQL5SlIB6dcL+bvDOqretGbR5yVZh3Ghsg9MiTtaTF296qNlDCS8jKqoDRZGGyT7mivVHeGgvrU7+13nnOcpAGtdLRREIQq0adSq2kKRg spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: text/plain; charset="utf-8" Content-ID: <5ECF16F3A081F64F...@eurprd06.prod.outlook.com> Content-Transfer-Encoding: base64 MIME-Version: 1.0 X-MS-Office365-Filtering-Correlation-Id: 019c6784-fd7d-4623-c539-08d5c610fb1a X-MS-Exchange-CrossTenant-Network-Message-Id: 019c6784-fd7d-4623-c539-08d5c610fb1a X-MS-Exchange-CrossTenant-originalarrivaltime: 30 May 2018 09:37:37.6311 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB4333 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 T24gMzAvMDUvMjAxOCwgMTA6MzMsICJUaG9tYXMgU3RyZWljaGVyIiA8c3RyZS4uLkBtYXRoZW1h dGlrLnR1LWRhcm1zdGFkdC5kZT4gd3JvdGU6DQoNCiAgICBUaGF0IGNhdGVnb3JpY2FsIHN5bnRh eCBhbmQgb3JkaW5hcnkgc3ludGF4IGFyZSBpc29tb3JwaGljIGlzIGp1c3QgYQ0KICAgIHB1cmVs eSBzeW50YWN0aWMgcmVzdWx0IGFsbG93aW5nIG9uZSB0byByZXBsYWNlIGNvcnJlY3QgYWxnZWJy YWljDQogICAgc3ludGF4IGJ5IG9uZSBtb3JlIGFjY2Vzc2libGUgZm9yIHRoZSBodW1hbiBtaW5k Lg0KDQpGb3IgdGhlIGh1bWFuIG1pbmQgYWNjdXN0b21lZCB0byB0aGUgc2VwYXJhdGlvbiBvZiBj b2xsZWN0aW9ucyBhbmQgcHJlZGljYXRlcyBhcyBwcmVzZW50IGluIGNvbnZlbnRpb25hbCBNYXRo ZW1hdGljcy4NCg0KDQoNCgoKClRoaXMgbWVzc2FnZSBhbmQgYW55IGF0dGFjaG1lbnQgYXJlIGlu dGVuZGVkIHNvbGVseSBmb3IgdGhlIGFkZHJlc3NlZQphbmQgbWF5IGNvbnRhaW4gY29uZmlkZW50 aWFsIGluZm9ybWF0aW9uLiBJZiB5b3UgaGF2ZSByZWNlaXZlZCB0aGlzCm1lc3NhZ2UgaW4gZXJy b3IsIHBsZWFzZSBjb250YWN0IHRoZSBzZW5kZXIgYW5kIGRlbGV0ZSB0aGUgZW1haWwgYW5kCmF0 dGFjaG1lbnQuIAoKQW55IHZpZXdzIG9yIG9waW5pb25zIGV4cHJlc3NlZCBieSB0aGUgYXV0aG9y IG9mIHRoaXMgZW1haWwgZG8gbm90Cm5lY2Vzc2FyaWx5IHJlZmxlY3QgdGhlIHZpZXdzIG9mIHRo ZSBVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0uIEVtYWlsCmNvbW11bmljYXRpb25zIHdpdGggdGhl IFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbSBtYXkgYmUgbW9uaXRvcmVkIAp3aGVyZSBwZXJtaXR0 ZWQgYnkgbGF3LgoKCgoK