Lemma equiv_Cokernel1_isCoequalizer {a b : C} (f : C⟦a, b⟧) (CK : Limits.Cokernels.Cokernel (equiv_Zero2 Z) f) : isCoequalizer C f (ZeroArrow Z a b) CK (CokernelArrow CK) (equiv_Cokernel1_eq f CK). Proof. use (make_isCoequalizer _). intros w h H. use unique_exists. - use CokernelOut. + exact h. + rewrite postcomp_with_ZeroArrow in H. use (pathscomp0 _ (!(equiv_ZeroArrow a w Z))). exact H. - use CokernelCommutes. - intros y. apply hs. - intros y T. cbn in T. use CokernelOutsEq. unfold CokernelArrow. use (pathscomp0 T). apply pathsinv0. use CokernelCommutes. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Cokernels.