Can one create such function in Agda ?

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

I am particularly interested in proof using cubical Agda.


1 Answer 1


ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.

  • $\begingroup$ What about coq? Is it possible to prove it there? $\endgroup$
    – srghma
    Sep 5, 2019 at 9:11
  • 2
    $\begingroup$ @srghma no, the same thing holds for Coq. Consistency with LEM (classical logic) is a common expected feature in proof assistants. $\endgroup$ Sep 5, 2019 at 17:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.