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