Martin Escardo 2012.

\begin{code}

{-# OPTIONS --without-K #-}

module Extensionality where

open import Equality

postulate 
 funext : {X : Set}  {Y : X  Set}  ∀{f g : (x : X)  Y x}  (∀ x  f x  g x)  f  g

\end{code}