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-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5140da38 for ; Thu, 10 Jan 2019 13:37:36 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id z22sf4476990oto.11 for ; Thu, 10 Jan 2019 05:37:35 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=GmAVxcKeqXVONyypd73QLtZUdTFa69z/mjvT8f1tKko=; b=fvfFSjCk1euDl8AEBrWkXiagJhbvYAql5ZIPwvDrulgp61SgjwgqvKc/ksKESdBlY7 CsOacixwcYmi4IiaTpyXom06SACGqp4Q/ZGzfEwQK1tBNqq3qYGZOQxulT93mC4OVWjs ajWk4mxhC9/tIGzOcfiS4iLHuINpqvWpgca4PyX1xqMmUxSGIPeGHxwiFq1xFzq8OxZ8 nPeOQ61rwQGqVLhDb+H40jc/zm5d7FWoIshn+GpdDSoEm6pwnHBwU18uymski0b5tnqc AgRpeJowYOahFvL0ZoNgxWnOW82Xq27xztwobBULmQ5/7i+wfOiBvqwxIDA09y2PuqD2 HlDA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=GmAVxcKeqXVONyypd73QLtZUdTFa69z/mjvT8f1tKko=; b=OSZeY/LNxbCEATc0CugU41NC+SG2rxVUK2/TFpfkI6ba+vNJQwh7zCbXNFDKNqTxcs RLfKG11g/A9zKxgHMh3BsHki9LhPxcw4xMX7E1rlxn/noitnsmIGnLQurrylci38sLe+ s9IQIc9gUPZbdZveTYyQLNCrnE1RHuajs2vR+m7vXwmvXzX981T2bxvm45GG6471zMDd PgQgtZWalJ0VzAtceEiGSWCTFkeCAJKpifTir+StvlW20uR3tyLA/UrChnnh+Izxn0F/ 9QmMZBjrspgt9nzK584ZxirdEf1llyWb/ntE/Y38jYFyqzDcp9iTC25y5ZVC/v8owrDt exLg== 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: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=GmAVxcKeqXVONyypd73QLtZUdTFa69z/mjvT8f1tKko=; b=hO56M/RS6x8Da8LBCq2ekMdl3T3IvxEEX3qtyO8JqUecRnrreoGknaPSJXZmoqMjgT 7+D6ouQfzj4SCSgF+WHBuvwnq/cT8mzQ8bCECnrSeOcsmYaXCbZwlXYz8pe1GKF40JTN REO3FnfoHI6C8nhBXEPb5/Q1VimdpXVb+vZqX0nniKPn1dZrvN7e/AkYdeio61AAaxse 7HdDRh3CObdW3vonknoGDWl/PIHbvH0HZ/G0agprLPTQAMMkh8joFYxKPk5VsxSvQJlk u10qnT7AaxcqL+Nsp96i+p8qH4/DmgHelhSnUT6iD2PdegqAWj32PFDddsuuGpKODjrh d5UQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukcYJbOElDG2EEWQuzQ6TEkf85a1AjAk5qMvb+olAjl/dfx8zzX2 n9f3huas8paTgTE235hcoSA= X-Google-Smtp-Source: ALg8bN4fGPy8SOnsPrwLlJD3XozfmAmptuMiI2u63e1qT8Bb8LxSjnnRJMNcK/8Z4fyixzT2AXiStg== X-Received: by 2002:a9d:6f9a:: with SMTP id h26mr117774otq.0.1547127454836; Thu, 10 Jan 2019 05:37:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:32c8:: with SMTP id u66ls58090otb.0.gmail; Thu, 10 Jan 2019 05:37:34 -0800 (PST) X-Received: by 2002:a9d:24c3:: with SMTP id z61mr114213ota.1.1547127454233; Thu, 10 Jan 2019 05:37:34 -0800 (PST) Date: Thu, 10 Jan 2019 05:37:33 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] HITs in Agda MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_329_320496665.1547127453723" 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_329_320496665.1547127453723 Content-Type: multipart/alternative; boundary="----=_Part_330_1470623124.1547127453723" ------=_Part_330_1470623124.1547127453723 Content-Type: text/plain; charset="UTF-8" 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_330_1470623124.1547127453723 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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?= =C2=A0

Do they work without axiom K?=C2=A0

What can and can'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_330_1470623124.1547127453723-- ------=_Part_329_320496665.1547127453723--