On analysis of one of the explicit assignments in FreeAb, we discovered that the implication additive_effective_congruences_imply_normal can be strengthened by removing the assumption of having pullbacks. The revision to be made is:
Given $i : Y \hookrightarrow X$, form the congruence of $\equiv \pmod{i(Y)}$ as $E := X \times Y$, with one map being $(x, y) \mapsto x+i(y)$ and the other map being $(x,y) \mapsto x$.
On analysis of one of the explicit assignments in FreeAb, we discovered that the implication additive_effective_congruences_imply_normal can be strengthened by removing the assumption of having pullbacks. The revision to be made is:$i : Y \hookrightarrow X$ , form the congruence of $\equiv \pmod{i(Y)}$ as $E := X \times Y$ , with one map being $(x, y) \mapsto x+i(y)$ and the other map being $(x,y) \mapsto x$ .
Given