proposition: Proposition isaprop_enrichment_equalizers {V : monoidal_cat} {C : category} (HC : is_univalent C) (E : enrichment C V) : isaprop (enrichment_equalizers E).
proof: 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.
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.Monoidal.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.Limits.Equalizers