Lemma precompose_underlying_morphism_enriched_cat_comp {A : enriched_precat} {w x y z : A} (f : underlying_morphism w x) : ((identity _ #⊗ precompose_underlying_morphism y f) · enriched_cat_comp w y z = enriched_cat_comp x y z · precompose_underlying_morphism z f)%cat. Proof. unfold precompose_underlying_morphism. rewrite !assoc. rewrite tensor_rinvunitor. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. apply idpath. } refine (!_). rewrite assoc. rewrite (assoc' _ _ (enriched_cat_comp w x z)). rewrite (@enriched_assoc A). rewrite !assoc. rewrite !tensor_comp_id_l. do 2 apply cancel_postcomposition. rewrite assoc'. rewrite <- tensor_id_id. apply pathsinv0. etrans. { apply cancel_precomposition. apply tensor_lassociator. } rewrite assoc. apply cancel_postcomposition. rewrite <- mon_rinvunitor_triangle. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. apply mon_rassociator_lassociator. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Core.Isos. Import MonoidalNotations.