Can one create such function in Agda ?
ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g))
ℕ→ℕ-undecidable = ?
I am particularly interested in proof using cubical Agda.
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this communityCan one create such function in Agda ?
ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g))
ℕ→ℕ-undecidable = ?
I am particularly interested in proof using cubical Agda.
ℕ→ℕ-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.