Proposition precomp_copow_on_enriched_mor_commute (x r₁ r₂ : C) : (precomp_arr EC x (copow_on_enriched_mor r₁ r₂) · is_copower_enriched_map EC _ _ _ _) #⊗ identity _ · internal_eval _ _ = enriched_comp EC r₁ r₂ x. Proof. rewrite !tensor_comp_r_id_r. unfold is_copower_enriched_map. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. unfold precomp_arr. rewrite !tensor_comp_r_id_r. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. etrans. { apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- mon_inv_triangle. apply idpath. } rewrite <- !tensor_comp_id_l. rewrite <- tensor_id_id. apply maponpaths. rewrite tensor_linvunitor. refine (_ @ mon_linvunitor_lunitor _). rewrite !assoc'. apply maponpaths. refine (_ @ copow_on_enriched_mor_commute _ _). rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold is_copower_enriched_map. rewrite internal_beta. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_split. rewrite <- tensor_split'. apply idpath. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Import MonoidalNotations.