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. 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.
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.