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-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 400c5fe4 for ; Mon, 16 Sep 2019 01:04:32 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id w6sf15908238otm.19 for ; Sun, 15 Sep 2019 18:04:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568595871; cv=pass; d=google.com; s=arc-20160816; b=iGqiElUJaarLl3YMnL8K8Z7Uwtt+CR8P4eAhftjeebl4vtvDR/ltHjCOzvcCUpwN6J V1yb70dqmP9n+9Ap4bHa6MQzJV9z1JzYg/YuA9t+q9lNRiyV4/3NrSmWEeF9TZjBTJHp BrzfBiUAz/mWLVZDCYelZLKSofmj8Dp4sx6H8lwK6cRK91SGtfAFTZ7c6/dqmx/QN0Ie x/F5IzXsked0Z2vLOrNlOdlnSFjl6P6HA7P8dKp2D5SA6C5RJbsPxK1JmM0eTXvA0p5B Zwr5UdV9Ed+JFcXLvJCkeuF/zlU+W1N89Dr7T/zB0Laagy7seOQuVxg0hqBcHovP2/q2 NGdA== 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:content-transfer-encoding:subject:to:from :date:references:in-reply-to:message-id:mime-version:user-agent :sender:dkim-signature; bh=nm5xgG8VzoplktXddxtv997D+no4IoH3jXbq6kn24YE=; b=weDxnnWW7Pcp1Z0Z4ac4sggC9RjgpTesSq67dVM4FbngFXuHLhBvylgYreJSLlWuLU q/Y9vi9RJykZNL/tKwV1Db/z8LMHgfzU1Oq8n4Y0xm3aPCmaY0fAKsPs/aSgBF7fohrs Uiw2Sx87FEijHNFmA0AJlzY5hVioqUyxDoqznNRhjXhzaL4Gfz6p7UidY3iNz52wyIvg G+syHUKgHCEF5aPJ8F51tbm62K3qAxmDMbuY98B6NkBJpWw46NBwyO/+oqR0EoqZnWIY CMS6FY4qIPvOgOWwpSmaEagR+bPWjxg+A10NWC/9AaZL8DEFMsDk5nzCSchSOxvUjQsW JCUw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=R6NA1Fgp; spf=neutral (google.com: 66.111.4.25 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:subject:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=nm5xgG8VzoplktXddxtv997D+no4IoH3jXbq6kn24YE=; b=TURCl3EnbaCT6DJ3PHHN+5oqSIQKy+axs50Az/PPKUrekWxrDuMiFo2Toay2siBUGt rcAobLI0+ePxv9NGKlfjjAOO9LCizCVhqRSTfdIdWmehvYgpagPrNQEcP+1unYlFd09N XM+pWblhVOkjGvjxIPAkpRg3EOH5/zqbi4xq5c/uTKYwmgQJr0C+YjsEHHcrtLkwANaE 6tSFgrHOOxZ/hF/5Be/7EUqlsE9iXrbcrSP2QrXfxIvJ++jYjFCfw8NHzmJtXELQRGPP 6n6hGqQiWAphDo8RXh31pLFlQPjZwCKy9qZtG53r+Fe6Az1JF6TDgJfmqkf3udUq7zHv Jr5w== 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:subject:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=nm5xgG8VzoplktXddxtv997D+no4IoH3jXbq6kn24YE=; b=hDwmtN4w63En6bTwkC1NfxzVVm1LgD9THNffERjEHEOOXbP8p61yDA4iG909d8xWiw iptndJo4fDXUo/kQV1eStk7eK4lJlK5TlGmcSJ19c6qpHCk5J2lmDXxPMC6JjH1bV1id Y/lWvRzuX2EvqJbnTYjGxh4J9oCjWtj3bUdQIsunKOdReAMGwsxN6KWGQYjXBre6BeGK xc5LgD7KbvDXjChVNuzdRn7S6HDhqDLeGKx7TtpHm+4jfbhcFXApC4hCZKK13Gubwx6L wdIiPwBR7KLp0IcfxxWwXuDvr0O1trNNoHaNzZuoejvOAAUzxpfzS1a2JFf3jFCjcVEJ BIfg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU5u5FqjwhfX4zRyTZC689p8+iImGtpY7Uip6xo6YxcYefw70WL sORLM8vkNTgkx7TiyeJC+A4= X-Google-Smtp-Source: APXvYqyDYVnbE1d5gsDW7T+ihq4u7GVDxbn2N8w4wRAjY3oU6gC8Tl7ARn4E8+4C1XGswpJXl7H6sQ== X-Received: by 2002:aca:685:: with SMTP id 127mr3078733oig.58.1568595871731; Sun, 15 Sep 2019 18:04:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1a12:: with SMTP id a18ls1506841oia.14.gmail; Sun, 15 Sep 2019 18:04:31 -0700 (PDT) X-Received: by 2002:aca:cc96:: with SMTP id c144mr12256512oig.72.1568595871231; Sun, 15 Sep 2019 18:04:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568595871; cv=none; d=google.com; s=arc-20160816; b=T2Yj2MzBmffPx5XGeYsr9ildcChhpGdupp2gDGaGcXlhTcTx6wQNo8HtSnOzAww5gW beWlCSXEr8gAl81U3XQEO32njGi0UI2VRy0IU3TrnFKci/eq9ZICESvKmyNSkJYek0GD z6PSUHxiClzTAcUflsdQn7Z4TFrUZjfutqkaKPmzfJWfEX9s8LS1k4mqaoU1nuDMKzE+ kHLkLyVzqSaRlt6WNKBdoEdMdEmd4reDFiGK1x/IaMDaFl/ALyunXIjNrMZuLO9CKF1L 2p8I4/vRlemwhjM8C8eELj25F065ai4mWXi7bosXkFOfORwGtPihW8mg3ODYnnS2NOoj 2N6A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:to:from:date:references:in-reply-to:message-id:mime-version :user-agent:dkim-signature; bh=G3Z5ASNw3FG42988/mlfW4q/uZ58BwGuzJGeIvySqu8=; b=DnG8j3sOpXC6S9rFnQzgrlYD9dA10fvwuCuZbzBinKaEmIUw90wQGeIf8GBwGL0xIY 2g+Y7lKEa5y9Dvwm2VpkYIIXuHCBXVNd5L6N2AqpIVccy7421tfS1MDG12RHSvCPmD2/ Yjiw2Go0wPYdMdpcxleR2GfWVw2Csq8UDwoO4VomUeiuOFGWJI8oyi9kL5IGPzUQdLgo xajGPGrZmj5IRPnxDDzawQS3DfHkXSfc68m1bSbJfGTtADZ/ERDXejmb7VCtLHhu86MZ SIYY1/5yg33YXNPbHn3SgnxiOMgXBWdoQUPnpw0X2q1vdiYa5fWe8V6hCKqgU/7wsMAn yDtA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm3 header.b=R6NA1Fgp; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out1-smtp.messagingengine.com (out1-smtp.messagingengine.com. [66.111.4.25]) by gmr-mx.google.com with ESMTPS id w8si3969otl.2.2019.09.15.18.04.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 15 Sep 2019 18:04:31 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.25; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 8731C2104A for ; Sun, 15 Sep 2019 21:04:30 -0400 (EDT) Received: from imap5 ([10.202.2.55]) by compute2.internal (MEProxy); Sun, 15 Sep 2019 21:04:30 -0400 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedufedruddvgdegvdcutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfghnecu uegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmdenog fuuhhsphgvtghtffhomhgrihhnucdlgeelmdenucfjughrpefofgggkfgjfhffhffvufgt sehttdertderreejnecuhfhrohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjohhnse hjohhnmhhsthgvrhhlihhnghdrtghomheqnecuffhomhgrihhnpegrrhigihhvrdhorhhg pdhgohhoghhlvgdrtghomhdptghhrghlmhgvrhhsrdhsvgenucfrrghrrghmpehmrghilh hfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmnecuvehluhhsthgvrhfu ihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 579405C0099; Sun, 15 Sep 2019 21:04:30 -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: <80a2be3b-afaa-4106-9c69-0df6567ec709@www.fastmail.com> In-Reply-To: <16b3b92f-069b-468c-94f8-f3859e152338@googlegroups.com> References: <16b3b92f-069b-468c-94f8-f3859e152338@googlegroups.com> Date: Sun, 15 Sep 2019 21:04:10 -0400 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Re: A question about the problem with regularity in CCHM cubical type theory Content-Type: text/plain; charset="UTF-8" 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=R6NA1Fgp; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Content-Transfer-Encoding: quoted-printable 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 Andrew, Does "all monomorphisms are cofibrations" imply that identity and path type= s 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 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 universe = does not satisfy regularity. > > Since comp^i [ phi |-> E ] A is defined as (roughly) Glue [ phi |-> equ= iv^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 regulari= ty 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 r= egularity for the universe was supposed to follow from a different argument= . > >=20 > > Context: > > I've been studying and using CCHM cubical type theory recently, and oft= en 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 th= e composition operation, but as discussed in this thread on the HoTT mailin= g 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 d= egenerate in that direction, reduces to just the bottom of the box. This se= ems to be closed under the usual type formers, plus Glue, but not the unive= rse 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). > >=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-468c-9= 4f8-f3859e152338%40googlegroups.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/80a2be3b-afaa-4106-9c69-0df6567ec709%40www.fastmail.com.