Definition copow_mor {v₁ v₂ : V} (f : v₁ --> v₂) (r : C) : copow_ob v₁ r --> copow_ob v₂ r. Proof. use arr_to_copower. { exact (pr2 (copowC v₁ r)). } exact (internal_lam (mon_lunitor _ · f · mor_of_copow_ob v₂ r)). Defined.
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.