Martin Escardo 2012. \begin{code} module Extensionality where open import Equality postulate extensionality : {X : Set} → {Y : X -> Set} → ∀{f g : (x : X) → Y x} → (∀ x → f x ≡ g x) → f ≡ g \end{code}