Proposition yoneda_inv_right : enriched_yoneda_enrichment E EqV PV PV' x y · yoneda_inv = identity _. Proof. cbn. rewrite !assoc. rewrite EqualizerCommutes. etrans. { do 3 apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } rewrite tensor_rinvunitor. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. rewrite internal_beta. rewrite <- enrichment_id_right. apply idpath. } apply mon_rinvunitor_runitor. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.Yoneda. 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.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.