proposition: Lemma KernelInComp {y z : C} {f : y --> z} (K : Kernel f) {x x' : C} (h1 : x --> x') (h2 : x' --> y) (H1 : h1 · h2 · f = ZeroArrow Z _ _) (H2 : h2 · f = ZeroArrow Z _ _) : KernelIn K x (h1 · h2) H1 = h1 · KernelIn K x' h2 H2.
proof: Proof. use KernelInsEq. rewrite KernelCommutes. rewrite <- assoc. rewrite KernelCommutes. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Zero