Lemma transport_source_KernelIn {x' x y z : C} (f : x --> y) {g : y --> z} (K : Kernel Z g) (e : x = x') (H : f · g = ZeroArrow Z _ _) : transportf (λ x' : ob C, precategory_morphisms x' K) e (KernelIn Z K _ f H) = KernelIn Z K _ (transportf (λ x' : ob C, precategory_morphisms x' y) e f) (transport_source_KernelIn_eq f K e H). Proof. induction e. use KernelInsEq. cbn. 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.