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.