Lemma equiv_isCoequalizer1 {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 := Limits.Coequalizers.make_Coequalizer f g h H X). use (make_isCoequalizer C). intros e' h' H'. use (unique_exists (Limits.Coequalizers.CoequalizerOut E e' h' H')). - exact (Limits.Coequalizers.CoequalizerCommutes E e' h' H'). - intros y. apply C. - intros y T. cbn in T. use (Limits.Coequalizers.CoequalizerOutsEq E). use (pathscomp0 T). exact (!(Limits.Coequalizers.CoequalizerCommutes E e' h' H')). 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.