Definition copow_enriched_mor (v₁ v₂ : V) (r : C) : v₁ ⊸ v₂ --> EC ⦃ copow_ob v₁ r , copow_ob v₂ r ⦄. Proof. use mor_to_copower. { exact (pr2 (copowC v₁ r)). } use internal_postcomp. apply mor_of_copow_ob. 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.