Lemma CoequalizerOfArrowsEq {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') : CoequalizerArrow cfg · CoequalizerOfArrows cfg cfg' u v eqf eqg = v · CoequalizerArrow cfg'. Proof. apply CoequalizerArrowComm. Qed.
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.