∀ {X Y Z : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  AddCommGrpCat.ofHom (MonoidHom.toAdditive (CommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))) =
    CategoryTheory.CategoryStruct.comp (AddCommGrpCat.ofHom (MonoidHom.toAdditive (CommGrpCat.Hom.hom f)))
      (AddCommGrpCat.ofHom (MonoidHom.toAdditive (CommGrpCat.Hom.hom g)))