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--