proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums