Proposition arr_to_copower_precomp {v : V} {x y r : C} (f : I_{ V} --> v ⊸ (EC ⦃ r , x ⦄)) (g : x --> y) : arr_to_copower _ _ _ (pr2 (copowC v r)) f · g = arr_to_copower _ _ _ (pr2 (copowC v r)) (f · internal_postcomp _ (postcomp_arr EC r g)). Proof. use arr_to_copower_eq. { exact (pr2 (copowC v r)). } refine (!_). etrans. { apply arr_to_copower_commutes. } use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_postcomp, is_copower_enriched_map. rewrite !internal_beta. rewrite tensor_split. refine (!_). etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_comp_l_id_l. apply idpath. } rewrite !assoc'. apply maponpaths. rewrite enriched_from_arr_comp. rewrite !assoc. rewrite tensor_comp_r_id_r. rewrite !assoc'. rewrite enrichment_assoc. unfold postcomp_arr. rewrite !assoc. apply maponpaths_2. refine (!_). etrans. { do 4 apply maponpaths_2. exact (!(arr_to_copower_commutes EC _ _ (pr2 (copowC v r)) f)). } rewrite !tensor_comp_r_id_r. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. unfold is_copower_enriched_map. rewrite internal_beta. apply idpath. } rewrite !assoc. rewrite <- tensor_split'. refine (!_). etrans. { apply maponpaths_2. rewrite !assoc'. rewrite tensor_lassociator. rewrite !assoc. apply maponpaths_2. rewrite tensor_split. rewrite !assoc'. rewrite mon_linvunitor_triangle. rewrite tensor_linvunitor. apply idpath. } rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. refine (!_). etrans. { apply maponpaths_2. etrans. { apply maponpaths. rewrite tensor_split. apply idpath. } rewrite !assoc'. rewrite tensor_comp_l_id_r. apply idpath. } rewrite !assoc'. apply maponpaths. rewrite <- !tensor_comp_mor. rewrite id_left, !id_right. 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.