proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.Monoids UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive