Definition map_between_coequalizer_enriched {a b : enriched_coequalizer_cocone} (Ha : is_coequalizer_enriched a) (Hb : is_coequalizer_enriched b) : a --> b := underlying_Coequalizer_arr Ha (enriched_coequalizer_cocone_in b) (enriched_coequalizer_cocone_eq b).
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. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Import MonoidalNotations. Section CoequalizersFromUnderlying. End CoequalizersFromUnderlying.