Lemma EqualizerKernel_isKernel {x y : ob C} {f : x --> y} (E : Equalizer f (ZeroArrow Z _ _)) : isKernel Z (EqualizerArrow E) f (EqualizerKernel_eq E). Proof. use (make_isKernel). intros w h H'. use unique_exists. - use EqualizerIn. + exact h. + rewrite ZeroArrow_comp_right. exact H'. - use EqualizerCommutes. - intros y0. apply hs. - intros y0 X. use EqualizerInsEq. rewrite EqualizerCommutes. 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.Monics. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Zero. isKernel (ZeroArrowFrom x) (identity x) (ArrowsFromZero C Z x (ZeroArrowFrom x · identity x) (ZeroArrow Z Z x)). - exact (ZeroArrowFrom x). - use ArrowsFromZero.