module equalityNarN where

data ℕ : Set where
  Z : ℕ
  S : ℕ -> ℕ

postulate _==_ : ℕ -> ℕ -> Set


_==ℕ->ℕ_ : (ℕ -> ℕ)  -> (ℕ -> ℕ)  -> Set
f ==ℕ->ℕ g = (n : ℕ) -> f n  == g n