Proposition graph_enriched_profunctor_enrichment_hom_mor_pr1 {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_pr1 _ _ = l. Proof. unfold graph_enriched_profunctor_enrichment_hom_mor. unfold graph_enriched_profunctor_enrichment_hom_pr1. rewrite !assoc. rewrite EqualizerCommutes. apply BinProductPr1Commutes. 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.