Definition graph_enriched_profunctor_enrichment_from_arr {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : I_{V} --> P y₁ x₁} {g : I_{V} --> P y₂ x₂} {hx : x₁ --> x₂} {hy : y₁ --> y₂} (p : g · lmap_e_arr P _ hy = f · rmap_e_arr P hx _) : I_{V} --> graph_enriched_profunctor_enrichment_hom f g. Proof. use graph_enriched_profunctor_enrichment_hom_mor. - exact (enriched_from_arr E₁ hx). - exact (enriched_from_arr E₂ hy). - abstract (rewrite !tensor_rinvunitor ; rewrite !assoc' ; apply maponpaths ; rewrite !assoc ; rewrite <- !tensor_split' ; rewrite (tensor_split (enriched_from_arr _ _) f) ; rewrite (tensor_split (enriched_from_arr _ _) g) ; unfold lmap_e_arr, rmap_e_arr in p ; rewrite !assoc in p ; rewrite !tensor_linvunitor in p ; pose proof (maponpaths (λ z, mon_lunitor _ · z) p) as q ; cbn in q ; rewrite !assoc in q ; rewrite !mon_lunitor_linvunitor in q ; rewrite !id_left in q ; exact (!q)). Defined.
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.