Definition equiv_Coequalizer1 {a b : C} (f g : C⟦a, b⟧) : Limits.Coequalizers.Coequalizer f g -> Coequalizer C f g. Proof. intros E. exact (make_Coequalizer C f g _ _ _ (equiv_isCoequalizer1 (Limits.Coequalizers.CoequalizerObject E) (Limits.Coequalizers.CoequalizerArrow E) (Limits.Coequalizers.CoequalizerEqAr E) (Limits.Coequalizers.isCoequalizer_Coequalizer 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.