{-# OPTIONS --cubical-compatible #-}


module Terra.Data.Function.Postulates where
open import Terra.Data.Level.Variables
open import Terra.Data.Equality

postulate
  extensionality : {A : Set ℓ} {B : A -> Set ℓ′} {f g : (x : A) -> B x} -> ((some : A) -> f some ≡ g some) -> f ≡ g