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.