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-yw1-xc39.google.com (mail-yw1-xc39.google.com [IPv6:2607:f8b0:4864:20::c39]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 60173f48 for ; Thu, 10 Jan 2019 21:05:10 +0000 (UTC) Received: by mail-yw1-xc39.google.com with SMTP id u126sf6581485ywb.0 for ; Thu, 10 Jan 2019 13:05:09 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547154309; cv=pass; d=google.com; s=arc-20160816; b=ydynFz+qetPgsCh6mpbzQG5lgZdDcp6grGJ25HTQTKHqFz5kGBnXn5bMbHRa3b6QPT +Yl/GPPVgUBJ0Gr/vlmv8mg06j5avl/t4ZOrQ0sFe9/OxlLM8wFxLaA+pgYAJI2Chy3A 5fuegpytJrudVzIRWkMf55OcwCmJykCL0dZTBuIhagFssHR7670V9Jb2l+787DlRw9z1 JfLYesRzFT4dSLNjhsxqHKzNkwKK1GjEsjjEnjqpfGz50rrETqvE/3rpjM8fjMkL64l0 lJMdKXwd5aJkQ+LflyCmdVBKXOhNlY7pbCqjGSV2csVJaxg2/nBbWH5gmOCfCXbZG9cS egSg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=735pdwC5r5Xrx0OPW/mqy/KaZFnNWVH/nX4htmbSTgs=; b=Tnt6kV2ROsUGgnIbc1Kx7Erps1Ot8kYSQOFLi9PkcmB7PKrfMyGqPOhbCcmDtTP4kj 6zsH3M/FHpPyVQInz0cBqjQtcbE0/+Rnur5j2KRRogsm5e/COfVuN1Kb7wSei2gy1gdp U7SjYK0anb0dR7xoxv7BLVA2hXhuMFZUz5dnxYt21zFzk/eGz3w6VtpJ+a/nQw1ee1vd B6JtypSxFGw4g5s13nZYmm6Wng3UbccIDoa6SvVehlxRQWEBhdZGjEkw6/3iM+vM4Dqs 3edTil/QdxhU01b7qHcPgmBcj5UbFrIajC7HB0W932kEckoo2tk4ZySUBAu/ESjDST+z euTw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=oIAI2oy3; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=735pdwC5r5Xrx0OPW/mqy/KaZFnNWVH/nX4htmbSTgs=; b=b3nhA3qCo6hqQVbH9+vQbSo6XN30G4PsBVKuTB0EoPw1oRR5foI7TEdBHG9d5Mptjn 26J2SDP8E01fSFa7wsWQKcmwXf7K8v3sp6SL8DNThhE6xpzommgqCQgSuzfWVumeVUol kQ370xNcUdPb8iA5sFmX46AC+t1ISlNrCgnhQLIOzA4b7w4HdDGcS0n5hapUGLWn/CVA 8H78YqKuoCscJLYTOKUdzoabW8mFLti+lUpUFDDlkYR5c8OF2DRRRNUxqDfCLRAAM1k/ 5thR7qu8ibZbzz1T8n6b58nD08176TF5O/KE9eQeuVg5wZ914/9YwfBKFrWTUn7crEx1 XGsg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=735pdwC5r5Xrx0OPW/mqy/KaZFnNWVH/nX4htmbSTgs=; b=iWSxKf080eHOb+BnsBZ0bfRGiNCYICKOEcJXxjuVTYBmHvgrqApnxGtExTnf/xK0M/ vGgMKxEr9BzYkFW/2VHw9T51GQDIHyQzkSexVtxSZqoT9f0aBlwzZMSAO4TU3YqgSrxK 3Z2pR3HBrg6rYpcMI/JxfkefE1huLUKfnTSt43aLONN1VcbuUoVDQGXFmcQPZFnXPFCL RO56FxhTl0xHAhyp+wQwaF0luYzc9ThPh9uRM0OU0wnXW9+vX7xNEQKTtgNeLrzmFYmW clS9mIkJIm+ZNYz4gLIF2GZS3hGFzF45W5rVyuwiatr4c3lNuzlPNF5rbFp8z+wl9vJF L2YQ== 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:cc: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=735pdwC5r5Xrx0OPW/mqy/KaZFnNWVH/nX4htmbSTgs=; b=RbMaL8VtyopVxN8KpkECmwbJAulTgGlp8249c8MBalrCmdhlFISnTn7crgv96QYi8k acVBLhQyamwW5Ab+VCoKxu1SNfZWgJaIJmJFqsNNQq6YvyzHA7rzDtrZAT4OfjXHJqi0 kB6gS65/MRPhnWrCEILJiIgCa3lyjv7KgqjJGVDsedBLb6ssLQ7tokISYpKSKjtb9FI1 7fyxNKpFpdK6VJnYL0YYFSn8ynXRiBWPWiMnr6s8ON9eUPoZVP4iNqjGT6T7rH9uWFre 9yvnUbuSssVex2Q3n6ydzJC1vsoqXZwJe+xseOkgl2SBLwQ5GDHjZZVHZy91L6r3DbmD ISFg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukf+gwafXBXFCIEw02clFbPLNij+4e2BzUyQv9VLon/S6XgquNWl 6kj3+PVWLQreeJo0uPInGoo= X-Google-Smtp-Source: ALg8bN6G2HEACT79tnlL8ihAZMDFVqRuFTiDEiiEViOe7pDO+yTFHpLOyAfcuLqCl1q+lR9dX6gGqQ== X-Received: by 2002:a25:9bc9:: with SMTP id w9mr76253ybo.5.1547154308953; Thu, 10 Jan 2019 13:05:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:238d:: with SMTP id j135ls3191053ybj.8.gmail; Thu, 10 Jan 2019 13:05:08 -0800 (PST) X-Received: by 2002:a25:388a:: with SMTP id f132mr3558244yba.82.1547154308492; Thu, 10 Jan 2019 13:05:08 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547154308; cv=none; d=google.com; s=arc-20160816; b=eRIata83weUansVeaDzwEx6Oyzcmve4TD6j+fAobw8mQTskiC4TbY18fAJNLTVVf8n 5ey3AqylZV5OSspNsYk2ufyY1O+f3Am4qv16i66X2sE/gVnGsB2mvQCMAzISbe8cJUTn y63+7GdTITLYO93rtiYWmD5ImLAR/kJ5uXLnV5URfNBIcvFXi3PJyEMDDt0JZsHzz5BV or45WcWZDhGJ++/PA08v4/Prym2Q/aiL0frS9Xwo7h/x/u55AF0DTbQJgmhBfBL1RZG/ Nq5MXU2sqzghbmUoxOai6jejm1X5nrWSEG/EE4jhmxx5qZOuoWD3of8XfUcdJi8Yuf7c WqGA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=TYD/LySmvFMZiNUoSKFHBt89FUwopcZk66ikGJHuvlM=; b=bG1Q2DsadLGY/bSMkXILMAu1qkzFv3dgXj4kmAgbRSmeXM9NLi5ZHMKF9VIXKQTqPK DeX2LdeiRyFbScqll5EfnrfhI0eA1F/Itor8GGD5rMRoqLcnoHIsyUlmmTtTTOTU1yvu S2Wy/jIe/QAIeNpSzw6V4UewGb7NEb+Hga6CE3WCGkvru2uRubSic0gVJ64KHlcuCKdq JFzYSv3I9Qib2wCz2vu2W7eQSjj/exF1MLQTTjSJygz66xvFwP/WvF2K1vpQA0H4gEj+ wXHL7519BYHKa4KIDPFwMnkSukWMEFD5wLLQPnbWf0MeMgXcoB6HVv9yILjiJkJQ5dcK Y6UQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=oIAI2oy3; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-oi1-x235.google.com (mail-oi1-x235.google.com. [2607:f8b0:4864:20::235]) by gmr-mx.google.com with ESMTPS id i1si4386727ywg.5.2019.01.10.13.05.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 10 Jan 2019 13:05:08 -0800 (PST) Received-SPF: pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::235 as permitted sender) client-ip=2607:f8b0:4864:20::235; Received: by mail-oi1-x235.google.com with SMTP id m6so10443916oig.11 for ; Thu, 10 Jan 2019 13:05:08 -0800 (PST) X-Received: by 2002:aca:4155:: with SMTP id o82mr7775839oia.172.1547154307995; Thu, 10 Jan 2019 13:05:07 -0800 (PST) MIME-Version: 1.0 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> In-Reply-To: <8cf858c0-6778-4d7f-98c4-68210041b857@googlegroups.com> From: Evan Cavallo Date: Thu, 10 Jan 2019 16:04:56 -0500 Message-ID: Subject: Re: [HoTT] Re: HITs in Agda To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000f0de2d057f20ee0a" X-Original-Sender: evancavallo@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=oIAI2oy3; spf=pass (google.com: domain of evancavallo@gmail.com designates 2607:f8b0:4864:20::235 as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000f0de2d057f20ee0a Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi all, Our recent paper explains how to handle inductive families in cartesian cubical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf. We believe something similar will work for De Morgan cubical type theory, and I think Andrea and Anders are planning to work that out and add it to cubical Agda. For the moment it looks like cubical Agda will let you declare inductive families, but will not reduce the Kan operations in those types. 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 : > 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 it = 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 cubica= l > model(s). > > Any development in Agda invoking --cubical that tries to be sound should, > for the moment, refrain from using inductive families. > > In fact, in would be good to discuss the precautions one should take when > using --cubical in Agda so that one is guaranteed to be consistent, and > better, be talking about something 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 which ones we should not use and which on= es > 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. >> >> -- >> /NAD >> > -- > 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. > 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. --000000000000f0de2d057f20ee0a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi all,

Our recent paper explains how to handle inductive families in cartesian cu= bical type theory: http://www.cs.cmu.edu/~ecavallo/works/popl19.pdf. We believe somet= hing similar will work for De Morgan cubical type theory, and I think Andre= a and Anders are planning to work that out and add it to cubical Agda. For = the moment it looks like cubical Agda will let you declare inductive famili= es, but will not reduce the Kan operations in those types.
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 <e= scardo.martin@gmail.com>:
Actually, I think it is not a priori clea= r how Agda's --without-K interacts with --cubical.

F= or one thing, the cubical identity type (derived from the cubical path type= via Andrew Swan's technique) is not an Agda inductive family and it is= not Agda's inductively defined identity type. And also, as far as I kn= ow, inductive families RE an open problem in cubical type theory / the cubi= cal model(s).

Any development in Agda invoking --c= ubical that tries to be sound should, for the moment, refrain from using in= ductive families.

In fact, in would be good to dis= cuss the precautions one should take when using --cubical in Agda so that o= ne is guaranteed to be consistent, and better, be talking about something t= hat 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 which on= es 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.
--000000000000f0de2d057f20ee0a--