"Representing Nested Inductive Types Using W-Types."

Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani (2004)
a service of Schloss Dagstuhl - Leibniz Center for Informatics