On Wed, Sep 13, 2017 at 9: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.
>

All reductions (be it in extensional TT or MLTT with funext) that I know of
carve the (homotopy) indexed W-type X out of a "larger" (homotopy) W-type Y.

In book-style HoTT (where one has enough nice universes), the carving out
can be done simply by defining a "predicate" P : Y -> U (not valued in
propositions in general) by recursion on Y and letting X = (y : Y) x P(y).
I believe I've seen Coq code by Peter Lumsdaine from quite a while ago
doing this.

But even without large elimination, the carving out can still be done using
a certain coreflexive equalizer, just like Gambino-Hyland do it for
extensional type theory using a equalizer (also coreflexive, but which
doesn't matter in the 1-categorical context). I wanted to write this up
nicely for a quite a while now, but I am still lacking a nice way of
talking about internal higher functors and so on without universes.

Christian


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