Lemma EqualizerKernel_eq {x y : ob C} {f : x --> y} (E : Equalizer f (ZeroArrow Z _ _)) : EqualizerArrow E · f = ZeroArrow Z E y. Proof. rewrite <- (ZeroArrow_comp_right _ _ _ _ _ (EqualizerArrow E)). exact (EqualizerEqAr E). 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.