Definition graph_enriched_profunctor_enrichment_hom_mor {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : I_{V} --> P y₁ x₁} {g : I_{V} --> P y₂ x₂} (v : V) (l : v --> E₁ ⦃ x₁ , x₂ ⦄) (r : v --> E₂ ⦃ y₁ , y₂ ⦄) (p : l · mon_rinvunitor _ · identity _ #⊗ f · rmap_e P y₁ x₁ x₂ = r · mon_rinvunitor _ · identity _ #⊗ g · lmap_e P y₂ y₁ x₂) : v --> graph_enriched_profunctor_enrichment_hom f g. Proof. use EqualizerIn. - exact (BinProductArrow _ _ l r). - abstract (unfold graph_enriched_profunctor_enrichment_hom_left ; unfold graph_enriched_profunctor_enrichment_hom_right ; rewrite !assoc ; rewrite BinProductPr1Commutes ; rewrite BinProductPr2Commutes ; exact p). 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.