Apologies, hit reply when reply all was more appropriate (better than the other way around).

---------- Forwarded message ----------
From: Jasper 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 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 <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_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,  <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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.