module funext where

open import preliminaries

postulate funext : {i j : 𝕃} {X : Set i} {Y : X  Set j} {f g : (x : X)  Y x} 
                 ((x : X)  f x  g x)  f  g