Add property of every regular congruence being effective (and its dual)

[dschepler]

At the moment, this is very much in draft status: I have 24 undecided categories for "has effective regular congruences" and 21 undecided categories for "has effective regular cocongruences".

The immediate purpose of this PR is to get the last preliminary property in place before I can introduce the property of "Grothendieck quasitopos" along with the Giraud-like theorem for such quasitopoi (Johnstone C2.2.13). (Which is why I was formulating this one before the related property of "has quotients of regular congruences".)

[dschepler]

I think maybe a lot of these can be settled by an argument similar to this one for Top: Take the quotient of the underlying congruence in Set and put the quotient topology on it. Then $E$ has the same underlying set as the kernel pair since Set has effective congruences, and the same topology as the kernel pair by the regularity assumption. That brings to mind the concept of "topological functor" which is certainly true for the forgetful functor $\mathbf{Top} \to \mathbf{Set}$. I might be able to prove that in general, if $F : C \to D$ is a functor which satisfies a weakened version of the "topological functor" property, maybe just for non-empty finite collections of morphisms, and $D$ has effective regular congruences, then so does $C$. And hopefully, that weakened version will also hold for forgetful functors from categories like Meas, Ban, etc.