Definition make_isKernel {x y z : C} (f : x --> y) (g : y --> z) (H1 : f · g = ZeroArrow Z x z) (H2 : ∏ (w : C) (h : w --> y) (H' : h · g = ZeroArrow Z w z), ∃! ψ : w --> x, ψ · f = h) : isKernel f g H1. Proof. unfold isKernel. intros w h H. use unique_exists. - exact (pr1 (iscontrpr1 (H2 w h H))). - exact (pr2 (iscontrpr1 (H2 w h H))). - intros y0. apply hs. - intros y0 X. exact (base_paths _ _ (pr2 (H2 w h H) (tpair _ y0 X))). 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.