Definition CoequalizerOfArrows {a a' b b' : C} {f g : a --> b} {f' g' : a' --> b'} (cfg : Coequalizer f g) (cfg' : Coequalizer f' g') (u : a --> a') (v : b --> b') (eqf : f · v = u · f') (eqg : g · v = u · g') : CoequalizerObject cfg --> CoequalizerObject cfg'. Proof. unshelve eapply CoequalizerOut. - refine (v · _). apply CoequalizerArrow. - abstract (rewrite ! assoc, eqf , eqg, ! assoc' ; apply cancel_precomposition, CoequalizerArrowEq). 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.