Definition enriched_profunctor_collage_comp {x₁ x₂ x₃ : C₁ ⨿ C₂} (f : enriched_profunctor_collage_mor x₁ x₂) (g : enriched_profunctor_collage_mor x₂ x₃) : enriched_profunctor_collage_mor x₁ x₃. Proof. induction x₁ as [ x₁ | y₁ ] ; induction x₂ as [ x₂ | y₂ ] ; induction x₃ as [ x₃ | y₃ ] ; cbn in *. - exact (f · g). - exact g. - use (enriched_to_arr E₁). refine (f · _). apply InitialArrow. - exact f. - exact (f · rmap_e_arr P g y₁). - use (enriched_to_arr E₂). refine (g · _). apply InitialArrow. - exact (g · lmap_e_arr P x₃ f). - exact (f · g). 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.