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-x238.google.com (mail-oi1-x238.google.com [IPv6:2607:f8b0:4864:20::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6c5baa05 for ; Thu, 10 Jan 2019 21:13:37 +0000 (UTC) Received: by mail-oi1-x238.google.com with SMTP id d7sf5754323oif.5 for ; Thu, 10 Jan 2019 13:13:36 -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=RKDWZg5/1hCL0uxY/M5C4kfzOn/bSDgfWOcm7+GeTDI=; b=Z8x5CRnVWq3JraQNWzrXLLO8loMty3CsxZFZqCAufxkE9WtH3cJYYi02i/1r1Og+4Q bM5OJeL3nYj+zFWG3Ed+eJbADUOowYkiQQdjcCM3XfWY2d0LrxYuQTWc1PKKDVKXWPH5 SkesTVTYeFSOsUcxF+/Asatx7V08bszgNhwxzIaBfPfOhL0KWsQUIwZcBeHgO78Z1l44 o+g9xqy2JhBlBOo4fNilhV+IT+yqpf5Vsrdf09RJnZBYgo2Jpn5y+Y5JHrBBZGy8arcX APGC4vY1UDZkp5wzk7bnk7LYMsKZwWkMgkdJ+lSYYyFOVncj2UNPS8I+zI+E5CbzcuYS Y+Qg== 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=RKDWZg5/1hCL0uxY/M5C4kfzOn/bSDgfWOcm7+GeTDI=; b=isbT2cPnPgvLM7FETIYerwbCciILvQfyha7D8RF0ByMt9N82seZ/r83hYHBhgS7Z+j dfg/nsfy0gM0T2XmyYbGhbP5dlk3n+Q73CeUYjN8dxf5dDF6fovw9T2eI5Obfj1nHRKV kKTQtKdNrhfPCfrPwot3EHQ5O2mMKqcztSJhlY9FQCgRLegORxpNpR7ctC5Fq14GRR0Z ++oWQ4B1dGafZgwIJR0zH4t/CWgV5fUYkJKGjLbKtIk6YcuXBxlMsuGYngC7qK1SKYqa UGyrs8p9F1lB52w5eDZkUArf3vWxYxh1NqFC/IPF+ju6w9LRj7gJPt4nuGhvKdGyPeQM 2xcA== 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=RKDWZg5/1hCL0uxY/M5C4kfzOn/bSDgfWOcm7+GeTDI=; b=Ntn1WdIZRvMcYWlURyrffyW15elXxcXUmQ5Ud7+bhhC7pGUbTV2PDqhV82yl4kDBXo fwiS3gtRpzTSPC8PDClIF1/12paIj7+AFzQHdo4o6oeWvp/y2DwnmSvUsaY9zezp4/By Ar4n85jR9t5U6cMVhR+pCsuhoyD5y1pUSwrfR8xRsrZWBYz94U36i+SOyOzAzKXEPppt P5dDoPfOUfIbLzd1fp2RY/OO1yf5FlmY9tx9YD7tAEBKlCd5br43Kii4YNWnDQezACuz ZoLdf7rZKt3KtYz4QVfjwPJeCNtrQ8SGf1GG98I+kaRqjQZDr+oAsEn0iPv7Ev/kfeYQ wZQw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukcetFRJeoMywUEKw+WVgPeF2XD/VyW+ArbihGQov8ln06vlBx7D K8EVNdhEtterDwMiGCeAeJw= X-Google-Smtp-Source: ALg8bN4WVHuUr1BlImdPh9bJqMvSqDXSM4RsGARWj4xDafOpoeP2p9JIAJlGfCITdTXa4v9YJ6dtWQ== X-Received: by 2002:aca:4c97:: with SMTP id z145mr66142oia.2.1547153615762; Thu, 10 Jan 2019 12:53:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:d40f:: with SMTP id l15ls5941069oig.6.gmail; Thu, 10 Jan 2019 12:53:35 -0800 (PST) X-Received: by 2002:aca:308d:: with SMTP id w135mr66860oiw.0.1547153615076; Thu, 10 Jan 2019 12:53:35 -0800 (PST) Date: Thu, 10 Jan 2019 12:53:34 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_520_516147574.1547153614541" 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_520_516147574.1547153614541 Content-Type: multipart/alternative; boundary="----=_Part_521_1091555469.1547153614541" ------=_Part_521_1091555469.1547153614541 Content-Type: text/plain; charset="UTF-8" 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_521_1091555469.1547153614541 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Thursday, 10 January 2019 13:37:33 UTC, Ali Cag= layan wrote:
= I just noticed that [agda supposedly has support for HITs](https://github.com/agda/agda/issues/2= 761) 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?=C2=A0

Do t= hey work without axiom K?=C2=A0

What can and can&#= 39;t be done with them?

--
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_521_1091555469.1547153614541-- ------=_Part_520_516147574.1547153614541--