proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Zero