proposition: 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: Proof. etrans. { do 2 apply maponpaths_2. apply arr_to_copower_commutes. } unfold internal_from_arr. rewrite internal_beta. apply id_right. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers