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-yw1-xc3d.google.com (mail-yw1-xc3d.google.com [IPv6:2607:f8b0:4864:20::c3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b1cff519 for ; Mon, 20 May 2019 23:26:12 +0000 (UTC) Received: by mail-yw1-xc3d.google.com with SMTP id i125sf16080004ywf.5 for ; Mon, 20 May 2019 16:26:12 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558394771; cv=pass; d=google.com; s=arc-20160816; b=yGhXOWQDdBtZIuAtIIbOAd872B30M+9Uwm/hkOHRcZECKfKUjaGmTgHXYottLkLnDZ VzpqjZi+Epj3Vghj505JDnDXMWdvBDV9G3MW705qu2PZj2qQ9aWBE7Vhhqf3j3fMsT2O WysPs9BcVDj4CgJ3304+CTPd1N6hQ/8M+DqNEJAuGX7eWLjq8Omv0mVgM9F26XxNpQHe p4pDP+VyLVATeCV46uckAD5hB1dENVuzzS8QIC3OKci6ZmX9igBCePwbFSnZxZm0LBUm n9gJeLh4XvMJ+RbG5CC2ts18xK9bDj+aMpG2+Tz8KryFDKhke2TV8E+Aq9gjJA+nZzaf szQA== 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:content-transfer-encoding:subject:to:from :date:references:in-reply-to:message-id:mime-version:user-agent :sender:dkim-signature; bh=3ndugrBc5/SZMt5iYNwFgkMnp8pwJlaj38w9GCn4c7M=; b=ehx4JwgeLC4XXPZGcXSj+oT9N0DG2hz/V9E57Kxrn9KOTgpwe0g15YHNhmJe7jETyF W2Zmd5gh14UT+pkqZeB7hMzs8jpRGm43FQIDfGqUiiHL4t6g9QAbykFAKA+8Ueb5PwAa GEpXPXnW8xHeX+6v1nQyyS6g+i3TL4vELfFyZLiOHNMMC7ezpfha5ya8yo+8vTNbAkda GgnLyOjRn2YLeE0PMhHbHAHxDrbAmfZoGaxBHVtQXZHD/XNSxDq7mDTvHEatoKkSnkn8 6lFkMfueQnRwEgyv292wqHu3hcKUFH+XpsYNJwvv7xAF+yQdl2Kc8iFh/j4JNCiAzNSA lYig== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=ge80joUY; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:user-agent:mime-version:message-id:in-reply-to:references :date:from:to:subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=3ndugrBc5/SZMt5iYNwFgkMnp8pwJlaj38w9GCn4c7M=; b=tlDfwO+fb4Vx0cqYBy1E5kfezZGmvxwtclnfjVclgiwtBgPiVLqlMKsg3QbBvvFEni F9xZlI/OcDHK0xyywGwtRdHk8hUwgxTnvQtGP1H+JvElan0AQgEo+nfwUi+q/qXJH+d9 LJXqIHyNGHocLm1BQnDDgpbfmTTAsurPkrLHCG7Wc7mVUgyOEPXYEcs4FHu+6Cf20Ny0 A9MprLi7nY69ELv340mZw8i21VltHfMQo89yrylxiuBf4YZPePVF9sH0Kxlw1+7c60YE ioya4qrG5UfQeAo12mZPmc1OsAZlbcbUQr1PuTFgwzWyEM8v4shCWSF6ZXIbDB4EhDWP Yg/Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:user-agent:mime-version:message-id :in-reply-to:references:date:from:to:subject :content-transfer-encoding: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=3ndugrBc5/SZMt5iYNwFgkMnp8pwJlaj38w9GCn4c7M=; b=JXuAbIUhC2vqHW/cSdSu0cRLbIbrEnHBPmN8mzFMsrYnIXzkTAYWd3cvE4Rgkp6LQt dabqOefX4lMGI7UM9yv8kyuGKxN0kreLybUfdcja2/aom8mIYgP+lMOtnV+QFSthMlUM O+zysMWruKfMpucENbaibNo4ZHl0fSYwtljY1ujIc52r6cmUnYsDxxlTgJxKjSbT5XTV 4Kgp8lT4KMM2qocieY9heAMesQ/YHv9EI9zDkOPTJ7LGXXXMmEA+kjZQ8vJeY+e4eiYk h8BrbZov/fIz1Gh2R5oMPcpWQ+wxnMoHPuGLSvYd8LlxVCT9ikEtsRgK/TCPx3baTcCF DWCg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWdgPlS5H38rR46OEZX7vLEsdYPe9U5xUigIvIQY0OLuYc+vGd3 aClDJAZf7xothVt2H4xxR2I= X-Google-Smtp-Source: APXvYqwbD8Q/yvrsstAkTmw6zMHsYkYhPg31VrFNsqcu6TrQ0tH94JPfXRm23mxIEJL3l3PTEpPhiQ== X-Received: by 2002:a81:343:: with SMTP id 64mr20828045ywd.419.1558394771492; Mon, 20 May 2019 16:26:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:ed7:: with SMTP id 206ls478466ybo.9.gmail; Mon, 20 May 2019 16:26:11 -0700 (PDT) X-Received: by 2002:a25:ad60:: with SMTP id l32mr10843991ybe.461.1558394771081; Mon, 20 May 2019 16:26:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558394771; cv=none; d=google.com; s=arc-20160816; b=CUhXktAze6RJftlU7JJaYNIMN9sMQ++8c9bugsbuvhsOvmK9lBCNRLdEe0u8TdBmWt 7ef+hPLSRs9HUIQilbV+shsNgPHV+kJywM61L9Z6uIHRZYlki4F8OpqkxPIxK6T88RFo ywnP3MUqhV6foQdLcQnC8aF8DIfwxr1TiAsqlfcOlvxD5yQMY4OPuK+NXRLumX6pR4ge 4KEhZMbv92JyHp/EYPthCZ/HBWccj1y2QgtkmM9uQyiA9SosXfUkrZRf0wn9YsVkqXUV Ry5M+LLvegdINH0V06FuXlobxMtNHvmjwSmB0mAQ6PTNBSyA6zj9Zlw2G9VUYb2sV+6M rclQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:to:from:date:references :in-reply-to:message-id:mime-version:user-agent:dkim-signature; bh=s6CLxlVfQvsKJD472/Slqf3Nb6JyuVK6+BbGwynFLaE=; b=0bQrEzULCQ+Zygo/HmncXkD6BBUbdrvycSAm6TBiuRstt5lgQ9yHGxGRcB8EPt4/es 4r7wVXS7/+F2EEvLIOUbe2rxZveMS5lbxGObRvEA++qbfcv6uWV1HPAf1F+5dOM/qoNQ c/UdmhwgLzTzU1KLJfzkK7rCIfs0LK+EQyeu3EwYMgZAh6EgHJeZ/CdKUlQyoeL+De6u zIHKhoviWXegbFjaYq4BfaIMjjY21nVv/JldSPiXp2CxNjMA4dZLSkObdd5/ju5GRoqv IKUP4TUHEC9fCAkwU65ptEnjYG2nyYwaeLPW/XmJqNpAAbooJiHVI9eeXQuDfkDO5ZSn OzOA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=ge80joUY; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id s21si1479578ywg.0.2019.05.20.16.26.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 16:26:11 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.26; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 8A1352444D for ; Mon, 20 May 2019 19:26:10 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Mon, 20 May 2019 19:26:10 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduuddruddtledgvddvucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne goufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepofgfggfkjghffffhvffu tgfgsehtqhertderreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjoh hnsehjohhnmhhsthgvrhhlihhnghdrtghomheqnecuffhomhgrihhnpegrrhigihhvrdho rhhgpdhgohhoghhlvgdrtghomhenucfrrghrrghmpehmrghilhhfrhhomhepjhhonhesjh honhhmshhtvghrlhhinhhgrdgtohhmnecuvehluhhsthgvrhfuihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id E5FC930616; Mon, 20 May 2019 19:26:09 -0400 (EDT) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.6-549-ge400f56-fmstable-20190516v3 Mime-Version: 1.0 Message-Id: <96fea5d2-535c-43fc-9832-48ce96e916ca@www.fastmail.com> In-Reply-To: <4CAE313E-7B00-41D3-A13A-3AAC0A496AB0@exmail.nottingham.ac.uk> References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> <4CAE313E-7B00-41D3-A13A-3AAC0A496AB0@exmail.nottingham.ac.uk> Date: Mon, 20 May 2019 19:26:09 -0400 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Semantics of QIITs ? Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=ge80joUY; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com 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: , Dear Thorsten, As Andras noted in his message to this thread, it is very much an open ques= tion whether QIITs can be modeled without using UIP (this is part of what p= eople are trying to distinguish from, when they are asking about "homotopic= al" models); therefore, "interpreting them in cubical sets using the gener= al construction of HITs" is definitely not a slam-dunk, and novel + worthwh= ile research will be needed to determine if it works. Echoing Andras, I recall that a new encoding due to Jasper Hugunin enable u= s to interpret IITs without using UIP, and it is an open question to determ= ine whether Jasper's ideas can be extended to QIITs. I hope they can, and s= omeone should find out :) Best, Jon On Mon, May 20, 2019, at 6:17 PM, Thorsten Altenkirch wrote: > What exactly do you mean by =E2=80=9Ca model=E2=80=9D? I=E2=80=99d think = we can interpret them=20 > in cubical sets using the general construction of HITs. They don=E2=80=99= t seem=20 > to cause problems in cubical Agda as far as I can see. >=20 > Sent from my iPhone >=20 > > On 20 May 2019, at 22:04, Bas Spitters wrote= : > >=20 > > Do we even have a model that would capture all the QIIT constructions > > in the HoTT book? > >=20 > > I recall an argument where one constructs the Cauchy numbers as a QIIT > > *within* the Dedekind numbers (assuming impredicativity) and then show > > that this indeed has the right initiality property. However, I don't > > recall whether anyone ever worked out the details of this, or how > > general this method is. > >=20 > >> On Mon, May 20, 2019 at 9:59 PM Jon Sterling wr= ote: > >>=20 > >> Hi Thorsten, > >>=20 > >> I think that in the way I interpreted Bas's question, setoids probably= don't count --- by that token, even sets would also be "homotopical" becau= se sets are a special case of setoids which are a special case of groupoids= which are a special case of infinity groupoids, but what people are wonder= ing is probably more along the lines of whether there is a model of type th= eory in which the universes are both univalent and closed under general QII= Ts. And as Bas notes, non-finitary QIITs are not just a special case of som= ething well-known like generalized algebraic theories or something like tha= t, so there are some really deep questions involved. > >>=20 > >> This is not a bad thing: it means there are some very interesting ques= tions left to figure out, maybe suitable for an ambitious phd student :) > >>=20 > >> Best, > >> Jon > >>=20 > >>=20 > >>=20 > >>=20 > >>> On Mon, May 20, 2019, at 2:36 PM, Thorsten Altenkirch wrote: > >>> The setoid model is just a restriction of the groupoid model where al= l > >>> the Homs are propositional - does this not count as homotopical? > >>>=20 > >>>=20 > >>>=20 > >>> Sent from my iPhone > >>>=20 > >>>> On 20 May 2019, at 18:55, Bas Spitters wr= ote: > >>>>=20 > >>>> As you say, Mike and Peter note that: > >>>> "the idea is that higher inductive types can be used to construct fr= ee > >>>> algebras for infinitary algebraic theories. However, Blass showed > >>>> (modulo a large > >>>> cardinal assumption) that these cannot be constructed in ZF [Bla83].= " > >>>> In fact, they construct an uncountable regular cardinal explicitly (= Thm 9.1). > >>>> https://arxiv.org/abs/1705.07088 > >>>> So, QITs do add extra expresivity. > >>>>=20 > >>>>=20 > >>>> My question is about "small" QIITs (Cauchy reals, ...) in homotopica= l > >>>> models, so the setoid model does not really count. > >>>> However, has it been proved even in that case that such QIITs exist? > >>>>=20 > >>>> On Mon, May 20, 2019 at 6:17 PM Thorsten Altenkirch > >>>> wrote: > >>>>>=20 > >>>>> Do we know wether the existence of QI(I)Ts isn't a new constructive= principle? > >>>>>=20 > >>>>> Mike and Peter show that there are QITs which aren't constructible = from quotients. However, we may still be able to justify a type theory with= QITs without using them. E.g. in the Setoid model we can construct many QI= Ts including the Reals (I think) but this is maybe because choice is provab= le for the setoids which are obtained from sets (like Nat). But what about = a QIT which uses a setoid for which we don't have choice? > >>>>>=20 > >>>>> Thorsten > >>>>>=20 > >>>>>=20 > >>>>> =EF=BB=BFOn 16/05/2019, 19:50, "Bas Spitters" wrote: > >>>>>=20 > >>>>> Thanks for confirming that this is still open in homotopical mode= ls. > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>> This message and any attachment are intended solely for the address= ee > >>>>> and may contain confidential information. If you have received this > >>>>> message in error, please contact the sender and delete the email an= d > >>>>> attachment. > >>>>>=20 > >>>>> Any views or opinions expressed by the author of this email do not > >>>>> necessarily reflect the views of the University of Nottingham. Emai= l > >>>>> communications with the University of Nottingham may be monitored > >>>>> where permitted by law. > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>>=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, s= end an email 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.no= ttingham.ac.uk. > >>>>> For more options, visit https://groups.google.com/d/optout. > >>>=20 > >>>=20 > >>>=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 > >>> where permitted by law. > >>>=20 > >>>=20 > >>>=20 > >>>=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, sen= d > >>> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >>> To view this discussion on the web visit > >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/FBCD91A3-4A6F-45= 6E-93FA-E36EFB56D607%40exmail.nottingham.ac.uk. > >>> For more options, visit https://groups.google.com/d/optout. > >>>=20 > >>=20 > >> -- > >> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> To view this discussion on the web visit https://groups.google.com/d/m= sgid/HomotopyTypeTheory/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail= .com. > >> For more options, visit https://groups.google.com/d/optout. > >=20 > > --=20 > > You received this message because you are subscribed to the Google Grou= ps "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send = an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/ms= gid/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%= 40mail.gmail.com. > > For more options, visit https://groups.google.com/d/optout. >=20 >=20 >=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 >=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 >=20 >=20 >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send=20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/4CAE313E-7B00-41D3-A= 13A-3AAC0A496AB0%40exmail.nottingham.ac.uk. > For more options, visit https://groups.google.com/d/optout. > --=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/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.com. For more options, visit https://groups.google.com/d/optout.