Definition is_conical_lim_enriched_arrow (w : C) (gs : ∏ (i : I), w --> D i) (qs : ∏ (i j : I) (f : i --> j), gs i · # D f = gs j) : w --> a. 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_postcomp ; apply maponpaths ; exact (qs i j 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.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.