Preuve que le type n'a pas d'égalité décideable dans Agda

Question

Peut-on créer une telle fonction dans Agda?

ℕ→ℕ-undecidable : ¬ ( (f g :  ℕ → ℕ ) → Dec (f ≡ g)) 
ℕ→ℕ-undecidable = ?

Je suis particulièrement intéressé par la preuve en utilisant Agda cubique.