Definition is_conical_lim_enriched_cone (a : enriched_conical_lim_cone) (w : C) : cone (is_conical_lim_enriched_diagram a w) (E ⦃ w, a ⦄). Proof. use make_cone. - exact (λ i, postcomp_arr E w (enriched_conical_lim_cone_pr a i)). - abstract (intros i j f ; cbn ; rewrite <- postcomp_arr_comp ; rewrite enriched_conical_lim_cone_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.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.