Has this 'group product equivalence quotient' construction been substantially studied? Recently I've seen a few examples of an 'equivalence class' subgroup of a product of two groups: given $G$ and $H$ with homomorphisms $\gamma: G\mapsto K$ and $\eta: H\mapsto K$, one can form a group $(G\times H)/K$ as the subgroup of $G\times H$ consisting of those elements $\langle g,h \rangle$ with $\gamma(g)=\eta(h)$. It's easy to see that the order of the group is $\dfrac{|G|\cdot|H|}{|K|}$ so the notation makes sense (at least to me). Another way to think about this is as the coequalizer of $G\times H$ by the compositions of the two projection maps with the corresponding homomorphisms as maps from $G\times H\mapsto K$. This comes up most notably (for me) in the classification of finite subgroups of $SO(4)$ where groups like $\frac12(S_4\times S_4)$ show up (the homomorphisms in this case being the usual parity homomorphism onto $C_2$), but I've seen the same construction or versions of it in a few places; it shows up in analyzing puzzles, for instance. This seems like such a natural notion that I'm surprised I haven't seen it covered more frequently; are there any references that anyone might be able to point me to?

As mentioned in the comments, this is the pullback / fiber product $G \times_K H$. It appears in group theory in the context of Goursat's lemma classifying subgroups of $G \times H$. It is quite misleading, in my opinion, to refer to this construction using quotient terminology or notation, because it is not in any way a quotient: it is a (categorical) limit, and quotients are colimits.
