Proposition enriched_weighted_to_conical_is_conical_colim_mor_eq (i : I) : enriched_weighted_to_conical_is_conical_colim_mor · precomp_arr E w (enriched_to_arr E (enriched_colim_cocone_in E D W a i)) = fs i. Proof. pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) (mor_to_end_comm _ (pr2 a w) enriched_weighted_to_conical_is_conical_colim_wedge i)) as p. cbn in p. rewrite tensor_comp_id_r in p. rewrite !assoc' in p. rewrite !internal_beta in p. rewrite !assoc in p. rewrite <- tensor_split' in p. refine (_ @ id_left _). rewrite <- mon_rinvunitor_runitor. rewrite !assoc'. rewrite <- p. unfold precomp_arr. rewrite !assoc. apply maponpaths_2. rewrite tensor_rinvunitor. rewrite !assoc'. apply maponpaths. rewrite <- tensor_split'. rewrite enriched_from_to_arr. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Ends. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedConicalColimits. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers. Import MonoidalNotations.