[TYPES] Representing inductive types with W-types

[Peter Dybjer]

Dear Russell,

"Does anyone have a reference on how to encode (non-mutually recursive)
inductive data type declarations of a language similar to CiC using
W-Types?"

Have a look at

http://www.cse.chalmers.se/~peterd/papers/Wellorderings.pdf

Best wishes,
Peter