"Two" definitions of injectivity on constructive mathematics

Question

In classical mathematics, following two statements are equivalent:

1. If $f(x) = f(y)$ then $x = y$ for each $x$ and $y$.

2. If $x\neq y$ then $f(x)\neq f(y)$ for each $x$ and $y$.

However, in a constructive sense, they could not be equivalent. Clearly, 1 implies 2, but the other direction is not trivial.

My question is:

a) Is there a counterexample $f$ (in constructive sense) satisfying 2. but not 1.? I think some function over reals (I even don't know about real numbers in the constructive sense!) might be a counterexample, but I can't find it.

b) Consider the function $f:\Bbb{N}\to\Bbb{N}$. If $f$ satisfies 2 then it should satisfy 1? For computable $f$ it seems trivial but I don't certain in case of more complex $f$.

Thanks for any help!

Answer 1

This is a partial answer:

b) Yes. This is because the $=$ relation on $\mathbb{N}$ is decidable (use induction to prove that). Suppose $f$ satisifes 2 and $f(x) = f(y)$. If $x \neq y$, then $f(x)\neq f(y)$ (Contradiction). So $\neg x\neq y$. Beacause $=$ ist decidable, we have $x = y$.

My understanding of constructive mathematics is to basic to answer a). I want to point out something else though: In many cases (where equality is not decidable), constructive mathematicians are not primarily interested in the relation given by negating the equality of a set, called denial inequality, but instead in an apartness relation $\neq$. That is a relation on a set, such that: $$\neg x\neq x$$ $$x\neq y \Rightarrow y \neq x$$ $$x \neq z \Rightarrow x \neq y \text{ or } y\neq z$$ If $x\neq y$ and $x = y$, then $x\neq x$ (Contradiction). So $x\neq y \Rightarrow \neg(x = y)$. The negation of an apartness relation is always an equivalence relation, the converse is only provable classically. In particular, denial inequality need not be an apartness relation. Therefore, in general the existence of an apartness relation is an extra property a set may have. Of course, with this the definition of an injection between sets equipped with apartness relations according to 2. changes (and may become more interesting and useful).