Proposition graph_enriched_profunctor_enrichment_hom_mor_pr2 {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₂) : graph_enriched_profunctor_enrichment_hom_mor v l r p · graph_enriched_profunctor_enrichment_hom_pr2 _ _ = r. Proof. unfold graph_enriched_profunctor_enrichment_hom_mor. unfold graph_enriched_profunctor_enrichment_hom_pr2. rewrite !assoc. rewrite EqualizerCommutes. apply BinProductPr2Commutes. 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.