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