From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53f.google.com (mail-ed1-x53f.google.com [IPv6:2a00:1450:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c1dc6d7f for ; Mon, 20 May 2019 16:16:59 +0000 (UTC) Received: by mail-ed1-x53f.google.com with SMTP id e21sf25950239edr.18 for ; Mon, 20 May 2019 09:16:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558369019; cv=pass; d=google.com; s=arc-20160816; b=IUtoRLFDyJlfsGv6Qspx6QMG2U8/rwK9qEZTfkwyywPAsClJ5nXNHLaX5ZkBlC2Wjl /Q7i9SLF+3cjLsR8ZiInV6JeCEjXaXbLSgyJ8+xJ13RPb3acjDqkzbHxJnHQGuCIj5Y7 evK1d4R4CX2JK9icjw8kHfD/fCnYmxPMLqu4OictyJ4HHlyM2r9O5VE+nRGIIKljcnwC B1GWPhxIwXCdruxUX2L2cTkopB3QkcbZePQASWslHldo5+95TM7/EDriwE0gjxZS7Bqp DdnhhE7/xE+UTFNago8RVeaNMvyquB4dPdpVZlOsJXSiTDA/TNQt5y+m04498YjSJxcn EH1A== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:mime-version:content-transfer-encoding :content-id:user-agent:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:sender:dkim-signature; bh=mOb1KqFdCkkAWIbyUr6Lg3KAcg2a2Zfq4bMKtlCOX+s=; b=kWfCCu1dwWPM19jKGB8ZJ+GSAXvNqZi0gXxeNvJWedwdKUqXMQVvINvI9IX8fond2y DhdOl5/uqn6PWvpzLtSw7YP408NIRPcsS8WFTpHkfd+ZWtpjtCAqhYXSqslXdzbdzeSf uVcNZ3OFT6lOrtjamrhXJrWJFBTel4xoMDZSwBFjlEF3huSasI67NJo2be7Bk/6MSU0O 5qBzeMwBy20Zzmhle9ROa+BNnofuNm3QeFn9YMGuJ5CQBOp5nUnocYp9jol+tpHNG1iI hFLgXYWW5bSVibt0CeiVERYRUHE+yu7B2dBWwTscjwRyKr00eyHcOQocutOtTyH4Y23k oxZw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id:content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=mOb1KqFdCkkAWIbyUr6Lg3KAcg2a2Zfq4bMKtlCOX+s=; b=EA9LGlYfLEkv3rFi9g8th3j6UbfOMYkveRS9D+Hc8sCo7tBA5/33PiVJE0gNfuXYc+ urwpp7q8gBM5Bu2GO5p9dLZn+sztVP0OdLi+BkF9R6CqeRIfEZITQRwldaWkN6Jzlbgg K3yAc9chEOo9JbioVCGA6Df5Jlz85w13qUpnVPlXbo4FG6yGSDuURl5i2moR3aFrD0he dBWP0FppsNgoq8sHUKuJh5aFtVJ4dUqtGVKK0337XJXyZqdPUbnQKj8nV//OCFhuge01 UmtfmVP2vijbTFWNuL8B0ZaSt0PDJn+N+63f4rDJxqPejAGR5Koys9b3hZ31onZ/R9j/ YkqQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id:content-transfer-encoding :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=mOb1KqFdCkkAWIbyUr6Lg3KAcg2a2Zfq4bMKtlCOX+s=; b=JxaSxS1N3sDE16REetiSI2GWhH6yy1LTN9O0vfdt4vZ1hQk/sDgarPDN2LfAiywKPi QNg2QlUFyzm/n2mqhppDfJOHimNT+kQhDlDw9R7r/Hh6InVcPuJX0sAJ6MChwXf1pR99 06S0xWHPZ8CTbR4P6Ty1UgAVzJo3kdd8cITBGrs4qSExlqlXrsodtVADDxF6A8aAI7m8 FCUsveGInfuzoSaPuzzEqzIEU/vIRfN4T8OejBoMh/lQh/TeU7rULvdxGkX6WhLorL/+ fGGrSrFmzGS3wcSFEGbhiKASyfvTBOTg9vvw88TsDEaBDWlNBVcLcWQcOkSg/Ju86fwR E/HQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVmqMbkkMPI1RbRucqrQ9It9XyqKAvyjkuGlgLQl7B8Z0M/GwJY aqZLHUOUICedDky9jwMGOoU= X-Google-Smtp-Source: APXvYqzVIxTYmiWb6iBMLe4+WF95ZL80OblKgEu4XzI+xZTBrevKKvhv3vAQeJpgXejLdVfRANGF8A== X-Received: by 2002:a50:95ed:: with SMTP id x42mr76657528eda.103.1558369018876; Mon, 20 May 2019 09:16:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:ba2d:: with SMTP id g42ls5147330edc.0.gmail; Mon, 20 May 2019 09:16:58 -0700 (PDT) X-Received: by 2002:a50:8965:: with SMTP id f34mr75943236edf.296.1558369018360; Mon, 20 May 2019 09:16:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558369018; cv=none; d=google.com; s=arc-20160816; b=Pcy6I+aFJoMMKkwZ40YSav/ecAr1cn9wmaz0DJOr++iDUS+IPOIRxwoBdg3EKTzik7 953ebvu/1Uul3Z/MMFNPYwC84ubEGNTXAU3Qr2utuUh8O2iUM/ecbNaLh6ctgTfic4r6 bqxz+b0oI1bBkratRpPEO0IVV2hQd8piN0OQbzWcnrnybOT8e2u5FASYz1DNBnXWMKij WupBdgYdGzzV8wPgkYheuriAIuNB0rh/mM1Ya71+Qfxvx44hyWkJHetimIhu/SzoveuY 6IaJrtqFJ8ancZsZpaf1FH8otowRIPvxVFZ+mpIoU+n4iaEvheriau7im2noOzrRQ86l +Ocw== 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:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from; bh=TKQZ3FtkV3bQCuGsrE0b0WGKWu63T5ttOgyqjtcozXc=; b=Vwi92kOjFhl/c73vMX01L8r0T8Sh7X4DAItoO0UdX5akTpppVs8xJJ71iy8WYtFgU+ em75mJCZhTm3aRCPxI8q88ZM2q8uQ/Axxup6hdRcRMnQu0AlJeBdj+3jX6f2n71JJLMu FDLeO3A+ALn3a778fdanOfG8X7UghhA2JG6IOhkVGBsw6+bigV8PSXK3GoqVHZLuSiXI 4Gsdl+E7SLxtMDPIey3wc9nQ2g3/aQY1u2qwZkBnzVgw+c6OJQra5FJjXfzDdAkpSpY+ NgcXgtZ8bKAupuBmqoRpJkzt9WLhcBwe0z7drCbAIInMEJP5FYHNijb8+t7gjAfVRZYq 1Fcg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id w5si2273732edw.1.2019.05.20.09.16.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 09:16:58 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 00A8C2B7E15_CE2D2FAB for ; Mon, 20 May 2019 16:16:58 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id D11412DE808_CE2D2F9F for ; Mon, 20 May 2019 16:16:57 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hSky7-0000IP-JF; Mon, 20 May 2019 17:16:57 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 20 May 2019 17:16:55 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Mon, 20 May 2019 17:16:55 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Mon, 20 May 2019 17:16:55 +0100 Received: from EUR01-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 20 May 2019 17:16:54 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5598.eurprd06.prod.outlook.com (20.177.202.26) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1900.17; Mon, 20 May 2019 16:16:52 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5%5]) with mapi id 15.20.1900.020; Mon, 20 May 2019 16:16:52 +0000 From: Thorsten Altenkirch To: Bas Spitters , =?utf-8?B?QW5kcsOhcyBLb3bDoWNz?= CC: homotopytypetheory , Ambrus Kaposi Subject: Re: [HoTT] Semantics of QIITs ? Thread-Topic: [HoTT] Semantics of QIITs ? Thread-Index: AQHVC/fCTTpdQv6taUilYMlObALJqKZt8+sA///yOACAAAcWAIAAKzqAgAYvPAA= Date: Mon, 20 May 2019 16:16:52 +0000 Message-ID: <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.19.0.190512 x-originating-ip: [128.243.20.140] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 2db75889-5799-4280-cde0-08d6dd3e91c7 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600141)(711020)(4605104)(2017052603328)(7193020);SRVR:VI1PR06MB5598; x-ms-traffictypediagnostic: VI1PR06MB5598: x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 004395A01C x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(346002)(376002)(366004)(39860400002)(136003)(189003)(199004)(91956017)(4326008)(229853002)(446003)(11346002)(186003)(102836004)(6486002)(66446008)(64756008)(66556008)(66476007)(66946007)(73956011)(25786009)(76116006)(71200400001)(14454004)(478600001)(33656002)(82746002)(71190400001)(83716004)(68736007)(6512007)(6246003)(476003)(6436002)(2616005)(3846002)(256004)(6116002)(486006)(53936002)(2906002)(54906003)(74482002)(5660300002)(316002)(786003)(7736002)(305945005)(76176011)(86362001)(8676002)(66066001)(6506007)(81166006)(81156014)(58126008)(110136005)(26005)(4744005)(99286004)(8936002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5598;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-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: rRdQHZ0/QD8sqAKHEAFW3kZzqBqmhMgX6gQxFZg2VqmlAGaQwuOyNRTe1e0sTsawXJVH8veFBMJej0Sa32cHPMoiHqbFwQd3MaMIKbhykGjroB/4QwlxVR+YMl9c6b8zgfwTjSVyxKh30gMrney3KrxmFsSPsUCyErL2KnwCDdeXiBJOSOECmZ2h8aC/n2eoTCjFZhkVPBmbnghiNuSTgsHE8ExwsnJME2maEzWCgOHV4hPY1HxPhccGywH5SShww2UqnqhTD9vFVOmJcY538tbYwR99nttE/Nr7Ik+oKoQg0mEWpLSfeUJVhuJ/AM6JdggIaQN7wjhTmBotIRrN9RyCMmvgqYjgeLciCpTrTWeQhk6NuhO7mTlAk4/NqDCk+Z6Y3WdRh6bKNPamOqH1IOmDuWGCnFfO6LHDpvva3Es= Content-Type: text/plain; charset="UTF-8" Content-ID: <652D145CCAF94140948CEEE6DFC5AB74@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 2db75889-5799-4280-cde0-08d6dd3e91c7 X-MS-Exchange-CrossTenant-originalarrivaltime: 20 May 2019 16:16:52.1166 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5598 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Do we know wether the existence of QI(I)Ts isn't a new constructive princip= le? Mike and Peter show that there are QITs which aren't constructible from quo= tients. However, we may still be able to justify a type theory with QITs wi= thout using them. E.g. in the Setoid model we can construct many QITs inclu= ding the Reals (I think) but this is maybe because choice is provable for t= he setoids which are obtained from sets (like Nat). But what about a QIT wh= ich uses a setoid for which we don't have choice? Thorsten =EF=BB=BFOn 16/05/2019, 19:50, "Bas Spitters" wr= ote: Thanks for confirming that this is still open in homotopical models. =20 This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.nottingham= .ac.uk. For more options, visit https://groups.google.com/d/optout.