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-qk1-x73f.google.com (mail-qk1-x73f.google.com [IPv6:2607:f8b0:4864:20::73f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ca163505 for ; Mon, 16 Sep 2019 16:18:30 +0000 (UTC) Received: by mail-qk1-x73f.google.com with SMTP id q62sf541073qkd.3 for ; Mon, 16 Sep 2019 09:18:29 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1568650708; cv=pass; d=google.com; s=arc-20160816; b=KUldxwGQQ8gxrdLUGsGrGdWvFbeqU12OsGUs21tU+jUiL1miUMxfF60QZwPc16mX/V pGV+hOg3n8Yh67tE62ak9u/cEyuLLDX8LcCJ2LL7xyyBPPmiu+wvY13EMLbofFWgHBrC TV6/x/3S0a/n2bZzK427aHcFaGpDVEticBiD523M71+g4/8V2Hg+3Q4kYrvKXJ5LxRFj RjWY7LW7Igo36baxCmvp3UIlGDnQjvDFyYQl0opmFAYo2F4b8MAvyRFXIelKlTBq4NdX GPuqY67XP72w+ANRPjbMv3WR+2qFQUai9tD9ZYe1IP3xK2I3IbLUmHx/Xd3nJlhy2Pr/ XtMQ== ARC-Message-Signature: i=3; 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:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=Kzf7LohCkdqj8Wk4XYbTW8JKZwLtRGomvmPvxsGCYA4=; b=Y+3xC9h6N1LOKmiU+VKIVn7TwymsT+H5/ZcVdA+1EN0+gQrOwJmt9Zctk6pkCWsEyO 39DYUlQciNehu8HqQ4ns0vs7B85G19Hv2h37+tZ2m+6fOZxH0msrloO9/Q00SPDHCVHr Sx0Ih/Rxiaj0l6RUTvY6tW1kbdWbwek9l5V4mAKPWj58A4iSDYDQ1hxOg1sEBsT0o4ky kul6owG3kcHNlyJwSY938pFpYz3SYwc40hJgRWY+XiPDQwotgz9K3mzlVNdLYeKNRkIU mh4PGmWdQIp4MHMBrGB+8d4NCbDBvFNQTQaZXMLHiDdssaLvxLPhOzBzXpbUYvaaBybc dHvw== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=TZGpCPa+; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.76.102 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu 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-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=Kzf7LohCkdqj8Wk4XYbTW8JKZwLtRGomvmPvxsGCYA4=; b=PldI9117ghaVE1wVl5FbDOOXPnWLg6zEHmF7C9flUdtRmjkEpBwnRtzqebfzo2xiZM JxDrmikLqXQB80vo/aVt14nMLanQxt3UAy4om4ZDued+x8gFSa5+nnkf+qZEC+vRqEQe lavxqN3S6wDj7U6K11R75+EuWUJzbT4KqlsBS1N4L3K8tCRJ3xZJXxNjSyY1Su5fh41C OxOXU5rAO+jZ6wI4Pua2gshV4RNT53OGcX2yxC2CwqM+9cYGyppiKoUk6iIru7oPNDoU OBoduXkM7mdyGynBCi+NDNLR9vsWeyRdmGE4T+ZiKdmF+EO2L2py4aMKjiMowvS+hwFZ +RLg== 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-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=Kzf7LohCkdqj8Wk4XYbTW8JKZwLtRGomvmPvxsGCYA4=; b=rhkyCfoxvb+hrG2VxxdPgJ/8rRGqTtWubJ4kae4J2MBDyKgi5Rq8io0rmZwaIIgGpE PZ76vEZeFHmbWNnX25gbZPJKUPmRxO523cKTBR57/0aP6OrKqx/nkVdOpGzp8UxjVL41 lQR8aVUObjq1FiVA52dNQbwdUWLfUHotijFFSEjkvBlIXo2d1YQV2YYOGOlKldL5wOOq uXzolprUZdM8J6cMzg6MDxfk1FlBDFzrtHkLM8JRrfnH96nqgeLvMy6AJovsHrqeAMEp iJPtEwOGKFlhBp9Z000s4Ky837CyDth6LoowYY9z+pa1odZu9IOeh2HtUQeBBJIMpwvf FwaA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVOlXLYIMdRPCkgkD9Vx+1TN4uJGSv/hiaDIzwpUW67fTwozXgF jQe37uBmDg6nvnrWt4ZAOY0= X-Google-Smtp-Source: APXvYqwndkm+2rEjoUFcgPrLgh1YlgyxAFs+MTMWk2qfZLCOx0nTAZzjvE7aHOpkK+wJ+DWrPP/3TA== X-Received: by 2002:a37:4ecb:: with SMTP id c194mr827278qkb.126.1568650708308; Mon, 16 Sep 2019 09:18:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:a209:: with SMTP id l9ls185139qke.14.gmail; Mon, 16 Sep 2019 09:18:28 -0700 (PDT) X-Received: by 2002:a37:a946:: with SMTP id s67mr824398qke.470.1568650707986; Mon, 16 Sep 2019 09:18:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568650707; cv=pass; d=google.com; s=arc-20160816; b=ZkOIIJDd2X805FTB2GhTZcEhljuX6yOwdEnLdWfAkDMaEnS9I3tnLrfQHN+Y/1aOG+ iWOp9640LjBq/Da15/+PaDv2KjQfosbE/QGu/fimB7C1VuL50oBOnzyqn2RIt6ocuKbt GenZYUDMkZdH1kIMHV7yBEXv89el6tSNxLZGIHOY3NiK1ettEbBCQCi5A1Ana1uYDU50 qleT8m1eT+aZscdoU6jcjBO3bnm0H7/OVcaFHd5iMw/pClF/wkdhFLGaK+lg5IptDnsE d0K3E14atbpYA+ZPSU3Z7VC/2R1l0F3tmMsTbGDG7OhfDORcZ+1/QHeb8mCJtYPKSl9F s6eQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=sphqaXCBwOoqcRQJV8vTO2U/brH4yDQMfcqbN1AMjtI=; b=IRT2jm7DrXz2KIWtAGi+REOV3yukFpFx6QPQi/5n2UfWJi8mYmf3CzqGi2DBzQVFLU sF1q6PDbaTFxOiZselq0ozVj/i8mzZGP7alRCX5LuDKkyHXugYP0kjgxeTpVKxwM0TB4 /lU2p+Ja8b1nAtCAhFgb04y/ov9b9zsmnuCVCaL2zjLd9NB6QpXY5rg5UiE5luTlv2Cs o2hi5hA4QwFIjOCJMI71yT8lEyRoIGVreIZib1Hm7YRkI3kx972UoJsclcSywqj6yCWb smAoM7Vu1HyBHdCsVoXddygQlN3MeA1ueIvDcEBww4rAZ7smsys27YjYQW7isI00QTxR 4r0w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=TZGpCPa+; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.76.102 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM02-CY1-obe.outbound.protection.outlook.com (mail-eopbgr760102.outbound.protection.outlook.com. [40.107.76.102]) by gmr-mx.google.com with ESMTPS id u44si113905qtb.5.2019.09.16.09.18.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 16 Sep 2019 09:18:27 -0700 (PDT) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.76.102 as permitted sender) client-ip=40.107.76.102; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=bLAjl3PGhCJW4oR4Bswc7G7DIPdFtdnDQJNAQVLfyI0v21YfhGm9bnWYevhhrMR5XLvp+IMpLVD6c2X/2sNgx6Ily5YfZvbiDm3gBtJn2r+uCPt+l6pr96l9n4E2lGVoeczb7oIjTSjldLBeXqxYAHCQhfUPjmr0fwekHnl/Xcd/qKNfVOKDV4ZtJjvCBMD9ibbH1LeL055JmzZGSj3B/Bq4ABxfhyf2FsctFTrfqXeH/JZPrYDe7BI9tOclGd6X0JrRpREtUY3YWQbKcOs60FvnsNhbCc29vfPzSBrcgqIUiYHezrY1FfH+zmXalTLSQ+7EOu8BnF86shoQHEJ1oA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=sphqaXCBwOoqcRQJV8vTO2U/brH4yDQMfcqbN1AMjtI=; b=kIaBJ/rI/CCbXfKCIs28Ah5HdR5vdw8uuPPLYZ+P/F4CktT97A30aD2YXdhpU5v/AqHaJGm8dhkR8uDH23uRJ+U5QOVhi57wIfZR91W283ra4A2oqZNw0zBAhdSNSumsUGVL0Hfxs9Mx7KRZiAtroeZsBFDmNaxtythqguvuJN1kDqwx9sVMUGP8/e6BryxQfWtvhxVxSe3ZPdyi8DVVthC4d4mZ/8L+uT/50tulmA9CCH9Sn3hkqRkXvIC703vfI6HkRVjxiT7rzhfG3S490LPidji5QrG9EX30pKJMNoHdIkx/nLi+KMwuCAunATO4kC7BRjcQmcorpZERjIMz9w== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=wesleyan.edu; dmarc=pass action=none header.from=wesleyan.edu; dkim=pass header.d=wesleyan.edu; arc=none Received: from BYAPR04MB4597.namprd04.prod.outlook.com (52.135.237.151) by BYAPR04MB5175.namprd04.prod.outlook.com (20.178.52.11) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2263.23; Mon, 16 Sep 2019 16:18:26 +0000 Received: from BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4]) by BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4%7]) with mapi id 15.20.2263.023; Mon, 16 Sep 2019 16:18:26 +0000 From: "Licata, Dan" To: Jasper Hugunin CC: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] A question about the problem with regularity in CCHM cubical type theory Thread-Topic: [HoTT] A question about the problem with regularity in CCHM cubical type theory Thread-Index: AQHVbKpe711HRq+Kj06GbYpV/1lFtA== Date: Mon, 16 Sep 2019 16:18:25 +0000 Message-ID: <10B7D7E9-3155-4FA0-90E0-BB6BE2C37B1B@wesleyan.edu> References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: f0e83af4-33cb-4149-61eb-08d73ac180cc x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(5600167)(711020)(4605104)(1401327)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7193020);SRVR:BYAPR04MB5175; x-ms-traffictypediagnostic: BYAPR04MB5175: x-ms-exchange-purlcount: 5 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8273; x-forefront-prvs: 0162ACCC24 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(4636009)(346002)(366004)(376002)(396003)(39850400004)(136003)(53754006)(199004)(189003)(6512007)(6306002)(99286004)(446003)(6916009)(86362001)(7736002)(316002)(305945005)(786003)(2906002)(6506007)(6246003)(476003)(102836004)(2616005)(53546011)(186003)(2171002)(26005)(11346002)(5660300002)(76116006)(91956017)(76176011)(66446008)(64756008)(66556008)(66946007)(88552002)(66476007)(53936002)(3846002)(6116002)(8676002)(486006)(81166006)(71190400001)(81156014)(256004)(6436002)(6486002)(71200400001)(8936002)(229853002)(966005)(14454004)(33656002)(36756003)(25786009)(4326008)(478600001)(75432002)(66066001);DIR:OUT;SFP:1102;SCL:1;SRVR:BYAPR04MB5175;H:BYAPR04MB4597.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: JC99FTIdA2Vz+IX1IceZKim5/4ykPmBoh839mscxg0kKVd6oDRsMdkz+L8b8F5S76VCuJKFkPV/BA4SoNXDcEia+aWhmur3okaokGaeFnXn5ivwHfy1XVJwTUQJcSyQRD0jGObUYUS8iWqzgMbo+gbhWJ+XXvUN74HIQLHLl16HRmpWRNwKE5gn4V0bBbs3UmRPRaiDcC+mToWP2qxOWkyOH6GonfHysbHlfZDFLkSo7STv5gpwYWKheiVD0cseliH7gyEZaYnaZhu73syzDruY1vf9C3bQOnfEczqxYyaac/o5ds5x6vbdzcmzN/vb7V159caJKDFY6qMuzyrgxEnbIehl7Vb64rH3b1Srz121pw7x2hj6d5nv86rxGUgbV98RJ+AP4ZsABe9QivVaEn5/cNFR7WJmBOvMvavs7Mkc= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" Content-ID: <33D78BD4E44A7E48BE3171E6AB9BE13C@namprd04.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: f0e83af4-33cb-4149-61eb-08d73ac180cc X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Sep 2019 16:18:25.9262 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: xEmcW7pPuHUj3kjKTMQJvHc25Towd4PPIcEERTwF5PdqtGW77WTxwtlS6c/Y0OEOjZRRwh9WBPqIafKhj9ccug== X-MS-Exchange-Transport-CrossTenantHeadersStamped: BYAPR04MB5175 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=TZGpCPa+; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.76.102 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu 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 Jasper, It would help me follow the discussion if you could say a little more about= (a) which version of composition for Glue exactly you mean (because there = is at least the one in the CCHM paper and the =E2=80=9Caligned=E2=80=9D one= from Orton-Pitts, which are intensionally different, as well as other poss= ible variations), and (b) include some of your reasoning for why you think = things are regular, to make it easier for me and others to reconstruct. =20 My current understanding is that - For CCHM proper https://arxiv.org/pdf/1611.02108.pdf the potential issue = is with the =E2=80=98pres=E2=80=99 path omega, which via the equiv operatio= n ends up in alpha, so the system in a1 may not be degenerate even if the i= nput is. Do you think this does work out to be degenerate? =20 - For the current version of ABCFHL https://github.com/dlicata335/cart-cube= /blob/master/cart-cube.pdf which uses aligning =E2=80=9Call the way at the = outside=E2=80=9D, an issue is with the adjust_com operation on page 20, whi= ch is later used for aligning (in that case beta is (forall i phi)). The p= otential issue is that adjust_com uses a *filler*, not just a composition f= rom 0 to 1, so even if t doesn=E2=80=99t depend on z, the filling does, and= the outer com won=E2=80=99t cancel. In CCHM, filling is defined using con= nections, so it=E2=80=99s a little different, but I think there still has t= o be a dependence on z for it to even type check =E2=80=94 it should come u= p because of the connection term that is substituted into the type of the c= omposition problem. So I=E2=80=99d guess there is still a problem in the a= ligned algorithm for CCHM. =20 However, it would be great if this is wrong and something does work! =20 -Dan > On Sep 15, 2019, at 10:18 PM, Jasper Hugunin = wrote: >=20 > This doesn't seem right; as far as I can tell, composition for Glue types= in CCHM preserves regularity and reduces to composition in A on phi. >=20 > - Jasper Hugunin >=20 > On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg wrote: > Hi Jasper, >=20 > Indeed, the problem is to construct an algorithm for comp (or even > coe/transp) for Glue that reduces to the one of A when phi is true > while still preserving regularity. It was pointed out independently by > Sattler and Orton around 2016 that one can factor out this step in our > algorithm in a separate lemma that is now called "alignment". This is > Thm 6.13 in Orton-Pitts and discussed in a paragraph in the end of > section 2.11 of ABCFHL. Unless I'm misremembering this is exactly > where regularity for comp for Glue types break down. In this step we > do an additional comp/hcomp that inserts an additional forall i. phi > face making the comp/coe irregular. >=20 > One could imagine there being a way to modify the algorithm to avoid > this, maybe by inlining the alignment step... But despite considerable > efforts no one has been able to figure this out and I think Swan's > recent paper (https://arxiv.org/abs/1808.00920v3) shows that this is > not even possible! >=20 > Another approach would be to have weak Glue types that don't strictly > reduce to A when phi is true, but this causes problems for the > composition in the universe and would be weird for cubical type > theory... >=20 > In light of Swan's negative results I think we need a completely new > approach if we ever hope to solve this problem. Luckily for you Andrew > Swan is starting as a postdoc over in Baker Hall in October, so he can > explain his counterexamples to you in person. >=20 > Best, > Anders >=20 > On Sun, Sep 15, 2019 at 7:57 AM Jasper Hugunin > wrote: > > > > Offline, Carlo Angiuli showed me that the difficulty was in part 1, bec= ause of a subtlety I had been forgetting. > > > > Since types are *Kan* cubical sets, we need that the Kan operations agr= ee as well as the sets. > > So part 1 could be thought of as (Glue [ phi |-> equivRefl A ] A, compG= lue) =3D (A, compA), and getting that the Kan operations to agree was/is di= fficult. > > (Now that I know what the answer is, it is clear that this was already = explained in the initial discussion.) > > > > Humbly, > > - Jasper Hugunin > > > > On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin wrote: > >> > >> Hello all, > >> > >> I've been trying to understand better why composition for the universe= does not satisfy regularity. > >> Since comp^i [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> eq= uiv^i E ] A, I would expect regularity to follow from two parts: > >> 1. That Glue [ phi |-> equivRefl A ] A reduces to A (a sort of regular= ity condition for the Glue type constructor itself) > >> 2. That equiv^i (refl A) reduces to equivRefl A > >> I'm curious as to which (or both) of these parts was the issue, or if = regularity for the universe was supposed to follow from a different argumen= t. > >> > >> Context: > >> I've been studying and using CCHM cubical type theory recently, and of= ten finding myself wishing that J computed strictly. > >> If I understand correctly, early implementations of ctt did have stric= t J for Path types, and this was justified by a "regularity" condition on t= he composition operation, but as discussed in this thread on the HoTT maili= ng list, the definition of composition for the universe was found to not sa= tisfy regularity. > >> I don't remember seeing the regularity condition defined anywhere, but= my understanding is that it requires that composition in a degenerate line= of types, with the system of constraints giving the sides of the box also = degenerate in that direction, reduces to just the bottom of the box. This s= eems to be closed under the usual type formers, plus Glue, but not the univ= erse with computation defined as in the CCHM paper (for trivial reasons and= non-trivial reasons; it gets stuck at the start with Glue [ phi |-> equiv^= i refl ] A not reducing to anything). > >> > >> Best regards, > >> - Jasper Hugunin > > > > -- > > 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/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAcAefiTg4JJVHemV3HUPcPE= g%40mail.gmail.com. >=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/CAGTS-a8SZx8PiaD-9rq5QWffU75Wz8myrXD1g5P3DCjSO%3DfvOQ%= 40mail.gmail.com. --=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/10B7D7E9-3155-4FA0-90E0-BB6BE2C37B1B%40wesleyan.edu.