proposition: 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: 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.
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