[Agda] 'Dummie' question - why records?

[Jesper Louis Andersen]

On Tue, Oct 18, 2011 at 11:05, Nils Anders Danielsson <nad at chalmers.se> wrote:

> One might wonder why we don't simply implement η-equality for, say,
> non-recursive single-constructor data types. One reason is that, while
> there are many situations in which η-equality is nice to have, there are
> some where it's nice not to have η. Ulf's "inspect on steroids" is one
> example.

I've never heard about η-equality. η-expansion for the lambda calculus
yes, but not equality. Are the two related in any way?

-- 
J.