{-# OPTIONS --without-K #-}
module Function.Extensionality where

open import Relation.Binary.PropositionalEquality

postulate
    FunExt : Set
    λ= : ∀ {a b}{A : Set a}{B : A → Set b}{f₀ f₁ : (x : A) → B x}(f= : ∀ x → f₀ x ≡ f₁ x){{fe : FunExt}} → f₀ ≡ f₁