[Agda] 'Dummie' question - why records?

[Nils Anders Danielsson]

On 2011-10-18 12:47, Dirk Ullrich wrote:
> So taking dependent records together with dependent function types
> (where we have eta-equality in Agda, too, right?)

Yes.

> looks a little bit like Martin-Löf's logical framework where you have,
> as far as I know, dependent product and function types, both with
> eta-equality.

I don't think you have (definitional) η-equality in the intensional
variant of the framework.

-- 
/NAD