Definition make_Coequalizer {y z w : C} (f g : y --> z) (e : z --> w) (H : f · e = g · e) (isE : isCoequalizer f g e H) : Coequalizer f g. Proof. use tpair. - use tpair. + apply w. + apply e. - simpl. exact (tpair _ H isE). 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.Epis. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Retracts. Section CoequalizersFromReflexiveCoequalizers. Section CoequalizersFromReflexive. End CoequalizersFromReflexive. End CoequalizersFromReflexiveCoequalizers.