The meat of this is definitely the third homomorphism theorem. I worried that it was completely non-constructive but according to the linked paper you can defin

The meat of this is definitely the third homomorphism theorem. I worried that it was completely non-constructive but according to the linked paper you can define the corresponding associative operation as follows: t * u = h (g t ++ g u) where g is a pseudo-inverse of h such that hgh = h. The left and right folding of the function is used to prove associativity. Sure finding a pseudo inverse isn't always easy but it's at least somewhat doable.