Definition opposite_power_enriched {V : sym_mon_closed_cat} {C : category} (E : enrichment C V) {v : V} {x : C} (e : copower_cocone E v x) (He : is_copower_enriched E v x e) : is_power_enriched (op_enrichment V E) v x e. Proof. intros w. use (is_z_isomorphism_path _ (He w)). abstract (unfold is_copower_enriched_map, is_power_enriched_map ; use internal_funext ; intros a h ; rewrite tensor_split ; rewrite !assoc' ; rewrite internal_beta ; refine (!_) ; rewrite tensor_split ; rewrite !assoc' ; rewrite internal_beta ; do 2 apply maponpaths ; cbn -[sym_mon_braiding] ; rewrite !assoc ; rewrite sym_mon_braiding_inv ; apply id_left). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Equalizers. Import MonoidalNotations.