[Agda] 'Dummie' question - why records?

[Dirk Ullrich]

Hallo,

thank you for clarification. Before this I saw, like Wojciech, only
rather pragmatic differences between `record' and `data', but having
Eta-equality or not is more than this.

So taking dependent records together with dependent function types
(where we have eta-equality in Agda, too, right?) 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.

Dirk