Definition underlying_Equalizer_arr {w : C} (h : w --> x) (q : h · f = h · g) : w --> a. Proof. use (enriched_to_arr E). use (EqualizerIn (is_equalizer_enriched_to_Equalizer Ha w)). - exact (enriched_from_arr E h). - abstract (rewrite !enriched_from_arr_postcomp ; rewrite q ; apply idpath). 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.