Definition KernelEqualizer {x y : ob C} {f : x --> y} (K : Kernel Z f) : Equalizer f (ZeroArrow Z _ _). Proof. use make_Equalizer. - exact K. - exact (KernelArrow K). - exact (KernelEqualizer_eq K). - exact (KernelEqualizer_isEqualizer K). Defined.
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.