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-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 65f6f9c5 for ; Thu, 10 Jan 2019 15:19:32 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id q23sf4709824otn.3 for ; Thu, 10 Jan 2019 07:19:31 -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=TOUrfia7fUNeS2wU2fT49Pd3khLcC1a1/IyqgjvhLqo=; b=ouhD+YuHUzHzHjjT7CP1pht0FgYaK8+8Ul3bw4rhlA7bnjBEL9+QS65+Mu/WDeL3M+ MvBGuwAhyUkQAX4+KFonLalhrpwqLRKwqGjNosWG/zRLIuLOwzsBkq0X1w104fUj0bC4 AknCbMHDIMsw5sbFkF1lrM1Zpe1w7hANRYlh14PxeBIm4c/0QoQn0g1cOvW1NcqiOPTg Es+iHJW+FzMihZwA5iE0PrC/inAfQMEotw1Z2iG97zz0SnbSY3EUbPweMZ61rtZpCRCF 0zIxHl2FwvuZcO1yNcYeEZhCiON78u7UJOQhC+FOp4qJtsKAhPniaeCC4EVy09JE+OIf ltaw== 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=TOUrfia7fUNeS2wU2fT49Pd3khLcC1a1/IyqgjvhLqo=; b=OnNP+Ovl/pOuiCOyxpvxM3lMux+AzsMlhIIEEcfTFG6pKghPTiLeNwbUi6M/Tm2ZIF KTUDB7Uv451n1y7escO0L9N7Kgu7UdgrU3ZDNb5gyYVuCKow4LevXk7AiaSsFXXOFrou DCiaM/XkP43WryH95ELBogLYLFtF0SfCNMi4sFVzXWCMINHp3MCm/lFNYh9y0bP6Q0D7 FC7LeS9lDySm4yh7838seUQkKTFfJQjdZOeZuONG3J5EkHHVvIsPQNtZMTrE/0vfPC9R Ydj/a+oEmolt+bw1pYpINhWKFhTiLoxTIZHfwk8Qn9ADse+f3SARNDKyk8yh5hO2ptJm s8og== 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=TOUrfia7fUNeS2wU2fT49Pd3khLcC1a1/IyqgjvhLqo=; b=glFS2VgM5KO3vfsXYM6+DLcBdUrp22KW1vUUDwpNfNo0umTQUQc/ufBX+RCdJkFgXL sfVeh0Sc39NgArSg9exA6QGsXXrwMtStawY+y1mqmwxELmSu8cMr33o5/DBMVj7RnxaY wlVPAEfw0Zl6V+c7SUrgBKUq59eG66vY4Cm3SqDkHE7F8loCBB3KQsj8Ww+S8ebVMwIk YlvJpAOU9SRinQ67z2CNsnvJpcXoKmPYfghNEDjI2Hq9JzCfpd4kY4qZGDisEOdrJ3nP JBBMDT7WbeQaf0RsaxluejIN079Fsl90OUkxJxVBWQcyOu/9tbkM+C8JPFS4uYxSKVUL y22A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukeCdLtRW8O0og4zeykl+Ggo1GGP1aMWyq7Cc1gWCje11NUUZi7I KRgd3gKXvaRz0gbObcYFSLI= X-Google-Smtp-Source: ALg8bN6tWdF4SMeDKr2Gfw0oqtI//gwMkO+XYZLGY3hu99nt3YEZBevngpWtVp94kVvWNzbupXceTg== X-Received: by 2002:aca:4eca:: with SMTP id c193mr56933oib.7.1547133570434; Thu, 10 Jan 2019 07:19:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:27e9:: with SMTP id c96ls194720otb.10.gmail; Thu, 10 Jan 2019 07:19:29 -0800 (PST) X-Received: by 2002:a9d:6f14:: with SMTP id n20mr127153otq.2.1547133569585; Thu, 10 Jan 2019 07:19:29 -0800 (PST) Date: Thu, 10 Jan 2019 07:19:28 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <45e2ceb4-dc90-4d66-a728-d075bccac399@googlegroups.com> In-Reply-To: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> References: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> Subject: [HoTT] Re: HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_304_976312805.1547133568865" X-Original-Sender: alizter@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_304_976312805.1547133568865 Content-Type: multipart/alternative; boundary="----=_Part_305_1227019402.1547133568865" ------=_Part_305_1227019402.1547133568865 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I was under the impression that this was in plain agda, that's why it was= =20 more suprising. I didn't realise it was about the cubical agda. On Thursday, 10 January 2019 13:53:19 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: > > You will find answers in the blog post by Anders Mortberg: > > https://homotopytypetheory.org/2018/12/06/cubical-agda/ > > Martin > > > On Thursday, 10 January 2019 13:37:33 UTC, Ali Caglayan wrote: >> >> I just noticed that [agda supposedly has support for HITs]( >> https://github.com/agda/agda/issues/2761) since November. Since I didn't= =20 >> realise this was the case I am letting people here know too. >> >> Now my questions: >> >> Are these really HITs?=20 >> >> Do they work without axiom K?=20 >> >> What can and can't be done with them? >> > --=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. ------=_Part_305_1227019402.1547133568865 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I was under the impression that this was in plain agda, th= at's why it was more suprising. I didn't realise it was about the c= ubical agda.

On Thursday, 10 January 2019 13:53:19 UTC, Mart=C3=ADn = H=C3=B6tzel Escard=C3=B3 wrote:
You will find answers in the blog post by Anders Mo= rtberg:


Marti= n


On Thursday, 10 January 2019 13:37:33 UTC, Ali Ca= glayan wrote:

--
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_305_1227019402.1547133568865-- ------=_Part_304_976312805.1547133568865--