Proposition is_conical_lim_enriched_arrow_eq {w : C} {f g : w --> a} (q : ∏ (i : I), f · enriched_conical_lim_cone_pr a i = g · enriched_conical_lim_cone_pr a i) : f = g. Proof. refine (!(enriched_to_from_arr E _) @ _ @ enriched_to_from_arr E _). apply maponpaths. use (arr_to_LimCone_eq (is_conical_lim_enriched_to_Lim (pr2 a) w)). intro i ; cbn. rewrite !enriched_from_arr_postcomp. rewrite q. 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.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.