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

[oleg at okmij.org]

> 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.