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-wr1-x43f.google.com (mail-wr1-x43f.google.com [IPv6:2a00:1450:4864:20::43f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f849f955 for ; Tue, 21 May 2019 08:39:15 +0000 (UTC) Received: by mail-wr1-x43f.google.com with SMTP id h4sf7741940wrp.21 for ; Tue, 21 May 2019 01:39:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558427954; cv=pass; d=google.com; s=arc-20160816; b=ZNdZtIlRJ0Kd6umcuj6rv3uIkhRTFbe5Zk9YqWD/wejKAxX1vXpPbGoerj3M2prcDh PmxknmYwbB1AQ4fw4rVb65h9OQ/rSQsgIlVxOgpfDX4XSGHyf4Ye4CjP9wZfdd75KnoH TpcsH/ogwVEENMkFXUu/eS72Z4Pu6gqdsTtr0fnxHKtFuttsC5Sht4B+gv3QH6hBS69H edbOiqWEYzjVs3JdKvvM6p+4DVpzvLDVVcOvbeIXRiClTp+3S+3FWQfOOaiuTJuAvfrB 5kaZiBS81IKsbhnSyrIDnqwWhOUlsrWkqRZraIDcHyBNhcdptdlMHrtTtprITgXXvL9n j13w== 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-id:user-agent:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from:sender:dkim-signature; bh=MYwnGmR/TzPNWBGZ0s4jHqNbre+SX82giKwSJ9j988w=; b=jIK+eX49ithagLukGWPtP0vH3VTr6sGuO04mpMYT8N0Pqso2NTWlQN8Sj2H7en6GBF 6ADBNN/+AonagW8z8ex9QyXMVAzqFD1fQ5Cr3E4pVkiAB4efpp5LVrClFYbeTq6ztXyI e7+d3UvBq2+s+rMUd5r0kzSCxxA25x3C1bgG7kYnMv3x/HY2LuQ6IQZSRIZHlx3Lu4nc oEt4JbXMU6CQOMNGuRCIArb8weMzMSLjA89wbxdK2oBMWXDmH97bF9trQ0cBSMQ338IE /qjCjum1KSwOXBxp4UmMvhvBNKg0IbrDTdmYI8Uo677uJYoGEiIxhz2pre0pHfhfaxN8 3Kbg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 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:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :content-id: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=MYwnGmR/TzPNWBGZ0s4jHqNbre+SX82giKwSJ9j988w=; b=NbXj8JTe/q172p5C+kEuzNhpprIp7+2NMBt2Sv4rmCZiRv0/A4CwaCfQy7LP5xSY5h g5Myy0KE6dhQ7qrtAybxWUWl8FC1aB3hZPFm8gPcp9UixQga8zP2k1ymw4rC6UnD5427 h8X5BQ2+YtorDp8VH+RktIGjFfmc2M9d7I70ZGPl7CRVMhfhKfGhgYxCfaibI43jXdyb 2uJCAd+Os8pRWzcx2edqjjBlClDECZsrJLMYghlhP+STcfi2EUMVdZk2LnYDOj1zRMwE BpLJKivNdbf0oU5UELs9oi+t/9yr56y7zJ+v70ozYKFpjnVAx+gOfPYVwbc9GziFouBm Jqnw== 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:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent:content-id: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=MYwnGmR/TzPNWBGZ0s4jHqNbre+SX82giKwSJ9j988w=; b=bIaNIR2PqjNonZwSEci/Na5Pg6koq9cDsbs/07kfeHe2nEAuQYcEPg9XHa81IvHGP6 /yOC5GE4XpJoEjeXSa3fQrbSunf6lXGgGkgn+iGVnO4YMuRFRpdSSJzRPXiY8S6YrVEy qcHQCWcb9y71sYPc4L5xuvl8XqEyKMp+1kDQpXvT5oJPtD8Y0wTubUEi8oDLz8K9EpVW Kaylms9ykQo0b/vf1jREHfAOtV9AiSWCDhonZ183wr0rbaZad/qq/B+YA+y1WMduNX/N SJRIyPRngIV8h+FadVT7dOxdwyx/nxZJeF0Mo4Zhle2kuCW4hOBJKfgLc9sobYErXp9M EmZw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXt//CZTHWyXd51iGeUzHwjyQvqXgNeFQtXpoR/SzrIeIyZzgmr dTI7k1aurgScpEttHoedDLc= X-Google-Smtp-Source: APXvYqw24UBMbtA9sjV8wx/HGqYPxXwPSImIZUUhDhm82U6/TYnCK3zA6S2tc3nl5Ypu+pLl47Uxhw== X-Received: by 2002:a5d:4206:: with SMTP id n6mr4166102wrq.58.1558427954740; Tue, 21 May 2019 01:39:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:2304:: with SMTP id 4ls637152wmo.4.canary-gmail; Tue, 21 May 2019 01:39:14 -0700 (PDT) X-Received: by 2002:a7b:ce83:: with SMTP id q3mr2515943wmj.32.1558427954121; Tue, 21 May 2019 01:39:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558427954; cv=none; d=google.com; s=arc-20160816; b=BLyOgUYTEvX0p0OSf+Pe3jJUrpcCeI5KbWepm2oeW8hSsKQQ8WghvQ0uMam8c0mXit PiUi8gASA1aiManTxZkNbWK8rDk+nikGjEk63Ya6ehUKjYunycnVsUJD64BuwwaYC5GB TM4I4Y3cA+MGmwUNsWMh3U9Sb2S6NuKeD04Wc9L0DKE4RnS/l/Y+xf4u7U7diN88u1Xl GpX1cStGs6Sl0A2xv6BfDX3zTcPhdjgani1+fYG6qZDn47E6eq7nuxOFEKgVsq6r9yge G9BdoPI3oQ870TzGuYpU7TDhtQoT4NrLpa5l3kU/ez87hM9L8MPtJYmzQvH0nq9yIUqn qohQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from; bh=HNJhzXywanFVY0pEXXZ/LyNRGNroM0rSQQjpi2Bfc5Y=; b=ITc6G+6Jaoblw112LYJ6BD7wzbpNIPHxXVfOcxRYOoscLByeV0A9xS/HWFdZqHz2ez yxe3S5DdV+cz5SK9j+6N5UPuLTAw6gJYA39lvn2dkWZ7z/8nRRo6tII+Aj0pUwRC/KlV TaC+QmvWN/HqgEZS9uq3xX/mKNEHUIl/+Y1gySwd2ZJNa3cNgU1Zz6kxYSQEBHxKftAu UrSp5guyIHjguG1HCraRAq3fV9U2flArxkPHyy/SofX2iQxK7rVhoVl0ikYAcOyLo/Ac sIJ/z3olLWYw3nyMDGMeaOqZ4yaFAXm/xxR2CPV9xb8kCSKvWiPREeaVX066V25zI7ux CiMw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 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 uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTPS id h189si46799wmh.2.2019.05.21.01.39.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 21 May 2019 01:39:14 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id A5BDC6CE612_CE3B931B for ; Tue, 21 May 2019 08:39:13 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 0D4816CE047_CE3B931F for ; Tue, 21 May 2019 08:39:13 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hT0Ii-0001H0-UF; Tue, 21 May 2019 09:39:12 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Tue, 21 May 2019 09:39:12 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.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_GCM_SHA256) id 15.1.1531.3; Tue, 21 May 2019 09:39:12 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Tue, 21 May 2019 09:39:12 +0100 Received: from EUR04-HE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Tue, 21 May 2019 09:39:12 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB5869.eurprd06.prod.outlook.com (20.178.123.91) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1900.17; Tue, 21 May 2019 08:39:10 +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; Tue, 21 May 2019 08:39:10 +0000 From: Thorsten Altenkirch To: Jon Sterling , "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Semantics of QIITs ? Thread-Topic: [HoTT] Semantics of QIITs ? Thread-Index: AQHVC/fCTTpdQv6taUilYMlObALJqKZt8+sA///yOACAAAcWAIAAKzqAgAYvPACAAAqdgIAAC3o6gAAXbwCAABIVgIAAFHztgAATGYCAAKtFgA== Date: Tue, 21 May 2019 08:39:10 +0000 Message-ID: <29D54132-775E-43EE-8439-544FF3EA6C4F@nottingham.ac.uk> References: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> <68D3FF39-6345-47B0-B905-72BDD282583A@exmail.nottingham.ac.uk> <4CAE313E-7B00-41D3-A13A-3AAC0A496AB0@exmail.nottingham.ac.uk> <96fea5d2-535c-43fc-9832-48ce96e916ca@www.fastmail.com> In-Reply-To: <96fea5d2-535c-43fc-9832-48ce96e916ca@www.fastmail.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.19.0.190512 x-originating-ip: [31.91.158.117] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 6c8b779a-9020-4142-877f-08d6ddc7cbcd 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:VI1PR06MB5869; x-ms-traffictypediagnostic: VI1PR06MB5869: x-ms-exchange-purlcount: 8 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-forefront-prvs: 0044C17179 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(376002)(39860400002)(346002)(136003)(366004)(396003)(189003)(199004)(51444003)(8676002)(81166006)(76176011)(81156014)(99286004)(36756003)(55236004)(102836004)(53546011)(6506007)(786003)(316002)(6306002)(6512007)(25786009)(9686003)(186003)(6436002)(446003)(256004)(6116002)(3846002)(14444005)(5024004)(486006)(476003)(11346002)(33656002)(5660300002)(82746002)(8936002)(6486002)(6246003)(2906002)(26005)(229853002)(53936002)(66066001)(68736007)(64756008)(66556008)(66476007)(66446008)(66946007)(86362001)(76116006)(91956017)(73956011)(74482002)(110136005)(966005)(478600001)(305945005)(58126008)(14454004)(7736002)(71200400001)(71190400001)(83716004)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB5869;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A: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: Ib4dmZLwuM+bQOE/DykRMUnAK2ARarF2LKWZ2wqT0TGl1G0d7b3GadXL491kV2QtBLBb/G0jP78DiDfsaPgavSfx0z05gBhxsAClWawCNVH2U0V42vhaCOHFlFptNzaUas2vU2J3EZb2VAuNE7sSAIpxJINjZI2HFOBSXVlOGy6XGMMxT5VwO2bZxrOw9wH3SDupDtKqwc4hSZvpwml4z2uzlW+TUwk39ODjacN2KlxepuTWXEed/Qpp5UzlvckonS6VpyWVqlA+VqlYaUp5sS50rO+pm6imNKLa6NeUpWPPDs79fEASRlpHa/K6Zcuxhie2xJ14Z6p4zMHGpvttqGvK3DlW+LxVmsFiw050Oay6A9lWZdWtwTGlvnhKGDy6D9UnZVshXEcVegNQLXMX8XIotnuarA67qL8c4ke2H4E= Content-Type: text/plain; charset="UTF-8" Content-ID: <85B6C476EB66CA4380F5F88290CE8C82@eurprd06.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 6c8b779a-9020-4142-877f-08d6ddc7cbcd X-MS-Exchange-CrossTenant-originalarrivaltime: 21 May 2019 08:39:10.6089 (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: VI1PR06MB5869 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.128 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: , Hi Jon, Thank you for this explanation. Indeed, I think the question of how to inte= rpret QITs without UIP is interesting and open.=20 I do think the setoid model is useful in this context. It can be defined wi= thout using UIP by using propositional relations. Within this model you hav= e limited instances of choice, namely for types that can be obtained by the= embedding. Hence I think that QITs that just require countable choice like= the Reals should not be a problem. However, this does not give you an expl= anation for infinitary QITs indexed over a QIT but I don't actually know a = natural example of such a thing. Thorsten =EF=BB=BFOn 21/05/2019, 00:26, "homotopytypetheory@googlegroups.com on beha= lf of Jon Sterling" wrote: Dear Thorsten, =20 As Andras noted in his message to this thread, it is very much an open = question whether QIITs can be modeled without using UIP (this is part of wh= at people are trying to distinguish from, when they are asking about "homot= opical" models); therefore, "interpreting them in cubical sets using the g= eneral construction of HITs" is definitely not a slam-dunk, and novel + wor= thwhile research will be needed to determine if it works. =20 Echoing Andras, I recall that a new encoding due to Jasper Hugunin enab= le us to interpret IITs without using UIP, and it is an open question to de= termine whether Jasper's ideas can be extended to QIITs. I hope they can, a= nd someone should find out :) =20 Best, Jon =20 =20 On Mon, May 20, 2019, at 6:17 PM, Thorsten Altenkirch wrote: > What exactly do you mean by =E2=80=9Ca model=E2=80=9D? I=E2=80=99d th= ink we can interpret them=20 > in cubical sets using the general construction of HITs. They don=E2= =80=99t seem=20 > to cause problems in cubical Agda as far as I can see. >=20 > Sent from my iPhone >=20 > > On 20 May 2019, at 22:04, Bas Spitters w= rote: > >=20 > > Do we even have a model that would capture all the QIIT constructio= ns > > in the HoTT book? > >=20 > > I recall an argument where one constructs the Cauchy numbers as a Q= IIT > > *within* the Dedekind numbers (assuming impredicativity) and then s= how > > 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. > >=20 > >> On Mon, May 20, 2019 at 9:59 PM Jon Sterling wrote: > >>=20 > >> Hi Thorsten, > >>=20 > >> I think that in the way I interpreted Bas's question, setoids prob= ably don't count --- by that token, even sets would also be "homotopical" b= ecause sets are a special case of setoids which are a special case of group= oids which are a special case of infinity groupoids, but what people are wo= ndering is probably more along the lines of whether there is a model of typ= e theory 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= something well-known like generalized algebraic theories or something like= that, so there are some really deep questions involved. > >>=20 > >> 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 := ) > >>=20 > >> Best, > >> Jon > >>=20 > >>=20 > >>=20 > >>=20 > >>> On Mon, May 20, 2019, at 2:36 PM, Thorsten Altenkirch wrote: > >>> The setoid model is just a restriction of the groupoid model wher= e all > >>> 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 construc= t free > >>>> algebras for infinitary algebraic theories. However, Blass showe= d > >>>> (modulo a large > >>>> cardinal assumption) that these cannot be constructed in ZF [Bla= 83]." > >>>> In fact, they construct an uncountable regular cardinal explicit= ly (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 homoto= pical > >>>> models, so the setoid model does not really count. > >>>> However, has it been proved even in that case that such QIITs ex= ist? > >>>>=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 construc= tive principle? > >>>>>=20 > >>>>> Mike and Peter show that there are QITs which aren't constructi= ble 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 man= y QITs including the Reals (I think) but this is maybe because choice is pr= ovable for the setoids which are obtained from sets (like Nat). But what ab= out a QIT which uses a setoid for which we don't have choice? > >>>>>=20 > >>>>> Thorsten > >>>>>=20 > >>>>>=20 > >>>>> On 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 add= ressee > >>>>> and may contain confidential information. If you have received = this > >>>>> message in error, please contact the sender and delete the emai= l 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 monitor= ed > >>>>> where permitted by law. > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>>=20 > >>>>> -- > >>>>> You received this message because you are subscribed to the Goo= gle Groups "Homotopy Type Theory" group. > >>>>> To unsubscribe from this group and stop receiving emails from i= t, send 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%40exmai= l.nottingham.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 addre= ssee > >>> and may contain confidential information. If you have received th= is > >>> 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 no= t > >>> necessarily reflect the views of the University of Nottingham. Em= ail > >>> 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 Googl= e > >>> 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-4A6= F-456E-93FA-E36EFB56D607%40exmail.nottingham.ac.uk. > >>> For more options, visit https://groups.google.com/d/optout. > >>>=20 > >>=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 email 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.fast= mail.com. > >> For more options, visit https://groups.google.com/d/optout. > >=20 > > --=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, s= end an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/= d/msgid/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DM= Pwg%40mail.gmail.com. > > 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, sen= d=20 > an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit=20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/4CAE313E-7B00-41= D3-A13A-3AAC0A496AB0%40exmail.nottingham.ac.uk. > For more options, visit https://groups.google.com/d/optout. > =20 --=20 You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/96fea5d2-535c-43fc-9832-48ce96e916ca%40www.fastmail.= com. For more options, visit https://groups.google.com/d/optout. =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=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/29D54132-775E-43EE-8439-544FF3EA6C4F%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout.