Proposition enriched_conical_colim_from_coprod_coequalizers_unique : isaprop (∑ (φ : v --> E ⦃ colim , w ⦄), ∏ (i : I), φ · precomp_arr E w (enriched_conical_colim_in_from_coprod_coequalizers i) = fs i). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use (EqualizerInsEq (is_coequalizer_enriched_to_Equalizer _ _ _ enriched_conical_colim_ob_from_coprod_coequalizers_is_coequalizer w)). use (ProductArrow_eq _ _ _ (is_coprod_enriched_to_Product _ _ is_coprod_tar w)). intro i ; cbn. rewrite !assoc'. rewrite <- !precomp_arr_comp. exact (pr2 φ₁ i @ !(pr2 φ₂ i)). 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.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.