Definition enriched_conical_colim_from_coprod_coequalizers_is_colim : is_conical_colim_enriched E D enriched_conical_colim_from_coprod_coequalizers_cocone. Proof. intros w v cc ; cbn. use iscontraprop1. - exact (enriched_conical_colim_from_coprod_coequalizers_unique w v (pr1 cc)). - simple refine (_ ,, _). + exact (enriched_conical_colim_from_coprod_coequalizers_mor _ _ (pr1 cc) (pr2 cc)). + exact (enriched_conical_colim_from_coprod_coequalizers_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.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.