proposition: Lemma tensor_comp_right {X Y Z W : Mon_V} (f : X --> Y) (g : Y --> Z) : (id W #⊗ (f · g)) = (id W #⊗ f) · (id W #⊗ g).
proof: Proof. rewrite <- (functor_comp tensor). change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w). rewrite id_left. apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering