From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Tue, 12 Sep 2017 21:41:30 -0700 (PDT) From: jas...@cs.washington.edu To: Homotopy Type Theory Message-Id: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> Subject: Characterizing the equality of Indexed W types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_20862_1962730847.1505277690465" ------=_Part_20862_1962730847.1505277690465 Content-Type: multipart/alternative; boundary="----=_Part_20863_1219112386.1505277690465" ------=_Part_20863_1219112386.1505277690465 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Hello, I have uploaded to GitHub a Coq development characterizing the equality of Indexed W types (dependent W types, inductive families) up to equivalence, as an Indexed W type. https://github.com/jashug/IWTypes We define an Indexed W type as an inductive family, where every node in a regular W type is assigned an index. We then show that the types a = b are inductively generated by (sup x children1) = (sup x children2) with children (children1 c = children2 c). Calling the map from the data of a node to its index f, we show if the fibers of f have positive h-level, then the Indexed W type has the same h-level. Assuming the children are finite enumerable, we also show that decidable equality is inherited from the fibers of f. I am not aware of these results in any of the literature; hopefully they are a useful contribution to the understanding of inductive types in ITT / HoTT. Please send any comments, questions or suggestions. - Jasper Hugunin ------=_Part_20863_1219112386.1505277690465 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hello,

I have uploaded to GitHub a Coq = development characterizing the equality of Indexed W types (dependent W typ= es, inductive families) up to equivalence, as an Indexed W type.
=
https://github= .com/jashug/IWTypes

We define an Indexed W= type as an inductive family, where every node in a regular W type is assig= ned an index.
We then show that the types a =3D b are inductively= generated by (sup x children1) =3D (sup x children2) with children (childr= en1 c =3D children2 c).

Calling the map from the d= ata of a node to its index f, we show if the fibers of f have positive h-le= vel, then the Indexed W type has the same h-level.
Assuming the c= hildren are finite enumerable, we also show that decidable equality is inhe= rited from the fibers of f.

I am not aware of thes= e results in any of the literature; hopefully they are a useful contributio= n to the understanding of inductive types in ITT / HoTT.
Please s= end any comments, questions or suggestions.

- Jasper Hugu= nin

------=_Part_20863_1219112386.1505277690465-- ------=_Part_20862_1962730847.1505277690465-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.43.210 with SMTP id h201mr1374230ita.30.1505289064662; Wed, 13 Sep 2017 00:51:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.52.213 with SMTP id b204ls2531292ioa.37.gmail; Wed, 13 Sep 2017 00:51:03 -0700 (PDT) X-Received: by 10.202.172.79 with SMTP id v76mr9851759oie.65.1505289063819; Wed, 13 Sep 2017 00:51:03 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505289063; cv=none; d=google.com; s=arc-20160816; b=pQ5Vo+pRsuhkkKp6FYvMIpqrHIMWTt4ZRtyVNZCuVOycwmfS907P15iRavnqJS6ZqP aK0WzFv/uIrTuUuswRU1U0gYf7uFgWL75KlAHiLFcNylqCWVeZc7Z8D03a1QTBSbjCeW w2aMJM9ArAPkvRtPnoKJH+1BEmtxnqLV/K/eN0N4aaqJBUGG5lZL4vE+URedGCi3Sur1 XrBDaueU6MdjsOoUIQeD25LGIH9ZjXUGZFAElEcpjfENJLF6hcDeNtOkvYpzM81SFa9R esdbDltj9IDFmG3smAo5/MQ1bNqkwefd0QnPrK9KtDpUBGVCpaYuctjHjZN0NhrVIAUr IJWw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=PpVV3FsRDmRBQhYILHq4KeVASAkyi7Bg0FknYBCOvIY=; b=O3tezGzb14dCxjbDzEI57AgZvWF5lzc/ndhNCQ6cticCfl5muFz5auJAas0ift0ZZo 5Kb4DBISNYGmh7n7XvpMT3FY7Ll1kXHwNr5UHSolh7qUIzz3W8a3PFIV8orpPxz5+iNb M5Nqp82PfbOTgxXBJTvNzy1SPi2pHERoN5hj0hZYvmjltSAcKfrjur0HV2V9AX+FpxVQ QzFQCtzcQXLUYusyEJJESHzKxGvhz33hf/WbcjpiX8gw+DyHwUDSHTesP+Qmi4EgRxjV NKDgJKYMmyKCY9JOcc/IvVSxSWknADMxD1mDKkU6STufeh23BYN8p2LsZ6rUNJm1DCqx V+HA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=FER1lUYh; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x22d.google.com (mail-vk0-x22d.google.com. [2607:f8b0:400c:c05::22d]) by gmr-mx.google.com with ESMTPS id s125si654045vke.6.2017.09.13.00.51.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 00:51:03 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) client-ip=2607:f8b0:400c:c05::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=FER1lUYh; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::22d as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22d.google.com with SMTP id w23so6483378vkw.2 for ; Wed, 13 Sep 2017 00:51:03 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=PpVV3FsRDmRBQhYILHq4KeVASAkyi7Bg0FknYBCOvIY=; b=FER1lUYh9hHnJ81TFmYiJRIRpmUvs85FibP5WaXLXMNdN5Sdi5WXO347PAcbwJcabR vcEBDZMHAj/yagV1Nkvnf2RGgPVe3NsMyKsLMAiI8CaCvKqUc6CR1AjsxBklwrU0/dUb 0UamWGyJTo6zBQQI1KNtZptBPKvOj4OZ9QF0B2gv4Av66kYzUZm9tWZFB4tTYrY7dW1o m+IP4+39pBkAFyk6qiQsjkSk6GZsW7ClTXg3qH6xGs0xPgn6g1C4VL9Ol7AbwdT6reyJ KFeRav2DqJXQzxc7jtP6TLW1xrRS0z4nTNxOj8KyKAWUZLpU1bP8et69O+BnW5LE6ZrS qZKw== X-Gm-Message-State: AHPjjUhRms502Zn2fNbTBmP0pbm0JUVNrHzS+yAzLraNrt/cwsWGKDok 2aN2jrpu+khry96h3eNCQJ5WJsR2XNdI5ESEdI4= X-Received: by 10.31.85.67 with SMTP id j64mr12278483vkb.187.1505289063591; Wed, 13 Sep 2017 00:51:03 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.124.68 with HTTP; Wed, 13 Sep 2017 00:50:43 -0700 (PDT) In-Reply-To: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Bas Spitters Date: Wed, 13 Sep 2017 08:50:43 +0100 Message-ID: Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: jas...@cs.washington.edu, Thorsten Altenkirch , Christian Sattler Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Dear Jasper, Thanks. This is a nice result. Thorsten and Christian will correct me, but I believe the reduction from indexed W-types to W-types was not fully worked out in HoTT before. Christian announced a beautiful route to it using ideas from higher category theory, but I don't think the full details in HoTT ever appeared. I've tried to collect references here: https://ncatlab.org/nlab/show/inductive+family#higher_categorical_version_homotopy_type_theory I think it would be nice to add your results both to the HoTT library and to Unimath. Best regards, Bas On Wed, Sep 13, 2017 at 5:41 AM, wrote: > Hello, > > I have uploaded to GitHub a Coq development characterizing the equality of > Indexed W types (dependent W types, inductive families) up to equivalence, > as an Indexed W type. > > https://github.com/jashug/IWTypes > > We define an Indexed W type as an inductive family, where every node in a > regular W type is assigned an index. > We then show that the types a = b are inductively generated by (sup x > children1) = (sup x children2) with children (children1 c = children2 c). > > Calling the map from the data of a node to its index f, we show if the > fibers of f have positive h-level, then the Indexed W type has the same > h-level. > Assuming the children are finite enumerable, we also show that decidable > equality is inherited from the fibers of f. > > I am not aware of these results in any of the literature; hopefully they are > a useful contribution to the understanding of inductive types in ITT / HoTT. > Please send any comments, questions or suggestions. > > - Jasper Hugunin > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.215.6 with SMTP id o6mr4726832oig.84.1505294956622; Wed, 13 Sep 2017 02:29:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.147.195 with SMTP id v186ls2551062iod.2.gmail; Wed, 13 Sep 2017 02:29:15 -0700 (PDT) X-Received: by 10.129.84.193 with SMTP id i184mr11489189ywb.197.1505294955746; Wed, 13 Sep 2017 02:29:15 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505294955; cv=none; d=google.com; s=arc-20160816; b=BEIV2ETaXt/HffSGvyNiUmZulSFi3cHcmQWkcpW1RCV4RZk9j7vrP85hoorZAfCT5R 3x/shCewb4U7FzpfrpfXJA3GVttRyaVFYXG6JC4XEV5StvZ7dqQrZZ+H+KaiN/2AkLsG Yx+10eI+TjjsIYG+wKDOKOusYuDGm2APluhhUxFhz1XG2tjdW1qsgnAa8oEVILtof/nr ZAcW6tmnRBMp5enffF+ZNqjREfR0hCij2TRo2O6sV6eYsMaV1zA9RA8Zn06NSHQs5hEh MrfmqkMb/XhvauerGsLki3Om0AbmAw5JJtP+1H2KIqsXUcSJERDDMyY3Tu4nJVJ4y4aq BxkQ== 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 :arc-authentication-results; bh=2Q7mN19JqDdvF/DaJNwW5ixPmf50ExJHd09TdJaHRPA=; b=HxWeKz0DFpVWvydfr6i8CkE9CvekpplRYFVHnKzty08dgpvO30ruaeBnKdgAfLBeWT m2fHZPY/ULrM1cV0JfzXQbxnMNLOR1FLAQ1gsu5yveQgv1ZJlo+CceVGyFUqCBU8zOvZ u56ITo1CHW407nZSGQwnI9fUWYH7+0rs+px6VBhfQdiHgxMix7DdrE4gmNG6vak0iepW vgoxZJp7EgqevBtTEUDieAGTFR00P3etbBtJ7psE6M+TLAw5qhBQM9Aot//DI4+SXK7U P69fwYfHPg0IMo4+A44s1Qmsl0XrcZ2GX5K8GWuxs5mbU1ZofXFurVgY6YLmwkrzNucI Jzvw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of gaetan....@skyskimmer.net designates 2001:4b98:c:538::196 as permitted sender) smtp.mailfrom=gaetan....@skyskimmer.net Return-Path: Received: from relay4-d.mail.gandi.net (relay4-d.mail.gandi.net. [2001:4b98:c:538::196]) by gmr-mx.google.com with ESMTPS id s81si171455pfg.19.2017.09.13.02.29.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 02:29:14 -0700 (PDT) Received-SPF: pass (google.com: domain of gaetan....@skyskimmer.net designates 2001:4b98:c:538::196 as permitted sender) client-ip=2001:4b98:c:538::196; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of gaetan....@skyskimmer.net designates 2001:4b98:c:538::196 as permitted sender) smtp.mailfrom=gaetan....@skyskimmer.net Received: from [IPv6:2a01:e35:8b61:e250:f467:20e3:43be:542d] (unknown [IPv6:2a01:e35:8b61:e250:f467:20e3:43be:542d]) (Authenticated sender: gaetan....@skyskimmer.net) by relay4-d.mail.gandi.net (Postfix) with ESMTPSA id 7BEFC1720EB for ; Wed, 13 Sep 2017 11:29:11 +0200 (CEST) Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: HomotopyTypeTheory@googlegroups.com References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: =?UTF-8?Q?Ga=c3=abtan_Gilbert?= Message-ID: <22e91045-b135-02d0-5786-0eced9325601@skyskimmer.net> Date: Wed, 13 Sep 2017 11:29:10 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0 MIME-Version: 1.0 In-Reply-To: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 8bit I've been experimenting with similar results in https://github.com/SkySkimmer/HoTTClasses/blob/inductives/theories/theory/inductives.v , mostly looking for a syntactic criterion for an inductive family being propositional. Gaëtan Gilbert On 09/13/2017 06:41 AM, jas...@cs.washington.edu wrote: > Hello, > > I have uploaded to GitHub a Coq development characterizing the equality > of Indexed W types (dependent W types, inductive families) up to > equivalence, as an Indexed W type. > > https://github.com/jashug/IWTypes > > We define an Indexed W type as an inductive family, where every node in > a regular W type is assigned an index. > We then show that the types a = b are inductively generated by (sup x > children1) = (sup x children2) with children (children1 c = children2 c). > > Calling the map from the data of a node to its index f, we show if the > fibers of f have positive h-level, then the Indexed W type has the same > h-level. > Assuming the children are finite enumerable, we also show that decidable > equality is inherited from the fibers of f. > > I am not aware of these results in any of the literature; hopefully they > are a useful contribution to the understanding of inductive types in ITT > / HoTT. > Please send any comments, questions or suggestions. > > - Jasper Hugunin > > -- > 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 HomotopyTypeThe...@googlegroups.com > . > For more options, visit https://groups.google.com/d/optout. From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 13 Sep 2017 02:42:49 -0700 (PDT) From: Paolo Capriotti To: Homotopy Type Theory Message-Id: <9b7e0489-0762-49cf-92f3-512652fd3ae5@googlegroups.com> In-Reply-To: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> Subject: Re: Characterizing the equality of Indexed W types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_3998_1395408500.1505295769410" ------=_Part_3998_1395408500.1505295769410 Content-Type: multipart/alternative; boundary="----=_Part_3999_354255266.1505295769410" ------=_Part_3999_354255266.1505295769410 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Wed, Sep 13, 2017, at 05:41 AM, Jasper Hugunin wrote: > I am not aware of these results in any of the literature; hopefully they > are a useful contribution to the understanding of inductive types in ITT I have a similar development here: https://github.com/pcapriotti/agda-base/tree/master/. Look in `src/container/w`. BR, Paolo ------=_Part_3999_354255266.1505295769410 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Wed, Sep 13, 2017, at 05:41 AM, Jasper Hugunin=C2= =A0wrote:
> I am not aware of these results in any of the lite= rature; hopefully they=C2=A0
> are a useful contribution to th= e understanding of inductive types in ITT

I have a= similar development here: https://github.com/pcapriotti/agda-base/tree/mas= ter/. =C2=A0Look in `src/container/w`.

BR,
Paolo
------=_Part_3999_354255266.1505295769410-- ------=_Part_3998_1395408500.1505295769410-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.78.238 with SMTP id x46mr11864842uah.54.1505300707964; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.127.21 with SMTP id r21ls2967113itc.11.canary-gmail; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) X-Received: by 10.36.4.20 with SMTP id 20mr1598341itb.13.1505300707120; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505300707; cv=none; d=google.com; s=arc-20160816; b=aqCTcW2cwDx7FwmEjm5nXiVRjso8Dup7OStdITmT/SdAmEFz9SqEuKHwbcyo/HhmUk 6b01uIx6+r+eWf4cjPEn11FUCO3eouwwI6C+AOOgapjnfiXIJwKN8sldOeZQgzyf4W8n OnJVXm6wB1Ea81yVpyUq5NK6ag7XPuUi1DMtzlUZrtKP3ZwRT43W7vZaJsUt/oVgM9hV 7tZZl54Pb9Yglyalr+PAU/HrAp17EsgOjoIjpeZyfTq+AaAJQPHtq6LjWTT0vSO1NFuu oR+glXfYCVEMHv5MeC7lCOufbrn4BNDl7mNteDqmfkyVOL45UbmBGcx7KdLu8Wx47lqN nlOg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=5J171h+s6Pb/LmZpvvCMkW+L4foU+2iPeQaeST+GqK0=; b=J6Y41qIDAWdx/nXsw5MyR3AgvRxQ0LT6v7khXl0ll3bHV/zzhWpwjAw+ndBQFbk80W 8s5vM693JHqjbFd184otdfkqucqHz8UNFSvl9DTVGPInjJEb3O2eEytwIE0Yn7kR5ciA NtRzNOfBZ5dABaer1xhChvl9/w7faa5QLrUSAA22eSmLhv35hvV88LX2BNCmOb5Ha7XE ZtbXtrWXeJkmVE7hVPcyJwNBhg8reNhCTPwex7SOsVn+wW++ZzYV3u7sntFXjqutupGV w+MNqAfQ/t0R2id8hJ94sYjMi0e24AQPmPlxxwLmMt7GJATVa9Fri/+1wUbDA8qJFVN6 N/yg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e/LEXG5j; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-pf0-x230.google.com (mail-pf0-x230.google.com. [2607:f8b0:400e:c00::230]) by gmr-mx.google.com with ESMTPS id a17si1394149pfk.15.2017.09.13.04.05.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 04:05:07 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) client-ip=2607:f8b0:400e:c00::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=e/LEXG5j; spf=pass (google.com: domain of sattler....@gmail.com designates 2607:f8b0:400e:c00::230 as permitted sender) smtp.mailfrom=sattler....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-pf0-x230.google.com with SMTP id e1so22929999pfk.1 for ; Wed, 13 Sep 2017 04:05:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=5J171h+s6Pb/LmZpvvCMkW+L4foU+2iPeQaeST+GqK0=; b=e/LEXG5j9jp3lGHfe/BkefiNoE1Mp5BFgU06TEzvHO1Tvr2snwtQ/LUaJQ5eEPmHZH V3Wtj9kvnk07Qs6DO6Drm3WS7VUUGdywJTkehYKvWfL24t/TLx6sQaFoS2g6aqyP5LKy a2uxgjw8PyCYjki+48DyOJoa8iYjnhoWTDDy+P7KZdmCWs2ksRFYlsklFfSt3g46cAho UfdZgPzXDQPVV1x0IDK4d6aNToF0JZ1da7yt7oXHoixXP7at29uGsFp6UAYsFHKqB5ac hgjhA6nWwyRUlA9/G+42zbG/yk0hX6XiOuSK6Dg8gJr1zTdhsgJk/+5vZhW+ZqFMwr+M Ubfg== X-Gm-Message-State: AHPjjUiww2XXqpzX+/f31Rzayh/f07U/A4lMC4Zrx68ok2vLWbe1GDSV e45rv364aRWybjHyIlZ07uNhzQQEaJY1PJzB4jk= X-Received: by 10.99.7.205 with SMTP id 196mr17378655pgh.356.1505300706838; Wed, 13 Sep 2017 04:05:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.100.183.110 with HTTP; Wed, 13 Sep 2017 04:05:06 -0700 (PDT) In-Reply-To: References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Christian Sattler Date: Wed, 13 Sep 2017 13:05:06 +0200 Message-ID: Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: Bas Spitters Cc: jas...@cs.washington.edu, Thorsten Altenkirch , Homotopy Type Theory Content-Type: multipart/alternative; boundary="94eb2c085842e94b1a05591021bf" --94eb2c085842e94b1a05591021bf Content-Type: text/plain; charset="UTF-8" On Wed, Sep 13, 2017 at 9:50 AM, Bas Spitters wrote: > Dear Jasper, > > Thanks. This is a nice result. > > Thorsten and Christian will correct me, but I believe the reduction > from indexed W-types to W-types was not fully worked out in HoTT > before. > All reductions (be it in extensional TT or MLTT with funext) that I know of carve the (homotopy) indexed W-type X out of a "larger" (homotopy) W-type Y. In book-style HoTT (where one has enough nice universes), the carving out can be done simply by defining a "predicate" P : Y -> U (not valued in propositions in general) by recursion on Y and letting X = (y : Y) x P(y). I believe I've seen Coq code by Peter Lumsdaine from quite a while ago doing this. But even without large elimination, the carving out can still be done using a certain coreflexive equalizer, just like Gambino-Hyland do it for extensional type theory using a equalizer (also coreflexive, but which doesn't matter in the 1-categorical context). I wanted to write this up nicely for a quite a while now, but I am still lacking a nice way of talking about internal higher functors and so on without universes. Christian > > Christian announced a beautiful route to it using ideas from higher > category theory, but I don't think the full details in HoTT ever > appeared. > I've tried to collect references here: > https://ncatlab.org/nlab/show/inductive+family#higher_catego > rical_version_homotopy_type_theory > > I think it would be nice to add your results both to the HoTT library > and to Unimath. > > Best regards, > > Bas > > On Wed, Sep 13, 2017 at 5:41 AM, wrote: > > Hello, > > > > I have uploaded to GitHub a Coq development characterizing the equality > of > > Indexed W types (dependent W types, inductive families) up to > equivalence, > > as an Indexed W type. > > > > https://github.com/jashug/IWTypes > > > > We define an Indexed W type as an inductive family, where every node in a > > regular W type is assigned an index. > > We then show that the types a = b are inductively generated by (sup x > > children1) = (sup x children2) with children (children1 c = children2 c). > > > > Calling the map from the data of a node to its index f, we show if the > > fibers of f have positive h-level, then the Indexed W type has the same > > h-level. > > Assuming the children are finite enumerable, we also show that decidable > > equality is inherited from the fibers of f. > > > > I am not aware of these results in any of the literature; hopefully they > are > > a useful contribution to the understanding of inductive types in ITT / > HoTT. > > Please send any comments, questions or suggestions. > > > > - Jasper Hugunin > > > > -- > > 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 HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > --94eb2c085842e94b1a05591021bf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On W= ed, Sep 13, 2017 at 9:50 AM, Bas Spitters <b.a.w.s...@gmail.com>= wrote:
Dear Jasper,

Thanks. This is a nice result.

Thorsten and Christian will correct me, but I believe the reduction
from indexed W-types to W-types was not fully worked out in HoTT
before.

All reductions (be it in extens= ional TT or MLTT with funext) that I know of carve the (homotopy) indexed W= -type X out of a "larger" (homotopy) W-type Y.

In book-style HoTT (where one has enough nice universes), the carvin= g out can be done simply by defining a "predicate" P : Y -> U = (not valued in propositions in general) by recursion on Y and letting X =3D= (y : Y) x P(y). I believe I've seen Coq code by Peter Lumsdaine from q= uite a while ago doing this.

But even without larg= e elimination, the carving out can still be done using a certain coreflexiv= e equalizer, just like Gambino-Hyland do it for extensional type theory usi= ng a equalizer (also coreflexive, but which doesn't matter in the 1-cat= egorical context). I wanted to write this up nicely for a quite a while now= , but I am still lacking a nice way of talking about internal higher functo= rs and so on without universes.

Christian
=C2=A0

Christian announced a beautiful route to it using ideas from higher
category theory, but I don't think the full details in HoTT ever
appeared.
I've tried to collect references here:
https:= //ncatlab.org/nlab/show/inductive+family#higher_categorical_versi= on_homotopy_type_theory

I think it would be nice to add your results both to the HoTT library
and to Unimath.

Best regards,

Bas

On Wed, Sep 13, 2017 at 5:41 AM,=C2=A0 <jas...@cs.washington.edu> wrote:
> Hello,
>
> I have uploaded to GitHub a Coq development characterizing the equalit= y of
> Indexed W types (dependent W types, inductive families) up to equivale= nce,
> as an Indexed W type.
>
> https://github.com/jashug/IWTypes
>
> We define an Indexed W type as an inductive family, where every node i= n a
> regular W type is assigned an index.
> We then show that the types a =3D b are inductively generated by (sup = x
> children1) =3D (sup x children2) with children (children1 c =3D childr= en2 c).
>
> Calling the map from the data of a node to its index f, we show if the=
> fibers of f have positive h-level, then the Indexed W type has the sam= e
> h-level.
> Assuming the children are finite enumerable, we also show that decidab= le
> equality is inherited from the fibers of f.
>
> I am not aware of these results in any of the literature; hopefully th= ey are
> a useful contribution to the understanding of inductive types in ITT /= HoTT.
> Please send any comments, questions or suggestions.
>
> - Jasper Hugunin
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "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/opto= ut.

--94eb2c085842e94b1a05591021bf-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.108.130 with SMTP id h124mr11443930ywc.211.1505302720304; Wed, 13 Sep 2017 04:38:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.73.220 with SMTP id e89ls3091419itd.8.gmail; Wed, 13 Sep 2017 04:38:39 -0700 (PDT) X-Received: by 10.99.178.30 with SMTP id x30mr11007168pge.113.1505302719411; Wed, 13 Sep 2017 04:38:39 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505302719; cv=none; d=google.com; s=arc-20160816; b=n+F+hbR73sfJl2OXzYCaf/eI+tUlG2xZI9hmsw3v5hCWP0DDxYwpbuEtVYZCSkEnjE BsWKplyfwZLRGlX7Me5H7gHBQ30XAJsowpt31HgvL1un1oZA0cskYvVCFbJc6qNRaub4 st3Dac/nCqofAAqLvPsxA0nOMK26oy/5xOpgR1qSNWufKxy8FOwYP45Lugif89ZPsCZx 6NKYmE3iqkKl9h9zTbawdaYFLf4V+35nhZ0d5+vlsSZC1/ZF+YPmqteWN8bVVG9YIz0C KB2wTTATotUZhHKg4mtbko+Re+rHI6ck2+vhKEA4Mtq5CriwWQrr5N6s4PwL62zcKPA1 3xbA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=KSw48oPvO3nnfLqHxS5mOIvUmr3J1prA/9oLJhjTxQ0=; b=no03XaLhhC6zyHoizDJnySYt6nzH2EzsH59LKkcRiXCsTDoyfFPeyg0/WbClyACwl9 fknZDWb7yHLMfw7MqucOQJ6ZafaQ4sYOzK1Z94osdBeY52GM7hO637R5KqAK7Kj/eH24 2XbEvNO50fFJJNlJkZqvJI7h/KBRqMXjnusqdHqnaheqd/kMgGR27kYZGjBNa3tuJCf+ RbKvKb2f5bXbnl/kxJefXadGkIPnxLUkchF6lNYwi38UBnhz1zWJyi0nfuii9NhQyQZO /yC3dgVa3SVXJ8NfqzjdK6U018tK/Lpkg/rsoX4qAYmkVCYSrmGK73KXRJbULwgWbh3n yYNw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@cs.washington.edu header.s=goo201206 header.b=gbGSBc6D; spf=neutral (google.com: 2607:f8b0:400c:c08::22d is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) smtp.mailfrom=jas...@cs.washington.edu Return-Path: Received: from mail-ua0-x22d.google.com (mail-ua0-x22d.google.com. [2607:f8b0:400c:c08::22d]) by gmr-mx.google.com with ESMTPS id s125si662865vke.6.2017.09.13.04.38.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 04:38:39 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400c:c08::22d is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) client-ip=2607:f8b0:400c:c08::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cs.washington.edu header.s=goo201206 header.b=gbGSBc6D; spf=neutral (google.com: 2607:f8b0:400c:c08::22d is neither permitted nor denied by best guess record for domain of jas...@cs.washington.edu) smtp.mailfrom=jas...@cs.washington.edu Received: by mail-ua0-x22d.google.com with SMTP id q29so18388288uaf.3 for ; Wed, 13 Sep 2017 04:38:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.washington.edu; s=goo201206; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=KSw48oPvO3nnfLqHxS5mOIvUmr3J1prA/9oLJhjTxQ0=; b=gbGSBc6DkXi4dsX50KydDhTc0CYYQ2i7PGhJByquugzNeNtysIgKSjvm2Z2BtWu7M1 AP5ufkGF94gdxBC4HRRd7K45RV7u9xic33WLBVJ/YxbZ56OHvktYD9gJDteH5wavwlLH 3tPAEcCSBp177/gyvlqdRZjl2P8aXkDZ8MuYc= X-Gm-Message-State: AHPjjUgI5LoKk026tyw4C6ZL6DmI0Hl+l27bnac7MijB+dX8MyOVsZxe AvXqiMYV7qtwuBMF2SxVkNiobDXFDC5wk4J5dTkVjQ== X-Received: by 10.159.37.201 with SMTP id 67mr14288978uaf.59.1505302718872; Wed, 13 Sep 2017 04:38:38 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.4.134 with HTTP; Wed, 13 Sep 2017 04:38:38 -0700 (PDT) In-Reply-To: References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Jasper Hugunin Date: Wed, 13 Sep 2017 04:38:38 -0700 Message-ID: Subject: Fwd: [HoTT] Characterizing the equality of Indexed W types To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="001a113c4f3cd6981d055910997e" --001a113c4f3cd6981d055910997e Content-Type: text/plain; charset="UTF-8" Apologies, hit reply when reply all was more appropriate (better than the other way around). ---------- Forwarded message ---------- From: Jasper Hugunin Date: Wed, Sep 13, 2017 at 4:27 AM Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: Bas Spitters Hello Bas, During my research, I read something by Christian about the higher categorical theory route, decided that right now understanding higher category theory was harder than the messy, adhoc manipulations they were trying to avoid, and went for it. I agree that having these results in https://github.com/HoTT/HoTT and/or https://github.com/UniMath/UniMath would be useful for visibility. After the HoTT book, I looked for results about Indexed W types in both, but couldn't find anything. However, I am not particularly familiar with (the style, definitions, lemmas) in either. And with fall quarter starting soon, I doubt I'll have much time to spend on this. Best regards, - Jasper Hugunin On Wed, Sep 13, 2017 at 12:50 AM, Bas Spitters wrote: > Dear Jasper, > > Thanks. This is a nice result. > > Thorsten and Christian will correct me, but I believe the reduction > from indexed W-types to W-types was not fully worked out in HoTT > before. > > Christian announced a beautiful route to it using ideas from higher > category theory, but I don't think the full details in HoTT ever > appeared. > I've tried to collect references here: > https://ncatlab.org/nlab/show/inductive+family#higher_catego > rical_version_homotopy_type_theory > > I think it would be nice to add your results both to the HoTT library > and to Unimath. > > Best regards, > > Bas > > On Wed, Sep 13, 2017 at 5:41 AM, wrote: > > Hello, > > > > I have uploaded to GitHub a Coq development characterizing the equality > of > > Indexed W types (dependent W types, inductive families) up to > equivalence, > > as an Indexed W type. > > > > https://github.com/jashug/IWTypes > > > > We define an Indexed W type as an inductive family, where every node in a > > regular W type is assigned an index. > > We then show that the types a = b are inductively generated by (sup x > > children1) = (sup x children2) with children (children1 c = children2 c). > > > > Calling the map from the data of a node to its index f, we show if the > > fibers of f have positive h-level, then the Indexed W type has the same > > h-level. > > Assuming the children are finite enumerable, we also show that decidable > > equality is inherited from the fibers of f. > > > > I am not aware of these results in any of the literature; hopefully they > are > > a useful contribution to the understanding of inductive types in ITT / > HoTT. > > Please send any comments, questions or suggestions. > > > > - Jasper Hugunin > > > > -- > > 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 HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --001a113c4f3cd6981d055910997e Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Apologies, hit reply when reply all was more appropriate (= better than the other way around).

-----= ----- Forwarded message ----------
From: J= asper Hugunin <jas...@cs.washington.edu>
Date: Wed, Sep 13, 2017= at 4:27 AM
Subject: Re: [HoTT] Characterizing the equality of Indexed W= types
To: Bas Spitters <b.a.= w.s...@gmail.com>


Hello Bas,

During my research, I read something by Christian about the higher = categorical theory route, decided that right now understanding higher categ= ory theory was harder than the messy, adhoc manipulations they were trying = to avoid, and went for it.

I agree that having the= se results in=C2=A0https://github.com/HoTT/HoTT=C2=A0and/or=C2=A0https://github.com/Uni= Math/UniMath=C2=A0would be useful for visibility. After the HoTT book, = I looked for results about Indexed W types in both, but couldn't find a= nything.
However, I am not particularly familiar with (the style,= definitions, lemmas) in either. And with fall quarter starting soon, I dou= bt I'll have much time to spend on this.

Best = regards,
- Jasper Hugunin

On We= d, Sep 13, 2017 at 12:50 AM, Bas Spitters <b.a.w.s...@gmail.com>= wrote:
Dear Jasper,

Thanks. This is a nice result.

Thorsten and Christian will correct me, but I believe the reduction
from indexed W-types to W-types was not fully worked out in HoTT
before.

Christian announced a beautiful route to it using ideas from higher
category theory, but I don't think the full details in HoTT ever
appeared.
I've tried to collect references here:
https:= //ncatlab.org/nlab/show/inductive+family#higher_categorical_versi= on_homotopy_type_theory

I think it would be nice to add your results both to the HoTT library
and to Unimath.

Best regards,

Bas

On Wed, Sep 13, 2017 at 5:41 AM,=C2=A0 <jas...@cs.washington.edu> wrote:
> Hello,
>
> I have uploaded to GitHub a Coq development characterizing the equalit= y of
> Indexed W types (dependent W types, inductive families) up to equivale= nce,
> as an Indexed W type.
>
> https://github.com/jashug/IWTypes
>
> We define an Indexed W type as an inductive family, where every node i= n a
> regular W type is assigned an index.
> We then show that the types a =3D b are inductively generated by (sup = x
> children1) =3D (sup x children2) with children (children1 c =3D childr= en2 c).
>
> Calling the map from the data of a node to its index f, we show if the=
> fibers of f have positive h-level, then the Indexed W type has the sam= e
> h-level.
> Assuming the children are finite enumerable, we also show that decidab= le
> equality is inherited from the fibers of f.
>
> I am not aware of these results in any of the literature; hopefully th= ey are
> a useful contribution to the understanding of inductive types in ITT /= HoTT.
> Please send any comments, questions or suggestions.
>
> - Jasper Hugunin
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "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/opto= ut.

--
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 https://groups.google.com/d/optout.


--001a113c4f3cd6981d055910997e-- From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.52.79 with SMTP id b76mr11394170ywa.209.1505303271010; Wed, 13 Sep 2017 04:47:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.6.170 with SMTP id f42ls2856402ioi.12.gmail; Wed, 13 Sep 2017 04:47:50 -0700 (PDT) X-Received: by 10.55.209.202 with SMTP id o71mr9459016qkl.2.1505303270219; Wed, 13 Sep 2017 04:47:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1505303270; cv=none; d=google.com; s=arc-20160816; b=JPs+nMe8KgFFU9izZS2B0EsUX+Rf0xtdcbsj4SwRXEE7AKChOATa3S3/3O598qM3ph UW0l1ESYCmXgLl1suDFa6pH7yD5lvFEcd1YnL3wIuTp0MbyMg+45ErSouVTpwFFOioa6 J05hhKBoWTVFAz8xjpUkTa54ST8bnPPWjRE3jY9k3s6CM2jejcATer56uD6qKnJShD8k hYkAPcDsDyvwnnzOlzVBDB5LsdbqMSB6cMvtNvz/z2UfcrfVzFUOFOY0LnNECOq/RBSw QGAp//QfexGdermmlNh7khFPDFgsQ1kqbGmowJrTc4p3Ey3XpelxK9b/0tpCBui4Xquw 0xjQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=a2Oe+IkSZ+ju9/3P/7RlxrOrJibVI8euJLwG3cl0FcE=; b=vP2p45RMVXrP1fNI039CVqdjtW0csfAKME0kD/43wSVV8qIHG0Go171v+ygRVDHO2b kUMA2oByWntVX1eGG0wzYdOMEDPQSHj4oPXnfQ5GlDpbpRk55o+PWCjNbzouDaYNO0P7 JG7ZsGUFkgER9I8dW8coCN8Bkzq7LfUKHKqH3iDgAsjHaXUCINgqGXgfGKvbiFusddRx cWDruWZCOukwTIIVb0cKVoE3B+YeDSMY/Z/kEl2WoJFOteABmp6w02JRFUf9CIDgy0z9 YfStit9tAr/0xUj7oFipVyyPsMjTBA4XnhrLdToO9wPjgg6TjyIr9da0ZP004NASRB/M a0Zg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lG2Vzaqe; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-vk0-x232.google.com (mail-vk0-x232.google.com. [2607:f8b0:400c:c05::232]) by gmr-mx.google.com with ESMTPS id n19si750344vkf.13.2017.09.13.04.47.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 13 Sep 2017 04:47:50 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) client-ip=2607:f8b0:400c:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lG2Vzaqe; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:400c:c05::232 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x232.google.com with SMTP id w23so6991433vkw.2 for ; Wed, 13 Sep 2017 04:47:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=a2Oe+IkSZ+ju9/3P/7RlxrOrJibVI8euJLwG3cl0FcE=; b=lG2VzaqeHxB8Wny8xA4zJo1kWEaXgpsT1V1HGgnYjcZ/mhb017iQVndNeChnMcJUL0 +eloW9j/5QKbKpH5pROwnniStZXjdWD7UiYCa6lJ89CDnq5yekHvoIBz/5DKgRvFDlnL 6a9H7kVikXPOh2O6alFfR7wjJjCgrL7SmMUWLTUtFZQD3VIPLaYOIW5sgsmFj5yFrvEv lUSpWbOdMdaKdeOcszcHMTIBGfnEiDn4PrDqC7HwsBeZ7nj5xJdm9Z/D9yRBy8RCI5uj KhUWLudKpJVoxLnuPCCwrqiUy9W/qMucRGW44CdijYeCM3guCnt/CDSPWs0DGi8HQjU4 Eo7A== X-Gm-Message-State: AHPjjUjE7t3NalraBu3QHSRkTUxQxeiTJGJuKdS1IZ3uu9bETzv+bc6H MiNXESdugGfhUkGakRMdCQW7NUNuYl07I30Gov0= X-Received: by 10.31.63.12 with SMTP id m12mr12453530vka.26.1505303269905; Wed, 13 Sep 2017 04:47:49 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.124.68 with HTTP; Wed, 13 Sep 2017 04:47:29 -0700 (PDT) In-Reply-To: References: <53258baf-7832-4919-8ab1-3e653c97241a@googlegroups.com> From: Bas Spitters Date: Wed, 13 Sep 2017 12:47:29 +0100 Message-ID: Subject: Re: [HoTT] Characterizing the equality of Indexed W types To: Christian Sattler , Peter LeFanu Lumsdaine Cc: jas...@cs.washington.edu, Thorsten Altenkirch , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Thanks. I have updated the nlab and also included links to the three formalizations. https://ncatlab.org/nlab/show/inductive+family @Peter, if your formalization is available, we should add a link too. On Wed, Sep 13, 2017 at 12:05 PM, Christian Sattler wrote: > On Wed, Sep 13, 2017 at 9:50 AM, Bas Spitters > wrote: >> >> Dear Jasper, >> >> Thanks. This is a nice result. >> >> Thorsten and Christian will correct me, but I believe the reduction >> from indexed W-types to W-types was not fully worked out in HoTT >> before. > > > All reductions (be it in extensional TT or MLTT with funext) that I know of > carve the (homotopy) indexed W-type X out of a "larger" (homotopy) W-type Y. > > In book-style HoTT (where one has enough nice universes), the carving out > can be done simply by defining a "predicate" P : Y -> U (not valued in > propositions in general) by recursion on Y and letting X = (y : Y) x P(y). I > believe I've seen Coq code by Peter Lumsdaine from quite a while ago doing > this. > > But even without large elimination, the carving out can still be done using > a certain coreflexive equalizer, just like Gambino-Hyland do it for > extensional type theory using a equalizer (also coreflexive, but which > doesn't matter in the 1-categorical context). I wanted to write this up > nicely for a quite a while now, but I am still lacking a nice way of talking > about internal higher functors and so on without universes. > > Christian > >> >> >> Christian announced a beautiful route to it using ideas from higher >> category theory, but I don't think the full details in HoTT ever >> appeared. >> I've tried to collect references here: >> >> https://ncatlab.org/nlab/show/inductive+family#higher_categorical_version_homotopy_type_theory >> >> I think it would be nice to add your results both to the HoTT library >> and to Unimath. >> >> Best regards, >> >> Bas >> >> On Wed, Sep 13, 2017 at 5:41 AM, wrote: >> > Hello, >> > >> > I have uploaded to GitHub a Coq development characterizing the equality >> > of >> > Indexed W types (dependent W types, inductive families) up to >> > equivalence, >> > as an Indexed W type. >> > >> > https://github.com/jashug/IWTypes >> > >> > We define an Indexed W type as an inductive family, where every node in >> > a >> > regular W type is assigned an index. >> > We then show that the types a = b are inductively generated by (sup x >> > children1) = (sup x children2) with children (children1 c = children2 >> > c). >> > >> > Calling the map from the data of a node to its index f, we show if the >> > fibers of f have positive h-level, then the Indexed W type has the same >> > h-level. >> > Assuming the children are finite enumerable, we also show that decidable >> > equality is inherited from the fibers of f. >> > >> > I am not aware of these results in any of the literature; hopefully they >> > are >> > a useful contribution to the understanding of inductive types in ITT / >> > HoTT. >> > Please send any comments, questions or suggestions. >> > >> > - Jasper Hugunin >> > >> > -- >> > 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 HomotopyTypeThe...@googlegroups.com. >> > For more options, visit https://groups.google.com/d/optout. > >