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