Lemma equiv_Cokernel2_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_Cokernel2_eq f CK). Proof. use (make_isCoequalizer _ ). intros w h H. use unique_exists. - use CokernelOut. + exact h. + use (pathscomp0 H). apply pathsinv0. rewrite postcomp_with_ZeroArrow. apply equiv_ZeroArrow. - use CokernelCommutes. - intros y. apply hs. - intros y T. cbn in T. use CokernelOutsEq. rewrite T. rewrite CokernelCommutes. apply idpath. 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.