Lemma Kernel_up_to_iso_isKernel {x y z : C} (f : x --> y) (g : y --> z) (K : Kernel Z g) (h : z_iso x K) (H : f = h · (KernelArrow K)) (H'' : f · g = ZeroArrow Z x z) : isKernel Z f g H''. Proof. use make_isKernel. intros w h0 H'. use unique_exists. - exact (KernelIn Z K w h0 H' · inv_from_z_iso h). - cbn beta. rewrite H. rewrite assoc. rewrite <- (assoc _ _ h). cbn. rewrite (is_inverse_in_precat2 h). rewrite id_right. apply KernelCommutes. - intros y0. apply hs. - intros y0 X. cbn beta in X. use (post_comp_with_z_iso_is_inj h). rewrite <- assoc. use (pathscomp0 _ (! (maponpaths (λ gg : _, KernelIn Z K w h0 H' · gg) (is_inverse_in_precat2 h)))). rewrite id_right. use KernelInsEq. rewrite KernelCommutes. rewrite <- X. rewrite <- assoc. apply cancel_precomposition. apply pathsinv0. apply H. 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.