Definition graph_enriched_profunctor_pr2_enrichment : functor_enrichment graph_enriched_profunctor_pr2 graph_enriched_profunctor_enrichment E₁. Proof. simple refine (_ ,, _ ,, _ ,, _). - intros xyf₁ xyf₂. apply graph_enriched_profunctor_enrichment_hom_pr1. - abstract (intros xyf ; cbn ; apply graph_enriched_profunctor_enrichment_id_pr1). - abstract (intros xyf₁ xyf₂ xyf₃ ; cbn ; apply graph_enriched_profunctor_enrichment_comp_pr1). - abstract (intros xyf₁ xyf₂ h ; cbn ; rewrite graph_enriched_profunctor_enrichment_from_arr_pr1 ; apply idpath). 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.