proposition: Proposition enriched_weighted_to_conical_is_conical_lim_mor_eq (i : I) : enriched_weighted_to_conical_is_conical_lim_mor · postcomp_arr E w (enriched_to_arr E (enriched_lim_cone_pr E D W a i)) = fs i.
proof: Proof. pose (maponpaths (λ z, z #⊗ identity _ · internal_eval _ _) (mor_to_end_comm _ (pr2 a w) enriched_weighted_to_conical_is_conical_lim_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. rewrite tensor_sym_mon_braiding in p. refine (_ @ id_left _). rewrite <- mon_rinvunitor_runitor. rewrite !assoc'. rewrite <- p. unfold postcomp_arr. rewrite !assoc. apply maponpaths_2. rewrite tensor_linvunitor. rewrite sym_mon_braiding_rinvunitor. rewrite !assoc'. apply maponpaths. rewrite <- tensor_split. rewrite enriched_from_to_arr. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.OppositeCategory.Core UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Ends UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedConicalLimits UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers