Re: [TYPES] Representing inductive types with W-types

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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