In constructive mathematics, why does the category of abelian groups fail to be abelian?

Question

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)?

Answer 1

There are many different flavors of constructive mathematics. The theory that was used in this paper is weak, it lacks some useful constructions from the usual set theory such as quotient sets. Another problem is that it lacks function extensionality (that is, if you can prove that two functions are pointwise equal, this does not imply that they are equal). For these reasons we usually work with setoids (which authors of the paper call Bishop sets) in such weak theories. You can define the setoid of functions with the correct equivalence relation on it and you obviously can define quotient setoids. But this approach still has problems as the example of abelian group shows.

We can solve these problems by strengthening our theory (but still keeping it constructive and even predicative if we want). Homotopy type theory does precisely that. Note that if we don't care about higher types, we can define a theory which is between the ordinary type theory and HoTT. We just add axioms for function extensionality and propositional extensionlity (logically equivalent propositions are equal). This makes the theory into an internal language of a topos (assuming that the type of propositions is impredicative as in the paper). In this theory we can construct quotient types in the usual way as the type of equivalence classes. Even if we don't want to add an impredicative type of propositions, we still can add quotient types explicitly as a special case of higher inductive types. Then we can prove that the category of abelian groups is abelian without any problems.