proposition: Lemma PullbackSplitEpi {M:AdditiveCategory} {A A'' C : M} (q : A --> A'') (g : C --> A'') : isSplitEpimorphism q -> ∃ PB : Pullback q g, isSplitEpimorphism (PullbackPr2 PB).
proof: Proof. intros s. apply (squash_to_hProp s); clear s; intros [A' [i e]]. apply (squash_to_hProp e); clear e; intros [p [j e]]. apply (squash_to_hProp (to_hasBinDirectSums A' C)); intros A'C. apply hinhpr. use tpair. - use tpair. + exists A'C. exists (π₁ · i + π₂ · g · j). exact π₂. + simpl. rewrite rewrite_op. use tpair. * rewrite leftDistribute. rewrite (assoc' _ j q). rewrite (to_IdIn2 e). rewrite id_right. rewrite (assoc' _ i q). rewrite (to_Unel1 e); unfold to_unel. rewrite zeroRight, lunax. reflexivity. * intros T r s eqn. apply iscontraprop1. { apply invproofirrelevance. intros h k. apply subtypePath. { intros l. apply isapropdirprod;apply to_has_homsets. } induction h as [h [H H']], k as [k [K K']]. simpl. rewrite <- (id_right h), <- (id_right k). rewrite <- (to_BinOpId' A'C). rewrite 2 rightDistribute. rewrite 4 assoc. rewrite H', K'. apply (maponpaths (λ z, z + s · ι₂)). rewrite rightDistribute in H, K. rewrite 3 assoc in H, K. rewrite H' in H. rewrite K' in K. apply (maponpaths (λ z, z · ι₁)). apply (to_In1_isMonic _ (make_BinDirectSum _ _ _ _ _ _ _ _ e)). change (h · π₁ · i = k · π₁ · i). apply (grrcan (T-->A) (s · g · j)). exact (H @ !K). } exists (r · p · ι₁ + s · ι₂). split. { rewrite leftDistribute, 2 rightDistribute. rewrite assoc'. rewrite (assoc _ _ i). rewrite (to_IdIn1 A'C). rewrite id_left. rewrite (assoc' (r · p)). rewrite 2 (assoc ι₁). rewrite (to_Unel1 A'C); unfold to_unel. rewrite 2 zeroLeft, zeroRight, runax. rewrite (assoc' s). rewrite (assoc ι₂). rewrite (to_Unel2 A'C); unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite 2 assoc. rewrite (assoc' s). rewrite (to_IdIn2 A'C). rewrite id_right. rewrite (!eqn). rewrite 2 assoc'. rewrite <- (rightDistribute r). rewrite (to_BinOpId' e). apply id_right. } { rewrite leftDistribute. rewrite (assoc' (r · p)). rewrite (to_Unel1 A'C); unfold to_unel. rewrite zeroRight, lunax. rewrite assoc'. rewrite (to_IdIn2 A'C). apply id_right. } - cbn. exact (hinhpr(A',,ι₁,, hinhpr (π₁,,ι₂,,BinDirectSum_isBinDirectSum _ A'C))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions