Proposition profunctor_square_to_enriched_nat_trans_left_right_point {V : benabou_cosmos} {C₁ C₂ : category} {E₁ : enrichment C₁ V} {E₂ : enrichment C₂ V} {F G : C₁ ⟶ C₂} {EF : functor_enrichment F E₁ E₂} {EG : functor_enrichment G E₁ E₂} (τ : enriched_profunctor_square EF EG (identity_enriched_profunctor E₁) (identity_enriched_profunctor E₂)) (x y : C₁) : EG x y · mon_linvunitor _ · enriched_from_arr E₂ (square_to_enriched_nat_trans_data τ y) #⊗ identity _ · enriched_comp E₂ (G x) (G y) (F y) = τ x y. Proof. cbn. rewrite enriched_from_to_arr. rewrite tensor_linvunitor. rewrite tensor_comp_id_r. rewrite !assoc'. pose (enriched_profunctor_square_lmap_e τ y x y) as p. cbn in p. rewrite !assoc in p. rewrite tensor_sym_mon_braiding in p. pose (maponpaths (λ z, sym_mon_braiding _ _ _ · z) p) as q. cbn in q. rewrite !assoc in q. rewrite !sym_mon_braiding_inv in q. rewrite !id_left in q. etrans. { apply maponpaths. rewrite !assoc. rewrite <- tensor_split. rewrite tensor_split'. rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite <- tensor_split. exact q. } refine (_ @ id_left _). rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite <- enrichment_id_left. apply mon_linvunitor_lunitor. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.whiskering. 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.Invertible. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Coend. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.CompositionProf. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.SquareComp. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Unitors. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Associators. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Whiskering. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Import MonoidalNotations.