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,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pl1-x639.google.com (mail-pl1-x639.google.com [IPv6:2607:f8b0:4864:20::639]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 401e93c9 for ; Mon, 16 Sep 2019 19:01:28 +0000 (UTC) Received: by mail-pl1-x639.google.com with SMTP id m8sf394665plt.14 for ; Mon, 16 Sep 2019 12:01:27 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1568660486; cv=pass; d=google.com; s=arc-20160816; b=qHpJYjIZX/hSNfl7vezTPCG6sshsUYIW2wbozvEcmD3iWmsAblIuyaWmB81a4B/eKF 8KovYIH/gdw/OydDtxb3Np9NauFrKC9LcjH5HD7zei/ZXzAv5Xw82XZ5qTAe3QQxpAMP qjOgdIZ1XaRv3g2qH1i0ASctVB/ueEPtR1EEc481b1YxDxoxLwVYI8dLLCyjqXMoeuOk awS47WnpHJOrUAX7In0f7nMvnMM37JKnpNlrGGP4XcLVdERhpFE2j1EKvEjCDIs6wNMh zv64hgJH/RwLZ3tUmfYtlBcnXNZQ6oJT+vOjXwWW8B83OS2ZU5ocHUb4vqCQ1r8LeLYM JH6Q== 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-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:sender:dkim-signature; bh=PNOuBYdUzGTF52gY+YNGuvrUeeuGwtzGt/ifHoeKgUQ=; b=EdFsjXVl7o3nYQ7eQX0U2kKoocGZDX5MPZU5H3N4YP8a/knz8bMka1m/V6ya36YV+k bNK2ifh2weOwOcsC1U9Sn7qKbF4O07tJJKetMnNIVC9+YyRU1Jw8ypskSr0Z3sb3OtPN uOzFRkvJ/Fv1kSHAIDD+BoVbZBHfCxjddzCBcF/NrS5M+Hgt31BscLvbijOS6SKBN6Dw krO+gjgwGbKDZRP9Jk3dmhH0RZw3mlfAzHGagNBr+oE5kkceiPURtyt6HQTe6Q6F5Mwm 2W/mKpdWnHZai5hbJvKpsvtTZelG1fnWaVfMDDHhlpU3S608NSknxItxOdnfcv5pXLm7 RLeQ== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b="IsxA6z/v"; 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.71.127 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 :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=PNOuBYdUzGTF52gY+YNGuvrUeeuGwtzGt/ifHoeKgUQ=; b=BTJ9G6yc46+MaLihCaAdtayEUu87Oz9oUNFtWhC/60jIrIvzSvnq0EmHt1nWBWRHSE KGXqQVUcJwXj67KURi8xUimusq0hB7rPppmGMaP7Iw+mPX2pCyo1/8FFVP/WqN6Qdj5v vOMrvq9XUmD0nQ1BZcfWb8tZstvEjMMMN6KD6lkci7pEnkfhMguvsuFr1zxAtuejiaV3 SAieryWrXLkzEKPSpWCzPL1Ra9oN7OX1LwHhM7bS/V16VYWpfHji7ds6CLwl2T0at+hp w9agh5C/yeBaIhx3dOBtYk81P/RtEWrngW1WpGGyEL2o/F8mlKsJVvZbwdNi1y22tRrj VrNw== 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: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=PNOuBYdUzGTF52gY+YNGuvrUeeuGwtzGt/ifHoeKgUQ=; b=t1xp8TYZX+9TZwiB0u+f9hqadblTvNNq0CBu+FyCi7OXXIkrXiU/sJ0mCbxqgsRVpq lqwlrcCrkUT82zqQa7psMwDyQ1O2UfQMN+zcyUIjmLL3XZX70lO6Dch56e9YpNJmeArv JjU2YLhoc/AlfQdpUr22chRdS3CoqdVcb/4ztWQLdEyRO5AEfMYNGePcpj6L1rk3cnKQ MQE06mL+VkgbrASRWhhcHNFPyqslDMRLRX6kxJ+JKhTW9bz6vXvOEQT5nXW4y5J9A6Xq JH7zYFdhf6N7M1D4V4OLK2X8dizq6JMvWXnWpcbDqrzkWC8kWprgcjlLYPL+kMtwfu79 hkQg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW5HteEen1RTNXy3C9hQoP1HnC4Jbbx2GeqJaqPfspnhYaua3QL 2D8iwCEhNBtwYXbUcJ4H/wE= X-Google-Smtp-Source: APXvYqx+Aw7bf/AYeIRh2VZimiTYHPs9H3bEzwaReZPLgniNwLw0N1JQnN4kIINZWzeVNPw/XaIUuQ== X-Received: by 2002:a62:ab04:: with SMTP id p4mr844742pff.227.1568660486334; Mon, 16 Sep 2019 12:01:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90a:2766:: with SMTP id o93ls92679pje.4.gmail; Mon, 16 Sep 2019 12:01:25 -0700 (PDT) X-Received: by 2002:a17:902:6b07:: with SMTP id o7mr1357524plk.215.1568660485586; Mon, 16 Sep 2019 12:01:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568660485; cv=pass; d=google.com; s=arc-20160816; b=vGwNVSeYVGKGGz7UMsTr/h+ZOJM7lhmeLRHEeSI+8jX+qsHqN8DcuI/TzBlKnLVbwc y+cfVmGVVrwEdOgHi0MxsUi0F0bRZAvyyJ4tnr+VF2Fq7p+yhpywBMecQHEjbvA7Ny3Q SBpHN7qZxjIXLoetxSzO0fqUahb1AanYHy2wByEwYYTFfNI7DmrdTAhLN02SXcU7HTa5 BKUD9XvsHeHatbFbKYBE4GySiA4i/50Br7cKOKd8X9VAR8bROoGnOoh6Ti+6JLlfOx0R et/xkb+rwGY52EdOuJ8FI/+YhfGFvFcxFUwDZQbO4J00XolfU3jb0E4RTztsJjdqZUIl Tenw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:cc:to :from:dkim-signature; bh=n5lwfmROYKDxqgrjHSec3/pGV3sNMYo9oFiYFD+gegE=; b=DuTmQA1BjZIrSkPMgzLT14ZQzp1asP2Usg+snulcOkD0YyvbPl3abLODo1d3aFVJHe js4VkD4f6hPM2dYCMxWgQkQuHBRpqZHyuBXXAE/UiB669QjqdutMTwS3HYdnNi/xGF41 i2Z3u+01PGjjHrawaNpnKbNaD7FzG58qIa3RlUbqe72jzYwKJKIGtyBkrHuL++/7ABOh FrpFwJsb7x7VpzYQXSPovXshFnahHBMx+tVAbgfbuInB2y1tMCWi6WRgg889eweGscFS b7yl7aGs37fIAoZc8EKecDM4/alRXmUQJcddhuL3DgTX0wBh6AHUTovAnTl3pR/RlcFW JHaw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b="IsxA6z/v"; 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.71.127 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM05-BY2-obe.outbound.protection.outlook.com (mail-eopbgr710127.outbound.protection.outlook.com. [40.107.71.127]) by gmr-mx.google.com with ESMTPS id b64si95625pfg.0.2019.09.16.12.01.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 16 Sep 2019 12:01:25 -0700 (PDT) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.71.127 as permitted sender) client-ip=40.107.71.127; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Fyn5bmT3Dbj9Kwffu9uRC0QniTyo0eTewaVX6/Ln6DnXSJrTDKPkkAoqBfo9dc90m67CVeYI8nT5p7cSvbh5+1SY+hD1f+1cR04Mpi33TEQdnpFeXUWNZOT48zhOBPO2fPASNKiZqP+hwvChAX20a0UUOVP3skEoTS576C6HU1D0ETdPogWWTF13oOC8HyQmH8tId7SqoQAE1cyInFV9/BjKpzLBlD4j8xjEUCwela2zC+iIdLORviQwMXSIttwNfpwHgwDvHlRYrJ64OAkIi7JDi1p/yi4PLhMDH3uqRvcflHRuGdZEgzqO4Fpq9QttEqr5OqccW6Tn6gOPgo93pg== 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=n5lwfmROYKDxqgrjHSec3/pGV3sNMYo9oFiYFD+gegE=; b=etu8Als+zKanm0GNk+P7lszgOfXmgZjr1nTNzwJyqZJPFvT5UTW/Q1P66ef7vcDqfS2qeTmuRnQBQ7qBEJJT8NTrSsOLR7X2T3iXOycC1zFFdFyu/ry5rZZO0VfzCJD5Ep4pg2GnN7ToUGr+LB3byx0DMbAIbPZvd0aTNQJ/MFERvKca1xN3EygeP6rIx9MHXOGtE/xmfymEhsShU7UTVB39TEZIq+uHXBfwZoyIv2NqPyrgAZ6+YsZVZFczqZXCzqg1pUxtgMBqZ84/2nPOxyKbMvO0JnUtDgxmy8TiLtQHxSRCY0/wxneXrKY+q8F5X1iqWDNGeu/kYjhHFz4lHA== 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 BYAPR04MB3814.namprd04.prod.outlook.com (52.135.214.145) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2263.15; Mon, 16 Sep 2019 19:01:22 +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 19:01:22 +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: AQHVbKpeBzI9iCM0iEKTQD21NankDacuiawAgAAfQbI= Date: Mon, 16 Sep 2019 19:01:22 +0000 Message-ID: References: <10B7D7E9-3155-4FA0-90E0-BB6BE2C37B1B@wesleyan.edu>, In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [2600:1000:b10a:8d55:b83e:c844:fad5:63f1] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: e60f7128-fe08-4dcc-4f07-08d73ad8440f x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(5600167)(711020)(4605104)(1401327)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(2017052603328)(7193020);SRVR:BYAPR04MB3814; x-ms-traffictypediagnostic: BYAPR04MB3814: x-ms-exchange-purlcount: 5 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:5797; x-forefront-prvs: 0162ACCC24 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(4636009)(39850400004)(396003)(376002)(346002)(366004)(136003)(189003)(199004)(53754006)(478600001)(6306002)(66476007)(66446008)(2616005)(64756008)(66556008)(81166006)(8936002)(81156014)(99286004)(86362001)(8676002)(71190400001)(71200400001)(88552002)(256004)(5660300002)(7736002)(66946007)(54896002)(6512007)(236005)(11346002)(486006)(476003)(446003)(186003)(46003)(102836004)(33656002)(53936002)(30864003)(14454004)(76116006)(966005)(606006)(91956017)(6506007)(53546011)(25786009)(75432002)(6486002)(786003)(6436002)(76176011)(229853002)(316002)(6916009)(4326008)(2171002)(6246003)(36756003)(2906002)(6116002);DIR:OUT;SFP:1102;SCL:1;SRVR:BYAPR04MB3814;H:BYAPR04MB4597.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A: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: k56ipsR/OmslNW3Dlo+wKHtcsREm0b7BRKidE+qpWnT42FYxCUv16fA+mnyhhPJcZooUhenutO780xOQImMMZ3ndDgqzYa9JYBxF6N6ZY7njockkgN2fp9gMp0iLaYUze0HhW/XhgZ1YoVnXgX1ln7ekFSQIyg5jFKvHkVtLp1IiSgrp8RW8oqX/8mN933hd1taYbx3WAXSBpQsUBQutEj9OYhNp7J4tMYWOcS9x4Ybr8eWtAx7BlCHnAyi/o4xv2Hv+owQIqouuKNhj6CJW9b2I/Vh9ttP5+C6aV67ueVMCWk02LkYsw+O/1EXOvqpgEoIVvygsZrdxfIsU5+eQR0Rsf3kGxV9kJtjaUVOb8IGzeLcc3k02yrFEZIDK54bkSAAQWmukgmak6gGz0ICMHuBqLjMt5DZLBlqI/A/L4Nc= x-ms-exchange-transport-forked: True Content-Type: multipart/alternative; boundary="_000_CB28E4E173EC4405A268350D028A0C93wesleyanedu_" MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: e60f7128-fe08-4dcc-4f07-08d73ad8440f X-MS-Exchange-CrossTenant-originalarrivaltime: 16 Sep 2019 19:01:22.0718 (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: ZKy7aXeje4nHc1sdFfOQuDTp0VGN9J+3GHQX5kuVxO258b/JzrgRCqKczk8eNxQzH97PgrAhPhkxADkH6YO3+g== X-MS-Exchange-Transport-CrossTenantHeadersStamped: BYAPR04MB3814 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="IsxA6z/v"; 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.71.127 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: , --_000_CB28E4E173EC4405A268350D028A0C93wesleyanedu_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Wow! I read that pretty closely and couldn=E2=80=99t find a problem. That i= s surprising to me. Will look more later. What I was saying about fill for the aligning algorithm is also wrong =E2= =80=94 I wasn=E2=80=99t thinking that the type of the filling was also dege= nerate, but of course it is here. So that might work too. However, even if there can be a universe of regular types that is closed un= der glue types, there=E2=80=99s still a problem with using those glue types= to show that that universe is itself regularly fibrant, I think? If you de= fine comp U [phi -> i.T] B to be Glue [phi -> T(1),...] B then no matter ho= w nice the equivalence is (eg the identity) when i doesn=E2=80=99t occur in= T, the type will not equal B =E2=80=94 that would be an extra equation abo= ut the Glue type constructor itself. Does that seem right? -Dan On Sep 16, 2019, at 1:09 PM, Jasper Hugunin > wrote: Hi Dan, Of course. I'm thinking primarily of composition for Glue given in the CCHM= paper you linked, reproduced below. As you know, the single potential issue is that we need pres of a degenerat= e filling problem and function to be reflexivity. I claim that this holds b= y regularity of composition in T and A, partly as a consequence of the fact= that regularity of composition implies regularity of filling (that fill of= a degenerate system is refl), which certainly holds for fill defined by co= nnections (and I believe also holds for fill as defined in ABCFHL). (a) Given i |- B =3D Glue [ phi |-> (T, f) ] A, with psi, i |- b : B and b0 : B= (i0)[ psi |-> b(i0) ], we want to compute b1 =3D comp^i B [ psi |-> b ] b0 = : B(i1)[ psi |-> b(i1) ]. We set a :=3D unglue b and a0 :=3D unglue b0. Set delta :=3D forall i. phi. Then we take: a1' :=3D comp^i A [ psi |-> a ] a0 delta |- t1' :=3D comp^i T [ psi |-> b ] b0 delta |- omega :=3D pres^i f [ psi |-> b ] b0 phi(i1) |- (t, alpha) :=3D equiv f(i1) [ delta |-> (t1', omega), psi |-> (b= (i1), refl a1') ] a1' a1 :=3D hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1' (note that= in the regular setting the psi face is redundant) b1 :=3D glue [ phi(i1) |-> t1 ] a1 With given i |- f : T -> A, with psi, i |- b : T and b0 : T(i0)[ psi |-> b(= i0) ], we define pres^i f [ psi |-> b ] b0 =3D comp^i A [ psi |-> f b, j =3D 1 |-> f (fi= ll^i T [ psi |-> b ] b0) ] (f(i0) b0). (b) Now consider the regular case, where phi, T, f, and A are independent of i.= We want that b1 =3D b0. We have that a is independent of i, and delta =3D phi. First consider delta (=3D phi) |- pres^i f [ psi |-> b ] b0. (This is the e= xplanation of your first dash) Note that if comp^i A is regular, then fill^i A [ psi |-> b ] b0 =3D b This is comp^i A [ psi |-> f b, j =3D 1 |-> f (fill^i T [ psi |-> t ] t= 0) ] (f t0) =3D comp^i A [ psi |-> f b, j =3D 1 |-> f t0 ] (f t0) =3D <= j> f t0. Thus pres of a degenerate filling problem and function is reflexivity. Going back to composition of Glue, a1' =3D a0 phi |- t1' =3D b0 phi |- omega =3D refl (f b0) phi |- (t1, alpha) =3D (t1', omega) (since delta =3D phi, so we end up in t= he delta face of equiv) a1 =3D a1' (the only dependence on j is via (alpha j), but alpha =3D omega = =3D refl, so this filling problem is degenerate) b1 =3D glue [ phi |-> t1 ] a1 =3D glue [ phi |-> b0 ] a0 =3D glue [ phi |->= b0 ] (unglue b0) =3D b0 (by eta, see Figure 4 in CCHM) Thus this algorithm for composition of Glue is regular. Other algorithms, such as the one in ABCFHL, may not be, but I am prone to = believe that there exist regular algorithms in other settings including Ort= on-Pitts and Cartesian cubes. Best regards, - Jasper Hugunin On Mon, Sep 16, 2019 at 12:18 PM Licata, Dan > wrote: 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. 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? - 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. However, it would be great if this is wrong and something does work! -Dan > On Sep 15, 2019, at 10:18 PM, Jasper Hugunin > wrote: > > 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. > > - Jasper Hugunin > > On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg > wrote: > Hi Jasper, > > 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. > > 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! > > 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... > > 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. > > Best, > Anders > > 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. > > -- > 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/CB28E4E1-73EC-4405-A268-350D028A0C93%40wesleyan.edu. --_000_CB28E4E173EC4405A268350D028A0C93wesleyanedu_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Wow! I read that pretty closely and couldn=E2=80=99t find a problem. That i= s surprising to me. Will look more later. 

What I was saying about fill for the aligning algorithm is also wrong = =E2=80=94 I wasn=E2=80=99t thinking that the type of the filling was also d= egenerate, but of course it is here. So that might work too.  

However, even if there can be a universe of regular types that is clos= ed under glue types, there=E2=80=99s still a problem with using those glue = types to show that that universe is itself regularly fibrant, I think? If y= ou define comp U [phi -> i.T] B to be Glue [phi -> T(1),...] B then no matter how nice the equivalence is (eg the = identity) when i doesn=E2=80=99t occur in T, the type will not equal B =E2= =80=94 that would be an extra equation about the Glue type constructor itse= lf. Does that seem right?

-Dan

On Sep 16, 2019, at 1:09 PM, Jasper Hugunin <jasperh@cs.washington.edu> wrote:

Hi Dan,

Of course. I'm thinking primarily of composition for Glue given in the= CCHM paper you linked, reproduced below.
As you know, the single potential issue is that we need pres of a dege= nerate filling problem and function to be reflexivity. I claim that this ho= lds by regularity of composition in T and A, partly as a consequence of the= fact that regularity of composition implies regularity of filling (that fill of a degenerate system is refl), = which certainly holds for fill defined by connections (and I believe also h= olds for fill as defined in ABCFHL).

(a)
Given i |- B =3D Glue [ phi |-> (T, f) ] A, with psi, i |- b : B an= d b0 : B(i0)[ psi |-> b(i0) ], we want to compute b1 =3D comp^i B [ psi = |-> b ] b0 : B(i1)[ psi |-> b(i1) ].
We set a :=3D unglue b and a0 :=3D unglue b0.
Set delta :=3D forall i. phi.
Then we take:
a1' :=3D comp^i A [ psi |-> a ] a0
delta |- t1' :=3D comp^i T [ psi |-> b ] b0
delta |- omega :=3D pres^i f [ psi |-> b ] b0
phi(i1) |- (t, alpha) :=3D equiv f(i1) [ delta |-> (t1', omega), ps= i |-> (b(i1), refl a1') ] a1'
a1 :=3D hcomp^j A(i1) [ phi(i1) |-> alpha j, psi |-> a(i1) ] a1'= (note that in the regular setting the psi face is redundant)
b1 :=3D glue [ phi(i1) |-> t1 ] a1

With given i |- f : T -> A, with psi, i |- b : T and b0 : T(i0)[ ps= i |-> b(i0) ], we define
pres^i f [ psi |-> b ] b0 =3D <j> comp^i A [ psi |-> f b, = j =3D 1 |-> f (fill^i T [ psi |-> b ] b0) ] (f(i0) b0).

(b)
Now consider the regular case, where phi, T, f, and A are independent = of i. We want that b1 =3D b0.
We have that a is independent of i, and delta =3D phi.

First consider delta (=3D phi) |- pres^i f [ psi |-> b ] b0. (This = is the explanation of your first dash)
Note that if comp^i A is regular, then fill^i A [ psi |-> b ] b0 = =3D b
This is <j> comp^i A [ psi |-> f b, j =3D 1 |-> f (fill^i = T [ psi |-> t ] t0) ] (f t0) =3D <j> comp^i A [ psi |-> f b, j = =3D 1 |-> f t0 ] (f t0) =3D <j> f t0.
Thus pres of a degenerate filling problem and function is reflexivity.=

Going back to composition of Glue,
a1' =3D a0
phi |- t1' =3D b0
phi |- omega =3D refl (f b0)
phi |- (t1, alpha) =3D (t1', omega) (since delta =3D phi, so we end up= in the delta face of equiv)
a1 =3D a1' (the only dependence on j is via (alpha j), but alpha =3D o= mega =3D refl, so this filling problem is degenerate)
b1 =3D glue [ phi |-> t1 ] a1 =3D glue [ phi |-> b0 ] a0 =3D glu= e [ phi |-> b0 ] (unglue b0) =3D b0 (by eta, see Figure 4 in CCHM)<= /div>

Thus this algorithm for composition of Glue is regular.
Other algorithms, such as the one in ABCFHL, may not be, but I am pron= e to believe that there exist regular algorithms in other settings includin= g Orton-Pitts and Cartesian cubes.

Best regards,
- Jasper Hugunin

On Mon, Sep 16, 2019 at 12:18 PM Lica= ta, Dan <dlicata@wesleyan.edu> wrote:
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 possible variations), and (b) include some of your reason= ing for why you think things are regular, to make it easier for me and othe= rs to reconstruct. 

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 operation ends up in= alpha, so the system in a1 may not be degenerate even if the input is.&nbs= p; Do you think this does work out to be degenerate? 

- 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 wi= th the adjust_com operation on page 20, which is later used for aligning (i= n that case beta is (forall i phi)).  The potential issue is that adjust_com uses a *filler*, not just a composition from 0 to= 1, so even if t doesn=E2=80=99t depend on z, the filling does, and the out= er com won=E2=80=99t cancel.  In CCHM, filling is defined using connec= tions, so it=E2=80=99s a little different, but I think there still has to be a dependence on z for it to even type check =E2=80=94 it s= hould come up because of the connection term that is substituted into the t= ype of the composition problem.  So I=E2=80=99d guess there is still a= problem in the aligned algorithm for CCHM. 

However, it would be great if this is wrong and something does work!  =

-Dan

> On Sep 15, 2019, at 10:18 PM, Jasper Hugunin <jasperh@cs.washington.edu>= wrote:
>
> This doesn't seem right; as far as I can tell, composition for Glue ty= pes in CCHM preserves regularity and reduces to composition in A on phi. >
> - Jasper Hugunin
>
> On Sun, Sep 15, 2019 at 3:28 AM Anders Mortberg <anders.mortberg@math.su.se> wrote:
> Hi Jasper,
>
> 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.
>
> 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 t= hat this is
> not even possible!
>
> Another approach would be to have weak Glue types that don't strictly<= br> > 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...
>
> 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.
>
> Best,
> Anders
>
> On Sun, Sep 15, 2019 at 7:57 AM Jasper Hugunin
> <jas= perh@cs.washington.edu> wrote:
> >
> > Offline, Carlo Angiuli showed me that the difficulty was in part = 1, because of a subtlety I had been forgetting.
> >
> > Since types are *Kan* cubical sets, we need that the Kan operatio= ns agree as well as the sets.
> > So part 1 could be thought of as (Glue [ phi |-> equivRefl A ]= A, compGlue) =3D (A, compA), and getting that the Kan operations to agree = was/is difficult.
> > (Now that I know what the answer is, it is clear that this was al= ready explained in the initial discussion.)
> >
> > Humbly,
> > - Jasper Hugunin
> >
> > On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu<= /a>> 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 |-> equiv^i E ] A, I would expect regularity to follow from two pa= rts:
> >> 1. That Glue [ phi |-> equivRefl A ] A reduces to A (a sor= t of regularity 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 issu= e, or if regularity for the universe was supposed to follow from a differen= t argument.
> >>
> >> Context:
> >> I've been studying and using CCHM cubical type theory recentl= y, and often finding myself wishing that J computed strictly.
> >> If I understand correctly, early implementations of ctt did h= ave strict J for Path types, and this was justified by a "regularity&q= uot; condition on the composition operation, but as discussed in this threa= d on the HoTT mailing list, the definition of composition for the universe was found to not satisfy regularity.
> >> I don't remember seeing the regularity condition defined anyw= here, but my understanding is that it requires that composition in a degene= rate 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 seems to be closed under the usual typ= e formers, plus Glue, but not the universe with computation defined as in t= he CCHM paper (for trivial reasons and non-trivial reasons; it gets stuck a= t 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 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/CAGTS-a9oS0CQDGKgj7ghC= h8%2BZwAcAefiTg4JJVHemV3HUPcPEg%40mail.gmail.com.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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/CAGTS-a8SZx8PiaD-9rq5Q= WffU75Wz8myrXD1g5P3DCjSO%3DfvOQ%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;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/CB28E4E1-73EC-4405-A268-350D028A0C93%40wesleyan.ed= u.
--_000_CB28E4E173EC4405A268350D028A0C93wesleyanedu_--