Definition enriched_profunctor_collage_enrichment_data : enrichment_data enriched_profunctor_collage_precategory_data V. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact enriched_profunctor_collage_enrichment_hom_ob. - exact enriched_profunctor_collage_enrichment_id. - exact enriched_profunctor_collage_enrichment_comp. - exact (λ _ _ f, enriched_profunctor_collage_enrichment_from_arr f). - exact (λ _ _ f, enriched_profunctor_collage_enrichment_to_arr f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Initial. 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. Import MonoidalNotations.