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

[Jasper Hugunin <jas...@cs.washington.edu>]

[-- Attachment #1: Type: text/plain, Size: 3567 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 5344 bytes --]