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-lj1-x239.google.com (mail-lj1-x239.google.com [IPv6:2a00:1450:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0f64a848 for ; Thu, 10 Jan 2019 15:28:08 +0000 (UTC) Received: by mail-lj1-x239.google.com with SMTP id p65-v6sf2844477ljb.16 for ; Thu, 10 Jan 2019 07:28:08 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1547134087; cv=pass; d=google.com; s=arc-20160816; b=IWQgqEKOWXXtTkncCXEQ0O/VoA7mBhbuyqoYa8U8AtZNd0jOZeo1aNCJfbXTfS88yg QfCN0XtyfVlhB5r0LgYhDZuaUE5TamjHHQixHaX+Zm8JT0O05vqjwexckmacoAhKj7W/ TTb9TzCRa1zA1b6gKny0nYNVuBb1b0V9CEpZOFBpMCSjeJGR7Pe6/LhjgovvbxJbHeLb xmoDOBFttZOnQ9haC4fLwPvsNRxxuk89DZ5lLYIknFVfeabo63fVO52rPB/aMbiT4yxH f3IpqHUb2oiKk4G0IABl4y/2eZHV+BIbA1Soa/hYO11Kjzmg8c7sZnlZBdubJKYJXr6Q /0Jg== 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-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature; bh=hdgC4bly/UL9+CLs0wTOMBG9L4FtD3isGzk6MBqZiCc=; b=MQF+Y5Iojjou3nBYucES8cqfuDwK+pag+XxatfMYIGUG9aGhhbCT0mbXYii021iRFa ybnpzA2bdYU3dWVCPtycxQdgk/t/b0DZXFSW07Z3ikqxKYq6ZViuet2IJ3pr1QuaJErj mmi+c29hiOXTsyswaaZugqBQBtIG6WoWGfOCXlHKmb/ZphHz+Nl3UVT+t0Niy1/88Bw/ YyHHdFTcj2Za6CYwZwACy7pjNto5pB7VJ1cXxQx/yZfyiJGhvx5rEDC0yUG1NspvxFBL oUmBlS7brAQbxOg97Ej1sXAC9a4zBGEMCot8Z2TAzFNI1uRn1y0/lVWrwlpVjI0gPxqB Ye8A== 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:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=hdgC4bly/UL9+CLs0wTOMBG9L4FtD3isGzk6MBqZiCc=; b=OVQwGBhRo50Zu0XyD1P/qSy3pRY9KiWyNlihwilcrDv9b6VjF+8OJ38pjwI6d4HmSc fSZk/LatAdOspPQKw/9pXg7CaQGxDREOAe1fNC7MC9lN5YMZ+A1Y0LnPT9HZlyJV7Dco IZh45IUzxX4avQKY44TPhwe5mhz2R2W+67/cuIlMhCRSvZlO7771VNBdcmupv0H5bvQj rtXJcuvbqvUpuK1YkeZC54hJU1WI8rYEUDr0WBvQ5kqF+hyYYWi5Pdd87tuLX1LKMujW eu7O6hvNFgT1oP/ApQYs9sNe4fjfpha+OC0H8xiiwXZelanBLstW6XC6RVtGanAgxOka TRww== 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 :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=hdgC4bly/UL9+CLs0wTOMBG9L4FtD3isGzk6MBqZiCc=; b=lABdsp13UXNstS7sz3sXOZhBk0F7eSE4Ww5DMIu+0P0yZdr5LuOaEhWWmPzl+0BIm0 6C42MWxRE/3vTIMtqXWTmrZfEtiwK9guzFdCgIP+4rX1hd+wUdg+9Dzt7PG8HfP2WmYP umLgem22qCvhne4rGzF/TklwG3dk+n5PncQztpAQH2jVGlHUCYGY2txGL9l905mYrmJd 1NFV2J1mr5vmIlAJ731Z91gB9d0U0RCrBUMBOaTuokKd9Joqs3vlX6bsUJjgNRO7/UCU uQt1PuTu995xcUhuR6WiQCDeMvHpC+xegySFHlFj3e0Pjk55O4Wq5GMAv8qqzMQr2EHf StGA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukeFF+fv72ZRIHW5jfcQqddpA6JyMecSFrSVFMybW0e8Wl22VRP+ 1FhP4JZJyxZKaRld3w6pvPQ= X-Google-Smtp-Source: ALg8bN7blwep8CDlpHGlaunOT94A8BExePh2WWZUpeJFpP11ElgB3rag7kf1uyxm3asAhooElcta+A== X-Received: by 2002:a2e:21d:: with SMTP id 29-v6mr40713ljc.3.1547134087274; Thu, 10 Jan 2019 07:28:07 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a19:9711:: with SMTP id z17ls1138281lfd.13.gmail; Thu, 10 Jan 2019 07:28:06 -0800 (PST) X-Received: by 2002:a19:5519:: with SMTP id n25mr496485lfe.1.1547134086764; Thu, 10 Jan 2019 07:28:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1547134086; cv=none; d=google.com; s=arc-20160816; b=WZ1jdjmARwzKS+zVQbj4NE+ygM7tM5Q/oVQ4rW5RHECl/dCRU1Khq6Sp5BmNklpJUI oRcM8MmW4gUpKyYGtn2jLOXeX9kZdpHAiKYwYzuSf1aT/5AB85I0I89Xl0IHSB0FmFeh AUCbw6IQnX9/yBpO9w43sLLufxvxTFOQEvQg16Y8RhVZMnBoDAzkOVgyxdTTYszv9amn wj6SCVp39zUemJNo/KcVsMowynMOfuqzs2nqHp1BbGGmOIbHhsI+WZJYsLzlSeVSQ2BR X2IgamBC6BUWESTuNPs557dQj0cNq0SEVtyTyZW6IlA7kwvyohPM/BHORX5suTjfqgiI iJhw== 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=FRR4gOr0Q4FSuojSD2KrBN2NJ6uyAkLlVxPxS+fyH4o=; b=ndjLsr+A990tti4qDqoARznXsvarhEBT4EUpTUqm3aV5jObHDSizIPAsZ56NB6wT7F YirkZrSV5fnwk1HjX2y0aJ5HzGCf8wnThCWa1LRZrzUl6/O5kL0icTaW9ZJDscphZsRv pMXXYYG79JF1fHMD2uN3HfO2mJrQHGWf68OdTGBz5CtICMlNcsSGN014EP4SxI/Uy6sZ 64cW2kpc5fFGJkeRlzjH7KcZUiZtDqtXdMpCW9gcevh5Oa/dk+EN8oIISImgBGTEfiPM KTSKedx6a7ZsX3v3gV2WhEObI8ysuxKjR/GR8D2b3F+T704suah8sP4pi/zUe7E7MB/i XE9w== 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 e17-v6si3011713ljg.5.2019.01.10.07.28.06 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 10 Jan 2019 07:28:06 -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; Thu, 10 Jan 2019 16:28:05 +0100 Subject: Re: [HoTT] Re: HITs in Agda To: Ali Caglayan , Homotopy Type Theory References: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> <45e2ceb4-dc90-4d66-a728-d075bccac399@googlegroups.com> From: Nils Anders Danielsson Message-ID: <510281bb-5b88-c64f-a8ac-5807365e096c@cse.gu.se> Date: Thu, 10 Jan 2019 16:28:05 +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: <45e2ceb4-dc90-4d66-a728-d075bccac399@googlegroups.com> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US 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 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.