Add a sentence to motivate eta-equality

[fangyi-zhou]

Addresses #1099.

[wadler]

Thank you!

In "put them back" grammatically "them" refers to either "the destructors" or "the constructors", neither of which I think you intend. How about replacing the first sentence with this:

Start with a product, apply the destructors to it, and then apply the constructor; the result is the original product.

[fangyi-zhou]

Thanks for the suggestion, my intention was the generalise the concept from the previous sentence to motivate the eta-quality law, since the preceeding sentence reads:

Applying each destructor and reassembling the results with the
constructor is the identity over products:

In the spirit of providing more clarity, what about this:

In the general sense, with a record, apply the projections to all fields, and then apply the record constructor; the result is the original record.

[wenkokke]

Thanks for the suggestion, my intention was the generalise the concept from the previous sentence to motivate the eta-quality law, since the preceeding sentence reads:

Applying each destructor and reassembling the results with the
constructor is the identity over products:

In the spirit of providing more clarity, what about this:

In the general sense, with a record, apply the projections to all fields, and then apply the record constructor; the result is the original record.

"For any record, projecting out each field and reassembling the results using the constructor should be the identity."

Maybe followed by (except using more appropriate unicode):

c (p1 r) ... (pN r) = r