Definition copow_on_enriched_mor (r₁ r₂ : C) : copow_ob (EC ⦃ r₁ , r₂ ⦄) r₁ --> r₂. Proof. use arr_to_copower. { exact (pr2 (copowC _ _)). } exact (internal_from_arr (identity _)). 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.