Characterizing the equality of Indexed W types

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

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