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}