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-yw1-xc38.google.com (mail-yw1-xc38.google.com [IPv6:2607:f8b0:4864:20::c38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2ffb5dec for ; Mon, 16 Sep 2019 01:45:00 +0000 (UTC) Received: by mail-yw1-xc38.google.com with SMTP id l16sf29310690ywb.15 for ; Sun, 15 Sep 2019 18:45:00 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568598299; cv=pass; d=google.com; s=arc-20160816; b=pOV37e2u8eEksFQ+RsYy+nGN9Ff1lbx8IOLdZeZj/qCkfD33RumSv/YnsB+8iaV0wX LiASzO/HbD9fZVU1vmdTCy2fPpr/7PETbFHsD37nSY4lJQAf9dEQ8IcnhctFrfECVrzw 7P5C+yBOq8yHVaOFnR7uX7aZBxI4/Ma9zBGJRb9urLUcFSywqrZUkkbaZ7RorYXUiejX 9SJrArPtB54bG6HAE6WA+N/pU5OVbQnB/2Edl9NV+SlhkZlI1PmDXI/Q8JrSg8ohJkc0 sWMm9GZx74A7Cd6Cm56Efn9zBcGNBe8U2tYajuS9iX8JE15q/JIRLvyZjZiqzfz//fZQ 8/9Q== 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:subject:cc:to:from:date:references :in-reply-to:message-id:mime-version:user-agent:sender :dkim-signature; bh=RuVWSZOyayY0gPzZyapczloP6clhFijFhvNgwTiVa+Y=; b=Jxm2QXkPLBwakMuRpBUzli5xTkdZMaPMnYidVtd1Nez9hai3KevdAhJ2WxtJb6X7pJ 0ak6Imlj8nuqBuUJlu+NxNPpeE4ymU9NLR3FSbbgA52CGK9NOF/VVoF+gCvvm/IfXMCq H0ySI/9GovygZbAaaeD7QNK4twLqQ3eV3fwfmjKn78mgkfmgQvhxdTNQxlr0UH2Xp1uO qCWjlwS9ipbxeeD3TQUSzvRa0U3U5Sl8p7SrfAI1YgT/skOz+CJbZCbcb9Kd3Bdjr0Yc 0PUmjq6zql69xNqBtVo4PVWMfMYRALQ2vC8cdm6pv8wWt9UeGnCPVJnj1vSYZD4Q7UEP 6gqg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=I99i1LFI; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:user-agent:mime-version:message-id:in-reply-to:references :date:from:to:cc:subject:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=RuVWSZOyayY0gPzZyapczloP6clhFijFhvNgwTiVa+Y=; b=WyZzmZ9mRUd2Btesr/TUrUF8sGmDz5kmqiEmlQPCvd9wCmERVWm1nCdpx064BhQRlH cHtzqfLOXAtcrBjiVT0+k9lkBxfXTuv9Vd0eAszg7ziP8kYLON/qXfBVxgl78iIBKw+m IUgf/L0JXXtOdilN5k/oUU2b/cTdHbgPCxpR8Rc0bOY+CvItilkdUJGA4OjrLYM1DlZn BRGMAK7C/OFH5jg2MSYR3bMVHeU2Q2Okmn5R2ri64Lw2rcW+iEMFQXUWBba80rBW+I3m MWK7GIgRBH8ZTEi+qldGrSGPoi6fid3fsFlGeqJfEnnV8y7b1J24otklvs3GFzYJ8g7N lNiA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:user-agent:mime-version:message-id :in-reply-to:references:date:from:to:cc:subject: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=RuVWSZOyayY0gPzZyapczloP6clhFijFhvNgwTiVa+Y=; b=H2AmoJW7YguCDD3Ovp3AQmxYuD8O2dt2BX6Cv2tPw9wCgAn6+sgyKYlM+qRV9F1x3W rWSM0K1kKHroqKhOmUkPmWFeoi9mp20jKW7YiLFCypa2rqc2u07XSQp4ytQNUSmG/GCN y4ggUkzou6W2rSaP861T/YwGzBj1cVAhGDwg10pMNcbT5vJDBb1T0NddRZMH+rXAbElu i3Z7vdrXfMTh6Cihs7p2FRQtZ/uSMBcO7mISYaEkQUqmYVJpvhnWHvRQsF9nfPBD0ij/ GnnBHBMCRXt+uAYONj8BqPMSc6eIDtav+rat4r04HL0eOxOdRIK3hTckPMir+KmERbye 5eKQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVUU5uLfS5DDpE/vytAXDnYe/mucg46F5eAiz6Xge2JqIsDOyCS WNp8F7r4nwjTbKUPHSo//hU= X-Google-Smtp-Source: APXvYqwrA+P6JFYRWIr1+aDvorVcWmCCZ2PNqc03KvyF3GiZXjtIonXkqwZc2U6lEJuFZZzzHu8kxg== X-Received: by 2002:a81:4e87:: with SMTP id c129mr11870012ywb.480.1568598299718; Sun, 15 Sep 2019 18:44:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:9d84:: with SMTP id v4ls143469ybp.0.gmail; Sun, 15 Sep 2019 18:44:59 -0700 (PDT) X-Received: by 2002:a25:5d0e:: with SMTP id r14mr8319465ybb.344.1568598299180; Sun, 15 Sep 2019 18:44:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568598299; cv=none; d=google.com; s=arc-20160816; b=IkRxmUmD6HYfT7M1XkNjo8DF/5QLWnW+riGc6o+lI50jI4sBpgYN0Qd9ujIgXA1hys uGksSGMcTiz6Yw9DYpZd0uoOtz9hrYJXa0jC1M6ozj67fWNe3x8MQiLP/v87ckuoUc18 VmeJMROX2SCaFJRrjqUMugtUZ8ri+hOnw1muXhihG72cJI2rjBdyZJx2Fn8tStruA5E1 Db8cnpA7ieqfFE7ZgyXUWPvPQdH/PPxKlnJxCDDoY0SIjSW0BcKoxj3ZLCYSTyACa6VR uhCq9iaFoJSWrs8GHn3/M7Cw3iYFTksZH2Ju0cbJfr8ZRGimCFCryq9nl85a6R2zjXwS M3UQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:cc:to:from:date:references:in-reply-to:message-id :mime-version:user-agent:dkim-signature; bh=CcThleY51lj8DVpP1AL4Lg+JaIukGO2EWjICzErZifs=; b=RvQJbqnn9uuIkfrkAHueU7hOWtvuDvAB7zq8YuJ2AH7mNht/tekI+6f79/moGeSo8E H3cXqNOLcyrqXP52Y4A+zj7decP+KLcFQOokzntscZNuLgyI1ifS+QwYjIKwuxcQwE0m VUv2mEjaW1YH6wlmeSkGEeJUw7jfZ7Qz0eggS3iI4v2R3L8HU9NGfCJ/XHe1pgp25iQn VduQBWZlzsHqL6DqeUCvBMH5xBEs6HVo+QO8SU4wEcoho1Om+RKUbuVukidgdyDubuG4 jTmw/t9wbwliRzQBQtjkY72s77ijBzpqb98KDBL5TZsI8XxPFXj7dCDKQU8YywuQa7rO dz5A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=I99i1LFI; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id p140si2199649ywg.4.2019.09.15.18.44.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Sep 2019 18:44:59 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.26; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 8E48221BF7; Sun, 15 Sep 2019 21:44:58 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Sun, 15 Sep 2019 21:44:58 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedufedruddvgdehtdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefofgggkfgjfhffhffvufgt segrtderreerreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjohhnse hjohhnmhhsthgvrhhlihhnghdrtghomheqnecuffhomhgrihhnpegrrhigihhvrdhorhhg pdhgohhoghhlvgdrtghomhdptghhrghlmhgvrhhsrdhsvgenucfrrghrrghmpehmrghilh hfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmnecuvehluhhsthgvrhfu ihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 437F55C0099; Sun, 15 Sep 2019 21:44:58 -0400 (EDT) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.7-237-gf35468d-fmstable-20190912v1 Mime-Version: 1.0 Message-Id: In-Reply-To: References: <16b3b92f-069b-468c-94f8-f3859e152338@googlegroups.com> <80a2be3b-afaa-4106-9c69-0df6567ec709@www.fastmail.com> Date: Sun, 15 Sep 2019 21:44:38 -0400 From: "Jon Sterling" To: "steve awodey" Cc: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Re: A question about the problem with regularity in CCHM cubical type theory Content-Type: multipart/alternative; boundary=18654bdf4b6a4ca7b87c475527c9d9b6 X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=I99i1LFI; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com 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: , --18654bdf4b6a4ca7b87c475527c9d9b6 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks Steve! On Sun, Sep 15, 2019, at 9:38 PM, steve awodey wrote: > It does: the relf term is always a weak equivalence by 3 for 2, and it=E2= =80=99s monic because it=E2=80=99s a section.=20 >=20 > Sent from my iPhone >=20 > > On Sep 15, 2019, at 21:04, Jon Sterling wrote: > >=20 > > Hi Andrew, > >=20 > > Does "all monomorphisms are cofibrations" imply that identity and path = types coincide? or only the other way around? > >=20 > > Thanks, > > Jon > >=20 > >=20 > >> 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= =20 > >> issues at https://arxiv.org/abs/1808.00920 . In that paper I didn't=20 > >> look at the original version of regularity, but a more recent version= =20 > >> ("all monomorphisms are cofibrations") that fits better with the=20 > >> general framework of Orton and Pitts. In that case it is definitely=20 > >> equality of objects that causes problems. > >>=20 > >> Best, > >> Andrew > >>=20 > >>> On Friday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wrote: > >>> Hello all, > >>>=20 > >>> I've been trying to understand better why composition for the univers= e does not satisfy regularity. > >>> Since comp^i [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> e= quiv^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 regula= rity 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 argume= nt. > >>>=20 > >>> Context: > >>> I've been studying and using CCHM cubical type theory recently, and o= ften finding myself wishing that J computed strictly. > >>> If I understand correctly, early implementations of ctt did have stri= ct 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 mail= ing list , the definition of composition for the universe was found to no= t satisfy regularity. > >>> I don't remember seeing the regularity condition defined anywhere, bu= t my understanding is that it requires that composition in a degenerate lin= e 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 uni= verse 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 reducin= g to anything). > >>>=20 > >>> Best regards, > >>> - Jasper Hugunin > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > >> Groups "Homotopy Type Theory" group. > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > >> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> To view this discussion on the web visit=20 > >> https://groups.google.com/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468= c-94f8-f3859e152338%40googlegroups.com . > >=20 > > --=20 > > 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/80a2be3b-afaa-4106-9c69-0df6567ec709%40www.fastmail.= com. >=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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/afe67df2-7f4a-4e51-abc9-3f8e3a985623%40www.fastmail.com. --18654bdf4b6a4ca7b87c475527c9d9b6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks Steve!

On Sun, Sep 15, 2019, at 9:38 PM, steve awodey wrote:
It does: the rel= f term is always a weak equivalence by 3 for 2, and it=E2=80=99s monic beca= use it=E2=80=99s a section. 

Sent from my iPhone
=

> On Sep 15, 2019, at 21:04, Jon Sterling <jon@jonmsterling.com>= ; wrote:

> Hi Andrew,

> D= oes "all monomorphisms are cofibrations" imply that identity and path types= coincide? or only the other way around?

> Thanks,=
> Jon

= > 
>> On Sun, Sep = 15, 2019, at 7:55 AM, Andrew Swan wrote:
>> You might have already seen this, but I have a paper on s= ome related 
>> issue= s 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 be= tter with the 
>> gen= eral framework of Orton and Pitts. In that case it is definitely 
<= /div>
>> equality of objects that ca= uses problems.
>> 
>> Best,
>> Andrew
>> 
>>&= gt; On Friday, 13 September 2019 08:10:42 UTC+2, Jasper Hugunin wrote:
<= /div>
>>> Hello all,
>>> 
>>> I've been trying to understand better why co= mposition for the universe does not satisfy regularity.
>>> Since comp^i [ phi |-> E ] A is def= ined as (roughly) Glue [ phi |-> equiv^i E ] A, I would expect regularit= y 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 cu= rious 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 t= heory recently, and often finding myself wishing that J computed strictly.<= br>
>>> If I understand cor= rectly, 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 <https://grou= ps.google.com/d/msg/homotopytypetheory/oXQe5u_Mmtk/3HEDk5g5uq4J>, the de= finition of composition for the universe was found to not satisfy regularit= y.
>>> 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 s= ystem of constraints giving the sides of the box also degenerate in that di= rection, reduces to just the bottom of the box. This seems to be closed und= er the usual type formers, plus Glue, but not the universe with computation= defined as in the CCHM paper <http://www.cse.chalmers.se/~coquand/cubic= altt.pdf> (for trivial reasons and non-trivial reasons; it gets stuck at= the start with Glue [ phi |-> equiv^i refl ] A not reducing to anything= ).
>>> 
<= div style=3D"font-family:Arial;">>>> Best regards,
>>> - Jasper Hugunin
>> 
>> -- 
>&= gt; You received this message because you are subscribed to the Google = ;
>> Groups "Homotopy Type= Theory" group.
>> To unsu= bscribe from this group and stop receiving emails from it, send 
>> an email to HomotopyTypeTheo= ry+unsubscribe@googlegroups.com.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/Homotop= yTypeTheory/16b3b92f-069b-468c-94f8-f3859e152338%40googlegroups.com <htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/16b3b92f-069b-468c-94f8-f= 3859e152338%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter&g= t;.

> -- 
> You received this message because you are subscribed to the Go= ogle Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails fro= m it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
=
> To view this discussion on the= web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/80a2be3b-af= aa-4106-9c69-0df6567ec709%40www.fastmail.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.co= m/d/msgid/HomotopyTypeTheory/afe67df2-7f4a-4e51-abc9-3f8e3a985623%40www.fas= tmail.com.
--18654bdf4b6a4ca7b87c475527c9d9b6--