Definition enriched_profunctor_collage_enrichment_to_arr {x₁ x₂ : enriched_profunctor_collage_precategory_data} (f : I_{ V} --> enriched_profunctor_collage_enrichment_hom_ob x₁ x₂) : x₁ --> x₂. Proof. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; cbn in *. - exact (enriched_to_arr E₁ f). - exact f. - exact f. - exact (enriched_to_arr E₂ 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.