Martin Escardo 2012.

\begin{code}

{-# OPTIONS --without-K --exact-split #-}

module FunExt where

open import SpartanMLTT

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

\end{code}