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}