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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, 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-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cc6c2fc8 for ; Thu, 10 Jan 2019 21:37:25 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id a19sf5189678otq.1 for ; Thu, 10 Jan 2019 13:37:24 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=VVYhU3aFc6ugUS/d0sDkdZI0h8q8+e4fC5ZG5xqQZdQ=; b=Gf2V2rfy7TZNZEvQ/pA4w1UDiUV6vSrs2WxLIYuuB/01LnyZh4O36yEEbg+YJRXnGE WFMhfIqXHA6zdRjv2t25oAGAdlLlMl8hUUv2aSbhwQ/weqtrRfSu0yj5wuUnv9DClRVC 4oZQUpxIMitVG7Su82y38jyCXbrXqOeC4Dl7I+F+lty06m2ehwKV6Zv2S97nrwTwmaZd VZ8b6cB/mzIONyPACt9YrBMTaPO9vkR+eVOEimddN1yHqJRWvqgaLsUBSreCOIbQqoWO D2htwZzqFJ0TZO8jXpiVG0mrmQHFpY8WPlwj2xwqeXU0H3qyDs02p5sTvnTJQVkKQVIN CTtA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=VVYhU3aFc6ugUS/d0sDkdZI0h8q8+e4fC5ZG5xqQZdQ=; b=riVrJNoomnL0pTJVQ3NIPGdweXFqadgsW8pt88cm4CZQizbJmlz9tF4XyKVdkKxxM9 VoRUNI/kMGoseYmiOlZI+aticAJuz/4qphZk3ib1+5UmzIPCOciqQ6bUy02Ggb7ophHn wVDA3Xt/Jix+f9keVyRUsthLncIVip+Ffz4udBwDCHVFKnUfZkGLrjHFQh/Z2Oia0cHh koFrq0txPkmHCcBnmpJL1WL0Y2yrmhGUN4cLh+hyOgB1zZ6nuFDD/y7TOlfjymykmnjQ MXNineBOxa7Vqwjn7PnLZoKeA8F3nXdVnDuTKek+95+hDL7+rEgizSG7MfTbb0Fhl+NG bCTw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=VVYhU3aFc6ugUS/d0sDkdZI0h8q8+e4fC5ZG5xqQZdQ=; b=man+r8KfWpiNhgl2DkQSDH9jYtNlQIXooQt1Emv+KAqZAkb8RoISsqRyxwEna0jsW9 BYamutuFwpFfQNoVnyZaVslB3Q29x1cvFGj+TNaj9yMohMsyTTLNhdGcKnbZxNnHK2av MU8NPX6ZaF7Z2nFA7xfbI+kebFqUDD4CaF9tMUlJSOCN5bso3LukACJzOITIAypemgqY GL8tiUBBXcvLYtjWMEHrgC5L1JAKOqmt69QkM0fme41EYdCSFOuPb7FXvCHX2FrQzK9i XNMmPSCLwoGxAb1qs5pz6ReM0ol0RpC4k8qc9GKh9P1GcUeNgJ46vHi98vQwEg8T36pr JAHQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukfrYZ2db69ki9VBTpF6IyP+12HY3P758FaOoh6ada943QcXxFjD imUeNve31xdBcCVM5qLWMa4= X-Google-Smtp-Source: ALg8bN6QK1uebRpDgHWbS7Ud2IZezqa1ZIF8PKnQR5QoTCX4B8g17Bexq0GHgWpEg7+w9HVfL7WiOQ== X-Received: by 2002:a9d:6f9a:: with SMTP id h26mr145483otq.0.1547156244068; Thu, 10 Jan 2019 13:37:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:7e81:: with SMTP id m1ls881414otp.9.gmail; Thu, 10 Jan 2019 13:37:23 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr143124otb.4.1547156243256; Thu, 10 Jan 2019 13:37:23 -0800 (PST) Date: Thu, 10 Jan 2019 13:37:22 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <8ede5289-382e-4ef9-a234-a7d830dfaac4@googlegroups.com> In-Reply-To: References: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> <45e2ceb4-dc90-4d66-a728-d075bccac399@googlegroups.com> <510281bb-5b88-c64f-a8ac-5807365e096c@cse.gu.se> <8cf858c0-6778-4d7f-98c4-68210041b857@googlegroups.com> Subject: Re: [HoTT] Re: HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_550_1731647661.1547156242612" X-Original-Sender: escardo.martin@gmail.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: , ------=_Part_550_1731647661.1547156242612 Content-Type: multipart/alternative; boundary="----=_Part_551_1094952753.1547156242613" ------=_Part_551_1094952753.1547156242613 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Thursday, 10 January 2019 21:05:09 UTC, E Cavallo wrote: > > Our recent paper explains how to handle inductive families in cartesian= =20 > cubical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf.=20 > Nice. =20 > We believe something similar will work for De Morgan cubical type theory,= =20 > and I think Andrea and Anders are planning to work that out and add it to= =20 > cubical Agda.=20 > This is good too. =20 > For the moment it looks like cubical Agda will let you declare inductive= =20 > families, but will not reduce the Kan operations in those types. > Right. For the moment, you can prove that Agda's identity type (defined as= =20 an inductive family) is equivalent to the cubical identity type (because=20 both have refl and J). However, the computations get stuck. In fact, I tried this in order to be able to use Agda's pattern macthing on= =20 refl, rather than J on the cubical identity type, by going back-and-forth,= =20 but, as you say, the computations get stuck.=20 If you manage to get the computations to go through, as you discuss above,= =20 with the work of Andreas and Anders, then this means that we can start=20 using pattern matching on refl in cubical Agda without having to change=20 Agda in any way other than accounting for inductive families (by the back= =20 and forth trick). That would be nice for me, because what is preventing me from migrating=20 from Agda to cubical Agda in my univalent development is that fact that it= =20 is populated by definitions by pattern matching on refl (and everything=20 else) everywhere (according to the Agda style).=20 So I am looking forward to the outcome of the developments you are=20 advertising. Martin =20 > Evan > > 2019=E5=B9=B41=E6=9C=8810=E6=97=A5(=E6=9C=A8) 15:54 Mart=C3=ADn H=C3=B6tz= el Escard=C3=B3 >: > >> Actually, I think it is not a priori clear how Agda's --without-K=20 >> interacts with --cubical. >> >> For one thing, the cubical identity type (derived from the cubical path= =20 >> type via Andrew Swan's technique) is not an Agda inductive family and it= is=20 >> not Agda's inductively defined identity type. And also, as far as I know= ,=20 >> inductive families RE an open problem in cubical type theory / the cubic= al=20 >> model(s). >> >> Any development in Agda invoking --cubical that tries to be sound should= ,=20 >> for the moment, refrain from using inductive families. >> >> In fact, in would be good to discuss the precautions one should take whe= n=20 >> using --cubical in Agda so that one is guaranteed to be consistent, and= =20 >> better, be talking about something that is currently understood (such as= =20 >> entities in the cubical model((s)). It is not entirely clear to me which= =20 >> features of Agda we can use and which ones we should not use and which o= nes=20 >> we could use if we knew more. >> >> Martin >> >> On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders Danielsson wrote: >>> >>> On 10/01/2019 16.19, Ali Caglayan wrote:=20 >>> > I was under the impression that this was in plain agda, that's why it= =20 >>> > was more suprising. I didn't realise it was about the cubical agda.= =20 >>> >>> You get Cubical Agda by using the option --cubical (for instance in a= =20 >>> pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound= =20 >>> to import Agda code that uses --without-K from Cubical Agda.=20 >>> >>> --=20 >>> /NAD=20 >>> >> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> email to HomotopyTypeTheory+unsubscribe@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout. >> > --=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. For more options, visit https://groups.google.com/d/optout. ------=_Part_551_1094952753.1547156242613 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Thursday, 10 January 2019 21:05:09 UTC, E Caval= lo wrote:
Our recent paper explains how to handle inductive famili= es in cartesian cubical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl= 19.pdf.

Nice.
<= div>=C2=A0
We believe something similar will work for De Morg= an cubical type theory, and I think Andrea and Anders are planning to work = that out and add it to cubical Agda.
This is good too.
=C2=A0
For the momen= t it looks like cubical Agda will let you declare inductive families, but w= ill not reduce the Kan operations in those types.

Right. For the moment, you can prove that Agda'= ;s identity type (defined as an inductive family) is equivalent to the cubi= cal identity type (because both have refl and J). However, the computations= get stuck.

In fact, I tried this in order to be a= ble to use Agda's pattern macthing on refl, rather than J on the cubica= l identity type, by going back-and-forth, but, as you say, the computations= get stuck.=C2=A0

If you manage to get the computa= tions to go through, as you discuss above, with the work of Andreas and And= ers, then this means that we can start using pattern matching on refl in cu= bical Agda without having to change Agda in any way other than accounting f= or inductive families (by the back and forth trick).
That would b= e nice for me, because what is preventing me from migrating from Agda to cu= bical Agda in my univalent development is that fact that it is populated by= definitions by pattern matching on refl (and everything else) everywhere (= according to the Agda style).=C2=A0

So I am lookin= g forward to the outcome of the developments you are advertising.

Martin

=C2=A0
Evan

2019=E5= =B9=B41=E6=9C=8810=E6=97=A5(=E6=9C=A8) 15:54 Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 <escardo...@gmail.com>:
Actually, I think it is not a priori = clear how Agda's --without-K interacts with --cubical.

For one thing, the cubical identity type (derived from the cubical path = type via Andrew Swan's technique) is not an Agda inductive family and i= t is not Agda's inductively defined identity type. And also, as far as = I know, inductive families RE an open problem in cubical type theory / the = cubical model(s).

Any development in Agda invoking= --cubical that tries to be sound should, for the moment, refrain from usin= g inductive families.

In fact, in would be good to= discuss the precautions one should take when using --cubical in Agda so th= at one is guaranteed to be consistent, and better, be talking about somethi= ng that is currently understood (such as entities in the cubical model((s))= . It is not entirely clear to me which features of Agda we can use and whic= h ones we should not use and which ones we could use if we knew more.
=

Martin

On Thursday, 10 January 2019 15:28= :07 UTC, Nils Anders Danielsson wrote:
On 10/01/2019 16.19, Ali Caglayan wrote:
> I was under the impression that this was in plain agda, that's= why it
> was more suprising. I didn't realise it was about the cubical = agda.

You get Cubical Agda by using the option --cubical (for instance in a
pragma: {-# OPTIONS --cubical #-}). The idea is that it should be sound
to import Agda code that uses --without-K from Cubical Agda.

--=20
/NAD

--
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.
For more options, visit https://groups.google.com/= d/optout.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_551_1094952753.1547156242613-- ------=_Part_550_1731647661.1547156242612--