Definition make_is_equalizer_enriched_from_underlying (EqV : Equalizers V) (a : enriched_equalizer_cone) (eq_a : isEqualizer f g (enriched_equalizer_cone_pr a) (enriched_equalizer_cone_eq a)) (HV : conservative_moncat V) : is_equalizer_enriched a. Proof. use (make_is_equalizer_enriched_from_z_iso EqV). intros w. use HV. use isweq_iso. - exact (equalizer_enriched_from_underlying_map EqV a eq_a w). - exact (equalizer_enriched_from_underlying_map_inv₁ EqV a eq_a w). - exact (equalizer_enriched_from_underlying_map_inv₂ EqV a eq_a w). Defined.
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.