Definition monoid_mor_comp (X Y Z : monoid_ob) (f : monoid_mor X Y) (g : monoid_mor Y Z) : monoid_mor X Z. Proof. use tpair; [| split]. - exact (f · g). - rewrite assoc. change (monoid_mult X · pr1 f · g = # tensor (f · g #, f · g) · monoid_mult Z). rewrite (pr1 (pr2 f)). rewrite <- assoc. change ((# tensor (f #, f) · (monoid_mult Y · g) = # tensor (catbinprodmor (f · g) (f · g)) · monoid_mult Z)). rewrite binprod_comp. change ((# tensor (pr1 f #, pr1 f) · (monoid_mult Y · pr1 g) = # tensor ((f #, f) · (g #, g)) · monoid_mult Z)). rewrite functor_comp. rewrite (pr1 (pr2 g)). rewrite assoc. apply idpath. - rewrite assoc. rewrite <- (pr2 (pr2 g)). rewrite <- (pr2 (pr2 f)). 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.