Lemma AbelianPullbackEpiisPushout1 {x y z : A} (f : Epi A x z) (g : y --> z) (Pb : Pullback f g) : isPushout (PullbackPr1 Pb) (PullbackPr2 Pb) f g (PullbackSqrCommutes Pb). Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) x y). set (Pb' := Pullback_from_Equalizer_BinProduct A _ _ _ f g (BinDirectSum_BinProduct _ DS) (Abelian.Equalizer A ((to_Pr1 DS) · f) ((to_Pr2 DS) · g))). set (i := z_iso_from_Pullback_to_Pullback Pb' Pb). use isPushout_up_to_z_iso. - exact Pb'. - exact i. - use isPushout_mor_paths. + exact (PullbackPr1 Pb'). + exact (PullbackPr2 Pb'). + exact f. + exact g. + apply pathsinv0. exact (PullbackArrow_PullbackPr1 Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb')). + apply pathsinv0. exact (PullbackArrow_PullbackPr2 Pb Pb' (PullbackPr1 Pb') (PullbackPr2 Pb') (PullbackSqrCommutes Pb')). + apply idpath. + apply idpath. + exact (PullbackSqrCommutes _ ). + set (CK := EpiToCokernel f). set (K := Abelian.Kernel f). fold K in CK. use make_isPushout. intros e h k Hk. use unique_exists. * use (CokernelOut (to_Zero A) CK). -- exact h. -- exact (AbelianPullbackEpiisPushout1_eq f g Hk). * cbn. split. -- use (CokernelCommutes (to_Zero A) CK). -- assert (Hk' : PullbackPr1 Pb' · h = PullbackPr2 Pb' · k) by apply Hk. set (comm := CokernelCommutes (to_Zero A) CK _ h (AbelianPullbackEpiisPushout1_eq f g Hk)). cbn in comm. rewrite <- comm in Hk'. clear comm. apply (AbelianPullbackEpi2 f g Pb'). rewrite <- Hk'. cbn. rewrite assoc. rewrite assoc. apply cancel_postcomposition. rewrite <- assoc. rewrite <- assoc. apply pathsinv0. use EqualizerEqAr. * intros y0. apply isapropdirprod; apply (homset_property A). * intros y0 X. cbn in X. use (CokernelArrowisEpi (to_Zero A) CK). rewrite CokernelCommutes. exact (dirprod_pr1 X). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Morphisms. 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. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.