Proposition isaprop_enrichment_equalizers {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) : isaprop (enrichment_equalizers E). Proof. use invproofirrelevance. intros φ₁ φ₂. use funextsec ; intro x. use funextsec ; intro y. use funextsec ; intro f. use funextsec ; intro g. use subtypePath. { intro. apply isaprop_is_equalizer_enriched. } use total2_paths_f. - use (isotoid _ HC). use iso_between_equalizer_enriched. + exact (pr2 (φ₁ x y f g)). + exact (pr2 (φ₂ x y f g)). - use subtypePath. { intro. apply homset_property. } rewrite pr1_transportf. rewrite transportf_enriched_arr_l. rewrite idtoiso_inv. rewrite idtoiso_isotoid. cbn. refine (_ @ enriched_from_to_arr E _). apply maponpaths. unfold map_between_equalizer_enriched ; cbn. apply underlying_Equalizer_arr_pr. 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.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Equalizers. Import MonoidalNotations. Section EqualizersFromUnderlying. End EqualizersFromUnderlying.