proposition: Lemma AdditiveExactnessProperties (M:AdditiveCategory) : ExactCategoryProperties (M,,isSplit).
proof: Proof. split;unfold ExactCategoryDataToAdditiveCategory,pr1. - split. { intros P Q. apply IsomorphicToSplit. } { intros P Q i e. use IsomorphicToSplit. 2 : { exact (InverseMorphismPairIsomorphism i). } exact e. } - split. { split. { intros A. apply (squash_to_hProp (to_hasZero M)); intros Z. apply hinhpr. exists Z. set (Q := TrivialDirectSum Z A). exact (to_Pr2 Q,, DirectSumToSplit Q). } { intros A. apply (squash_to_hProp (to_hasZero M)); intros Z. apply hinhpr. exists Z. set (Q := TrivialDirectSum' Z A). exact (to_In1 Q,, DirectSumToSplit Q). } } split. { intros P. exact (isSplitToKernelCokernelPair (Mor1 P) (Mor2 P)). } split. { split. { exact (@ComposeSplitMono M). } { exact (@ComposeSplitEpi M). } } { split. { exact (@PullbackSplitEpi M). } { exact (@PushoutSplitMono M). } } Defined.
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