Definition enriched_conical_colim_from_coprod_coequalizers_mor : v --> E ⦃ colim , w ⦄. Proof. use (EqualizerIn (is_coequalizer_enriched_to_Equalizer _ _ _ enriched_conical_colim_ob_from_coprod_coequalizers_is_coequalizer w)). - exact (ProductArrow _ _ (is_coprod_enriched_to_Product _ _ is_coprod_tar w) fs). - abstract (use (ProductArrow_eq _ _ _ (is_coprod_enriched_to_Product _ _ is_coprod_src w)) ; intros ijk ; cbn ; pose (ProductPrCommutes I V _ (is_coprod_enriched_to_Product E D is_coprod_tar w) _ fs) as p ; cbn in p ; rewrite !assoc' ; rewrite <- !precomp_arr_comp ; rewrite enriched_conical_colim_from_coprod_coequalizers_l_in ; rewrite enriched_conical_colim_from_coprod_coequalizers_r_in ; rewrite precomp_arr_comp ; rewrite !assoc ; rewrite !p ; refine (!_) ; apply qs). 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.