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-lj1-x23c.google.com (mail-lj1-x23c.google.com [IPv6:2a00:1450:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0283e324 for ; Mon, 20 May 2019 18:35:59 +0000 (UTC) Received: by mail-lj1-x23c.google.com with SMTP id t77sf2607203lje.17 for ; Mon, 20 May 2019 11:35:59 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558377358; cv=pass; d=google.com; s=arc-20160816; b=cOGh17EYjsRLI+CloSo7wiL/7nyhaDYWq9f2auqC1W14v/pugXEMi4G59Re6FG3Eu8 31FxDl3UR2uRSlkKbVBypHTrzGZEylpVjycF4/BssqsBzC4FQN+0iogWtCvCQpjfc9ia U/931ayWjxOqY7oYJNs5cvShNaWXujxfWrdeDlYQJZ64K3QH51wHHMkSjaNvYgDTDJO+ Ll1GHR6bS5BwfNtYvqhZI5+aCzvZVoEdHoGUx/bo5YJp7rIS+I43944GHCIbDwAVii7i lCmgpHwUnt5xytJl7jLmwxQBB8KEhaRckkm287OVTZ9WFqL+KDcZIORs1obOkHQXBN0Z 3SyQ== 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:mime-version:content-transfer-encoding :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=cTs4beGLkqwqDn6cHOhscIvXrP4tBSAM06vAT1TMDSg=; b=jvmWLRBfdX7Yn7JWKFJ/V/T1BSfyxAxxnsP/llkeIrXBxqKl3zlbVBGZvjGicxq405 RyKp/Akou/DGWJ0sny4IbZJWcq67r6tRefgalUmf3PWO/cXCB3cVvM5afH/DjAJaOVBd ZgZjyZGtsOAccjxeJf01hPsJx+P6fV46ucOtBQRyf2UWBjdESQsPpw9nvM8nHir3Yyl3 fwHok0E7MfJby74fhfhmu0+720zwPHzJlh1A//OESFHE9Lw3+c7mC+o60Il7bsrwbCqN LeCX+tjKUluJyJWES5jeyFd8ouhQbwiB7Bx8bFvQqC8JmfldnGhnpZLL7y5HLiPDCYER IcLg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=cTs4beGLkqwqDn6cHOhscIvXrP4tBSAM06vAT1TMDSg=; b=noF0B1rWQ5327vngoA1izu53SuyyYZipLnpGbmZ+lo4Faa+MI0YzKUOUn8NMxwVofj UWOekt27gj+ky9oLI+r16iJ9SCbvUgG+5isQEgu4tQMpQ5KDDKCM72uslAJrtn2JF5C1 Aohg7HTPn9X6EDms0IR+SCmdhQGGElmIieI7wSL5794bDGrPykWLGZj9vyKFg79EOGEC xN58Kz3g+FpNN9gTP78FNxm+TGK3pLumZDt1w3pCYD+xOsU/Gt8jscqajWFUv4uXvJGf 7P8PTEMRMzHzdHwn3Jz1ORRwFCzbv6DNU/PMcx8gtSz3fT9gmk7aISqovUmVgvUjbvix Mh/Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-transfer-encoding:mime-version :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=cTs4beGLkqwqDn6cHOhscIvXrP4tBSAM06vAT1TMDSg=; b=HtVTfqDF7vBuFSsiZtDTKLiL4gdnszbmmhizBIZ4lT4HENSnSTM7yKhnEV9TYRJv0i zphfjVyu0brLiYxem8adC0IG9ndxmMcGi+1AeAYBRI0UDR7XQnlpGKlltEJ5vhVO1XRt 4mbaik5ec4H2pUYJd4f9S8EIjAaCa+L10y3K6pt1ofYrQ+uzoBtxl9FStQeDC6N7OO5Y s05RUTgthQgyWkHm2mTMYfWT2NAkMvIJPWVpXm6TrkuKfgJ2zF8DZDpnpCG7aOVHKHaE zvKlB7W3iyI1vVwuSdbxUONVu19xRhVh/qGIwOKYCZyRiTlMZXy6h6l35le5xG10Jx3q ppGg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWeCZXmszQjdV43yYrj1+6vwnudS2X8KhE8dTGHZc4RsuvqfDgm aC3zbIJ1VbjukeZ0Dv9FtuI= X-Google-Smtp-Source: APXvYqzv/tM6ICr0IZ1kif0NnNUuMr2AB/+Eil0V6rvTp/rwTNouFLcj/UwgsKdvULo5bPlTI7Joog== X-Received: by 2002:a19:750b:: with SMTP id y11mr21194593lfe.6.1558377358718; Mon, 20 May 2019 11:35:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:909a:: with SMTP id l26ls1931044ljg.3.gmail; Mon, 20 May 2019 11:35:58 -0700 (PDT) X-Received: by 2002:a2e:41c:: with SMTP id 28mr35779341lje.69.1558377358077; Mon, 20 May 2019 11:35:58 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558377358; cv=none; d=google.com; s=arc-20160816; b=kbfKhUDdoSCLwh/F3c3HzsIZjAS/cLPdIqiOWf80SWIvfcqpXQrjr1yPMvVOMiwVyG fT3xh/HPwsb11qL9p4sUT69ThvQa4HhAc0TW6jiyXpQ/vrkyb3+QeufQtdqJiSUbebRk 9ANGZbgYtDSvFT7SrFL8007WvKCY6AtM8mS5OsOakrw/I/N44E9t+wFd5GiN3zyzE42Z /nw/OOD8K6lHR2sd4+iHUKN1MiSiN4rt/dEARPW8Q25wNCowykJ5DPMkR7ShbyBcGJfl fosmT3klhEiSHrFKCUs+2lm8mdOBEfaI2pS1mF/tEal1YjYzWckXIz2expGNRO0mtZi7 7NIw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from; bh=TqWwqciEmC9PhuZtJbH7NUMqrklTw9bRPmwiUz481OY=; b=aB4q+pbTkvxVYuHLh82G4zXbDJMI9wwjhOVBgzvmKPN0rbAbWdly+/9Ycqr5UrcSxT WDnPqMXWf4APGO+86RlVNtiIvAdyj1RDlUzvjsE+OAiRSkMV/BzSJCAL2RtGnTEXKEMA b2hya6HpUxBjuFzHps7nTDmduzlCaBq/1wz3XybQ3MxWfur4f8khn9t7kshyjqEGyCSI KQD8LsP3k1pFOToohoQbDPh8B6kElvsKxUnRDa/21l4Vhf9rNek6jXTCFspY6lPch+8K 6AU0M3clBqZiA33aEZ8gS81+YEF3tLgrVYFKtqTq9zHZeZb1gwT+DRB2y7P2KK+Q2CdK PdXA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTPS id m17si1990533ljg.4.2019.05.20.11.35.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 11:35:57 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 318562EAD25_CE2F38DB for ; Mon, 20 May 2019 18:35:57 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id E6278310277_CE2F38CF for ; Mon, 20 May 2019 18:35:56 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hSn8e-0007v3-2z; Mon, 20 May 2019 19:35:56 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 20 May 2019 19:35:55 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Mon, 20 May 2019 19:35:55 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Mon, 20 May 2019 19:35:55 +0100 Received: from EUR03-VE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 20 May 2019 19:35:55 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5214.eurprd06.prod.outlook.com (20.178.14.19) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1900.16; Mon, 20 May 2019 18:35:53 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::4c3d:4c42:fc4f:7bf5%5]) with mapi id 15.20.1900.020; Mon, 20 May 2019 18:35:53 +0000 From: Thorsten Altenkirch To: Bas Spitters CC: =?utf-8?B?QW5kcsOhcyBLb3bDoWNz?= , homotopytypetheory , Ambrus Kaposi Subject: Re: [HoTT] Semantics of QIITs ? Thread-Topic: [HoTT] Semantics of QIITs ? Thread-Index: AQHVC/fCTTpdQv6taUilYMlObALJqKZt8+sA///yOACAAAcWAIAAKzqAgAYvPACAAAqdgIAAC3o6 Date: Mon, 20 May 2019 18:35:53 +0000 Message-ID: References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk>, In-Reply-To: Accept-Language: en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [86.28.226.182] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: b7ea6689-e36a-403c-ab6d-08d6dd51fdc1 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(7168020)(4627221)(201703031133081)(201702281549075)(8990200)(5600141)(711020)(4605104)(2017052603328)(7167020)(7193020);SRVR:VI1PR06MB5214; x-ms-traffictypediagnostic: VI1PR06MB5214: x-ms-exchange-purlcount: 3 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-forefront-prvs: 004395A01C x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(346002)(39860400002)(376002)(396003)(136003)(199004)(189003)(6116002)(99286004)(478600001)(5660300002)(6246003)(3846002)(6506007)(53546011)(14454004)(102836004)(55236004)(86362001)(76176011)(53936002)(54906003)(8676002)(81156014)(81166006)(66066001)(4326008)(9886003)(966005)(256004)(14444005)(5024004)(786003)(316002)(2906002)(8936002)(71200400001)(71190400001)(83716004)(6436002)(68736007)(66946007)(73956011)(25786009)(33656002)(26005)(66476007)(186003)(66556008)(64756008)(66446008)(74482002)(76116006)(91956017)(476003)(2616005)(6486002)(486006)(7736002)(6916009)(305945005)(11346002)(229853002)(446003)(6306002)(6512007)(82746002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5214;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: ygd2js+FEm64wDbwlL1dI4ewDGmDGWnLkZ6sdKiX1EnsCuGGo7qoyiLTow4pbe3XwJXMVYs/dkoozVBcoNvrFR8GmwBpHMeovYLEzT6fF6SP6oZJ+srd3uNK2v0GNYESJLyf1KkAQkR2TaE3MybHgiroB+px30IMHfvjLnIcxVESf24gKLDzHmNdcENA+OwUHJjcekDleQrZxZJelF2UlNF1YdiclKXuNo1bGEs+896o9RDFxrbg2eBVET33Wu03usr/haE6J9zCiq12hvg1kgl8B6epfs9nwpp8PHHfTt8QpU0c4XK9xH92KWtRXcPnaeOlB2vcqJtr4n2dAnITLVQ+4cJxyJ0nznqp35EGHvROMz0GUEq7vmZy0mKcdS310Fi57k3wOSpI07h8JENLYnWyevWHRsCLrmDsE1E5czQ= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: b7ea6689-e36a-403c-ab6d-08d6dd51fdc1 X-MS-Exchange-CrossTenant-originalarrivaltime: 20 May 2019 18:35:53.6982 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB5214 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk 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: , 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 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 prin= ciple? >>=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 QITs in= cluding the Reals (I think) but this is maybe because choice is provable fo= r 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 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 Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/68D3FF39-6345-47B0-B905-72BDD282583A%40exmail.notting= ham.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.=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 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/FBCD91A3-4A6F-456E-93FA-E36EFB56D607%40exmail.nottingham= .ac.uk. For more options, visit https://groups.google.com/d/optout.