Definition is_conical_colim_enriched_arrow (w : C) (gs : ∏ (i : I), D i --> w) (qs : ∏ (i j : I) (f : i --> j), # D f · gs j = gs i) : a --> w. Proof. refine (enriched_to_arr E _). use (limArrow (make_LimCone _ _ _ (pr2 a w))). simple refine (_ ,, _). - exact (λ i, enriched_from_arr E (gs i)). - abstract (intros i j f ; cbn ; rewrite enriched_from_arr_precomp ; apply maponpaths ; exact (qs j i f)). 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.