Lemma KernelEndo_is_identity {y z : C} {g : y --> z} {K : Kernel g} (φ : C⟦K, K⟧) (H : φ · (KernelArrow K) = KernelArrow K) : identity K = φ. Proof. set (H1 := tpair ((fun φ' : C⟦K, K⟧ => φ' · _ = _)) φ H). assert (H2 : identity_is_KernelIn K = H1). - apply proofirrelevancecontr. apply (KernelisKernel K). apply KernelCompZero. - apply (base_paths _ _ H2). 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.