∀ (R : CommRingCat) (X : CommMonCat),
  CategoryTheory.Under.homMk
      (CommRingCat.ofHom
        (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.id X))))
      ⋯ =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Under.mk (CommRingCat.ofHom MonoidAlgebra.singleOneRingHom))