Lemma AbelianPushoutMonicisPullback1 {x y z : A} (f : Monic A x y) (g : x --> z) (Po : Pushout f g) : isPullback (PushoutSqrCommutes Po). Proof. set (DS := to_BinDirectSums (AbelianToAdditive A) y z). set (Po' := Pushout_from_Coequalizer_BinCoproduct A _ _ _ f g (BinDirectSum_BinCoproduct _ DS) (Abelian.Coequalizer A (f · (to_In1 DS)) (g · (to_In2 DS)))). set (i := z_iso_from_Pushout_to_Pushout Po Po'). use isPullback_up_to_z_iso. - exact Po'. - exact i. - use isPullback_mor_paths. + exact (PushoutIn1 Po'). + exact (PushoutIn2 Po'). + exact f. + exact g. + apply pathsinv0. exact (PushoutArrow_PushoutIn1 Po Po' (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po')). + apply pathsinv0. exact (PushoutArrow_PushoutIn2 Po Po' (PushoutIn1 Po') (PushoutIn2 Po') (PushoutSqrCommutes Po')). + apply idpath. + apply idpath. + exact (PushoutSqrCommutes _ ). + set (K := MonicToKernel f). set (CK := Abelian.Cokernel f). fold CK in K. use make_isPullback. intros e h k Hk. use unique_exists. * use (KernelIn (to_Zero A) K). -- exact h. -- exact (AbelianPushoutMonicisPullback_eq f g Hk). * cbn. split. -- use (KernelCommutes (to_Zero A) K). -- assert (Hk' : h · PushoutIn1 Po' = k · PushoutIn2 Po') by apply Hk. set (comm := KernelCommutes (to_Zero A) K _ h (AbelianPushoutMonicisPullback_eq f g Hk)). cbn in comm. rewrite <- comm in Hk'. clear comm. apply (AbelianPushoutMonic2 f g Po'). rewrite <- Hk'. cbn. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite assoc. rewrite assoc. apply pathsinv0. use CoequalizerEqAr. * intros y0. apply isapropdirprod; apply (homset_property A). * intros y0 X. cbn in X. use (KernelArrowisMonic (to_Zero A) K). rewrite KernelCommutes. 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.