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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts. Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Coequalizers.