Classically, we can explicitly construct the free Abelian group $\newcommand{\Z}{\mathbb{Z}}\Z[X]$ on a set $X$ as the set of finitely-supported functions $X \to \Z$, and so easily see that the unit map $X \to \Z[X]$ (inclusion of generators) is injective.

Constructively, this construction of $\Z[X]$ doesn’t work for arbitrary $X$. The unit map $X \to \Z[X]$ should send $x \in X$ to the function $1_x : X \to \Z$, sending $y \in X$ to $1$ if $y = x$ and $0$ otherwise; but this definition-by-cases requires that $X$ has decidable equality (i.e. for every $x,y \in X$, either $y = x$ or $y \neq x$).

Similarly, most other classical explicit constructions of $\Z[X]$ rely at some point on decidable equality of $X$. The abstract-nonsense construction of $\Z[X]$ as a free model of an algebraic theory works fine constructively; but from this construction, it’s not clear that the unit map is $X \to \Z[X]$.

Is there some constructive proof that the unit map $X \to \Z[X]$ is injective for arbitrary $X$, or can it fail?

[Note this is a self-answered question. It came up since the fact was required here; asking several experts, the answer seems to be not well-known. After a couple of days, I worked out an answer via an explicit construction, and then also got a reply pointing to a slightly less explicit answer in the literature; so I’m writing it up here to make the answer and construction more prominently available.]