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-oi1-x239.google.com (mail-oi1-x239.google.com [IPv6:2607:f8b0:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c4846944 for ; Mon, 20 May 2019 17:55:04 +0000 (UTC) Received: by mail-oi1-x239.google.com with SMTP id d198sf5076553oih.6 for ; Mon, 20 May 2019 10:55:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558374902; cv=pass; d=google.com; s=arc-20160816; b=VDdc0fAxeAYAEh/sUaKGA/tUyCSdwy789B8SgVBecVWsK/Bvld5XwygVzHlsy3DaCO DXmfj3u2BhXzcdXUSnVC9pQ3NY72P9Ph6yaIbF+uQr+PKNvDqAkQq9SVVp1aYu0O8186 dGVSryUCeINneXebHtSt+0YAh22JGgzQT9RQWwRfXfJS00uM2pPSlHAbt5Y0qDQJKZvC Ae7uhoNjD+5EN+idXe7Em0x6UqAQ5vodmck0f4OzRgaafCVdLqTZLKQ7Izkkl59+J9ya N3gxOztD6RPWcpz8dC5inj72zuqD6HUjd1P5qxIxe+DfQgTG97nbdrVolyycNxw/ydSw 5n5Q== 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=S++KnAaECCbylLCnJU23Dh0GOzrTiYHz1q7grPUF4CA=; b=pfmPMKkHz+hnRLTRL5lOD1NAyXHt2eNtw79LaBVYKI+1TN+FEalyJ7ZrfcwbjU99LE 7EzrNujvkq0AaooaRyazYkwdOCDT0zdSVzKgMv097xM8aOt4FGwEGHUnkA/N52Fa8xL4 7o3SltSa2NwhdUs66K7OTedDMDBlOiMGth7o+Ynxs50GN659ymafFBP7ypYchV0D//V4 kAFvxOeHf34sj/Cj1LG5uk4WZUuqLyW8JNUtHjX6E2VrRPOIn7M4iwl5kQqFPFc4ad76 QI1dgEpbAMRNODDJX8ap4EVLGoE1DOdJvrsR+z7/qMfCxjfnhUzg8cXAPweDBdzCpPYa KdTw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=nMcxCUfm; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2b 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=S++KnAaECCbylLCnJU23Dh0GOzrTiYHz1q7grPUF4CA=; b=OYGmdTTd5vmUMoMd3l9jsH1tp7EOEwDMvrPLTr22wDtSGB3HqfL18EawWdmxNiA+DR UfPK74oUbv3NWnWXo1bFTGA30fGU74v0cG4S9iKZmrDQ0Kj9Q0XWmJWlrEBU6WoxNr48 L2YiP7NhT2rsCVRwR7ibSusMIhRy+cqMAE8oXj+C3wARhJndaPjc5hYcv3JE+dmMwx0p +6bbksVGCkv0lFmSeXDjiLdZedasYfQ8zVE9yiNo/t57L78RmWk8B3l3ts7YDKGubB8u E58IIRYbozVnpq+AcnIMEHAXyJ7jMKwqosG/LgA4xZlPXBZQUYKZ6WGFJoxvYTwxRlzm jrvw== 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=S++KnAaECCbylLCnJU23Dh0GOzrTiYHz1q7grPUF4CA=; b=GAqFcuGPKLu2uzYVZJknjeaKzQj8PBEuaxCfEkn3z1m/eRQr7a6imAmxxJ+YGLCeKU pZ2e84OVoZfJgesfka3PYycoVG3LuTWlIabOmV5Y7bSNoN8226NREgF8WArbjhXoOuEH 0GGV2LotKtu7RLHhYIHmlYFpBkMtjoBHZL6F/Qylhqy17zAGRq/Wy4gE37nujWUjZIsA NN3Zixd7XT3yWWmagoy2x7qaEkSitORJqHKdNm27C/Se0F7j6bQ4gHJPUnVkBCt10xIJ b+euT5bJRMII1yrwLOLPB0CPxKnjS2UQrhVukjg4gF6AkR44oWbCui6oLNSAV0BlSHzG QQtQ== 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=S++KnAaECCbylLCnJU23Dh0GOzrTiYHz1q7grPUF4CA=; b=AYID3/5yNmNdXC1TOEgke025pR+tZD/STp+Wqa9+20XJrDafMA0hg+7xgOxU+tHtZ+ WTWd5T3kSOwcu8Q9kt6dRcvqwhjN+SoyoEj0zSru4F/ElORHLWtL7wkZ3Dn6M2ouThqS exUmY6hhlkVXkFoAGoz3HILEJGlmd4KzoJJOVDyt4nzwNA5kqXzUp4iMxCTgI3tmFca7 AiEynZwYXO51W+6nGMkpGUOWuGCC2W0xaJbHUsvkFkiI1TOulybVikh88HvZg+YdJHTZ /DiPyadpo9hx2/Gx8HzXJ/q+OGIzFiKSNooxj5mSQMebdz5ZZWeqfiQI1eFG0llTOUif Juow== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVpVkgRlViCLXNsPjyAboQ+9nwlcCg8LtUKkUtLXfn4sdyGZl0h fwPLpMRKaQLaFZXiHoWFp/M= X-Google-Smtp-Source: APXvYqwiXHmbt41yfs5ceKl8wtMMnZg65hhmSRZwVF66Hag4rJQGU4ubVu1aF3muONpEouFCDaeGeQ== X-Received: by 2002:aca:cc83:: with SMTP id c125mr297391oig.138.1558374902645; Mon, 20 May 2019 10:55:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:ec50:: with SMTP id k77ls2587993oih.10.gmail; Mon, 20 May 2019 10:55:02 -0700 (PDT) X-Received: by 2002:aca:5c06:: with SMTP id q6mr310155oib.8.1558374902242; Mon, 20 May 2019 10:55:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558374902; cv=none; d=google.com; s=arc-20160816; b=cuwx7xBaCSavrJYOY2wDpMzEs8SUrJKP0tabPtBWelYJFUwu71MlYLzH2bvKic2X5f 4H+DY41haMiSMpYoBkzR16ZR6Vn14HuJCZZ98npriHANVBRtaW+BiZVezNvq8sbL8J5H ZsP9QJEU9yz0kc5I0oD5Hx6M7YyC4O2Fj/4mU0NvgKjYgk3P7NRPE3BJzq1hBpkjGIcT AiyBsX/fhzz/eb2TcH9m7kBPI28ZD1H6l2P/NxFjOxUnauuxEBSsKqf1ulJW12SLbmJO KqBsvyt8RG5Tw+0aVFHBE9eAcbiYb2UskSlvcdhu48gfHDiyrZey1bNlOArAf0uf5N1+ chtA== 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=nCtmSzIE05+1SblqX1muqhAYkoH5WVvE9LySXnQzDWE=; b=gEExMStSbF9FTMYW2GV8eTYzwJkA84cs9HyNYJobttLmkEs7ckVuLk1xmLBZvuANlj DOj0+FqXlMxMNRdfgUSYNpBt4mCw56l8dbJIp/B/d3kVWejvjoVmMFd0dmvtpLOlmZK7 Oxum7OzAsOf9ytdN67yE3XUzBVKRKjbugjm7fj//6hVcq5v0FLxpnRSSXMoMb8Q18jO7 G4unFOMA4RKMiLg8zbCxVNlYoCRG+3whjG9STJl2d4sb43zg1D1bKSQ1slAFs5gcc8C2 cfzxJPlHTbc0khpkGAFAd0b6Mn+8qnSTvcENwTgZLntpj0AWbrxaWlKHgXRgoxoQ4tqk E37Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=nMcxCUfm; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2b 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-xc2b.google.com (mail-yw1-xc2b.google.com. [2607:f8b0:4864:20::c2b]) by gmr-mx.google.com with ESMTPS id k22si1411771otp.1.2019.05.20.10.55.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 10:55:02 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2b as permitted sender) client-ip=2607:f8b0:4864:20::c2b; Received: by mail-yw1-xc2b.google.com with SMTP id k128so3981041ywf.2 for ; Mon, 20 May 2019 10:55:02 -0700 (PDT) X-Received: by 2002:a81:5145:: with SMTP id f66mr35982502ywb.195.1558374901764; Mon, 20 May 2019 10:55:01 -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: <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> From: Bas Spitters Date: Mon, 20 May 2019 19:54:49 +0200 Message-ID: Subject: Re: [HoTT] Semantics of QIITs ? To: Thorsten Altenkirch Cc: =?UTF-8?B?QW5kcsOhcyBLb3bDoWNz?= , homotopytypetheory , Ambrus Kaposi 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=nMcxCUfm; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::c2b 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: , 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. 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 princ= iple? > > Mike and Peter show that there are QITs which aren't constructible from q= uotients. 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 QITs inc= luding 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 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 models. > > > > > > 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/msgi= d/HomotopyTypeTheory/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.nottingh= am.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/CAOoPQuRJ5QU2GTqctjGSJax0CXkBWWq7GEYcf0EEox3izZTDeQ%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.