eta equality should be motivated/explained

[fangyi-zhou]

In #1051 and #1052 (Presenting conjunction, truth and existentials using records first before using data types), the text mentions eta equality without much motivation or explanation. I suggest that the notion of eta equality to be introduced/mentioned either in the Connectives chapter or (maybe more appropriately) the Equality chapter.

[wenkokke]

That makes a lot of sense.

@wadler Thoughts?

[wadler]

The suggestion is that eta-equality be introduced in Connectives, but that is already where it is introduced.

I think Connectives is a better choice than Equality, because it is hard to talk about the eta-rule for products until one talks about products.

I'd be happy to consider a pull request with suggested text to improve the motivation.

[wenkokke]

The suggestion is that eta-equality be introduced in Connectives, but that is already where it is introduced.

I think the issue is that it isn't really explained. There's the matter of introduction and elimination rules, then there's a bit of Agda code that uses the letter η, and then the next line talks about η-equality.

Even a roughshod explanation of β- and η-equality rules would help, such as saying that there's two kinds of equality rules on objects formed by introduction and elimination rules: β-equality rules that say "elim (intro x) = x" and η-equality rules that say "intro (elim x) = x" (except phrased with a bit more care and less pseudo-formality).

[fangyi-zhou]

I've put a simple sentence for eta-equality in #1102, please let me know how it sounds!

P.S. Is there a canonical reference for the phrase "eta-equality" in the general sense? I learnt this concept in lambda calculus as (\x -> f x) == f, but I didn't know it generalises to introduction and elimination rules in general.