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-qk1-x739.google.com (mail-qk1-x739.google.com [IPv6:2607:f8b0:4864:20::739]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1c485b73 for ; Mon, 20 May 2019 19:59:50 +0000 (UTC) Received: by mail-qk1-x739.google.com with SMTP id x68sf1831791qka.6 for ; Mon, 20 May 2019 12:59:49 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558382389; cv=pass; d=google.com; s=arc-20160816; b=Xa/BUgBSocJnVRP/YhYFusoVITiyQeMF2pFEXM+cWSUv3ZqJ5xsvLkn7n3g5xgKJjX 4Qsl9kGckIo+aPxWPQF+fGEdgy+TSjQnxKGeenniU45Fv1j3SD6dEUERmsFhL+mV9QVw cuTg8FIn8N6LMtW2sRZVuBsA14C0wK9zPWuSmc9TjCHuyn80Fcrx4Rux3d84yRQDCizO SH3JSgco0ByP6Lo60sq5AWRdzljpcCz7YyieMY8voHqEqg1rntQTEBTWciJPdWiOsyuY DDzsdQd/RMhjUuLpMpDrFv19XNTHKqx07t52NJdz+SNN7n6ShkgtJOwvYakhUs0UBpo7 YxwQ== 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=SriRXSmoPa4yeg6iA1Aw59WsoCbwJ/8R7zkBvKRlkwE=; b=dMTfwuTGSosrrvFrODYU1L5bepyQufgI79fJtKkUHoAKtMLsOQyCI7gq1JFR855Rjt GJydsuw3NYyehly1+6g9jDu2xA1ZA7Ei1uR6V4M/x6nrL8WEVK6FKGtpXLvfrVjL60yr L4ypWgKxnekK6yE84bM6glOqGDnu+1qLOHwIG3SibR5vK8gQabPrQlML8bTTno5ttaBb whh/x6qmJo8ZsXT5dV3gbiGUGELC5OmHBu/esBd/PZWSAkbfu34qEU4dVIhmrawQz5Oa ox5E+x4q7+IsRwlAhbGh3DPsuPlA6sZ1+ygaHcByEqFl8pPH/4wYKge2kLSSc3ui2opW nB+Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=5aRHgGeG; spf=neutral (google.com: 66.111.4.27 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=SriRXSmoPa4yeg6iA1Aw59WsoCbwJ/8R7zkBvKRlkwE=; b=Yml7fkffwXRyyyMn9GdM86N5kYWCbxBBd5D7MuxoNG7lEYHhLWZLOw/GUeVPOE7LUb lmpXNVhN9g367kUJ5BVRURc6o8ao2XIvYYYHVQPMBsAQAVswVyYGFQiU/xs2mgnV7DsY zpCrRsGZPsrcXsVl45jIwHaKmgzMmjrCpwGYVFTUyQJkiSo+DBL0HS/uVXRIGZY686GT 7uKkRHstsy8zNuqK8AKgnB9H+zgPkgMmWEuFoE1X1p88MVOv7HH6dIvyPtiDr1WtA/3O KJdu4vyR4cBCJwunYzlJDWw9a1dk+UYPwQwYUtYv0pdHGon/wOYVRYjrXgcejW4bXf7o NBFw== 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=SriRXSmoPa4yeg6iA1Aw59WsoCbwJ/8R7zkBvKRlkwE=; b=tdsj69ZA8FPACPtEDB0hlbQKPMPIouyzAlOhFLWFSeNytcYEos/BcES7qpIdCNcqRv fTEU7umb7DjbhGvVTLObOwV1Gen0rIAorkpV0Hcmz9rnPEeEYPXRqtb5Oe37OWbVDoYq B/+c2QrPC59pIIlxc/a74IIleC+ejwVsrz7hzqZLMGLSuKRv1IJx2wBJztZCa5uSpuuK lN/UNjZs+ZzxIB4Nlgn9mDtWtWqDbA/aWr/wvwZYegUM62s1t4c8dHsw49GhNVn9x2Zc ZQRoMRSeBSfdQOxC9Ozymp5CYf+a7CjkVxjRI1fsZ9sesaengmTYHxLUtZvHSuzDq1xY Cy5Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXvi/aY1uWd2ULwJyVb0Ul2pDOs8AdysWyXVG7i4lXt1AU9Tlin lkr6Bu9ORMMoOQ101bN1RaE= X-Google-Smtp-Source: APXvYqwHDnNejJ0H65iyy60wuBlgjW5TZl9Ge4SNUCT0EShm/yDx9UOkt4uAGGTkMIzzmpg9yRTv6Q== X-Received: by 2002:ac8:2473:: with SMTP id d48mr10289673qtd.373.1558382387878; Mon, 20 May 2019 12:59:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:8a3c:: with SMTP id 57ls3428851qvt.9.gmail; Mon, 20 May 2019 12:59:47 -0700 (PDT) X-Received: by 2002:a0c:92c2:: with SMTP id c2mr48089352qvc.145.1558382387602; Mon, 20 May 2019 12:59:47 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558382387; cv=none; d=google.com; s=arc-20160816; b=E9qFJmrOvLgXcfnALeSjshCorxvXPJ966psRTjb7qpQmILe0prB0odGoKMsTYw2qxU raJMxsJ2LD5BQjJ7uqG0Mouxe/AHko32wgbwvPmAOE38gKm0e/MpCvAGTSpzPthyj3q5 XbBNv21/WXrLV9na6QRNiGsAoKdk0B/gTlH+sl1Yf2hFgm4LlUctuj9o+AONxM4+/VXY fJ/ysY3+9KI1aLc4+GXR2v5o9bHdjiNObS0CIb4gFV9ahDTkwI1r5e4mTHDiOsxSK8MC 3f7ORDW1/pwj/7twzjC6ythcrddGIvc2qBqBGqmkbecicRGkKU8aR2nuGnyT2J0F9VSo V0uQ== 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=wO2tJV5r0FS78lHp7Zn+bsHc9e4gdtg7xLOFPg2j7OA=; b=nLtuHpEzWMidMjiSv+0pNwMPvdRwPs1lA6ai0mi+SlS5TlApOjkJ6WIWVwiPFA4M6h 2WljdnHLCNAhde/nNJHsjjFgJ1rRUoUDO17PbAfm6AKxS8LIHpwm6H7MBDYqVIWpLT6c 5Fzjg2aVWr+BZNaIKtwpXdViSW4MItOoqgsXJKXN82EWLicEXA4PHK0mdUzttmosueFc Fj6vI/jt+tERFzxunMcTWRElVxacZ1qkQvdpFYgJy1atGWB1f6scscgwJMFiKb6vrIfE GmXqkj2MWA6NIYToamGMlpoRlhHziHVwaR7rW0uC3DNVf54HkkLB5NT4iDj3AF+g1yrr ZBpQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=5aRHgGeG; spf=neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out3-smtp.messagingengine.com (out3-smtp.messagingengine.com. [66.111.4.27]) by gmr-mx.google.com with ESMTPS id 45si1230650qtq.4.2019.05.20.12.59.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 12:59:47 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.27 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.27; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 2A334228BA for ; Mon, 20 May 2019 15:59:47 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Mon, 20 May 2019 15:59:47 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgeduuddruddtkedgudegjecutefuodetggdotefrod ftvfcurfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfgh necuuegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmd enogfuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefofgggkfgjfhffhffv ufgtgfesthhqredtreerjeenucfhrhhomhepfdflohhnucfuthgvrhhlihhnghdfuceojh honhesjhhonhhmshhtvghrlhhinhhgrdgtohhmqeenucffohhmrghinheprghrgihivhdr ohhrghdpghhoohhglhgvrdgtohhmnecurfgrrhgrmhepmhgrihhlfhhrohhmpehjohhnse hjohhnmhhsthgvrhhlihhnghdrtghomhenucevlhhushhtvghrufhiiigvpedt X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id DC3443109B; Mon, 20 May 2019 15:59:46 -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: In-Reply-To: References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> Date: Mon, 20 May 2019 15:59:46 -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=5aRHgGeG; spf=neutral (google.com: 66.111.4.27 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: , Hi Thorsten, 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" because se= ts are a special case of setoids which are a special case of groupoids whic= h are a special case of infinity groupoids, but what people are wondering i= s probably more along the lines of whether there is a model of type theory = in which the universes are both univalent and closed under general QIITs. A= nd as Bas notes, non-finitary QIITs are not just a special case of somethin= g well-known like generalized algebraic theories or something like that, so= there are some really deep questions involved. This is not a bad thing: it means there are some very interesting questions= left to figure out, maybe suitable for an ambitious phd student :) Best, Jon On Mon, May 20, 2019, at 2:36 PM, Thorsten Altenkirch wrote: > The setoid model is just a restriction of the groupoid model where all=20 > 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 wrote= : > >=20 > > As you say, Mike and Peter note that: > > "the idea is that higher inductive types can be used to construct free > > 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 homotopical > > 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 pr= inciple? > >>=20 > >> Mike and Peter show that there are QITs which aren't constructible fro= m quotients. However, we may still be able to justify a type theory with QI= Ts without using them. E.g. in the Setoid model we can construct many QITs = including the Reals (I think) but this is maybe because choice is provable = for the setoids which are obtained from sets (like Nat). But what about a Q= IT 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 models= . > >>=20 > >>=20 > >>=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 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/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.notti= ngham.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 >=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/FBCD91A3-4A6F-456E-9= 3FA-E36EFB56D607%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/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.com. For more options, visit https://groups.google.com/d/optout.