∀ (M : CommMonCatᵒᵖ) {X Y Z : CommMonCat} (f : X ⟶ Y) (g : Y ⟶ Z),
  CommMonCat.ofHom (MonoidHom.compHom (CommMonCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))) =
    CategoryTheory.CategoryStruct.comp (CommMonCat.ofHom (MonoidHom.compHom (CommMonCat.Hom.hom f)))
      (CommMonCat.ofHom (MonoidHom.compHom (CommMonCat.Hom.hom g)))