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. 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.
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.