Add a sentence to motivate eta-equality

Addresses #1099.

Author: fangyi-zhou

src/plfa/part1/Connectives.lagda.md

@@ -84,10 +84,16 @@ holds---how to _use_ the connective.[^from-wadler-2015]
 
 Applying each destructor and reassembling the results with the
 constructor is the identity over products:
+
 ```agda
 η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
 η-× w = refl
 ```
+
+Intuitively, if we first apply the destructors to a product,
+and then apply the constructors to put them back,
+we get back the original product.
+This concept is known as the *η-equality* (hence we name it `η-×`).
 For record types, η-equality holds *by definition*.
 While proving `η-×`, we do not have to
 pattern match on `w` to know that η-equality holds.