Re: [HoTT] Characterizing the equality of Indexed W types

[Bas Spitters <b.a.w.s...@gmail.com>]

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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.