Lemma are_inverses_from_Kernel_to_Kernel {y z : C} {g : y --> z} (K K': Kernel g) : is_inverse_in_precat (from_Kernel_to_Kernel K K') (from_Kernel_to_Kernel K' K). Proof. split. - apply pathsinv0. use KernelEndo_is_identity. rewrite <- assoc. unfold from_Kernel_to_Kernel. rewrite KernelCommutes. rewrite KernelCommutes. apply idpath. - apply pathsinv0. use KernelEndo_is_identity. rewrite <- assoc. unfold from_Kernel_to_Kernel. rewrite KernelCommutes. rewrite KernelCommutes. apply idpath. 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.