[Agda] Re: 'Dummie' question - why records?

[Jean-Philippe Bernardy]

On Wed, Oct 26, 2011 at 3:49 PM, Zhaohui Luo <zhaohui.luo at hotmail.co.uk> wrote:
> People in this thread may be interested in the following paper of mine on
> dependent record types

I would welcome integration of some of this in Agda.
In particular I think that well-designed DRTs should be able to subsume modules,
and I think you make a good case for that.

Cheers,
JP.