Lemma CokernelZeroisEpi {x y z : A} (f : x --> y) (H : f · ZeroArrow (to_Zero A) y z = ZeroArrow (to_Zero A) x z ) (isCK : isCokernel (to_Zero A) f (ZeroArrow (to_Zero A) _ _) H) : isEpi f. Proof. intros w u v H'. set (Eq := Equalizer A u v). set (Eqar := EqualizerIn Eq x f H'). set (Eqar_monic := EqualizerArrowMonic Eq). set (Eq_ker := MonicToKernel Eqar_monic). set (coker := @make_Cokernel A (to_Zero A) _ _ _ f (ZeroArrow (to_Zero A) y z) H isCK). assert (e0 : KernelArrow Eq_ker = EqualizerArrow Eq). { apply idpath. } assert (e1 : f = Eqar · (KernelArrow Eq_ker)). { apply pathsinv0. rewrite e0. set (XX := EqualizerCommutes Eq x f H'). fold Eqar in XX. apply XX. } assert (e2 : f · (CokernelArrow (to_Cokernels A _ _ Eqar_monic)) = ZeroArrow (to_Zero A) _ _). { rewrite e1. rewrite <- assoc. set (tmp := maponpaths (λ f : _, Eqar · f) (KernelCompZero (to_Zero A) Eq_ker)). use (pathscomp0 tmp). apply ZeroArrow_comp_right. } set (ar := CokernelOut (to_Zero A) coker (to_Cokernels A _ _ Eqar_monic) (CokernelArrow (to_Cokernels A _ _ Eqar_monic)) e2). set (com1 := CokernelCommutes (to_Zero A) coker (to_Cokernels A _ _ Eqar_monic) (CokernelArrow (to_Cokernels A _ _ Eqar_monic)) e2). assert (e3 : CokernelArrow coker = ZeroArrow (to_Zero A) _ _ ). { apply idpath. } assert (e4 : (CokernelArrow (to_Cokernels A _ _ Eqar_monic)) = ZeroArrow (to_Zero A) _ _). { rewrite <- com1. apply ZeroArrow_comp_left. } assert (e5 : is_iso (EqualizerArrow Eq)). { set (ker2 := CokernelZeroEpi_kernel e4 Eq_ker). apply (is_iso_qinv _ _ (KernelofZeroArrow_is_iso (to_Zero A) ker2)). } set (isoar := make_iso (EqualizerArrow Eq) e5). set (Eq_eq := EqualizerEqAr Eq). apply (maponpaths (λ f : _, inv_from_iso isoar · f)) in Eq_eq. rewrite assoc in Eq_eq. rewrite assoc in Eq_eq. assert(areq : EqualizerArrow Eq = isoar). apply idpath. rewrite areq in Eq_eq. rewrite (iso_after_iso_inv isoar) in Eq_eq. rewrite <- id_left. rewrite <- Eq_eq. apply pathsinv0. apply id_left. 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.