proposition: Lemma equiv_Kernel1_isEqualizer {a b : C} (f : C⟦a, b⟧) (K : Limits.Kernels.Kernel (equiv_Zero2 Z) f) : isEqualizer C f (ZeroArrow Z a b) K (KernelArrow K) (equiv_Kernel1_eq f K).
proof: Proof. use (make_isEqualizer _ ). intros e h' H'. use unique_exists. - use KernelIn. + exact h'. + rewrite precomp_with_ZeroArrow in H'. use (pathscomp0 _ (!(equiv_ZeroArrow e b Z))). exact H'. - cbn. use KernelCommutes. - intros y. apply hs. - intros y X. cbn in X. use Limits.Kernels.KernelInsEq. unfold KernelArrow. use (pathscomp0 X). apply pathsinv0. use Limits.Kernels.KernelCommutes. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Zero UniMath.CategoryTheory.Limits.Graphs.Equalizers UniMath.CategoryTheory.Limits.Kernels