Definition. Product of Groupoids [007X] TODO. Objects are pairs of G and H, morphisms are pairs of morphisms.