Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

do you have any references for the extension of lambda-encoding of data into dependently typed systems?

Is there a way out of this quagmire? Or are we stuck defining actual datatypes if we want dependent types?

Although not directly answering your question, the following paper Inductive Data Types: Well-ordering Types Revisited Healfdene Goguen Zhaohui Luo http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.17.8970&rep=rep1&type=pdf might still be relevant. Sec 2 reviews the major approaches to inductive data types in Type Theory.