proposition: Lemma mapdiagram_coequalizer_eq_diag {C : category}{D : category} (F : functor C D){a b : C}(f g : a --> b) : eq_diag (C := D) (mapdiagram F (Coequalizer_diagram _ f g)) (Coequalizer_diagram _ (# F f) (# F g)).
proof: Proof. use tpair. - use StandardFiniteSets.two_rec_dep; cbn; apply idpath. - use StandardFiniteSets.two_rec_dep; use StandardFiniteSets.two_rec_dep; try exact (empty_rect _ ). intro e. induction e; apply idpath. Defined.
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