proposition: Lemma KernelEqualizer_isEqualizer {x y : ob C} {f : x --> y} (K : Kernel Z f) : isEqualizer f (ZeroArrow Z x y) (KernelArrow K) (KernelEqualizer_eq K).
proof: Proof. use make_isEqualizer. intros w h H'. use unique_exists. - use KernelIn. + exact h. + rewrite ZeroArrow_comp_right in H'. exact H'. - cbn. use KernelCommutes. - intros y0. apply hs. - intros y0 X. use KernelInsEq. rewrite KernelCommutes. exact 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