Lemma KernelZeroisMonic {x y z : A} (f : y --> z) (H : ZeroArrow (to_Zero A) x y · f = ZeroArrow (to_Zero A) x z ) (isK : isKernel (to_Zero A) (ZeroArrow (to_Zero A) _ _) f H) : isMonic f. Proof. intros w u v H'. set (Coeq := Coequalizer A u v). set (Coeqar := CoequalizerOut Coeq z f H'). set (Coeqar_epi := CoequalizerArrowEpi Coeq). set (Coeq_coker := EpiToCokernel Coeqar_epi). set (ker := @make_Kernel A (to_Zero A) _ _ _ (ZeroArrow (to_Zero A) x y) f H isK). assert (e0 : CokernelArrow Coeq_coker = CoequalizerArrow Coeq). { apply idpath. } assert (e1 : f = (CokernelArrow Coeq_coker) · Coeqar). { apply pathsinv0. rewrite e0. set (XX := CoequalizerCommutes Coeq z f H'). fold Coeqar in XX. apply XX. } assert (e2 : (KernelArrow (to_Kernels A _ _ Coeqar_epi)) · f = ZeroArrow (to_Zero A) _ _). { rewrite e1. rewrite assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_left. } set (ar := KernelIn (to_Zero A) ker (to_Kernels A _ _ Coeqar_epi) (KernelArrow (to_Kernels A _ _ Coeqar_epi))). set (com1 := KernelCommutes (to_Zero A) ker (to_Kernels A _ _ Coeqar_epi) (KernelArrow (to_Kernels A _ _ Coeqar_epi)) e2). assert (e3 : KernelArrow ker = ZeroArrow (to_Zero A) _ _ ). { apply idpath. } assert (e4 : (KernelArrow (to_Kernels A _ _ Coeqar_epi)) = ZeroArrow (to_Zero A) _ _). { rewrite <- com1. apply ZeroArrow_comp_right. } assert (e5 : is_iso (CoequalizerArrow Coeq)). { set (coker2 := KernelZeroMonic_cokernel e4 Coeq_coker). apply (is_iso_qinv _ _ (CokernelofZeroArrow_is_iso (to_Zero A) coker2)). } set (isoar := make_iso (CoequalizerArrow Coeq) e5). set (coeq_eq := CoequalizerEqAr Coeq). apply (maponpaths (λ f : _, f · inv_from_iso isoar)) in coeq_eq. rewrite <- assoc in coeq_eq. rewrite <- assoc in coeq_eq. assert(areq : CoequalizerArrow Coeq = isoar). apply idpath. rewrite areq in coeq_eq. rewrite (iso_inv_after_iso isoar) in coeq_eq. rewrite <- id_right. rewrite <- coeq_eq. apply pathsinv0. apply id_right. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. isKernel (to_Zero A) (ZeroArrowFrom x) M (ArrowsFromZero A (to_Zero A) y (ZeroArrowFrom x · M) (ZeroArrow (to_Zero A) _ _)). make_Kernel (to_Zero A) (ZeroArrowFrom _) M _ (MonicKernelZero_isKernel M). - intros y0 Y. apply ArrowsFromZero.