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-x63d.google.com (mail-pl1-x63d.google.com [IPv6:2607:f8b0:4864:20::63d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 42357cdb for ; Sun, 15 Sep 2019 05:57:29 +0000 (UTC) Received: by mail-pl1-x63d.google.com with SMTP id p8sf18534453plo.16 for ; Sat, 14 Sep 2019 22:57:29 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568527047; cv=pass; d=google.com; s=arc-20160816; b=KtfxzUk58utFaQMNdxRRNVf3/mWNYisvJ+DhMvAAiewdRaN41M/lnw6rmVQs6HsuRd M2d9fspG25AXVlyIDE1/OJwcVdE1A07sYyTfew5eeHWIuVKA5fpHBAVF7yk4Hes4VZCv wXffe6hBGjO/Vo59snNUPz6g6PRFjqUmeXYFVf9TQaBFVn6iACzBJI7VwbswItEIg/Fm Yxndur5K/PsmsevP/N2PbMD3wTqQN/ZUB0iHdJeZDZN9GQeIGG7rk6XRocHLEn8YntQY O8J2cM4YjNIro1rk06duQhyt0NRMXPje05Xq9cE0Y1F110rIGdnExFerZ4cq70snsRXK L7cg== 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=vkseMeVKltV4r9KkWdWnGiNk3NRafQt5QvRlSmNvsGs=; b=eSzWT2bc+bAlRG45suBJyaf4mVbAiZ3egGyXsBy/3jrqxWb2qFmlIr60GniK6RVsgc wO4Mtd5Dr9OTKJNTncUF/c0yvpKkJnFM5/lZtUgiCsKT199iKagN5hCc806un18rfDb5 L0GOYxD/dLcxEQBPT5/2pODYMrffpph2QFFJZixLbR7RaRB4YyrkKlxx/esFB8/+WQ2d NAJiiHfXdvMjPjtLkktPV47SYFq4zrLqWIVcB5YqSFYoP6cL88fTagdU+OecmP7bfr+/ yfGreXVE33t8hNjpw6g31UWcj23OZ/kK0SSWBgSq0oyFjimr6A2ETyIgITvRnVroJAIL nfhg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=VykIb1U6; spf=neutral (google.com: 2607:f8b0:4864:20::336 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=vkseMeVKltV4r9KkWdWnGiNk3NRafQt5QvRlSmNvsGs=; b=loMdTn/P/9gS2U094THrL10l1zjwK2yneF5uem8HD/kTvan7P2rxAoZqBSvzPrY+YO B/CIfHYqRcOOldONnN+DhSy73vJRTGxbgTT/6qx0l7faGJ3JYFiR+mrQgnLc8pwP6DH6 2k+2W4EOtQcXN6uzQvKJ26IXfnH7AdhdqdKEao0W9EW2u/AxJaFTh5ZsXmwlFnkzhC9f FBtEWDAe/gA0LvGQVvtSP2yi3NPaM/YqRe7gWFel9NjpYTQTQWU86fvBFCHCFApOWKJy /nkr74yfzjg5N6FZXojCX91ri/BR8no3iXmcy4NOdK20CAkrPucJ7y2WEf9Y+db2Fc6u 7JGQ== 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=vkseMeVKltV4r9KkWdWnGiNk3NRafQt5QvRlSmNvsGs=; b=emAUz9JNrvPw7k7M8/WXGQi+RtooncRy1xbLCgEdcPnGAlxtJpUJtmZQdtcDhv1+vc H14S0vGyqvDIU+UdHnnCbXhq5OiO1N6tGFtWNtbbXbN6IRrEejvA6ZGsIa9M7CUHcSmw q9inlbB3hgPkqoITeAQXbVUx/AHAG/QWRwfwaV3+i7G0WSds4mN/Bu/pzlLFOSFtwxH4 HLk+SlnzkQx3Sj814iZK57G1dce+tYRCCBdIBEVGYBDE4+G6/E3aCxE/dicunuRd24w2 XHkJCGujNT6acqE7JiZaWU9/IIlOv90p4iOnYDWX/stKRDzyduoGQxlARx8SettXp+Vx FGQg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAV6NP5EGMDbljYwvkbH793mn1So889HhxJPgSLK2kUvMu61C5Eh hiTVnfLkJUO+5SZc5bU1jQA= X-Google-Smtp-Source: APXvYqxPSCfAiVyy6JUvf5JtS9UAVGeSh1VGI3zVsJy3FlW/kP3NPc1WJBD3RYWQEPqiud7Y5HLWKQ== X-Received: by 2002:a62:2643:: with SMTP id m64mr49916898pfm.76.1568527047188; Sat, 14 Sep 2019 22:57:27 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:a711:: with SMTP id w17ls3363821plq.14.gmail; Sat, 14 Sep 2019 22:57:26 -0700 (PDT) X-Received: by 2002:a17:90a:cc15:: with SMTP id b21mr440710pju.136.1568527046846; Sat, 14 Sep 2019 22:57:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568527046; cv=none; d=google.com; s=arc-20160816; b=JG2rdNMnUXVRXiU/0xGz2PrPvAfHeuXVLFO2eES7yoXKML617NHs9HHWIQSL1ElLil 8GmnXfCvkkvnP2/M/gvImorYFyGCwogZ3ZOXt1pjedG+ZKWhOM7uc4hVvZV7NGgzhqbJ PqOWimX+0ukRX4UjQ9uz4FjXlK1siKps2qWn+CUowkFCEhYobcgzVq+yOBQkJylV5rGp JGKMxNpyOu0+g0+MCaXnPNeKQGnTg09CBaWtLggzaDWMF3AvE5Y5F8vvJAO1trMKx9v5 Cr3rQHupF/+BTleVFkLU1OUWWCC0OH6EFkaMukakzml753MMxW9NFkDj8rwnKrS2eLxx HHfA== 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=e5Xc+GBNwQBGTi1trPjMiicAQGsQ04lmzD1XgC47yHU=; b=KSKM0GqT8sdTDYXhJuXW0ev5ttxui+fig1DZPFOPhiBKuUQa11EEX+rm2PqOMc+JGS oW7BCl91SDujewlhmPWvmU0lMqsby/Db8rsU21hzZaOj+f8ru7wiAaqxLRt7uGlB0sYi TDulQy9nNVFgWsCB/11oi3dXutURl/GhO3/uuQjqGYfmcZKRff0ot1F1R09mikj5ypRe jXf99H1hK2cSAI7f9/EpXJ/PFI01N4F6yM7G47MruteTNN8H6HfYFHFglbhNfcRejG1Q 8E3w3DDmw3VT4pfITomZm4LK5x7lGSSIDYPkRvnAuSLTcPYsypbO+EVOe9+oxWMAGKpu 4a4A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=VykIb1U6; spf=neutral (google.com: 2607:f8b0:4864:20::336 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-x336.google.com (mail-ot1-x336.google.com. [2607:f8b0:4864:20::336]) by gmr-mx.google.com with ESMTPS id w10si647064plq.4.2019.09.14.22.57.26 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 14 Sep 2019 22:57:26 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::336 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) client-ip=2607:f8b0:4864:20::336; Received: by mail-ot1-x336.google.com with SMTP id y39so32968496ota.7 for ; Sat, 14 Sep 2019 22:57:26 -0700 (PDT) X-Received: by 2002:a9d:7842:: with SMTP id c2mr5117409otm.171.1568527046262; Sat, 14 Sep 2019 22:57:26 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Jasper Hugunin Date: Sun, 15 Sep 2019 01:57:40 -0400 Message-ID: Subject: [HoTT] Re: A question about the problem with regularity in CCHM cubical type theory To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000069daeb05929129da" 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=VykIb1U6; spf=neutral (google.com: 2607:f8b0:4864:20::336 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: , --00000000000069daeb05929129da Content-Type: text/plain; charset="UTF-8" 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 operations agree as well as the sets. So part 1 could be thought of as (Glue [ phi |-> equivRefl A ] A, compGlue) = (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 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 |-> > 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/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAcAefiTg4JJVHemV3HUPcPEg%40mail.gmail.com. --00000000000069daeb05929129da Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Offline, Carlo Angiuli showed me that the difficulty was i= n part 1, because of a subtlety I had been forgetting.

S= ince types are *Kan* cubical=C2=A0sets, 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, compGlue) =3D (A, compA), and getting that the = Kan operations to agree was/is difficult.
(Now that I know what t= he answer is, it is clear that this was already explained in the initial di= scussion.)

Humbly,
- Jasper Hugunin

On Fri, Sep 13, 2019 at 2:10 AM Jasper Hugunin <jasperh@cs.washington.edu> wrote:
Hello all,<= div>
I've been trying to understand better why compo= sition 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 Glu= e [ phi |-> equivRefl A ] A reduces to A (a sort of regularity condition= for the Glue type constructor itself)
2. That equiv^i (refl A) r= educes to equivRefl A
I'm curious as to which (or both) of th= ese 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 Pa= th types, and this was justified by a "regularity" condition on t= he composition operation, but as discussed in=C2=A0this thread on the HoTT mailing list, the definition of composit= ion for the universe was found to not satisfy regularity.
I don&#= 39;t remember seeing the regularity condition defined anywhere, but my unde= rstanding is that it requires that composition in a degenerate line of type= s, with the system of constraints giving the sides of the box also degenera= te 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 wit= h 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 reducing 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 https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAGTS-a9oS0CQDGKgj7ghCh8%2BZwAc= AefiTg4JJVHemV3HUPcPEg%40mail.gmail.com.
--00000000000069daeb05929129da--