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-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e6cc0eb2 for ; Thu, 10 Jan 2019 13:53:21 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id e185sf5082666oih.18 for ; Thu, 10 Jan 2019 05:53:20 -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=ICoWULYnSrqPU+Jaxm8eqdgK0B8SrROkcRduQczgI9w=; b=UW61RCEx+sSzCBwb6wGtYTDHdlEqYklq/cK6kRiwsMkGNv6dYOdZHXNPxId0eR5/b/ oL9SLNLE8Lm54isLe4f8ED9BhroBComSpeAUabOgh+PfnejYb0qk0uDLF/MaUNMufGbM rNjwFWloMhRxOEQGhEpTHQ9YT8QeJ1kBVnpb+Iu9uETMp4dKlfK6BZ/UW3/LiSVJbC54 ouSs48Hsgdjmit+Tr1HwG50bG+kxHAFS67hWewFcUnT57TiMiNXXGYz4B/Apyn1jm0K0 a5PEaRM+R+iSbn+lAahkus243jRmi/iriajnU6JjSuODwkjo6jbuQPnILQb9cBwOcwhO vZGA== 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=ICoWULYnSrqPU+Jaxm8eqdgK0B8SrROkcRduQczgI9w=; b=hpAm1TkahmVSeg6xhshK5CEbg0KBv4AG7LfZ9nAIjsBX0dns/rNFmFOU1ajelLdUDY XFx7jQQiiZqmYLfCNB2suVkOsGmjY32JuJdXVgxT0b0zRj/SaDseUzmDSIzEchAdi9ga XErSEa1eAwJVY1Bimx64KJyuCaMnNbH5fyDau7gRbeA4Q6KefvmyD/FXqTusWjxJoiuT 0xuXwsi9U8TFBI0OFY8lCdLqY+SIhvNK9t/+QuS5WEh8+WtaHNsFi5fKeRiYMGkhqE0M OcLdC80z90P7jvM9JixYyTjM95XdzcwGV4+Fn4T4G+PMtWvvJtDzn/ARifVl+TYiMXJh yggg== 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=ICoWULYnSrqPU+Jaxm8eqdgK0B8SrROkcRduQczgI9w=; b=Uv6FhPeATNWfA0N4oGyLmCsmzeRwzCCgyeQSA1N/YOq/XFpdUmVZQBrLfZiKDPEajw DP4OqJhoqB3PrRTbWrTjULd15VpY3B0vGm4J/iv7licQfq078q+3xlbX2w09k+wXn+Os UJJmwG0D9it3cBnfemseEgTmmH3nM6f+Uwh/CwtFYSz2RTe6iKXVcQgTbVZxNQCJiAhe iEcaWWds/6qTm7wNLCgqH7lbN09/rwckl9xeX2xGsKFj59Iq084o6SKhAwtzAE5FOprV Hyr8BpOw9DHpFatMzVGOmauxnnLlwU2pz4ZFF4EcT4QajDrZfNVZAFbN+LDZOp49GIYA qawA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukcj9aW2Lnfj5bM6WGQE3CHV1KPpyH7+z9JCa7uDqAqL2mELNMqw 3mn5FD2aAJJIszLBJ32EdMg= X-Google-Smtp-Source: ALg8bN4M1rAJak9TNFSvUpaf4vJshTmIZnSuYcMyDpeKxPa/TzlavMLWh5E+LTAZnCZZgoAtZkdrOg== X-Received: by 2002:a9d:da3:: with SMTP id 32mr119022ots.3.1547128400052; Thu, 10 Jan 2019 05:53:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:803:: with SMTP id 3ls5206770oii.3.gmail; Thu, 10 Jan 2019 05:53:19 -0800 (PST) X-Received: by 2002:aca:d607:: with SMTP id n7mr55170oig.1.1547128399463; Thu, 10 Jan 2019 05:53:19 -0800 (PST) Date: Thu, 10 Jan 2019 05:53:18 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <349dbff3-08c1-4452-abc4-34531e2b8488@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_344_911723301.1547128398797" 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_344_911723301.1547128398797 Content-Type: multipart/alternative; boundary="----=_Part_345_1398016670.1547128398797" ------=_Part_345_1398016670.1547128398797 Content-Type: text/plain; charset="UTF-8" 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 > realise this was the case I am letting people here know too. > > Now my questions: > > Are these really HITs? > > Do they work without axiom K? > > What can and can't be done with them? > -- 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_345_1398016670.1547128398797 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
You will find answers in the blog post by Anders Mort= berg:

https://homotopytypetheory.org/2018/12/06/cu= bical-agda/

Martin


On Thur= sday, 10 January 2019 13:37:33 UTC, Ali Caglayan wrote:
I just noticed that [agda supp= osedly has support for HITs](= HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_345_1398016670.1547128398797-- ------=_Part_344_911723301.1547128398797--