Lemma CoequalizerCokernel_isCokernel {x y : ob C} {f : x --> y} (CE : Coequalizer f (ZeroArrow Z _ _)) : isCokernel Z f (CoequalizerArrow CE) (CoequalizerCokernel_eq CE). Proof. use (make_isCokernel). intros w h H'. use unique_exists. - use CoequalizerOut. + exact h. + rewrite ZeroArrow_comp_left. exact H'. - use CoequalizerCommutes. - intros y0. apply hs. - intros y0 X. use CoequalizerOutsEq. rewrite CoequalizerCommutes. 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.