Lemma postcompose_underlying_morphism_enriched_cat_comp {A : enriched_precat} {w x y z : A} (f : underlying_morphism y z) : ((postcompose_underlying_morphism x f #⊗ identity _) · enriched_cat_comp w x z = enriched_cat_comp w x y · postcompose_underlying_morphism w f). Proof. unfold postcompose_underlying_morphism. rewrite !assoc. rewrite tensor_linvunitor. rewrite !assoc'. refine (!_). etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_split'. apply idpath. } refine (!_). rewrite assoc. rewrite !tensor_comp_id_r. rewrite assoc'. rewrite (@enriched_assoc A). rewrite !assoc. do 2 apply cancel_postcomposition. rewrite assoc'. etrans. { apply cancel_precomposition. apply tensor_lassociator. } rewrite assoc. rewrite tensor_id_id. apply cancel_postcomposition. apply mon_linvunitor_triangle. 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.