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

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

Thanks. I have updated the nlab and also included links to the three
formalizations.
https://ncatlab.org/nlab/show/inductive+family

@Peter, if your formalization is available, we should add a link too.

On Wed, Sep 13, 2017 at 12:05 PM, Christian Sattler
<sattler....@gmail.com> wrote:
> 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_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.
>
>