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. 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.
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.