Lemma KernelCompMonic_isKernel {x y z : C} (f : x --> y) (M : Monic C y z) (K : Kernel Z (f · M)) : isKernel Z (KernelArrow K) f (KernelCompMonic_eq f M K). Proof. use make_isKernel. - intros w h H'. use unique_exists. + use KernelIn. * exact h. * rewrite assoc. rewrite <- (ZeroArrow_comp_left _ _ _ _ _ M). apply cancel_postcomposition. exact H'. + cbn. rewrite KernelCommutes. apply idpath. + intros y0. apply hs. + intros y0 X. apply pathsinv0. cbn in X. use (MonicisMonic C (make_Monic _ _ (KernelArrowisMonic Z K))). cbn. rewrite KernelCommutes. apply pathsinv0. apply 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.