Lemma equiv_Kernel2_isEqualizer {a b : C} (f : C⟦a, b⟧) (K : Kernel f) : isKernel (equiv_Zero2 Z) (EqualizerArrow C K) f (equiv_Kernel2_eq f K). Proof. use (make_isKernel). intros w h H. use unique_exists. - use EqualizerIn. + exact h. + rewrite H. rewrite precomp_with_ZeroArrow. apply equiv_ZeroArrow. - use EqualizerArrowComm. - intros y. apply hs. - intros y T. cbn in T. use EqualizerInUnique. exact T. 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.