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