Definition underlying_Coequalizer_arr {w : C} (h : y --> w) (q : f · h = g · h) : a --> w. Proof. use (enriched_to_arr E). use (EqualizerIn (is_coequalizer_enriched_to_Equalizer Ha w)). - exact (enriched_from_arr E h). - abstract (rewrite !enriched_from_arr_precomp ; 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. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Import MonoidalNotations. Section CoequalizersFromUnderlying. End CoequalizersFromUnderlying.