Proposition copow_enriched_mor_commute (v₁ v₂ : V) (r : C) : (copow_enriched_mor v₁ v₂ r · is_copower_enriched_map EC v₁ r _ _) #⊗ identity v₁ · internal_eval v₁ _ = internal_eval v₁ v₂ · mor_of_copow_ob v₂ r. Proof. pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) (mor_to_copower_commutes EC v₁ r (pr2 (copowC v₁ r)) (internal_postcomp _ (mor_of_copow_ob v₂ r)))) as p. cbn in p. unfold internal_postcomp in p. rewrite !internal_beta in p. exact p. 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.