Characterizing the equality of Indexed W types

Characterizing the equality of Indexed W types

[jas...]

[-- Attachment #1.1: Type: text/plain, Size: 976 bytes --]

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


[-- Attachment #1.2: Type: text/html, Size: 1220 bytes --]

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

[Bas Spitters]

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.

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

[Gaëtan Gilbert]

I've been experimenting with similar results in 
https://github.com/SkySkimmer/HoTTClasses/blob/inductives/theories/theory/inductives.v 
, mostly looking for a syntactic criterion for an inductive family being 
propositional.

Gaëtan Gilbert

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

Re: Characterizing the equality of Indexed W types

[Paolo Capriotti]

[-- Attachment #1.1: Type: text/plain, Size: 339 bytes --]

On Wed, Sep 13, 2017, at 05:41 AM, Jasper Hugunin wrote:
> 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

I have a similar development here: 
https://github.com/pcapriotti/agda-base/tree/master/.  Look in 
`src/container/w`.

BR,
Paolo

[-- Attachment #1.2: Type: text/html, Size: 455 bytes --]

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

[Christian Sattler]

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

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

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

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

[Jasper Hugunin]

[-- 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 --]

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

[Bas Spitters]

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