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

["Gaëtan Gilbert" <"gaetan...."@skyskimmer.net>]

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.