Definition KernelofZeroArrow_iso (x y : C) (K : Kernel (@ZeroArrow C Z x y)) : z_iso K x := make_z_iso (KernelArrow K) (from_Kernel_to_Kernel (KernelofZeroArrow x y) K) (KernelofZeroArrow_is_iso K).
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.