On Wed, Oct 28, 2009 at 5:32 PM, Jean-Philippe Bernardy <jeanphilippe.bernardy at gmail.com> wrote: > I have an Agda transcription of some of the "Generic Programming w/ > Dependent Types" paper. Thank you. I see there is also this talk by Thorsten: http://www.cs.nott.ac.uk/~txa/talks/fun08.pdf (it seems his code has an implicit --type-in-type!) Noam