Lemma CokernelOfDiagonal_is_iso {X : A} (BinProd : BinProduct A X X) : is_z_isomorphism ((BinProductArrow A BinProd (identity X) (ZeroArrow (to_Zero A) X X)) · (CokernelArrow (Cokernel (DiagonalMap BinProd)))). Proof. set (coker := Cokernel (DiagonalMap BinProd)). set (r := (BinProductArrow A BinProd (identity X) (ZeroArrow (to_Zero A) X X)) · (CokernelArrow coker)). set (M := make_Monic A _ (DiagonalMap_isMonic BinProd)). set (ker := MonicToKernel M). use monic_epi_is_iso. - use (@KernelZeroisMonic A (to_Zero A) _ _ _ (ZeroArrow_comp_left _ _ _ _ _ _)). use (make_isKernel). intros w h H'. use unique_exists. + exact (ZeroArrow (to_Zero A) w (to_Zero A)). + unfold r in H'. rewrite assoc in H'. set (y := KernelIn _ ker _ _ H'). cbn in y. set (com1 := KernelCommutes _ ker _ _ H'). cbn in com1. fold y in com1. unfold DiagonalMap in com1. assert (H : y = ZeroArrow (to_Zero A) w ker). { rewrite <- (id_right y). set (tmp := BinProductPr2Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite <- tmp. rewrite assoc. rewrite com1. rewrite <- assoc. rewrite (BinProductPr2Commutes A _ _ BinProd _ (identity X) _). apply ZeroArrow_comp_right. } cbn. rewrite ZeroArrow_comp_left. cbn in H. apply pathsinv0 in H. use (pathscomp0 H). rewrite <- id_right. rewrite <- (BinProductPr1Commutes A _ _ BinProd _ (identity X) (ZeroArrow (to_Zero A) _ _)). rewrite assoc. rewrite <- com1. rewrite <- assoc. rewrite (BinProductPr1Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite id_right. apply idpath. + intros y. apply hs. + intros y H. apply ArrowsToZero. - use (@CokernelZeroisEpi A _ _ (to_Zero A) _ (ZeroArrow_comp_right _ _ _ _ _ _)). use make_isCokernel. intros w h H'. use unique_exists. + exact (ZeroArrow (to_Zero A) (to_Zero A) w). + set(coker2 := CokernelOfKernelOfPr2 BinProd). set(coker2ar := CokernelArrow coker2). cbn in coker2ar. unfold r in H'. rewrite <- assoc in H'. set (y := CokernelOut _ coker2 _ _ H'). cbn in y. set (com1 := CokernelCommutes _ coker2 _ _ H'). cbn in com1. fold y in com1. assert (H : y = ZeroArrow (to_Zero A) X w). { rewrite <- (id_left y). set (tmp := BinProductPr2Commutes A _ _ BinProd _ (identity X) (identity X)). rewrite <- tmp. rewrite <- assoc. rewrite com1. rewrite assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_left. } rewrite H in com1. rewrite ZeroArrow_comp_right in com1. rewrite <- (ZeroArrow_comp_right A (to_Zero A) _ _ _ (CokernelArrow coker)) in com1. apply CokernelArrowisEpi in com1. rewrite <- com1. apply ZeroArrow_comp_left. + intros y. apply hs. + intros y H. apply ArrowsFromZero. 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.PrecategoryBinProduct. 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.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. + intros y H. apply ArrowsFromZero.