proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Zero UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Cokernels