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-wm1-x340.google.com (mail-wm1-x340.google.com [IPv6:2a00:1450:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 220ba278 for ; Mon, 20 May 2019 22:17:53 +0000 (UTC) Received: by mail-wm1-x340.google.com with SMTP id l9sf98284wmj.8 for ; Mon, 20 May 2019 15:17:53 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558390673; cv=pass; d=google.com; s=arc-20160816; b=bDgXxea54ts/uhHtUsTfyC6brWvtmn6z8hwUElqAuP+cMmbP7jxPnrgiilkOalVd5J gb02FVbrcZLbpFdWvirZmDYYQ9goj1TppsxRYezWyquQ+nsLRUGXJmaZND6Ph9JnSWej 4knAou083FUU5nWZsSTnsEu8Th0iMwWaEu5cu/tCENjuEz+XKBRAPAXHtrVv6S+FuOPd TstSs9xOIfKcr656stHmGY4Hyd0O/fsI4Whw64BwK9Nh7N8Oh58PkQsOz5kVp6PGi6d/ XktnT7N8O+tl+1syYH13LnbcgeY1ncKKrxKsp8UgfxJ+8h64ewO6Qc8gGPgdYXIPjRJ+ sOyw== 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=WvNsk0IspEL+bcOXHzQsFTpiC9DXCfVHEjG657xlrD8=; b=EMnK9uKc+Nn9ymOK7DzdyHrWyuvcpDIsiP+7jANUmwH/PO8QfSpHKj2HwbWFf/ay0s k4gDy9IJ8LjQcRBBse691D3d00CvTFrUchA5JrEP9cBzCSiLfnZkLcAKkNPvM9DTCG1Z 7DBo7j4ug7sK1LEmVJb0gpMXupBncktVTvmCDcX0sQ6o01M1JwG++zEQ/ZvDp7Rg8A+1 mcDcc9bsPgPS7aV1HvB2p9qdKR5piF1dfS759AxCVMINWb1SzhUQZthwHY3PeHQwvOxz gfRp6CKNUF9LgkGgaoNuadIhhUeKAJNDPPl8dfKJ4zxtWugIojpcj2JYPtYIvnuT2RXI 80iA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 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=WvNsk0IspEL+bcOXHzQsFTpiC9DXCfVHEjG657xlrD8=; b=OR6hY45UISrIOCz947xbwsKXPPTJ9wBlC7YkZdGVmRyLjXXUzERtf8UAm+7YUFcLIf 0fXmTNbabOnrJJujn91tuTOJ+XTmSjQLJChAIgc0ycnFShYNQoFcdcxoGm+WuwvZHDqt EOMBFWrFaeWn8z4PkJUsx+NBMIjcDKjlJaCDhwvsWFZaHbXnUTiGGQ1J3qgKvrKh1s5Z fLB4TGeb5rRb0Um7F/eP3eFFtDMJRtmiWdKEst/UFhRG2GoZXoHD+/qWp649yXLYXwB/ b66imZkEV01AQDK+Jj9vMo8igIvIi7uXQ/3Q0OHsxfgosgiLAeqpUCZIzs0kZ7zY0wDA VWMQ== 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=WvNsk0IspEL+bcOXHzQsFTpiC9DXCfVHEjG657xlrD8=; b=GPb4ofNNb89RfqF7N/DvWaI5YvCC9j9M8Oz2TEn8AJxkhdlsuMSJdjQSFWlLFFl3HX Z9dDszG/zZhuy2+uZDiIskJoT3Z1lS4pQgLT4U6WZuFcz60pJE650nmUSC798aQzj0wC 8gC4epHD89H8VwqSjlw3SOxiYgVH1dsHKg0qwiGKvsGgStTUO7bEW0wAq1znQEt4nJpG 2bIebCOmUcaAqA5/EoXEWW1iOxCeMlyfapht4ZlJUDEM3QpqYzWpVCdYtM9OLzeVf/9J 1tYGKRlL3zbBIIumR8K8bvS/pbfz4pI2o1ztBV8pzvFCQAaYskX1IdqMlFUsE9OIhk0P aO4g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWzVVKrsM/vZORHvXN/Lofn4YP1wqn6lRUVA4o69QKsrzgpyo+I y2Jv6RtH50KYueEKdj5iNcw= X-Google-Smtp-Source: APXvYqx9xcvqoro//U2rybV1qmUc+BKUhzezy6DGsdTttpss/bnqQ2NiJPX7cjpBWycudAJUg1OIBA== X-Received: by 2002:a5d:640d:: with SMTP id z13mr23302256wru.299.1558390673213; Mon, 20 May 2019 15:17:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:5186:: with SMTP id k6ls4477766wrv.12.gmail; Mon, 20 May 2019 15:17:52 -0700 (PDT) X-Received: by 2002:a5d:5381:: with SMTP id d1mr16785933wrv.333.1558390672476; Mon, 20 May 2019 15:17:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558390672; cv=none; d=google.com; s=arc-20160816; b=0x/tVKjritszOhm8rG13ech3i9hk4xI7rvUjmVLC1ifc0m0H/elFWecynM1fdy8lvg gvgcbvizPtjbmVUufHmV/7JpBHvCT5rbNyssyUUcLDcUJbhmkAZilV6mOD5jNcGt0FPf 0S3k4mQApp+3OmluHaG3imUfBFWVRJF8zKnKJAWGMXcIPia1UIMSBtZU9Uu4td+vf/3m tT7jdLEmxo709ZGWIvEKy/UqrxK4Gmv3w6Bbd59KajL+127W+SwTV0gP52FqUx3xuRkX wmzAEv5pYARH6OoXp912UpH/cch/lb09Hegb+VCRUUGHIlYhnceJRbdSlYHHyCPLYwkq ivmw== 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=ZrkjfBBt+5R5DGPOOnP3fH6hzEKOicfoadDsgzgBW5I=; b=uAr6KymnMusQuK/ZXluGMK3/4lcRMOrFDL7+Xke7Mcz9NxTcLmz5Dfhi+vQecx0xru 98c0zpqY6bT6SHMwRxGUs+ZkkRIQDKeHrVIAlMlfvcquM9NcT9km3BlwaohFZXWL7X1k IfEAgiCe8fzP64D5loN7qqHC7DJXSzn5wRs3hcKyBajdusVXm7eo2QbtLYswNKpXwzA5 wwnmEWcXQWi+t+dlaxKGg7pyNT8vGMbY+ZXMJKhg8eVEffU7aUIpgvHBbsJST/d/VjK6 FBw4VoHQwKMZc+MGg3URK5WF6Li3zDYJ9+mgCX1dT1V2GkJ9/oM8hDDE/MGZcd+wYNPX WPVA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 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 uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTPS id y70si72912wmd.0.2019.05.20.15.17.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 20 May 2019 15:17:52 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 0E36A3C466A_CE32790B for ; Mon, 20 May 2019 22:17:52 +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 uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 855EA9644EC_CE3278FF for ; Mon, 20 May 2019 22:17:51 +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 1hSqbP-0002Is-ER; Mon, 20 May 2019 23:17:51 +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; Mon, 20 May 2019 23:17:51 +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; Mon, 20 May 2019 23:17:51 +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; Mon, 20 May 2019 23:17:51 +0100 Received: from EUR02-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; Mon, 20 May 2019 23:17:50 +0100 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB4781.eurprd06.prod.outlook.com (20.177.63.219) 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 22:17:49 +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 22:17:48 +0000 From: Thorsten Altenkirch To: Bas Spitters CC: 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///yOACAAAcWAIAAKzqAgAYvPACAAAqdgIAAC3o6gAAXbwCAABIVgIAAFHzt Date: Mon, 20 May 2019 22:17:48 +0000 Message-ID: <4CAE313E-7B00-41D3-A13A-3AAC0A496AB0@exmail.nottingham.ac.uk> 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: 0f0c89c2-325b-4436-9198-08d6dd70fe10 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:VI1PR06MB4781; x-ms-traffictypediagnostic: VI1PR06MB4781: x-ms-exchange-purlcount: 6 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 004395A01C x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(39860400002)(346002)(376002)(396003)(136003)(189003)(199004)(51444003)(73956011)(66946007)(66446008)(64756008)(66556008)(186003)(66476007)(25786009)(91956017)(26005)(33656002)(74482002)(76116006)(83716004)(71190400001)(71200400001)(6436002)(68736007)(229853002)(82746002)(6512007)(446003)(6306002)(486006)(6486002)(2616005)(476003)(6916009)(7736002)(305945005)(11346002)(14454004)(53546011)(6506007)(76176011)(55236004)(102836004)(86362001)(53936002)(99286004)(6246003)(5660300002)(478600001)(6116002)(3846002)(54906003)(256004)(966005)(9886003)(81166006)(81156014)(786003)(5024004)(14444005)(2906002)(8936002)(316002)(8676002)(4326008)(66066001)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB4781;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: VGDlUFARuZRma6k98X1gu6hi2PCAVM+9rkSu2VBL945JO/bPBROrV1UwbPNy7XiF4S0f9AOr8ibxKWPq8sT/OBkcGPNquw0C7baGj+wP/o0spvwoDKGSmDYRXeMfeyTubYuw6HEiHl826xrl1OcoTN+yXR4s7//UwoC1326IryeL/uXZvGTlDDE1Jz8+18KVXIpoqmtdlVv9L9gYkKmEX18dAQK20I4rMXh54CgQ6QMUMm4XCwnstRcqPLw04/iUk4NNA3iZStWp0hxNAI/NfVAMGalRLyuXGX4sa/RwdH41DCLxwWGMQxM3U4c6ernZ6r6FlRnH7Xztzztx4898G+LtskAKSUXXDIy7Nk0YzGRlso0MrnT73ARvtW44CkApYtsOkvx/ub95fZXDXEfAGMu+i/bu+KTRB7wr61KpYB0= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: 0f0c89c2-325b-4436-9198-08d6dd70fe10 X-MS-Exchange-CrossTenant-originalarrivaltime: 20 May 2019 22:17:48.6369 (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: VI1PR06MB4781 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.124 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: , What exactly do you mean by =E2=80=9Ca model=E2=80=9D? I=E2=80=99d think we= can interpret them in cubical sets using the general construction of HITs.= They don=E2=80=99t seem to cause problems in cubical Agda as far as I can = see. Sent from my iPhone > On 20 May 2019, at 22:04, Bas Spitters wrote: >=20 > Do we even have a model that would capture all the QIIT constructions > in the HoTT book? >=20 > 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. >=20 >> On Mon, May 20, 2019 at 9:59 PM Jon Sterling wrot= e: >>=20 >> Hi Thorsten, >>=20 >> I think that in the way I interpreted Bas's question, setoids probably d= on'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 w= hich are a special case of infinity groupoids, but what people are wonderin= g is probably more along the lines of whether there is a model of type theo= ry 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 somet= hing 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 questi= ons 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 where 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 wrot= e: >>>>=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 (Th= m 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 p= rinciple? >>>>>=20 >>>>> Mike and Peter show that there are QITs which aren't constructible fr= om quotients. However, we may still be able to justify a type theory with Q= ITs without using them. E.g. in the Setoid model we can construct many QITs= including 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? >>>>>=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 Gr= oups "Homotopy Type Theory" group. >>>>> To unsubscribe from this group and stop receiving emails from it, sen= d 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.nott= ingham.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 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 >>> 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. >>>=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/b704d949-bf4b-4898-bee1-594cc7343de5%40www.fastmail.c= om. >> 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/msgi= d/HomotopyTypeTheory/CAOoPQuSYrG-u-i7jTvRHr6usa-PhMWs0SvD2HuMw0__z5DMPwg%40= mail.gmail.com. > 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/4CAE313E-7B00-41D3-A13A-3AAC0A496AB0%40exmail.nottingham= .ac.uk. For more options, visit https://groups.google.com/d/optout.