Proposition graph_enriched_profunctor_enrichment_hom_mor_eq {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : I_{V} --> P y₁ x₁} {g : I_{V} --> P y₂ x₂} (v : V) {h₁ h₂ : v --> graph_enriched_profunctor_enrichment_hom f g} (p : h₁ · graph_enriched_profunctor_enrichment_hom_pr1 _ _ = h₂ · graph_enriched_profunctor_enrichment_hom_pr1 _ _) (q : h₁ · graph_enriched_profunctor_enrichment_hom_pr2 _ _ = h₂ · graph_enriched_profunctor_enrichment_hom_pr2 _ _) : h₁ = h₂. Proof. use EqualizerInsEq. use BinProductArrowsEq. - rewrite !assoc'. exact p. - rewrite !assoc'. exact q. 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.