Definition Coequalizer_eq_ar {C : category} {x y c : C} {f g : x --> y} {e₁ e₂ : y --> c} (p : e₁ = e₂) (q₁ : f · e₁ = g · e₁) (q₂ : f · e₂ = g · e₂) (H : isCoequalizer f g e₁ q₁) : isCoequalizer f g e₂ q₂. Proof. induction p. use (isCoequalizer_path H). apply homset_property. 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.