Lemma KernelEqualizer_eq {x y : ob C} {f : x --> y} (K : Kernel Z f) : KernelArrow K · f = KernelArrow K · ZeroArrow Z x y. Proof. rewrite ZeroArrow_comp_right. apply KernelCompZero. 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.