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-pg1-x53d.google.com (mail-pg1-x53d.google.com [IPv6:2607:f8b0:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 16b3cfd3 for ; Tue, 21 May 2019 12:14:47 +0000 (UTC) Received: by mail-pg1-x53d.google.com with SMTP id p124sf12030831pga.6 for ; Tue, 21 May 2019 05:14:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558440885; cv=pass; d=google.com; s=arc-20160816; b=qx4SY/6WorpGCMyjgEVk0A4OeR3viv0GdElpeOiHX/UaMABrk6Vpf/LSHx4vkiRecG UXLazOzJ1WQ5X5Yt2dX9vcTBIbaWXwQnWUaQrQSBb3R9GUDvAOr0skPp9FxmW0fAl9kP vw/vUL8BhrruhMiZBiZiMHw1cdkvcf3GC1WHJKt5RC4BzSCr3JKqDdvo24ZHcEp8jcHC XV06+1usV3G5yoZiEoiDhuF37Oj0VEBU1k99d5g5FsoALXJ6/00yZex9PSeSQdfJQKL+ JrAMvQxPzRqHbvUztS7g2P2n/apqYSzDbIAAfZ4STf9pIpdoYlBWpy/Uc0W1TF/Wa9Mx fbCQ== 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=mrldEdgBnbCCi6C/G0UnZM+LztN4LgpQMl5dP4I/GdI=; b=JHUrWhbdTlu889ZlpH0inm1sLx7XU/vK5YIq3FtIZyfVqDywheb6xxqBVR6VdGV+Na Nn9W/qOpPf7o67nE/NcQ8rQiCye5orfuSm3oCGdA5oGE6QgkrbfB5TKe6RAAxz2S9S+z 1rtEkzzLhBdIr08Lw/x08ctvd6gI0TV/2gl+43PmnQtP7Yj6xmmR1uXIteZf2JSgPgIX djZlESLapv12sunddGSMK+LKfXDoYWlswXKgpVHSg+gL0R4kdWDxMjhPwMEXmDKXmkfd DcuHB9uaABgF9jGSgxRiRDGlFe4O4rx6I6s0HMK2AdzVlMQ1R4unwSRiu44hDRBTB8+A 5Vmg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=m+mMRUzW; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2d 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=mrldEdgBnbCCi6C/G0UnZM+LztN4LgpQMl5dP4I/GdI=; b=TdVihNfg8+NLGIXMIVh7WC0Q5gdR1+U4LpEtt8JReq4DFF8AGWcJTdcsnigsGx38d+ 2KcVmAqWMaho8raVzsz7DqOJ6whjivVP/Dw9sgMK1oxcJqz1VmuiK5kGO6RnvBb2l26p Ian8uq+z+H45y82KIPc7UXpEiLH41rY5EnlkCRfg9hoBXnufy8xlL6EseZqOQSSU3loc /3y76Pz+DR6cNaZDDAvlNCDgvg/Dg5idejbQmuBw6cGmyUL47y+n8o2Z6bwWSahDsbUn O70LAKVgpx7CZxiJeZY2gbbpxcmXFP0S89+2EJ8RRMZYbiAdoaW8zdv5DUGZ8FfQ/upe UnBw== 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=mrldEdgBnbCCi6C/G0UnZM+LztN4LgpQMl5dP4I/GdI=; b=WcLzpKdyF6eRF+TDwI7Y8rLZdNvBSMGIfayI+BwqfHGUDuCczUpj+xVVJ6it9jV0mQ Lx7g/EDmErCBYo7aA7TcOcrBQ6ia8e06R6Jksrh4lCePGLOGpHbkV5TEEC7Z/vpmZsIH JUsOS3gGqESZMj3E/58IsRqd3MhG22UqXKBTymfTz5L1PUsUs5wv2f8ZYQjyz0BQ337z iW2DXm5A5Qx80aPG93AM4XO3Sp68azrBoJrYWAPfnX4f586tAPuVBucJ+5tNpJXO/0jP mqKxaKkCkWW8fBW12vT4FHp1nDu+2L34pI1e3m4X5sbbU+olDtauUIVnqjYwZOfqTXnJ S3Fg== 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=mrldEdgBnbCCi6C/G0UnZM+LztN4LgpQMl5dP4I/GdI=; b=Jp9SEsIkEx+i1fV4xNFxBV2BiuM2Gw9ClvKUpQvaUFIuHcW6/5H3rnfYVC6vsOEhDT iMG73Jg86rPblF+N1C8UZUePO+PUXJ+5T5lOWpDWxhPSkFk1xG7LK1aVuHTnHk9vm/0d T9MOGQDPhgKavYMcTPh4NxHFODm5Dz0kxG62RhfTkdFIwgahpwBiBbwNRnkYje5yTTb+ shTxgQSa9PXxXmBoY1AwBNTs/cIFVzGykfrLMZ44RqfvVKC3skpSzqRa+B7vFwItz44P 5G29vV4iWpVuT0NfoHaz1WECQszr8a9LsYxZ4GYY0VJEB3ySD2DFNemVDUsZ9f668QP6 x7AQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUXSsWwZ/etm8Y9obABEvAtBppbaHQdvVZErhENIqK0fkWZa+U/ xM1IHu/q9tKNt4+aMzyVriw= X-Google-Smtp-Source: APXvYqwTqhSIjZzRHxth0Q7airwsO8TlZH2lWLPzM36/qBUN/haDiaNfNsa3CxwyMSMDhG2kyIJCHQ== X-Received: by 2002:a63:4c54:: with SMTP id m20mr82137818pgl.316.1558440885312; Tue, 21 May 2019 05:14:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:36cc:: with SMTP id d195ls5128077pga.6.gmail; Tue, 21 May 2019 05:14:44 -0700 (PDT) X-Received: by 2002:a63:c106:: with SMTP id w6mr78304516pgf.422.1558440884923; Tue, 21 May 2019 05:14:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558440884; cv=none; d=google.com; s=arc-20160816; b=r5d5/biW7nAn4usu4T/NW5BvyUpiApDkoCPvjGWQx6NZFtLojc6oahuwEXZ0wRMYUR mrycULBMYpa9MZV+Oq/fClzDSu48iwbqlmNaWed8ux+cZiUrDSTh3l5R5p2CoPPngAdV rE9vGpPOHU16o6fk5KEPTqwNhVYrMSdan+tIMdTtcRow4Zaiv1UEynd6hu/JdZKJVBEC 22Cy1GmpfaXl5R0ykI6U3A7HHLhvtOsC6EoDYd0ce+mxhcD2/DfRyPvIMnXgBCy2hP9o mgY8T8m51W4t36LsQE1gBUuDh6VCIBNrNyt2guDs5IL9W3ZRAEhWPBXupaqZLAU9sGt6 3cnw== 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=axAusI1ldnrYyWysHDwbhxy/z4jJva1VF/irmh9fuSQ=; b=IpEytOHsTr3/1URSsccXvVWAzHcRKHli7jNvyN8oBdug8KkAw0XPO6yMGwzIgKNZmb p3IqwgvLwkPn3LXoaPCO5NeePN7dF91OH6wMcv76pQ7b65YfY5SlnmdZQVFbLF5irWrB oEYUSlcPFpXzfgg4ZWdRCu/O8MpyrA+xGPKeO47eUxmbasDHeXI0jtBPiK6XJungBCM1 PFbrMdi8uqXqwYq5wJUZ+Xd2c0afz8atqvaRZRwW+J0M1ZsOz/hHfdcA+iojjJ90cpBK NORVYXU7lNqmkqP5TEt9enCRURh5NPRsZLtmxC6zrsdDunXpImFx3tyGhyK6tx5eYjzw YO/w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=m+mMRUzW; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2d 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-xc2d.google.com (mail-yw1-xc2d.google.com. [2607:f8b0:4864:20::c2d]) by gmr-mx.google.com with ESMTPS id r135si1528441pfc.4.2019.05.21.05.14.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 21 May 2019 05:14:44 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2d as permitted sender) client-ip=2607:f8b0:4864:20::c2d; Received: by mail-yw1-xc2d.google.com with SMTP id e68so7208096ywf.3 for ; Tue, 21 May 2019 05:14:44 -0700 (PDT) X-Received: by 2002:a81:49d6:: with SMTP id w205mr26704438ywa.263.1558440884481; Tue, 21 May 2019 05:14:44 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Bas Spitters Date: Tue, 21 May 2019 14:14:32 +0200 Message-ID: Subject: Re: [HoTT] Re: Semantics of QIITs ? To: Andrew Swan Cc: 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=m+mMRUzW; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2d 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: , Thanks. Yes, if we have CAC and set-quotients things simplify. Of course, the reason to use QIITs is precisely to have a more general treatment when CAC is not available. On Tue, May 21, 2019 at 1:47 PM Andrew Swan wrote: > > Regarding the Cauchy reals, I believe it is known that countable choice h= olds and set quotients exist in simplicial sets, but I think under these co= nditions the usual construction of the Cauchy reals as a quotient of sequen= ces of rationals satisfies the constructors for the HIT Cauchy reals, and a= lso the higher induction principle. > > I think the HIT cumulative hierarchy can be constructed using W types and= univalence, using the characterisation of it as a retract of the Aczel cum= ulative hierarchy by Hakon Gylterud in the paper at https://doi.org/10.1017= /jsl.2017.84 . If so, similar arguments should work for ordinals and surrea= l numbers. > > Are there any other examples in the HoTT book? > > Best, > Andrew > > On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters wrote: >> >> What is the status of the semantics of quotient inductive inductive type= s? >> Looking at the literature there's some progress on reducing QIITs to >> simpler constructions, but this does not seem to have led to a >> convenient semantic result. >> E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman= . >> >> https://ncatlab.org/nlab/show/inductive-inductive+type >> >> Do we know that the prototypical QIITs from the book (e.g. Cauchy >> reals) are supported in the usual models of HoTT? >> >> Thanks, >> >> Bas > > -- > 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/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.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/CAOoPQuTWGc04i%2BcwOFaGLDuD8_b_53hR%3DXRZ7UmHo8-fjO6zOw%= 40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.