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.

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