proposition: Lemma eq_coeq_pw {X Y: functor C D} (a b:X ⟹ Y) (c:C) : eq_diag (Coequalizer_diagram D (a c) (b c)) (diagram_pointwise (Coequalizer_diagram CD a b) c).
proof: Proof. intros. use tpair. use StandardFiniteSets.two_rec_dep; reflexivity. use StandardFiniteSets.two_rec_dep; use StandardFiniteSets.two_rec_dep; try exact (empty_rect _ ). intros g'. destruct g'. apply idpath. apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Epis UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Pushouts UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coequalizers