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. 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.
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.