[Agda] dependent extensionality

[David Leduc]

Hi,

Is it safe to add the following postulate in Agda?

  postulate extensionality : {l1 l2 : Level}{A : Set l1}{B : A -> Set
l2}{f g : (a : A) -> B a} -> (∀ x → f x ≡ g x) → f ≡ g

P.S. Note that the definition of Extensionality in
Relation.Binary.PropositionalEquality is not dependent, and forces
domain and codomain to be at the same level. Maybe it should be
generalized as above.