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-pg1-x53a.google.com (mail-pg1-x53a.google.com [IPv6:2607:f8b0:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 17a20ca4 for ; Sun, 15 Sep 2019 22:38:46 +0000 (UTC) Received: by mail-pg1-x53a.google.com with SMTP id m17sf21005117pgh.21 for ; Sun, 15 Sep 2019 15:38:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568587125; cv=pass; d=google.com; s=arc-20160816; b=xnIeMw/IVr+UgnPM2lUiBGg4+yOCYZ1I0zT2WiutiRbRppkkU3RZ1jTkbE6omfEucP YNruUU6oQVr336tL+W/VnFPBWwapnxUo+/93uuV8zCmEARpfYaPOtwXy5KaJh4zM11AD +vsOh/Ztt7UoIu78zXBum/Dpgh67g6dOgMulWuBEcrXz1JueP1mlLf26JwP3BGQlJyhL HIwbbfHRfwqPwoJPopEAVlXZIVZteHbrywXAH0iiW/8ZdrVBuJKV/mA7TZUsHg+apiPs moLgFL45qUEDgezYpXeGDjTnjUlWsENQ0g8Gx0mI9y3DXJqvmJhSSO3ofIUQgedcXkiT 7r/Q== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=5FozyxqOnj8L4B/O8/0Zwf5+D/VD7U/hc34ITl2NJHw=; b=gimH2M/TGgmdFrlDu4NmjnB+ISi7VcvDdmWgKfQYFuCiDpXCzvHN0c57Argg+CZTlu JHjOiHkE62kdLRtRjaK3Sk6QOsXlI1oV2V1y2uS0kCCcYHFtSVJZLYeuM5haRy6ZtlJg xXNpEiI+C5SqnRZPpYSqxhfHGPRazMPrRoN77/nFyLH+M5gQzLybtTEV17iIuwrtBBGg geS5nKszHas5sOOQ3Dc9yeJH7CNAStxDM/CLwZZcscI4UG8yVlStJ00PV7aK1PJKbNvu NIxnqty06GZMqHhWAT3dk/GuIRJgiAh/1qxdy8jPBzoZ5kSIF7+ckuvx/m4bQJMYgBal tbgg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=bJmFncIr; spf=neutral (google.com: 2607:f8b0:4864:20::331 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=5FozyxqOnj8L4B/O8/0Zwf5+D/VD7U/hc34ITl2NJHw=; b=iY8NmXLue+liqU8cf6UaMLGGDQQ5oaIjCqKjrhRPzhMo/w3DKAQxRjIGPvRKQXVrYk lmq8Yb13X4xHPzhPEZs8NQqCnNFgTFuQH7BS4mXNN6GOTqo8VUm5/2I+LwFp66A30pIU WAtj1acBQNby61hfLjYXZSMJKK+9S1VL6UFDLeASdndGdyvfZKvY1W066qz4QQwdvbJM QYtJOUh7vInDgyVTKCoNkj6Uj9pQF6XL/MlCct81IEMF63JX0/9IQ11H6JeA5QIp/fWA ZWpuDd+qbGudgFufy/ax34OD2vn8YfDbXInCzM7K6TLfL8iPczhlBdsH2rmd9aPHXD/z 1X4A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to: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=5FozyxqOnj8L4B/O8/0Zwf5+D/VD7U/hc34ITl2NJHw=; b=kzgp5mmG1YRu+cS1v9BR43Pxz5CyrZLuoVuzj87qEN165Fcat7xFRRnfmCkKFZYZXx d7csHWVTujEqmc1RtRXAMBu0zBPuQw1wwc1YcEnjrTlRbVaid5RF5Jy5BvUwH4OYkgmJ SWQOoy4zUr2eNnf4Cj1TvBjVnIHJlh9fgknObdCgTarv3bJ9Uzeymle3Um1pC7KQhpwD eQBcjFVAAilvh4IfPvEcDiHXZVoRdYMUcxCsT8JJGVTpy1e8gnn1+mbLeQM7aXLFpmZ8 kdRy+dqju55xqajnyBCXdpTPOWUvk3w+naenXrkCLFHoTFux9WJky94qaE2LTZ71bEIb BucQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXn721lgsPW8Rv1/tHZGupvzgQiiCqhvq8NjsdoZMO3eWTYO8QH 4M33zfa1ylleWksUd8y2rDI= X-Google-Smtp-Source: APXvYqyy4J7X5H4J0K6OmRBniQkN3Z+T1Ar/fZPrPFX5eKHP9/m43cXhRF+uCnZSLKpWmXJ3iZprZA== X-Received: by 2002:a63:546:: with SMTP id 67mr17334910pgf.429.1568587124906; Sun, 15 Sep 2019 15:38:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:9a81:: with SMTP id w1ls8716798plp.2.gmail; Sun, 15 Sep 2019 15:38:44 -0700 (PDT) X-Received: by 2002:a17:902:9686:: with SMTP id n6mr59272400plp.113.1568587124519; Sun, 15 Sep 2019 15:38:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568587124; cv=none; d=google.com; s=arc-20160816; b=XIf/6rPF6C51TgUJlOFdPZ/aZEBP1zv2m2mNc8AJMQPPwyhZ6G4y+PJSuUHyzGJ8E8 Tn88RigEC0ZhrKQH5OzNB9Z6UGoji1ufPLNwWXbcO0fP86Cc+4LS3zSuc66EMjlIMINT RlzYso/O0+FFotszMBDbZr54LCr8vaGvxgwUGUJbGVPEiDW7bsBiGLG3EcAdeRxPndhZ blFaKdI625HPd2h0HUD+m5xiNzxLAZzoxQx/pr3BBwXOpUhj2emii0HDJb496UVOBeWc hYLeI5/ypvpVygd5S5d4GrBLlnw3Ud1CWy7lBykR8JD+OCf2wn1AoqN2HM/DRHrnsbEx pbcQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=65i9g2fIs4qQddLs+hpOHlIjn+ymFRJ6RKypsf1bmPk=; b=jgFexu9NDWud3FN0xtYp7PE9KOeBNqOh0IzvA1jkhaqJ0xxen6l5XCwetOM59yJx/x pygXXqFz1kD8LfXmlLIE5EpYRBQJ7/ZNlqlZvldurkGxNCp/Wrwnj6qD1ttGQLZu+ask v1FTvrA/2rgG+8HSfYDRMe20Jj4Tx9dvnLgC/n9s9XHliVZ+hTKNrKYKI0qeWCfeubyO EpsnPb8Uc/XeGrTGipyGC/1FxK5J6N67zyFYz6+klpKJ9QFqaiLz1mWHU4aI2baFniJ3 k188F6PWzd1ZyORLsPNE30atRC39/f8e7SJ7b3yf1pdMTy31GiQ0QuEQmHS8fXt+DFGa bOoA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=bJmFncIr; spf=neutral (google.com: 2607:f8b0:4864:20::331 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.edu Received: from mail-ot1-x331.google.com (mail-ot1-x331.google.com. [2607:f8b0:4864:20::331]) by gmr-mx.google.com with ESMTPS id j21si744504pfe.5.2019.09.15.15.38.44 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 15 Sep 2019 15:38:44 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::331 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) client-ip=2607:f8b0:4864:20::331; Received: by mail-ot1-x331.google.com with SMTP id g25so32738977otl.0 for ; Sun, 15 Sep 2019 15:38:44 -0700 (PDT) X-Received: by 2002:a05:6830:1e2e:: with SMTP id t14mr9592795otr.354.1568587123913; Sun, 15 Sep 2019 15:38:43 -0700 (PDT) MIME-Version: 1.0 References: <16b3b92f-069b-468c-94f8-f3859e152338@googlegroups.com> In-Reply-To: <16b3b92f-069b-468c-94f8-f3859e152338@googlegroups.com> From: Jasper Hugunin Date: Sun, 15 Sep 2019 18:38:57 -0400 Message-ID: Subject: Re: [HoTT] Re: A question about the problem with regularity in CCHM cubical type theory To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000052080b05929f26e3" X-Original-Sender: jasperh@cs.washington.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=bJmFncIr; spf=neutral (google.com: 2607:f8b0:4864:20::331 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) smtp.mailfrom=jasperh@cs.washington.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cs.washington.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: , --00000000000052080b05929f26e3 Content-Type: text/plain; charset="UTF-8" In CCHM, my understanding is that composition for Glue [ phi |-> (T, f) ] A is actually regular, and reduces to composition in T on (forall i. phi), assuming composition is regular for A and T. The regularity does seem to fail in ABCFHL, as you pointed out Anders, but is perhaps repairable. What Carlo told me was that the problem is getting composition for Glue [ phi |-> (T, f) ] A which is regular, reduces to composition in T on (forall i. phi), *and* reduces to composition in A when (T, f) = (A, equivRefl). We get the first two but not the third in CCHM. The problem as Carlo explained it was that given a square of types i, j |- A and a point a : A (i0) (j0), we can prove Path (coe^i A o coe^j A) (coe^j A o coe^i A) (coercing around the square in right then up vs up then right), and (assuming regularity for A), we can take this to be degenerate when A is degenerate in i, or give a different path which is degenerate when A is degenerate in j, but constructing a path which is degenerate when A is degenerate in i or j is elusive. I have an idea for how to add new terms/operations (a sort of generalization of comp) such that such a path is constructible, but I haven't yet checked that there is a univalent universe with these more general operations. I also don't understand the negative results from Andrew well enough to tell if they rule out such an approach. The idea is to add terms witnessing that for every square x, y |- A x y we have Path (coe^i (A i i)) ((coe^i (A i 0)) o (coe^i (A 1 i))) which is degenerate when A is degenerate in x OR y, plus similar terms for higher cubes, since once you need dimensions one and two you probably need dimension n, and a similar thing for hcomp, or you can do coe and hcomp together in just comp. Composing two of these paths then gives the needed proof that coercing around the square either way is equal, in a degenerate fashion if A is degenerate in x or y. Best regards, - Jasper Hugunin On Sun, Sep 15, 2019 at 7:55 AM Andrew Swan wrote: > You might have already seen this, but I have a paper on some related > issues at https://arxiv.org/abs/1808.00920 . In that paper I didn't look > at the original version of regularity, but a more recent version ("all > monomorphisms are cofibrations") that fits better with the general > framework of Orton and Pitts. In that case it is definitely equality of > objects that causes problems. > > Best, > Andrew > > On Friday, 13 September 2019 08:10:42 UTC+2, 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 |-> >> equiv^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 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 issue, or if >> regularity for the universe was supposed to follow from a different >> argument. >> >> Context: >> I've been studying and using CCHM cubical type theory recently, and often >> finding myself wishing that J computed strictly. >> If I understand correctly, early implementations of ctt did have strict J >> for Path types, and this was justified by a "regularity" condition on the >> composition operation, but as discussed in this thread 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 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 >> seems to be closed under the usual type formers, plus Glue, but not the >> universe 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 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/16b3b92f-069b-468c-94f8-f3859e152338%40googlegroups.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/msgid/HomotopyTypeTheory/CAGTS-a9XATMbfyyp00M8kqiEoFyj7XsxahMa3AdzXth_%3DLbTiA%40mail.gmail.com. --00000000000052080b05929f26e3 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In CCHM, my understanding is that composition for Glu= e [ phi |-> (T, f) ] A is actually regular, and reduces to composition i= n T on (forall=C2=A0i. phi), assuming composition is regular for A and T.
The regularity does seem to fail in ABCFHL, as you pointed out= Anders, but is perhaps repairable.

What Carlo tol= d me was that the problem is getting composition for Glue [ phi |-> (T, = f) ] A which is regular, reduces to composition in T on (forall i. phi), *a= nd* reduces to composition in A when (T, f) =3D (A, equivRefl).
W= e get the first two but not the third in CCHM.

The= problem as Carlo explained it was that given a square of types i, j |- A a= nd a point a : A (i0) (j0), we can prove Path (coe^i A o coe^j A) (coe^j A = o coe^i A) (coercing around the square in right then up vs up then right), = and (assuming regularity for A), we can take this to be degenerate when A i= s degenerate=C2=A0in i, or give a different path which is degenerate when A= is degenerate in j, but constructing a path which is degenerate when A is = degenerate in i or j is elusive.

I have an idea fo= r how to add new terms/operations (a sort of generalization of comp)=C2=A0s= uch that such a path is constructible, but I haven't yet checked that t= here is a univalent universe with these more general operations.
= I also don't understand the negative results from Andrew well=C2=A0enou= gh to tell if they rule out such an approach.

The = idea is to add terms witnessing that for every square x, y |- A x y=C2=A0we= have Path (coe^i (A i i)) ((coe^i (A i 0)) o (coe^i (A 1 i))) which is deg= enerate when A is degenerate in x OR y, plus similar terms for higher cubes= , since once you need dimensions one and two you probably need dimension n,= and a similar thing for hcomp, or you can do coe and hcomp together in jus= t comp.
Composing two of these paths then gives the needed proof = that coercing around the square either way is equal, in a degenerate fashio= n if A is degenerate in x or y.
=C2=A0
Best regards= ,
- Jasper Hugunin

On Sun, Sep 15, 2019 at 7:55 AM Andrew Sw= an <wakelin.swan@gmail.com= > wrote:
You might have already seen this, but I have a paper on some r= elated issues at=C2=A0https://arxiv.org/abs/1808.00920 . In that paper I didn'= ;t look at the original version of regularity, but a more recent version (&= quot;all monomorphisms are cofibrations")=C2=A0that fits better with t= he general framework of Orton and Pitts. In that case it is definitely equa= lity of objects that causes problems.

Best,
An= drew

On Friday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wr= ote:
Hell= o all,

I've been trying to understand better wh= y 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 parts:
1. T= hat Glue [ phi |-> equivRefl A ] A reduces to A (a sort of regularity co= ndition for the Glue type constructor itself)
2. That equiv^i (re= fl 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 suppo= sed to follow from a different argument.

Context:<= /div>
I've been studying and using CCHM cubical type theory re= cently, and often finding myself wishing that J computed strictly.
If I understand correctly, early implementations of ctt did have strict J= for Path types, and this was justified by a "regularity" conditi= on on the composition operation, but as discussed in=C2=A0this thread on the HoTT mailing list, t= he definition of composition for the universe was found to not satisfy regu= larity.
I don't remember seeing the regularity condition defi= ned 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 o= f the box. This seems to be closed under the usual type formers, plus Glue,= but not the universe with computation defined as in=C2=A0the CCHM paper=C2=A0(for trivial reasons and non-trivial reasons; = it gets stuck at the start with Glue [ phi |-> equiv^i refl ] A not redu= cing to anything).

Best regards,
=
- Jasper Hugunin

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468c-94f8-= f3859e152338%40googlegroups.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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9XATMbfyyp00M8kqiEoFyj7X= sxahMa3AdzXth_%3DLbTiA%40mail.gmail.com.
--00000000000052080b05929f26e3--