Lemma CokernelCoequalizer_isCokernel {x y : ob C} {f : x --> y} (CK : Cokernel Z f) : isCoequalizer f (ZeroArrow Z x y) (CokernelArrow CK) (CokernelCoequalizer_eq CK). Proof. use make_isCoequalizer. intros w0 h H'. use unique_exists. - use CokernelOut. + exact h. + rewrite H'. apply ZeroArrow_comp_left. - use CokernelCommutes. - intros y0. apply hs. - intros y0 X. use CokernelOutsEq. rewrite CokernelCommutes. exact X. 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.Core.Isos. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Zero. - exact (ZeroArrowFrom w). - intros y X. cbn in X. use ArrowsFromZero.