Definition map_between_equalizer_enriched {a b : enriched_equalizer_cone} (Ha : is_equalizer_enriched a) (Hb : is_equalizer_enriched b) : a --> b := underlying_Equalizer_arr Hb (enriched_equalizer_cone_pr a) (enriched_equalizer_cone_eq a).
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.