Definition equalizer_enriched_to_equalizer (EqV : Equalizers V) (a : enriched_equalizer_cone) (w : C) : E ⦃ w , a ⦄ --> EqV (E ⦃ w, x ⦄) _ (postcomp_arr E w f) (postcomp_arr E w g). Proof. use EqualizerIn. - exact (postcomp_arr E w (enriched_equalizer_cone_pr a)). - exact (postcomp_eq_from_equalizer_cone 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.