Definition equiv_Coequalizer2 {a b : C} (f g : C⟦a, b⟧) : Limits.Coequalizers.Coequalizer f g <- Coequalizer C f g. Proof. intros E. exact (@Limits.Coequalizers.make_Coequalizer C a b (CoequalizerObject C E) f g (CoequalizerArrow C E) (CoequalizerArrowEq C E) (@equiv_isCoequalizer2 a b f g (CoequalizerObject C E) (CoequalizerArrow C E) (CoequalizerArrowEq C E) (isCoequalizer_Coequalizer C E))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Coequalizers.