I was reading the paper Towards Constructive Homological Algebra in Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be abelian, because we cannot verify that every monic and epic map is normal. In particular, they say that given a monic map $u:A \rightarrowtail B$, we cannot prove constructively that it is the kernel of $B \to B/\mathrm{Im}(u)$.

I'm new to constructive mathematics, so it isn't obvious to me exactly where the issue is. At what stage do we use excluded middle or some form of choice when proving that monos and epis are normal?

Also, could we correct this lack of normality somehow with some additional assumptions on the groups (countably or finitely generated, for example)?