∀ (X : AddCommGrpCat),
  CommGrpCat.ofHom (AddMonoidHom.toMultiplicative (AddCommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X))) =
    CategoryTheory.CategoryStruct.id (CommGrpCat.of (Multiplicative ↑X))