* Characterizing the equality of Indexed W types @ 2017-09-13 4:41 jas... 2017-09-13 7:50 ` [HoTT] " Bas Spitters ` (2 more replies) 0 siblings, 3 replies; 7+ messages in thread From: jas... @ 2017-09-13 4:41 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Characterizing the equality of Indexed W types 2017-09-13 4:41 Characterizing the equality of Indexed W types jas... @ 2017-09-13 7:50 ` Bas Spitters 2017-09-13 11:05 ` Christian Sattler [not found] ` <CAGTS-a_jmQVw3p8ROS6pR-sD0p6-Z_PsHR9R77nLSgNG1vHrLw@mail.gmail.com> 2017-09-13 9:29 ` Gaëtan Gilbert 2017-09-13 9:42 ` Paolo Capriotti 2 siblings, 2 replies; 7+ messages in thread From: Bas Spitters @ 2017-09-13 7:50 UTC (permalink / raw) To: jas..., Thorsten Altenkirch, Christian Sattler; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Characterizing the equality of Indexed W types 2017-09-13 7:50 ` [HoTT] " Bas Spitters @ 2017-09-13 11:05 ` Christian Sattler 2017-09-13 11:47 ` Bas Spitters [not found] ` <CAGTS-a_jmQVw3p8ROS6pR-sD0p6-Z_PsHR9R77nLSgNG1vHrLw@mail.gmail.com> 1 sibling, 1 reply; 7+ messages in thread From: Christian Sattler @ 2017-09-13 11:05 UTC (permalink / raw) To: Bas Spitters; +Cc: jas..., Thorsten Altenkirch, Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Characterizing the equality of Indexed W types 2017-09-13 11:05 ` Christian Sattler @ 2017-09-13 11:47 ` Bas Spitters 0 siblings, 0 replies; 7+ messages in thread From: Bas Spitters @ 2017-09-13 11:47 UTC (permalink / raw) To: Christian Sattler, Peter LeFanu Lumsdaine Cc: jas..., Thorsten Altenkirch, Homotopy Type Theory 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. > > ^ permalink raw reply [flat|nested] 7+ messages in thread
[parent not found: <CAGTS-a_jmQVw3p8ROS6pR-sD0p6-Z_PsHR9R77nLSgNG1vHrLw@mail.gmail.com>]
* Fwd: [HoTT] Characterizing the equality of Indexed W types [not found] ` <CAGTS-a_jmQVw3p8ROS6pR-sD0p6-Z_PsHR9R77nLSgNG1vHrLw@mail.gmail.com> @ 2017-09-13 11:38 ` Jasper Hugunin 0 siblings, 0 replies; 7+ messages in thread From: Jasper Hugunin @ 2017-09-13 11:38 UTC (permalink / raw) To: HomotopyTypeTheory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: [HoTT] Characterizing the equality of Indexed W types 2017-09-13 4:41 Characterizing the equality of Indexed W types jas... 2017-09-13 7:50 ` [HoTT] " Bas Spitters @ 2017-09-13 9:29 ` Gaëtan Gilbert 2017-09-13 9:42 ` Paolo Capriotti 2 siblings, 0 replies; 7+ messages in thread From: Gaëtan Gilbert @ 2017-09-13 9:29 UTC (permalink / raw) To: HomotopyTypeTheory 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. ^ permalink raw reply [flat|nested] 7+ messages in thread
* Re: Characterizing the equality of Indexed W types 2017-09-13 4:41 Characterizing the equality of Indexed W types jas... 2017-09-13 7:50 ` [HoTT] " Bas Spitters 2017-09-13 9:29 ` Gaëtan Gilbert @ 2017-09-13 9:42 ` Paolo Capriotti 2 siblings, 0 replies; 7+ messages in thread From: Paolo Capriotti @ 2017-09-13 9:42 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 7+ messages in thread
end of thread, other threads:[~2017-09-13 11:47 UTC | newest] Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2017-09-13 4:41 Characterizing the equality of Indexed W types jas... 2017-09-13 7:50 ` [HoTT] " Bas Spitters 2017-09-13 11:05 ` Christian Sattler 2017-09-13 11:47 ` Bas Spitters [not found] ` <CAGTS-a_jmQVw3p8ROS6pR-sD0p6-Z_PsHR9R77nLSgNG1vHrLw@mail.gmail.com> 2017-09-13 11:38 ` Fwd: " Jasper Hugunin 2017-09-13 9:29 ` Gaëtan Gilbert 2017-09-13 9:42 ` Paolo Capriotti
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).