Proposition copow_id_mor (v : V) (r : C) : copow_mor (identity v) r = identity _. Proof. use arr_to_copower_eq. { exact (pr2 (copowC v r)). } refine (copow_mor_commute (identity v) r @ _). rewrite enriched_from_arr_id. unfold is_copower_enriched_map. use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite tensor_split. rewrite !assoc'. rewrite !internal_beta. rewrite id_left. refine (!_). rewrite tensor_split. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. rewrite <- enrichment_id_left. rewrite tensor_lunitor. apply idpath. 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.