From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:af0e:: with SMTP id y14-v6mr165021wme.14.1527682124906; Wed, 30 May 2018 05:08:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:a00a:: with SMTP id j10-v6ls6552821wme.6.gmail; Wed, 30 May 2018 05:08:44 -0700 (PDT) X-Received: by 2002:a1c:f214:: with SMTP id s20-v6mr169181wmc.25.1527682124005; Wed, 30 May 2018 05:08:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527682123; cv=none; d=google.com; s=arc-20160816; b=p4WU3N6tYwNaJ2sFbGY13jBnqHRipwYImePHSOLwQ5GMhi43d81B/AvPvAO8+udLYf uDwMNFr2F6Q2vUgr+ZFbGXFKqkpeEU1Vx2nTjDr6Yl8P5IzSNS0kMQHjhDATvjMyintQ 7/2Fos6/LZbY0cUZko0uGRQFrDx6fxWO2+3c+ohm/hZQKeZnPXmScLWTpsXUXuDdjoe8 57DcjbMy7/OwxF6plOYvvybQZXi0BGM/a1Z6Oh9GCU7FLWIPN9eyG2Qju5hmtpybYoKt 4B5ftdmBcbuWWxC3iySIMJ4hRWMBhBda8fV7ha85hD2hsYvISxnnxd3eDnYLOuHvf+WA hUkw== 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=m0v/BOpsHfUdDeKvwR06zXJ1HzSkt33M1Vcz+Mj717w=; b=kYwnNGB/Y3F9p5wgbAc4DaEP8sFtNl7wRk18oE7xcaJUN6RCNDmmsw4NxV98reOfKF Kfr+xc6MJmejIF4rgKchCiE3LaWaM5HipXFSNG3y1vpsjQtKqMVVqiYFskYT+T0//DmU z1MQ4n3/E9bKvX9BLm3iLYNgofuYQFascC+jr4aPuX3kLiveDKp5frheSwuKZhtj500F uk8Bdi8nHbprlRPPIWNbjyDKxNRFurC8CbRohqig7tr77eE7m1d8DmXtBQxdY12vcred mw6DNDCLa/eznQ/gn/QcGsulvyimRNNfR8RGsJTsasW5KHWZXvaGABTn21VKQBENsSLe Pr+Q== 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 x3-v6si260090wrn.0.2018.05.30.05.08.43 for ; Wed, 30 May 2018 05:08:43 -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 8512A3EBFE7_B0E944BB for ; Wed, 30 May 2018 12:08:43 +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 E9D093DC6B7_B0E944AF for ; Wed, 30 May 2018 12:08:42 +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 1fNzuC-0004PS-TH; Wed, 30 May 2018 13:08:42 +0100 Received: from EUR01-HE1-obe.outbound.protection.outlook.com (213.199.154.210) by mail.nottingham.ac.uk (128.243.15.146) with Microsoft SMTP Server (TLS) id 14.3.389.1; Wed, 30 May 2018 13:08:39 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB3005.eurprd06.prod.outlook.com (10.170.229.144) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.20.797.11; Wed, 30 May 2018 12:08:38 +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 12:08:38 +0000 From: Thorsten Altenkirch To: Thomas Streicher CC: Michael Shulman , "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///5P4CAADDuAA== Date: Wed, 30 May 2018 12:08:37 +0000 Message-ID: References: <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk> <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk> <20180530101041.GA30885@mathematik.tu-darmstadt.de> In-Reply-To: <20180530101041.GA30885@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;VI1PR06MB3005;7:sve4gSAZITXCiN8h9qzIkmwnszD3vthn+4xSBhXI6DvkZBH2/yD6n75Rpdl0CTT1cHrjCmUTdefAcUk1X4mZzKSeTuR0KTfRPDCXMV8Lav4CMc0pV6Xqq4Zs2ATewIB335mWpLDBv/Ukr0d1CP7N0o3ruIMQInJi03gR02zNEgucQkpSG2sGCpK2CdKuRYcmfpGK8hxOknhNkuy4WPJ3r/SwkecNduNlktYc/i3oJMZu0+PnaXAhLw215EY7Gu6U 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:VI1PR06MB3005; x-ms-traffictypediagnostic: VI1PR06MB3005: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:; x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(6040522)(2401047)(5005006)(8121501046)(3231254)(944501410)(52105095)(93006095)(93001095)(10201501046)(3002001)(149027)(150027)(6041310)(20161123558120)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(201703061406153)(20161123562045)(20161123564045)(20161123560045)(6072148)(201708071742011)(7699016);SRVR:VI1PR06MB3005;BCL:0;PCL:0;RULEID:;SRVR:VI1PR06MB3005; x-forefront-prvs: 0688BF9B46 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(39860400002)(39380400002)(346002)(376002)(366004)(189003)(199004)(86362001)(6246003)(2906002)(58126008)(83716003)(97736004)(316002)(26005)(6916009)(54906003)(305945005)(786003)(229853002)(102836004)(99286004)(8936002)(4326008)(74482002)(81156014)(76176011)(81166006)(93886005)(25786009)(186003)(8676002)(2900100001)(106356001)(6436002)(3280700002)(6506007)(3846002)(478600001)(6512007)(68736007)(14454004)(6486002)(82746002)(5660300001)(105586002)(6116002)(558084003)(7736002)(446003)(53936002)(11346002)(66066001)(476003)(486006)(33656002)(5250100002)(2616005)(3660700001)(42522002)(42262002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB3005;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: EitvOIL26lT06IzKyAl5o+U8NLEfxq3MBaIrpa3qWXjfmHl5twJmJYojWN51GygXwEtWVTegROcD+WTSHMYLmFxF3gXOKeeIVIGB2d5ZhwEKx2tlN58wXx443rQTJNIIEHoJ3hJU2zcsypFI7rRGg49lbY7I4MvXNu4HtceLZuic7iywCGBKUjgwgQT+YxTX 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: e9dce16d-1e20-4b86-7f45-08d5c6261376 X-MS-Exchange-CrossTenant-Network-Message-Id: e9dce16d-1e20-4b86-7f45-08d5c6261376 X-MS-Exchange-CrossTenant-originalarrivaltime: 30 May 2018 12:08:37.8976 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB3005 X-OriginatorOrg: exmail.nottingham.ac.uk X-Spam-Score: 0.0 (/) X-SASI-RCODE: 200 TmFtZXMgYXJlIHN5bnRhY3RpYyBzdWdhci4gDQoNCkluIHRoZSBpbnRyaW5zaWMgc3ludGF4IGlu ZSB1c2VzIGEgZm9ybSBvZiB0eXBlZCBkZSBCcnVpam4uIFRvIHJlbGF0ZSB0aGVtIHRvIG5hbWUg Y2Fycnlpbmcgc3ludGF4IGlzIHN0cmFpZ2h0IGZvcndhcmQuDQoNCu+7v09uIDMwLzA1LzIwMTgs IDExOjExLCAiVGhvbWFzIFN0cmVpY2hlciIgPHN0cmUuLi5AbWF0aGVtYXRpay50dS1kYXJtc3Rh ZHQuZGU+IHdyb3RlOg0KDQogICAgQnV0IHRoYXQncyBub3QgdGhlIGlzc3VlIGhlcmUuIEl0cyBy YXRoZXIgc3ludGF4IHdpdGggdmFyaWFibGVzIGFzDQogICAgb3Bwb3NlZCB0byBzeW50YXggd2l0 aCBjb21iaW5hdG9ycy4NCiAgICANCiAgICANCg0KCgoKVGhpcyBtZXNzYWdlIGFuZCBhbnkgYXR0 YWNobWVudCBhcmUgaW50ZW5kZWQgc29sZWx5IGZvciB0aGUgYWRkcmVzc2VlCmFuZCBtYXkgY29u dGFpbiBjb25maWRlbnRpYWwgaW5mb3JtYXRpb24uIElmIHlvdSBoYXZlIHJlY2VpdmVkIHRoaXMK bWVzc2FnZSBpbiBlcnJvciwgcGxlYXNlIGNvbnRhY3QgdGhlIHNlbmRlciBhbmQgZGVsZXRlIHRo ZSBlbWFpbCBhbmQKYXR0YWNobWVudC4gCgpBbnkgdmlld3Mgb3Igb3BpbmlvbnMgZXhwcmVzc2Vk IGJ5IHRoZSBhdXRob3Igb2YgdGhpcyBlbWFpbCBkbyBub3QKbmVjZXNzYXJpbHkgcmVmbGVjdCB0 aGUgdmlld3Mgb2YgdGhlIFVuaXZlcnNpdHkgb2YgTm90dGluZ2hhbS4gRW1haWwKY29tbXVuaWNh dGlvbnMgd2l0aCB0aGUgVW5pdmVyc2l0eSBvZiBOb3R0aW5naGFtIG1heSBiZSBtb25pdG9yZWQg CndoZXJlIHBlcm1pdHRlZCBieSBsYXcuCgoKCgo=