∀ (A : CommGrpCat),
  CategoryTheory.CategoryStruct.comp
      (β_ (grpTypeEquivalenceGrp.inverse.obj ((CategoryTheory.forget₂ CommGrpCat GrpCat).obj A)).X
          (grpTypeEquivalenceGrp.inverse.obj ((CategoryTheory.forget₂ CommGrpCat GrpCat).obj A)).X).hom
      CategoryTheory.MonObj.mul =
    CategoryTheory.MonObj.mul