Definition monoid_mor_id (X : monoid_ob) : monoid_mor X X. Proof. exists (id _). red. rewrite id_right. rewrite tensor_id. rewrite id_left. rewrite id_right. split; apply idpath. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.