proposition: Proposition enriched_conical_lim_from_prod_equalizers_unique : isaprop (∑ (φ : v --> E ⦃ w, lim ⦄), ∏ (i : I), φ · postcomp_arr E w (enriched_conical_lim_pr_from_prod_equalizers i) = fs i).
proof: Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use (EqualizerInsEq (is_equalizer_enriched_to_Equalizer _ _ _ enriched_conical_lim_ob_from_prod_equalizers_is_equalizer w)). use (ProductArrow_eq _ _ _ (is_prod_enriched_to_Product _ _ is_prod_src w)). intro i ; cbn. rewrite !assoc'. rewrite <- !postcomp_arr_comp. exact (pr2 φ₁ i @ !(pr2 φ₂ i)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers