Characterizing the equality of Indexed W types

[jas...@cs.washington.edu]

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

[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

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

[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

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

[Paolo Capriotti]

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

[Christian Sattler]

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

 

> email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

[Jasper Hugunin]

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

> email to HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.

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

>> > email to HomotopyTypeThe...@googlegroups.com.