Proposition representable_enriched_profunctor_right_right_eq {V : benabou_cosmos} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {F : C₁ ⟶ C₂} (EF : functor_enrichment F E₁ E₂) : dwhisker_enriched_profunctor_square (linvunitor_enrichment EF) (uwhisker_enriched_profunctor_square (runitor_enrichment EF) (comp_h_enriched_profunctor_square (representable_enriched_profunctor_right_unit EF) (representable_enriched_profunctor_right_counit EF))) = id_v_enriched_profunctor_square EF. Proof. use eq_enriched_profunctor_transformation ; intros z x ; cbn. rewrite id_right. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. rewrite !enriched_from_arr_id. etrans. { apply maponpaths. rewrite !assoc. rewrite <- enrichment_id_left. rewrite mon_lunitor_linvunitor. rewrite id_left. rewrite tensor_sym_mon_braiding. rewrite !assoc'. rewrite <- enrichment_id_right. rewrite sym_mon_braiding_runitor. apply idpath. } apply mon_linvunitor_lunitor. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.