module funext where

open import preliminaries

postulate funext : {i j : Level} {X : Set i} {Y : X → Set j} {f g : (x : X) → Y x}
                → ((x : X) → f x ≡ g x) → f ≡ g