Definition enriched_conical_lim_from_prod_equalizers_is_lim : is_conical_lim_enriched E D enriched_conical_lim_from_prod_equalizers_cone. Proof. intros w v cc ; cbn. use iscontraprop1. - exact (enriched_conical_lim_from_prod_equalizers_unique w v (pr1 cc)). - simple refine (_ ,, _). + exact (enriched_conical_lim_from_prod_equalizers_mor _ _ (pr1 cc) (pr2 cc)). + exact (enriched_conical_lim_from_prod_equalizers_commute _ _ (pr1 cc) (pr2 cc)). 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.