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