Proposition is_conical_colim_enriched_map_in (w : C) (gs : ∏ (i : I), D i --> w) (qs : ∏ (i j : I) (f : i --> j), # D f · gs j = gs i) (i : I) : enriched_conical_colim_cocone_in a i · is_conical_colim_enriched_arrow w gs qs = gs i. Proof. unfold is_conical_colim_enriched_arrow, enriched_conical_colim_cocone_in. 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 mon_linvunitor_I_mon_rinvunitor_I. rewrite <- tensor_rinvunitor. 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.OppositeCategory.Core. 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.Colimits.EnrichedCoproducts. Require Import UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers. Import MonoidalNotations.