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=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-lf1-x13d.google.com (mail-lf1-x13d.google.com [IPv6:2a00:1450:4864:20::13d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b8a2b468 for ; Mon, 14 Jan 2019 22:48:30 +0000 (UTC) Received: by mail-lf1-x13d.google.com with SMTP id u23sf53118lfi.5 for ; Mon, 14 Jan 2019 14:48:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547506109; cv=pass; d=google.com; s=arc-20160816; b=Bnhpe2iTfO9MTQA3yzDHPQsLODsjpnXT7wwrsq+gMUHM9iYpnl5JEf0k3lQ8uFGIaZ plWTi9o3AEd9VU98lGWvJ+M/sf1lFaRDfXUd/d9rFj354aln8EyuFHvrdESQvFQ/sqOF cSYUqXEB8L3Oqd6j+45yGUSfm94MZIVM761kEI4aaBJDBA4wafJf8R0HMjRZ2wY7RFzN Cl2L8r/l0p3yfgxJ5UmRTCXQs+hLwflNh3+if491nCjtsuGU8vaQUtQZcjlCEmR8LDaR dJdFarQX2kjz7iGYyy1hfdnVih0STnuIh63WcDzFwAyWEfaS2nUHh8T7OxSzF8AmLo3V 3Ljw== 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:mime-version:spamdiagnosticmetadata :spamdiagnosticoutput:user-agent:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from:sender:dkim-signature; bh=T6yhnPRPpDeqMLrRdvAZzSJplCUOkSSqsSfbm6J8cxM=; b=UAVKK8L3/6NYTK7a/YnCWcrPdlJl7vt/1z5uLYSN84x7KmbizCYrToeF6iUaiMiGVp T6ff/CoSyKSUJ2xz6tUFaNZFFqM8V6EuG4/tN/g2UvaAmlUX0TRazkDNCdIv/F+Twg+I EhGhp3qvPpJk+mf4psfzTH3dLdbzmnlr3tGy4BqadhlV26ok/wYhCwKxUdb1PiaK+DkC 1w8yHzROr4ioY/J2FkBdniNDRKkO3oBGNz67sb4f7NA3vb08uqjs+ktMe5OQpH/Ao3T+ fUCCHhreS8sG12xpryfeqnVv/PsR42Y0DkHaAPgr1VnIRKOulAOj3nRH/j+qKUpDA5jB y/9A== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:user-agent :spamdiagnosticoutput:spamdiagnosticmetadata:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=T6yhnPRPpDeqMLrRdvAZzSJplCUOkSSqsSfbm6J8cxM=; b=N2EYbByUkjeNfEAYolr9au5gcoDFPnDDnGIr1FgxHGtMFmoif77WVABKJ7Up8sK3EL iErPxCYi3e3hqWKw+lH7NTTFJ+V0QEh10+u01HfrDfieAS34afL4+Zi9X1UDav6z31NS zGg1szAitYOxa9jX4l0/ZnQJGyYI+JPhmIBnjcR7cbpJVCx+AoLNYCO9B/xg01EKvXsQ AnjWR3DlTCUgkGxaPfZ9wzpiglvnsYIElruCSabtR/jq2s0Juo6teJmzhfnco+GwkWuV woelZer4DuMhWmG9g2v7pygmVWwQKVlgYdbtOiNRSXn/6Wo9L5OgvuhyqZo3gPf6Ce1n kFIA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:user-agent:spamdiagnosticoutput :spamdiagnosticmetadata:mime-version: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=T6yhnPRPpDeqMLrRdvAZzSJplCUOkSSqsSfbm6J8cxM=; b=IosnPMuJukTUdYz8yna8qheLv5tq/En3pdzP9Y0StBahR9k8bzb6AFqvYEfJMGeBB8 kO978Abx5DdNqnDZ39tOWbEinEDOaljyWd48qvEHOtPI4NN/pP2q+vF4kCcKCtFGuNV5 2pu34E80D88r8rO+2Qt4fDxaoby0xhP57M2uXqS98/wxYRT52JGLeO6rJWNWWvj84P9B 8fbRprsb1tJ6bu3jqymDjQQBgiPapM51fVH2q9CG/e15AZYeDiIMhpBt+nsa5gRxGJlz DQQSH4c7fWmwTdTROUAm7UJSzrpLDeVhbXwpyxT5gB+rrfwt4axGZ8nN9Pfi/iGKWhE+ 9LoA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukcSlsdgEHokra6CUXpqqtLSOTAtIbptARSv8Soq4rwx7fcQbTCV lJ3eaCVWcJnk+AzCUsm8dk8= X-Google-Smtp-Source: ALg8bN6rdViQZGbMQe6cU2DSX68YMuEee0GljlD5tOs7yTm6itpCL6UQMPBLoK3V6Rg5p/4jnoqE7A== X-Received: by 2002:a2e:98c3:: with SMTP id s3-v6mr3486ljj.6.1547506109140; Mon, 14 Jan 2019 14:48:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:4bca:: with SMTP id y193ls49934lfa.3.gmail; Mon, 14 Jan 2019 14:48:28 -0800 (PST) X-Received: by 2002:ac2:51b8:: with SMTP id f24mr40264lfk.6.1547506108384; Mon, 14 Jan 2019 14:48:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547506108; cv=none; d=google.com; s=arc-20160816; b=NHjVEIvB6/biYct2NZnvvKNeL2wu6G9jpj7UDSf4BkKImusnZW8SRK9+bFKU+Qv3rv yyApuI7WzVp6cvX+pQ+M3fgzjixxqTvRBQyzv5j2a/P6sKvWuHxNRt/DZA06cUYbKwLE JZ8zDaSX6qZTECZAgP+DeSC98icYPcEo9IpACzTkEFtGe5kGCC9aCWsfyD9j5H4SYEXQ R3m3+uTrJ4Gob4coCnxGsPDVki5x9Rsk2Btiu5V9QF11ivlRhKwysG1lbPZRqATiz8s4 WT0Gl3gStsUDqx9zEDHZ3YnsPyjE8EgjPzrJW+cI1W6liUHyWOuP3i3JYRM1PmQheeXU nuHQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:spamdiagnosticmetadata:spamdiagnosticoutput:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from; bh=n2bgK6PCm8r/9tDS0rfqEfVn67A3BajplmXIck/G5BU=; b=M/4DJOZiDb4WE+VHSaMfwMfY91egntaOBV3Wt2P4JK+ruBHXjZ9LxpnG4EYRaxMQeT kdnO4BwClhzJ6vih4skVWt8UQ6uf8UvzhxWYs44X65BJtyilwUzdROxP/+fRVv4lhIkS kXQ70+338Eg/HUn+MrKv8BPbH23nI7av/RdvMatANjPwDIwcDvZfI/AUcLH0eIVP6oKG mVp3NEpRehTNk5CtJ+RJZHz/+1+9oWWkoEmfbHOeyjEALrp9fT8rpUUiuWm4GnifJ7Jx z1kFlJUctYegZA6cJvtCVdz09HvA+D42oE88lRpa9rw05N5RWe9H6EdCfXuB0D598Rwi aHJw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk Received: from uidappmx01.nottingham.ac.uk (uidappmx01.nottingham.ac.uk. [128.243.43.124]) by gmr-mx.google.com with ESMTP id 81-v6si47015ljc.2.2019.01.14.14.48.27 for ; Mon, 14 Jan 2019 14:48:27 -0800 (PST) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) client-ip=128.243.43.124; Received: from uidappmx01.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 710DC3C1FEC_C3D11BBB for ; Mon, 14 Jan 2019 22:48:27 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) by uidappmx01.nottingham.ac.uk (Sophos Email Appliance) with ESMTP id 170A53C1FE0_C3D11BBF for ; Mon, 14 Jan 2019 22:48:27 +0000 (GMT) Received: from [10.159.172.13] (helo=UiWexEDG01.ad.nottingham.ac.uk) by smtp3.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1gjB1v-0000EU-1v; Mon, 14 Jan 2019 22:48:27 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 14 Jan 2019 22:48:26 +0000 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Mon, 14 Jan 2019 22:48:26 +0000 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Mon, 14 Jan 2019 22:48:26 +0000 Received: from EUR04-HE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Mon, 14 Jan 2019 22:48:26 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com (20.176.5.138) by VI1PR06MB3181.eurprd06.prod.outlook.com (10.170.230.140) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1516.18; Mon, 14 Jan 2019 22:48:25 +0000 Received: from VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::9df:659d:86d4:47a5]) by VI1PR06MB4029.eurprd06.prod.outlook.com ([fe80::9df:659d:86d4:47a5%3]) with mapi id 15.20.1516.019; Mon, 14 Jan 2019 22:48:25 +0000 From: Thorsten Altenkirch To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= , Homotopy Type Theory Subject: Re: [HoTT] Re: HITs in Agda Thread-Topic: [HoTT] Re: HITs in Agda Thread-Index: AQHUqOvi+GmmKWT26kad6vEnvQ6wTqWooHOxgABbHQCABmkZgA== Date: Mon, 14 Jan 2019 22:48:24 +0000 Message-ID: <572D1EE0-9E6B-44F5-A17B-AA6D91A8F303@nottingham.ac.uk> 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> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.14.0.181208 x-originating-ip: [150.203.114.149] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;VI1PR06MB3181;6:/JSR9mvE2RBMjGUeKNnUnzv/8pbQLVO76znJRQ4nmuYM2/vOVmM/ibNuNKewPOcBMstAJgev7djPvUDRmdarV+PgbhVJUB/nYZCVq48TC2n1HGcflSCriwANZgHKMN3ZnWMSUtZ00D9NM279hC7Iv5bGIp/XI6Ceztkpg+5kjf1msuh0eVcz6VVb/TH+h/1ei457tuv4CLHSp4e2DpIifYIxQRlDlhzCYNj6fu1RHOAWk9J9IxwY+AsdMd70U5tl2vFJAxxmW5tPBtXb8rmYGb1EOQjzz+nky99cNylJUkKDEKHEDX5dxH58w5KwqsoIEXiLpAW4MyNr6vb6OimjRw3oHtouYUb+2Du7+EjAMvRz+laoUAI62+NB5rRth575FVsxc+XdfZg4vQa4dSDjtwzGO5J94UJCyu4OS3lEizAjN+7bXSZ3TaGEqsPsY4BEx2evmxBkQBXoubDp3TAXEw==;5:vJtYvIQ3AFflH2nOZci8APqQU3SGx+OTRLhZBnTMCI2wrn9cSbk6NkNqInw56gB0YXJAuItpjaBFZdw7cRlnb+U8AjSoGyZ48YaKAxOtnNXaNu9bdGw15N09XxQZV0oYpgsYxEpdwnaxeD/VeG3I98kkN8wbas/a+jrWACw+flDFlHAoeJ7SevgonCByrN4+cVLw2Sb6sJASphBybCrxCQ==;7:uh93QY8quyvX6m8wPaUo1LTzknTC1fSGegoOnx2fZRUbPinVt9s86L3y1M+KvI/kjvg9nd3Xi+htqGyUBBzidMrA0yTxc4p5VuGf+RMUs9RyC1KWDXcMefbEWwd2d2SrFyIjLp8d2e51MC6A/kTDFw== x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: a1c27cdd-df0d-4772-70a6-08d67a726485 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600109)(711020)(2017052603328)(7153060)(7193020);SRVR:VI1PR06MB3181; x-ms-traffictypediagnostic: VI1PR06MB3181: x-microsoft-antispam-prvs: x-forefront-prvs: 0917DFAC67 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(376002)(136003)(346002)(39860400002)(366004)(189003)(199004)(74482002)(486006)(81156014)(66574012)(39060400002)(81166006)(6486002)(8676002)(68736007)(476003)(6246003)(71200400001)(110136005)(76176011)(8936002)(33656002)(83716004)(66066001)(25786009)(229853002)(93886005)(966005)(6436002)(99286004)(2906002)(478600001)(71190400001)(82746002)(105586002)(786003)(3846002)(97736004)(316002)(7736002)(6116002)(26005)(86362001)(186003)(5660300001)(6512007)(106356001)(54896002)(53546011)(6306002)(446003)(102836004)(11346002)(236005)(58126008)(606006)(36756003)(256004)(9686003)(14454004)(6506007)(53936002)(42522002);DIR:OUT;SFP:1102;SCL:1;SRVR:VI1PR06MB3181;H:VI1PR06MB4029.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: /tEczXyIh3/ni59TM5/xPgheo2JtyzqyuryaMAPSanINe0BwIfXQFhOTHJFxHyqc0bd7CLD+SV+sh3a4AOdf7aSKPzldUs9oHll8bz37WHNKzUd1h0oTy39n+L2MOB/F4bq/6DUoKmiC5z0WLvWndSv98xtawAOx+T0ZHwBBrv70wD/VfKuYMN2iFKXC9KxOrHqun/vzsuIqnrkC65KA17a40q+wd3ak4SmEyOvRUgqPnLQmiWUc7AvqcqOkA6Abq5qPFKu3qQj9VgXjISKwg4ZxXM7hQ1F8mZMeBVCHkpbBzG6OiGf9eHuGnoXWhWU3KdS//fd1/AOyovb0ECgq4ep6Dr+SE/6g/ifmmbapAMQcs+qBguutcL4vwDMDA18fXcWL5UJ0V3Ke9IEIDaQCMAmCc6l6U+pRAytiz05FUPI= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: multipart/alternative; boundary="_000_572D1EE09E6B44F5A17BAA6D91A8F303nottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: a1c27cdd-df0d-4772-70a6-08d67a726485 X-MS-Exchange-CrossTenant-originalarrivaltime: 14 Jan 2019 22:48:24.9737 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-Transport-CrossTenantHeadersStamped: VI1PR06MB3181 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.124 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk 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: , --_000_572D1EE09E6B44F5A17BAA6D91A8F303nottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I started working on this with Andrea at the Agda Implementer=E2=80=99s mee= ting. The idea is that you can add a constructor for transp to your inducti= ve families but then reduce it to during pattern matching. This is similar = to the way comp is implemented now. In the case of the equality type that s= hould give you a type which is isomorphic to the path type but intentionall= y behaves differently, in particular J-beta holds. This is an alternative t= o Andrew Swan=E2=80=99s solution, I think. Cheers, Thorsten From: on behalf of Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3 Date: Friday, 11 January 2019 at 07:54 To: Homotopy Type Theory Subject: Re: [HoTT] Re: HITs in Agda 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 typ= e via Andrew Swan's technique) is not an Agda inductive family and it is no= t Agda's inductively defined identity type. And also, as far as I know, ind= uctive families RE an open problem in cubical type theory / the cubical mod= el(s). Any development in Agda invoking --cubical that tries to be sound should, f= or the moment, refrain from using inductive families. In fact, in would be good to discuss the precautions one should take when u= sing --cubical in Agda so that one is guaranteed to be consistent, and bett= er, be talking about something that is currently understood (such as entiti= es 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 coul= d 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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. --_000_572D1EE09E6B44F5A17BAA6D91A8F303nottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

I started working on this with Andrea at the Agda Im= plementer=E2=80=99s meeting. The idea is that you can add a constructor for= transp to your inductive families but then reduce it to during pattern mat= ching. This is similar to the way comp is implemented now. In the case of the equality type that should give you a t= ype which is isomorphic to the path type but intentionally behaves differen= tly, in particular J-beta holds. This is an alternative to Andrew Swan=E2= =80=99s solution, I think.

 

Cheers,

Thorsten

 

From: <homotopytypethe= ory@googlegroups.com> on behalf of Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 = <escardo.martin@gmail.com>
Date: Friday, 11 January 2019 at 07:54
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: Re: [HoTT] Re: HITs in Agda

 

Actually, I think it is= not a priori clear how Agda's --without-K interacts with --cubical.

 

For one thing, the cubi= cal identity type (derived from the cubical path type via Andrew Swan's tec= hnique) is not an Agda inductive family and it is not Agda's inductively de= fined 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 go= od 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 so= mething that is currently understood (such as entities in the cubical model((s)). It is not entirely clear to m= e which features of Agda we can use and which ones we should not use and wh= ich 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, Al= i 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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.
--_000_572D1EE09E6B44F5A17BAA6D91A8F303nottinghamacuk_--