proposition: 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: Proof. apply CoequalizerArrowComm. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.Limits.Coequalizers