∀ {X Y Z : AddGrpCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  AddMonCat.ofHom (AddGrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    CategoryTheory.CategoryStruct.comp (AddMonCat.ofHom (AddGrpCat.Hom.hom f)) (AddMonCat.ofHom (AddGrpCat.Hom.hom g))