Chuangjie Xu, January 2018

We assume the axiom of function extensionality

\begin{code}

module FunExt where

open import Preliminaries

postulate
 funExt : {A B : Set} {f g : A  B}  (∀ x  f x  g x)  f  g

\end{code}