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.