Proposition copow_mor_commute {v₁ v₂ : V} (f : v₁ --> v₂) (r : C) : enriched_from_arr EC (copow_mor f r) · is_copower_enriched_map EC v₁ r _ _ = internal_lam (mon_lunitor _ · f · mor_of_copow_ob v₂ r). Proof. apply arr_to_copower_commutes. 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.