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=-0.9 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-x53f.google.com (mail-pg1-x53f.google.com [IPv6:2607:f8b0:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d5050196 for ; Fri, 13 Sep 2019 06:10:42 +0000 (UTC) Received: by mail-pg1-x53f.google.com with SMTP id j9sf16288626pgk.20 for ; Thu, 12 Sep 2019 23:10:42 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568355041; cv=pass; d=google.com; s=arc-20160816; b=OAmOZ2fD9WZ02mneAW3cI9ro4XwkQUvKuhvHtM2hFAJ//0HQ5298m4fGulgqiV0BI4 UMG5LdEHMFpzWm/5ulU2nK1TN8zcgWjtjZcBlJqV+STbfBVo7e3Oz7MXV/PXQ+FJr4/M EKeFceeeBJlxNUXjKY8m2Tqu7gIzHf10yHCvNIskFTclDO6uwzh8wf1LRioGG76oyywN LtyS537+COOqRghuFQFJI/xRXDMATb0HYs/VqF0AZd3RTF7veA5dglXpvEpeo6hia4ut fQVXwZk6XTU+YJBi/b6didH3nOcsPzbBL0HJWatG0adfW7b7DBysIf+sduqxG7gNq8gv LKRw== 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 :mime-version:sender:dkim-signature; bh=v4zVHWpmVRy1IQdI/6ulpvi+IMXRDctAE5ZwO+6OQng=; b=hKal2OddA7NTMBO1uz3s40fQwq/Dmh6M3oJ95q9g1ZbWRVDcC2B+VxdaYSGsU6T+0X 8OfE1+RlZlGhXvBjtvBFUOlNaD22qIQePicXi8KYd4kwBizloazF8Mp7ULDDLBFgKzwQ Tkmcjc27S87Lcy/GAEHKeVgkSSCpfZ/8BcXZg1DkefIgm8qkJ/v1vWp9x1DjtMfcEp9Y k0dHyTXtut03x8+iptCDugqZGh/tPa15FysUaobD/9j36otCp7Nsm0KPhyLI4qcYyorG XnfWNroneAoK+aSpIEJmO0A0/Wvw9jQV4TVRHPWebm0gujaFP24n5y8ThrPJ6r50Hxhk Q9DA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=REUesWRE; spf=neutral (google.com: 2607:f8b0:4864:20::335 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: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=v4zVHWpmVRy1IQdI/6ulpvi+IMXRDctAE5ZwO+6OQng=; b=CH0wBiySi5RNNJyZfDx57QwPgYmFJH8oeb69tHSpOV3wKZbPb1oNH4i09s9MUWDJZz pIOeg4s1AzoxTneRQqHd279oBu4ejzje1YyqISJIrPuQknBmx5v5ZW/Jf5tZ6HFMY2vA 1PV+q1kJyAnj5C2s1fF/BXBlT+RabO6r+HQ64hRSQnNV66oDW78kKWv76mtFycWt6LkZ F/Wyf70Fh8Chz1khwBg5Fa9Rb6nA1pLrje4AC01HjOjgEidOQ2bor5yJLVfy6CpGpQfS xFGyB8qFg3zIsTVUYeX1IFS7u/GulJtMixdpFKEsBXZmnPuFn+TjUE53M35Optd0+wqr RQ0w== 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: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=v4zVHWpmVRy1IQdI/6ulpvi+IMXRDctAE5ZwO+6OQng=; b=QXzVjYx32FdaR3Sqz1j/kmGvCWBLXO34MNWpxEmzivDYg6CCVdC/VucrElLUK1pVR3 V9ekniXLmd510WHMktki1SH5dzm+rPk+3C83SJzzdl5qlAMCxRBox4u75zzDPBs7MqD1 j0TgYh0MX8Fgh8hAhgmXKnpYIsWJzVcmVNg8ZlKuZrXwk1Td+WjmHaSY7Iw3CflXVFvx ONWFhIQT2J0Ac+k103TGa40xTHA0ZmZXPm2hVagH2PCqgDcBwPsEj332qZmOzapE0HT/ c9xsIgaROpVBybxJ/HMIkB8GQClDdEFIo8mRq0l1/HNqfs6Q2NhnuxSP/h2+iS8xj3Om QyPg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXyd63CK+5wq9v5VESi2NvdT46s/WyJBMLeBavdwADZxoRgyZYs mgEgKAcen7EVysoVW925Eo8= X-Google-Smtp-Source: APXvYqx41W2QtvqzaTzMTsHLfY/c+07U9feWEj1nglh1+zV5x8Bb+dfqnmwj6uJDCuFr1wPTg8YEcQ== X-Received: by 2002:a17:90a:340d:: with SMTP id o13mr3200721pjb.19.1568355041279; Thu, 12 Sep 2019 23:10:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:a9cb:: with SMTP id b11ls7022363plr.8.gmail; Thu, 12 Sep 2019 23:10:40 -0700 (PDT) X-Received: by 2002:a17:902:9896:: with SMTP id s22mr35472645plp.207.1568355040866; Thu, 12 Sep 2019 23:10:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568355040; cv=none; d=google.com; s=arc-20160816; b=Qk8j0keSSltuEH0Zc/jWKAvC9aCiroe24m+W6kp24OyD2CuRyt+/MHQj2qTb/ztP0V MnnsDwQkH0uwlkBJ0ak+7TNfBaJ7taAvcPDpsJjVzIbrZh4qC1kTkZZ7uCs9nMmwdBbv vqj/QcbymEteElEnjuF0eleaCEXeMxoFNsYxzRim5oy33CDNknEGtHKVl38X+OphsxOd oFxzu2WIQA7UQnZdlnnKMt/Yj8Naa+PEesbDOi7X2Od1x5HvffTJzJNoKbStPFAi+3Ji XureuJ1M7jix99/yCP/nismJTejJ3i/zIt26t/xPhgidpbw4uCqLp1yaAcy2WjVTmym0 w4cQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=Lgp/6ZIsfyoa+YgQhz//AKazlXflZoXp5uEK1tzKaFc=; b=Apk2JOGBVrN4uBrbGoR1lJwghHRHKRlcwsl94URKkxlWDSo3RficUSU3IeB0MYjEve vISClFI39zEoFS4rdyToXlV8xcWgz44Li89nwQzRduZEdm08LVQbLOLqVTkQ7LFxfZan qnqDx/2u+FqttnndD2Vtim94C7jSUk06MKVvdscdWZRgN+4vDb63mFtgXr5AqRM66gJn lXYh2sOCPj5FtEh0ABhDXi9n4xGUbsfvohU4u83/gxV2YkwVOX9CnwhqMVC5JDXy0hHi GPg8TO7UzA1IHKaBJtZJQ9/4ApbpC82SoUpDn9BLSQ5cK9JcP8U/wI87H1tRCy3ZyMfk DvZA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cs.washington.edu header.s=goo201206 header.b=REUesWRE; spf=neutral (google.com: 2607:f8b0:4864:20::335 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-x335.google.com (mail-ot1-x335.google.com. [2607:f8b0:4864:20::335]) by gmr-mx.google.com with ESMTPS id b64si1857455pfg.0.2019.09.12.23.10.40 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 12 Sep 2019 23:10:40 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::335 is neither permitted nor denied by best guess record for domain of jasperh@cs.washington.edu) client-ip=2607:f8b0:4864:20::335; Received: by mail-ot1-x335.google.com with SMTP id z26so19152341oto.1 for ; Thu, 12 Sep 2019 23:10:40 -0700 (PDT) X-Received: by 2002:a05:6830:2058:: with SMTP id f24mr10578116otp.65.1568355040209; Thu, 12 Sep 2019 23:10:40 -0700 (PDT) MIME-Version: 1.0 From: Jasper Hugunin Date: Fri, 13 Sep 2019 02:10:55 -0400 Message-ID: Subject: [HoTT] A question about the problem with regularity in CCHM cubical type theory To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000000dc3820592691dc6" 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=REUesWRE; spf=neutral (google.com: 2607:f8b0:4864:20::335 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: , --0000000000000dc3820592691dc6 Content-Type: text/plain; charset="UTF-8" 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-a8fo4FKCLiCVCYm6AGeVc%3DqB8QNUZ3Weho6kLT8NXtc-Q%40mail.gmail.com. --0000000000000dc3820592691dc6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello all,

I've been trying to= understand better why composition for the universe does not satisfy regula= rity.
Since comp^i [ phi |-> E ] A is defined as (roughly) Glu= e [ 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 t= he universe was supposed to follow from a different argument.
Context:
I've been studying and using CCHM c= ubical type theory recently, and often finding myself wishing that J comput= ed strictly.
If I understand correctly, early implementations of = ctt did have strict J for Path types, and this was justified by a "reg= ularity" condition on the composition operation, but as discussed in= =C2=A0this thread on the HoTT mailing list, the definition of composition for the universe was found to not satisfy= regularity.

Best regards,
- Jaspe= r 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-a8fo4FKCLiCVCYm6AGeVc%3Dq= B8QNUZ3Weho6kLT8NXtc-Q%40mail.gmail.com.
--0000000000000dc3820592691dc6--