Definition is_conical_colim_enriched_cone (a : enriched_conical_colim_cocone) (w : C) : cone (is_conical_colim_enriched_diagram a w) (E ⦃ a , w ⦄). Proof. use make_cone. - exact (λ i, precomp_arr E w (enriched_conical_colim_cocone_in a i)). - abstract (intros i j f ; cbn ; rewrite <- precomp_arr_comp ; rewrite enriched_enriched_conical_colim_cocone_commute ; apply idpath). Defined.
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.