Definition enriched_profunctor_collage_enrichment_comp (x₁ x₂ x₃ : enriched_profunctor_collage_precategory_data) : enriched_profunctor_collage_enrichment_hom_ob x₂ x₃ ⊗ enriched_profunctor_collage_enrichment_hom_ob x₁ x₂ --> enriched_profunctor_collage_enrichment_hom_ob x₁ x₃. Proof. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; induction x₃ as [ x₃ | y₃ ] ; cbn in *. - apply enriched_comp. - apply arrow_from_tensor_initial_r_benabou_cosmos. - apply arrow_from_tensor_initial_l_benabou_cosmos. - apply arrow_from_tensor_initial_l_benabou_cosmos. - apply (rmap_e P). - apply arrow_from_tensor_initial_r_benabou_cosmos. - exact (sym_mon_braiding _ _ _ · lmap_e P _ _ _). - apply enriched_comp. 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.