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-oi1-x23b.google.com (mail-oi1-x23b.google.com [IPv6:2607:f8b0:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 62a621ae for ; Thu, 10 Jan 2019 20:54:42 +0000 (UTC) Received: by mail-oi1-x23b.google.com with SMTP id k76sf5771383oih.13 for ; Thu, 10 Jan 2019 12:54:42 -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=tU2+UCBT/2jSQCOAeyDokJ9VKoU0JGCRzos7VN9YC8I=; b=bccPpwaMuLmVxPwTTMKkF2t94b7OLf89wUboNBSD0XyYKKNFhIrxAdLTor/gPLHihC KVtdf2UP9OqoPalVRR4z7Ypa3iaX6pwh94e/TN88/i3iC2wiKUuvusGWK1mIvyA5db96 p6yDURj41mVAnqBBwY9B0v6foENBSilrp8Oyc/PkAcBDvkRZutOBbgYCu7t3oSIEc+vx LNty6j2fgJZoEtnlPbqaiSis9Z6SmhnxESMNz4SMzoffW57SvUr2IWy4/Xb20kNFmTG5 mfjlccoBju3tyFMMRhAibXJ3A4J7AQrfZJtT7+EungxwBh7Q/cYApRJ+Kq/rivHNbRJx rimw== 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=tU2+UCBT/2jSQCOAeyDokJ9VKoU0JGCRzos7VN9YC8I=; b=VpaGdmN7SmB6Fept+8aGSKKEzU/yDBrxcChgZ75xzFvuiynCKfUSPSYz/tydF8camB RUph/u0tsFdYfhDoRHnwLLWYxEa/wp14Y/G+MEDYjihqns87Y2ryLVzSIWYLOHU8GSgZ aMNzfNJhRI1W+18ZeyKta7T3gyw4UnO3Zsqnm67RfcOP2NFvM0M0NQ1Ne5pV9PRTo2y0 iMDzHJ/V246H98wrhKqvXDf/oVGvuv9H6DNg7j3BdQRkv4yCHBnzEGXn8blYBLm2yobq /G8JaFuHUOtvMt3YkPZYnGtfWjRfq1srDJCg1jNa5m8FT63a3K3Fv+dMVCPyCxqSHM3G cojg== 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=tU2+UCBT/2jSQCOAeyDokJ9VKoU0JGCRzos7VN9YC8I=; b=ceNGhGD0PcsMjMnhWHDAkRFlqzx/v+LGAXUiF4O7xdXaSAMtqFD/p5GZ6DphSb1txi Fj+cGovAZGm2FNwB1yhsujLc2Iw+gvzUI4KEkzXKeHNjjKAm9Lnb0ZFHNKYek/wjRKgQ MRg+HFkMPgPZxhe2mDOK5IMk7V+QK3Tk61omHIncZ1vzXswhOtu0D/JufpadfcW71K3v lV2ywGp/j//DBGt61li9Llc/QA4JZUf2amryaJi7g8Qk5Tbkt3QkX61mXa2K6N+ubXFZ ldzP+lPEd1Q7dj9yzu9ICRm9q4bc72/am/I0i9z0Ki5v+BQVGZHgj/9crSqO/JsWWrF2 sBFA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukdqxepvw86SCKX/Uq6hvmSJIe7lUF0Vb2TJt3pC4Y9bTRPrGUWv PCOcrmMiepP4bVo1y7tcnMk= X-Google-Smtp-Source: ALg8bN4opdWyM3XZhN7ouXWtBeGl/mWdOQ1vFNS+AZiiwYnchYOdMSqhhD/yXRGSZHHE50nXqxANVg== X-Received: by 2002:aca:308d:: with SMTP id w135mr66893oiw.0.1547153681357; Thu, 10 Jan 2019 12:54:41 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:f3c5:: with SMTP id r188ls5697441oih.8.gmail; Thu, 10 Jan 2019 12:54:41 -0800 (PST) X-Received: by 2002:aca:d607:: with SMTP id n7mr66387oig.1.1547153680794; Thu, 10 Jan 2019 12:54:40 -0800 (PST) Date: Thu, 10 Jan 2019 12:54:40 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <8cf858c0-6778-4d7f-98c4-68210041b857@googlegroups.com> In-Reply-To: <510281bb-5b88-c64f-a8ac-5807365e096c@cse.gu.se> References: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> <45e2ceb4-dc90-4d66-a728-d075bccac399@googlegroups.com> <510281bb-5b88-c64f-a8ac-5807365e096c@cse.gu.se> Subject: Re: [HoTT] Re: HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_546_1787411965.1547153680263" 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_546_1787411965.1547153680263 Content-Type: multipart/alternative; boundary="----=_Part_547_759305741.1547153680263" ------=_Part_547_759305741.1547153680263 Content-Type: text/plain; charset="UTF-8" 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 cubical 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 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. > > -- > /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. ------=_Part_547_759305741.1547153680263 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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&= #39;s technique) is not an Agda inductive family and it is not Agda's i= nductively defined identity type. And also, as far as I know, inductive fam= ilies 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 using inductive families.=

In fact, in would be good to discuss the precauti= ons 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 ones we could use if we knew more.

M= artin

On Thursday, 10 January 2019 15:28:07 UTC, Nils Anders = Danielsson wrote:
On 10/01/201= 9 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 http= s://groups.google.com/d/optout.
------=_Part_547_759305741.1547153680263-- ------=_Part_546_1787411965.1547153680263--