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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa40.google.com (mail-vk1-xa40.google.com [IPv6:2607:f8b0:4864:20::a40]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 024fdf85 for ; Mon, 20 May 2019 21:04:44 +0000 (UTC) Received: by mail-vk1-xa40.google.com with SMTP id s6sf7134663vke.2 for ; Mon, 20 May 2019 14:04:43 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558386283; cv=pass; d=google.com; s=arc-20160816; b=yGwkZk9cUIVxVVJK/mEnChyJ1WMU4zzhZESwcq0UVNW1rQ/DL02nTyb9lf+DjN3+EX Iix8zeTN72X+m0krp9JiPJF4cvYTxqKSkYsFIAoVeNgn++7tK6NZTpie80fj6JpSm/79 5vt8hgXkl9zn6la4XbuZy4mT7jLo5YH0CVL9zFelQA4IB6R+pDlQppmj5RiIauE8yYfb 7dZQrA58wtWTPE+OIOYp0WoWZYQN+quqy92609VCekT/UDdYdfauoyOfEJKZDexu2kiG 2h1iM0gTXCnDnwTxnU3QKtV5mGmt3jm/6OzAHKGUFkHn1XXbTBI3yLpbaMPccWiTNT0o 16yw== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=XIZEFOZv8gpArEkgu/zS69xL91CYRtGZgOlkyYbRk5Y=; b=wLffgGVqAmfPE2pRm9lMHeTxPex9mJoTRdYW4nBTEFgekbp0W2Oo2s+iNt+v7ALVz9 7KMUBf3/wuwV5OCDgKdBm7tcz071dMRBzNE1qAT07DJuQDEe67Xbc0qnei7aWufOA542 OMXkJimGa7mC9b7YYqHWvoL3DzYOqiuE/leAIEOZSTN4oTVxZg9vrz3cf3Z2UZ1eaROh 4n2QXlGlpIkyVwHmEMv/cYDNyPaQCok7VID7UIY70xedWojpJ7qcuJodouaTFGEuwOCO M6j1N5OsFEeuQ8Xk2MIBS7HCNHWbf2uzJD4OSTODMW85C6jzec8p0ddUPWLxPL5pm9BD eNaQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DMR9/H/V"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c29 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=XIZEFOZv8gpArEkgu/zS69xL91CYRtGZgOlkyYbRk5Y=; b=JeaekNq06KpEuq8/a0ENH6PrsnoEWYHrEBVn3WYDpTJw4HEHEBwXmeGAh1co56FGUh e0Ol3SPuCDCPlKrlhAsN+3hyaX9CFsvgxKqaFA6OAQo0rwrA8BN9+tFaqDIaP3KGVpYs xlQ1Z+j8tFB+YinTC3eXU7B4n8Z3Tl07Hb4ygdbOSd7Aau/ITfG7y1lAoGx3Ki17rMGb KJoeN5dOUu/iITAfFHyuoVRv6tP2TA+O29tFqUq96wVu66YQ3+c6PfLRYRgXkBUmqsB5 JauVd+sxf0pPZAqcsq+D3TsIHoyg3t2yRebXm9/OIcKpDbEmQ5YuBmqlyveit5yviXNR DExQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=XIZEFOZv8gpArEkgu/zS69xL91CYRtGZgOlkyYbRk5Y=; b=RBQKRcGklMApKAFtAK+MwmT59wE8vqOmBMZzLR8063g1IIesp6TeNZM8u9jJHlsb0t vt/ZrLTIiZBfDverYZhv9l646DHPRlFBlV1bWbVp1hWuxCFt4UAPDGYRXPG2pUuUU+7G e9ArqbfRKW3Ipw3vAGerM/H3lkCFQwCQi5mYx2SFZF/Db2M7l+IgdcGhDzV7lf0JcxIY 9iVh5YMoBQKvK0ToVUfKVQMJLqH8nA02k4c3z0K6M/aJQIzAd3qG9y08BPbTeayiTF1N FbxhvVKLZEv3lkQd7KbNmTfJljv5Ovu/xQxq7aXMWBRQ4zvG2JMloMGfZebeIR93/7Si Oi8Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=XIZEFOZv8gpArEkgu/zS69xL91CYRtGZgOlkyYbRk5Y=; b=lN3P025tAL0ESIQqtzYJnhUDCO1If8rj0CpTzFPPhqT1kdgv87QhpE39IqNzVUt0+R ApE0oMGXbyhtytruVV0+q+Y8AcTeQma0NRu0o+dc/En8fNUq7I5uK2p26LUCyDvjavEW yjcg1Ru8gIfBa73LZKPLwFjiTrs7AoW47tgKgOym6j8WkQer4GP56AmXOl2LyQ+Xbj3n yXrHorykBjc6Ie4s4F8oX5ZBCoBMsmp6adcKDGZLQM2R+yjRu61+Qk5ak8D+BOiqEQgn 0BT8e/KDbiGcELTf1cUfnlr6GF+1BB6NVIAY2UAzHaqO+BAdEQAOz2rQVB70WKlKzcYK nxnw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUrR3FlZZGHtAq9k7piWZulBseWhPydou4RRv3aMspwmFKLMy2s PHpSFWkABYjeiOwoaOmBPfI= X-Google-Smtp-Source: APXvYqw4IPs0NWjMKA4zkCBdeqBdDnkT90J/5xZU66xb+XnD0bH03CO8jkfoBuYsH8nwkl3A0VCdvA== X-Received: by 2002:a67:be18:: with SMTP id x24mr31011722vsq.66.1558386283078; Mon, 20 May 2019 14:04:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:5f95:: with SMTP id t143ls229199vkb.6.gmail; Mon, 20 May 2019 14:04:42 -0700 (PDT) X-Received: by 2002:a1f:288c:: with SMTP id o134mr10180236vko.42.1558386282724; Mon, 20 May 2019 14:04:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558386282; cv=none; d=google.com; s=arc-20160816; b=tqJvN0RIXqUMUKVitvengj+bYnXRck6Z6Dux2Aulzu6OR9P7TLDC9owRTkuwURzHcS Yx0iF8l7SqTG7bt1Fq9R8mgZvN+6ROGMLkAGfeUsZ/zhpgjmHXhuz9kP1ujbGTfCoj9H jxgKlyqt6FnSN2KRk6nG4IbCbTeOmrlpgoiD+YdOaLXgUxUtQ18S0NkOROj9lsjZdfjW ZU6CnzaHmIVRH+dIy+0VWXa9RG4o4ezZIDRoorNG1TqruZ0zqA6L+IE/LMoiU7l3fsCO 4UkXYHn62Qx/4KM4IOrrCfCildgr0ICQbTn30Sj7WnYZJP8cFckkxx/+d3TaLMkhF0gY 9evw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=p/iJoVamz7A48Nb3xun+z+4Znobz7xfyAueNPEMndlY=; b=tM5CYxOEi/FvCpv8Cty222u3rNT1pbBCbxHBHsUwWPVZC5ohmddXzr3JSb0pb+I5Em rM9ogEEDnu/DWXbHkAfzzWyvhQrg6pTPPOEfIk2i8rKTWtK7tK6yNXPUZN/oFoUf9lSy 6OV4fQrXp0AnyCbkZ0qg0XNu1m+MO3EHdcUCtJdp37anYr4gtciknhonXuBPTN+n2hGd 3xEwe6N2STpew3/n0swApcxmT7p8TUWinXOl/RWx5EUdb9w7tN5uljn3F7GOebP7JR0V yPii800ExS0SXb3tiR3ODZilyQovyabVurnUR0Uwr27AsGVGqnSlXv6m+cjN6whxlKPk KZsA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DMR9/H/V"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c29 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yw1-xc29.google.com (mail-yw1-xc29.google.com. [2607:f8b0:4864:20::c29]) by gmr-mx.google.com with ESMTPS id r5si1105696vsi.2.2019.05.20.14.04.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 14:04:42 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c29 as permitted sender) client-ip=2607:f8b0:4864:20::c29; Received: by mail-yw1-xc29.google.com with SMTP id a130so6405481ywe.13 for ; Mon, 20 May 2019 14:04:42 -0700 (PDT) X-Received: by 2002:a81:ad4:: with SMTP id 203mr33939881ywk.403.1558386282165; Mon, 20 May 2019 14:04:42 -0700 (PDT) MIME-Version: 1.0 References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> In-Reply-To: From: Bas Spitters Date: Mon, 20 May 2019 23:04:29 +0200 Message-ID: Subject: Re: [HoTT] Semantics of QIITs ? To: Jon Sterling Cc: "'Martin Escardo' via Homotopy Type Theory" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DMR9/H/V"; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c29 as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , Do we even have a model that would capture all the QIIT constructions in the HoTT book? 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. On Mon, May 20, 2019 at 9:59 PM Jon Sterling wrote: > > Hi Thorsten, > > I think that in the way I interpreted Bas's question, setoids probably do= n't count --- by that token, even sets would also be "homotopical" because = sets are a special case of setoids which are a special case of groupoids wh= ich are a special case of infinity groupoids, but what people are wondering= is probably more along the lines of whether there is a model of type theor= y in which the universes are both univalent and closed under general QIITs.= And as Bas notes, non-finitary QIITs are not just a special case of someth= ing 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 questio= ns 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 > > the Homs are propositional - does this not count as homotopical? > > > > > > > > Sent from my iPhone > > > > > On 20 May 2019, at 18:55, Bas Spitters wro= te: > > > > > > As you say, Mike and Peter note that: > > > "the idea is that higher inductive types can be used to construct fre= e > > > 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 (T= hm 9.1). > > > https://arxiv.org/abs/1705.07088 > > > So, QITs do add extra expresivity. > > > > > > > > > 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? > > > > > > On Mon, May 20, 2019 at 6:17 PM Thorsten Altenkirch > > > wrote: > > >> > > >> Do we know wether the existence of QI(I)Ts isn't a new constructive = principle? > > >> > > >> Mike and Peter show that there are QITs which aren't constructible f= rom 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 QIT= s including the Reals (I think) but this is maybe because choice is provabl= e 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? > > >> > > >> Thorsten > > >> > > >> > > >> =EF=BB=BFOn 16/05/2019, 19:50, "Bas Spitters" wrote: > > >> > > >> Thanks for confirming that this is still open in homotopical mode= ls. > > >> > > >> > > >> > > >> > > >> > > >> This message and any attachment are intended solely for the addresse= e > > >> and may contain confidential information. If you have received this > > >> message in error, please contact the sender and delete the email and > > >> attachment. > > >> > > >> 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. > > >> > > >> > > >> > > >> > > >> -- > > >> You received this message because you are subscribed to the Google G= roups "Homotopy Type Theory" group. > > >> To unsubscribe from this group and stop receiving emails from it, se= nd 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.not= tingham.ac.uk. > > >> For more options, visit https://groups.google.com/d/optout. > > > > > > > > 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. > > > > 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. > > > > > > > > > > -- > > 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit > > https://groups.google.com/d/msgid/HomotopyTypeTheory/FBCD91A3-4A6F-456E= -93FA-E36EFB56D607%40exmail.nottingham.ac.uk. > > For more options, visit https://groups.google.com/d/optout. > > > > -- > 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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.co= m. > 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/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.