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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53f.google.com (mail-ed1-x53f.google.com [IPv6:2a00:1450:4864:20::53f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ebc68f86 for ; Fri, 11 Jan 2019 11:48:51 +0000 (UTC) Received: by mail-ed1-x53f.google.com with SMTP id o21sf5819831edq.4 for ; Fri, 11 Jan 2019 03:48:50 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547207330; cv=pass; d=google.com; s=arc-20160816; b=R/1tjsEqfohg42YpwLDy5ieCFeumjeDFkgQjChsg7N90QllekopD0HN6jnzoRDGkek FSoLnC3caxxt34ro9+kM8PkFNr/9VTlywhxdzHstuloIxkthxZGPgIPdyUtQgPmcDpkm akaBtEdosVjRvU36CJ6qH26x1a/c4031oyUjrWxJrWMZvqE2gJP2hsqMbezfP3wbDfA0 LH0OEXmP4ntetWPKDD+kcxlrvFtqzhja5iHZmYQ7ZRMJsRgMJ7E/S3BjnwupbwX97ix2 CT1USNdgUBw8jffliz3FUA5oAmHbNBtBK2mMaIt23XxuysxSTxg2TCJMOIcuxKHNrSo0 T6PA== 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:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature; bh=Sq7fvmaefovU58VgijsPmjnhsPRHIcymCuYoXVQ7L3s=; b=kAyt/3vrFnrqM8z2pAXC/SAPMZzVR8VvtyaD4M6oX+AqVcHBbnbvINk8wdTTLDs0/5 F/vDoMMLPh8hmJwvX+3f6yBjlDbZF6xK5JwnBHobF1gV1ROUyiItWajJ2Z30xoYHpa3Z XToSzPP4E/+pJUdND8y7sIg2hNyWo3IjDOzU1kIghgpdMWIiRU5QG2IO4d39JjrV+1LJ xLCMXsHQJGQX4krWOzqtUA9vCpJ2NtHIpaorluST1EQ3rgqftG2WflR+O0VkcmlOjgCm GTCHAaArWqYT8i1skNja0JzuGH7U1bFbDAHRwb3mSXssg7fbEDpnzpC408jUAIVZggu7 38NA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Sq7fvmaefovU58VgijsPmjnhsPRHIcymCuYoXVQ7L3s=; b=Fetp3+JrUWx5InsBUHHG3Ble5bQbh3aElShEMZbS4KaroEgWhfKujF0sD/QF45YCLU LdDirMkx1I5kYoopACSgb9Ltj3IygfPlRV5bM2CU66PgzeIflxIOh3pv/tCH71B3/WfT U/HhIAKSMp5iVYX+MHKyOmwqahViHVNlmoY0ePde6XqKoMI8RDj9pTYHqdqYWjSDBPQY 6CWIoSJJecnSNOQFY/Xi+HJXG1hNXoNCzhkmp3xJ+gVXH8Puz9cHm5950EONsAJLzrMl Gj1Ad7IRTIEAs1du4TNcZOHynkgW1BOjt3i1uhp0ABCNaFBty4j0L16UuILWgLbOARZL capw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding: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=Sq7fvmaefovU58VgijsPmjnhsPRHIcymCuYoXVQ7L3s=; b=gjafbNphpoaxpTjYyq0wNdfJA6/AKRDLdSOj5gt+A+fteJ6BxAf13HrqjXCFOdnVf/ t26ZrgkFtVJXaVH17fpmxyMJnPe6MhlIOECJKcWZyaXXb/rPsUXgmra4n5GaVVUJLyGl /rFGs/+Mta7uh+5cPGOvaA2SVBTf53uLLA+BzhQcM9P04fic4WKVFyThUG5OKizSWBKY Qh8r9RS2kuXtLC+cCj/GzsbDBaZNJj/ZrnJxr4BBl1RWagUAJROPDGuYHDZonGIWhPT8 CZFFto1xyl7VfgHGPDt1kb04qIUT8qWCJC8zIjyEkIYFEGzLI5sKZNNJ7O2buVjvop5O dhog== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUuke8dofkZbMsTiExNZKKZnppdt8+a3637VnjmNw4qidMnuSk3Dbd gg+uDf/FHXTUtHDx24Whvxk= X-Google-Smtp-Source: ALg8bN5/OG8/dozrs0upiCaWV5lgPFTDNxFf4Fm0ffP9LngS7EjtLiTezyNFm3F+rE7Eb8ZuITiL3g== X-Received: by 2002:a50:f5b5:: with SMTP id u50mr48194edm.5.1547207330446; Fri, 11 Jan 2019 03:48:50 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:994d:: with SMTP id l13ls4213317edb.1.gmail; Fri, 11 Jan 2019 03:48:50 -0800 (PST) X-Received: by 2002:a50:a5f1:: with SMTP id b46mr1826010edc.12.1547207329980; Fri, 11 Jan 2019 03:48:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547207329; cv=none; d=google.com; s=arc-20160816; b=mizkZ80/CklwnSIAWqK6dbd6G7iTnUt9R4kufqIORk56QlLKtGKS7n/erzHkUOmwpG wfqK3il+bHC+XRfp4P58BQhJJ3y815ujaSFxRyiU0xH8YzGZXdwhRoLmyUg1tEPuU+6r N+wI/IPvAL1u6+z1wTLZjw/fmHxjVHASDvi5O0Bg+LgY4sYQTMeAV301DcI0NVpk0K/n 27V34Jn1XfJ1CdVXHHqVc+WynKpSLXojlYlyoc6o8RzXZSEpo9rIjFm7co5UvWvJU1DK IzpGG+umcIH5V8l5DfwRCBjIu4ZZ/75W0xbLBemuO8TcqjDhYQNXVvKbHeFtcHMCchT1 6uZg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject; bh=DgmVU/n6ZJxbJwTEzy3QRkgvlyThIZgeSUZR/8N+OBg=; b=BuBHqEyDwTHn+Kstw57rEBke5KaTJpeWFeNaDcqGwbuwtMM2v5iw5VccIekcAZIQlf w3njJZjF6tk5/Al3C+E8aR7/1KseNfVMmygKlKIfOay3IYyO4M/jRw/0HCzYSzwhtZHG jhK9LxZufQF0uH5DnXGRU7ca7or3QAP3u/C1Ur6Hmly83IypxlFv1QBzI251CzfVXE4x qPNDW2f4OK8iSsAl2GnXtQTget+ls1d3nA0/zWDOXwb4Lfui75Aq2phX/j0zZ8Myscft /TnROWS332/12Ky2fwAeuxrg45CYCN1ClCu+M2TsxAzYY9IOG0h1IRxBsRJ7hNkwzVeq PViQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se Received: from stark.ita.chalmers.se (stark.ita.chalmers.se. [129.16.226.131]) by gmr-mx.google.com with ESMTPS id i2-v6si444926ejj.1.2019.01.11.03.48.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 11 Jan 2019 03:48:49 -0800 (PST) Received-SPF: pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) client-ip=129.16.226.131; Received: from [129.16.22.134] (129.16.10.245) by stark.ita.chalmers.se (129.16.226.131) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1531.3; Fri, 11 Jan 2019 12:48:49 +0100 Subject: Re: [HoTT] Re: HITs in Agda To: Homotopy Type Theory 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> From: Nils Anders Danielsson Message-ID: <3e468581-c990-d9d0-fc46-8283de25b0e9@cse.gu.se> Date: Fri, 11 Jan 2019 12:48:49 +0100 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:60.0) Gecko/20100101 Thunderbird/60.2.1 MIME-Version: 1.0 In-Reply-To: <8cf858c0-6778-4d7f-98c4-68210041b857@googlegroups.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Originating-IP: [129.16.10.245] X-ClientProxiedBy: tyrell.ita.chalmers.se (129.16.226.132) To stark.ita.chalmers.se (129.16.226.131) X-Original-Sender: nad@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of nad@cse.gu.se designates 129.16.226.131 as permitted sender) smtp.mailfrom=nad@cse.gu.se 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: , On 10/01/2019 21.54, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > Actually, I think it is not a priori clear how Agda's --without-K > interacts with --cubical. When I wrote that "The idea is that it should be sound to import Agda code that uses --without-K from Cubical Agda" I didn't mean to imply that there are any guarantees, or that there are no known problems with the current implementation. --=20 /NAD --=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.