Lemma KernelsIn_is_iso {x y : C} {f : x --> y} (K1 K2 : Kernel f) : is_iso (KernelIn K1 K2 (KernelArrow K2) (KernelCompZero K2)). Proof. use is_iso_qinv. - use KernelIn. + use KernelArrow. + use KernelCompZero. - split. + use KernelInsEq. rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes. rewrite id_left. apply idpath. + use KernelInsEq. rewrite <- assoc. rewrite KernelCommutes. rewrite KernelCommutes. rewrite id_left. 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.