Proposition copow_comp_mor {v₁ v₂ v₃ : V} (f : v₁ --> v₂) (g : v₂ --> v₃) (r : C) : copow_mor (f · g) r = copow_mor f r · copow_mor g r. Proof. use arr_to_copower_eq. { exact (pr2 (copowC v₁ r)). } refine (copow_mor_commute (f · g) r @ _). refine (!_). etrans. { apply maponpaths_2. apply maponpaths. apply arr_to_copower_precomp. } etrans. { apply arr_to_copower_commutes. } use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite tensor_split. refine (!_). rewrite tensor_split. rewrite !assoc'. apply maponpaths. unfold internal_postcomp. rewrite !internal_beta. rewrite !assoc. rewrite !internal_beta. rewrite !assoc'. do 2 apply maponpaths. pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) (copow_mor_commute g r)) as p. cbn in p. rewrite !tensor_comp_r_id_r in p. rewrite !assoc' in p. unfold is_copower_enriched_map in p. rewrite !internal_beta in p. rewrite !assoc in p. rewrite <- tensor_split' in p. refine (!(id_left _) @ _). rewrite <- mon_linvunitor_lunitor. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. exact (!p). } unfold postcomp_arr. rewrite !assoc. apply maponpaths_2. rewrite tensor_linvunitor. rewrite !assoc'. apply maponpaths. 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.