Proposition is_conical_lim_enriched_map_pr (w : C) (gs : ∏ (i : I), w --> D i) (qs : ∏ (i j : I) (f : i --> j), gs i · # D f = gs j) (i : I) : is_conical_lim_enriched_arrow w gs qs · enriched_conical_lim_cone_pr a i = gs i. Proof. unfold is_conical_lim_enriched_arrow, enriched_conical_lim_cone_pr. use (invmaponpathsweq (make_weq _ (isweq_enriched_from_arr E _ _))) ; cbn. rewrite enriched_from_arr_comp. rewrite !enriched_from_to_arr. rewrite tensor_split. rewrite !assoc. rewrite <- tensor_linvunitor. etrans. { rewrite !assoc'. rewrite !(maponpaths (λ z, _ · z) (assoc _ _ _)). apply (limArrowCommutes (make_LimCone _ _ _ (pr2 a w))). } cbn. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Import MonoidalNotations.