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. 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.
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.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers. Require Import UniMath.CategoryTheory.Limits.Kernels.