Proposition precomp_postcomp_arr_assoc {C : category} {V : monoidal_cat} (E : enrichment C V) {w x y z : C} (f : x --> y) : (precomp_arr E z f #⊗ identity _) · enriched_comp E w x z = (identity _ #⊗ postcomp_arr E w f) · enriched_comp E _ _ _. Proof. unfold precomp_arr. rewrite !tensor_comp_id_r. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. apply maponpaths_2. unfold postcomp_arr. rewrite !tensor_comp_id_l. apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. rewrite mon_inv_triangle. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import MonoidalNotations.