Equality over the computable reals is stable, but it is not necessarily stable for all PERs. For example, a set of equivalence sets of words modulo a rewrite relation. Two words are equal iff there exists a rewrite path between them. This relation has positive content and is not stable under double negation.

Coming up with that counterexample to Andrej's claim actually led me to answer my own question.

A subgroup is the equaliser of its cokernel pair, which in the category of groups is the amalgamated free product. So we just have to constructively prove that this exists. Schreier's construction is very explicit, but word reduction is not computable. So, instead of using the set of reduced words, we work with, yes, the set of equivalence sets of words modulo the reduction relation.

Given a PER as $(G,R,mult,inv)$, and a subgroup $H$ of $G$, we form $G^{\ast}$ as a set of finite sequences of elements from the disjoint sum $G+G$, $R^{\ast}$ as an appropriate equivalence relation for the amalgamated free product (allowing combination of adjacent elements from the same copy of $G$ via multiplication, and also allowing switching between different copies of $G$ if the element in question is in $H$). Then multiplication and inversion are computable, even though in general $R^{\ast}$ isn't.

This same construction can be done in abstract set theory, where quotient sets are not a problem and work in weak subtheories of CZF.

As discussed below, the above is mistaken. As I understand it now -- please point out any error -- the construction above is well-defined and gives the cokernel pair, and in CZF, the subgroup is the equaliser of the cokernel pair, which answers the original question in the affirmative.

But in PER, the subgroup is not quite the equaliser of it. The morphism asserted to exist by the universal property isn't quite constructible in PER, sometimes some necessary information has been lost. The failure has nothing to do with group theory. We can forget the group operations and ask if every PER-injection is the equaliser of two PER-functions, and the answer is still no. PER isn't as good an approximation to constructive set theory as I thought.

1

Equality over the computable reals is stable, but it is not necessarily stable for all PERs. For example, a set of equivalence sets of words modulo a rewrite relation. Two words are equal iff there exists a rewrite path between them. This relation has positive content and is not stable under double negation.

Coming up with that counterexample to Andrej's claim actually led me to answer my own question.

A subgroup is the equaliser of its cokernel pair, which in the category of groups is the amalgamated free product. So we just have to constructively prove that this exists. Schreier's construction is very explicit, but word reduction is not computable. So, instead of using the set of reduced words, we work with, yes, the set of equivalence sets of words modulo the reduction relation.

Given a PER as $(G,R,mult,inv)$, and a subgroup $H$ of $G$, we form $G^{\ast}$ as a set of finite sequences of elements from the disjoint sum $G+G$, $R^{\ast}$ as an appropriate equivalence relation for the amalgamated free product (allowing combination of adjacent elements from the same copy of $G$ via multiplication, and also allowing switching between different copies of $G$ if the element in question is in $H$). Then multiplication and inversion are computable, even though in general $R^{\ast}$ isn't.

This same construction can be done in abstract set theory, where quotient sets are not a problem and work in weak subtheories of CZF.