proposition: Proposition copow_id_mor (v : V) (r : C) : copow_mor (identity v) r = identity _.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers