Lemma equiv_isCoequalizer2 {a b : C} (f g : C⟦a, b⟧) (e : C) (h : C⟦b, e⟧) (H : f · h = g · h) : Limits.Coequalizers.isCoequalizer f g h H <- isCoequalizer C f g e h H. Proof. intros X. set (E := make_Coequalizer C f g e h H X). intros e' h' H'. use (unique_exists (CoequalizerOut C E e' h' H')). - exact (CoequalizerArrowComm C E e' h' H'). - intros y. apply C. - intros y T. cbn in T. use (CoequalizerOutUnique C E). exact T. Qed.
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.