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}