[Agda] Pointwise function equality

[Dominique Devriese]

Hi all,

I hope someone here can help me with another Agda beginner's question.
The following seems useful and intuitively makes sense to me, but I am
not sure if this is sound and if/where/how it fits in the
in-/extensionality range.

  postulate pointwise : ∀ {l} {A B : Set l} {f₁ : A → B} {f₂ : A → B}
→ ((x : A) → f₁ x ≡ f₂ x) → f₁ ≡ f₂

Can anyone here shed some light on this and/or provide interesting references?

Thanks in advance,
Dominique