proposition: 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: Proof. induction e. use KernelInsEq. cbn. rewrite KernelCommutes. 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