proposition: Lemma enriched_cat_comp_underlying_morphism_middle {A : enriched_precat} {w x y z : A} (f : underlying_morphism x y) : ((identity _ #⊗ postcompose_underlying_morphism w f) · enriched_cat_comp w y z = (precompose_underlying_morphism z f #⊗ identity _) · enriched_cat_comp w x z).
proof: Proof. unfold precompose_underlying_morphism, postcompose_underlying_morphism. rewrite !tensor_comp_id_r, !tensor_comp_id_l. apply pathsinv0. rewrite assoc'. rewrite (@enriched_assoc A). rewrite !assoc. do 2 apply cancel_postcomposition. rewrite assoc'. etrans. { apply cancel_precomposition. apply tensor_lassociator. } rewrite assoc. apply cancel_postcomposition. rewrite mon_inv_triangle. apply idpath. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Core.Isos