Definition KernelInPaths_is_iso_mor {x y : C} {f f' : x --> y} (e : f = f') (K1 : Kernel Z f) (K2 : Kernel Z f') : K1 --> K2. Proof. induction e. use KernelIn. - use KernelArrow. - use KernelCompZero. 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.