Proposition copow_on_enriched_mor_commute (r₁ r₂ : C) : (enriched_from_arr EC (copow_on_enriched_mor r₁ r₂) · is_copower_enriched_map EC _ _ _ _) #⊗ identity _ · internal_eval _ _ = mon_lunitor _. Proof. etrans. { do 2 apply maponpaths_2. apply arr_to_copower_commutes. } unfold internal_from_arr. rewrite internal_beta. apply id_right. 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.