Proposition graph_enriched_profunctor_enrichment_to_arr_eq : graph_enriched_profunctor_ob_mor xyf₂ · lmap_e_arr P (graph_enriched_profunctor_ob_pr2 xyf₂) k₁ = graph_enriched_profunctor_ob_mor xyf₁ · rmap_e_arr P k₂ (graph_enriched_profunctor_ob_pr1 xyf₁). Proof. unfold k₁, k₂. cbn. unfold lmap_e_arr, rmap_e_arr. rewrite !enriched_from_to_arr. etrans. { rewrite !assoc. rewrite tensor_linvunitor. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_split. rewrite tensor_split'. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite !assoc. rewrite <- tensor_rinvunitor. apply idpath. } etrans. { rewrite !assoc'. apply maponpaths. etrans. { apply maponpaths. rewrite !assoc. apply idpath. } rewrite !assoc. refine (!_). apply graph_enriched_profunctor_enrichment_hom_eq. } refine (!_). etrans. { rewrite !assoc. rewrite tensor_linvunitor. apply maponpaths_2. rewrite !assoc'. rewrite <- tensor_split. rewrite tensor_split'. rewrite mon_linvunitor_I_mon_rinvunitor_I. rewrite !assoc. rewrite <- tensor_rinvunitor. apply idpath. } rewrite !assoc'. do 2 apply maponpaths. rewrite !assoc. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.EnrichedCats.BenabouCosmos. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares. Require Import UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Import MonoidalNotations.