# What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this:
funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2
One may note a similarity in the definition of a (binary) logical relation
f1 [A -> B] f2 being:
∀ x1 x2 → x1 [A] x2 -> f1 x1 [B] f2 x2.

What is the relation of logical relations to function extensionality? Is there perhaps a relation to eta-equality?

• Might be relevant, since Univalence implies extensionality: arxiv.org/abs/1909.05027 Mar 23 at 4:56