proposition: Lemma ComposeSplitMono {M:AdditiveCategory} {A B C : M} (i : A --> B) (j : B --> C) : isSplitMonomorphism i ⇒ isSplitMonomorphism j ⇒ isSplitMonomorphism (i · j).
proof: Proof. intros s t. apply (squash_to_hProp s); clear s; intros [P [p ip]];cbn in P. apply (squash_to_hProp ip); clear ip; intros [p' [i' ip]]. change (hProptoType (isBinDirectSum i i' p' p)) in ip. apply (squash_to_hProp t); clear t; intros [Q [q jq]];cbn in Q. apply (squash_to_hProp jq); clear jq; intros [q' [j' jq]]. change (hProptoType (isBinDirectSum j j' q' q)) in jq. apply (squash_to_hProp (to_hasBinDirectSums P Q)); intros PQ. apply hinhpr;unfold ExactCategoryDataToAdditiveCategory,pr1. exists PQ. exists (q' · p · ι₁ + q · ι₂). apply hinhpr. exists (q' · p'). exists (π₁ · i' · j + π₂ · j'). repeat split; rewrite ? rewrite_op. { rewrite assoc'. rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite (to_IdIn1 ip). reflexivity. } { rewrite rightDistribute, 2 leftDistribute. rewrite (assoc' q'). rewrite (assoc' _ j). rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite assoc'. rewrite (assoc i'). rewrite (to_IdIn2 ip). rewrite id_left. rewrite (assoc _ q'). rewrite (assoc' _ j'). rewrite (to_Unel2 jq); unfold to_unel. rewrite zeroRight, zeroLeft, runax. rewrite (assoc' _ j). rewrite (assoc j). rewrite (to_Unel1 jq). unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite assoc'. rewrite (assoc j'). rewrite (to_IdIn2 jq). rewrite id_left. apply (to_BinOpId PQ). } { rewrite rightDistribute. rewrite assoc'. rewrite (assoc' q'). rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite assoc. rewrite (to_Unel1 ip); unfold to_unel. rewrite zeroLeft. rewrite lunax. rewrite assoc'. rewrite (assoc j). rewrite (to_Unel1 jq); unfold to_unel. rewrite zeroLeft, zeroRight. reflexivity. } { rewrite leftDistribute. rewrite assoc'. rewrite (assoc j). rewrite (to_IdIn1 jq). rewrite id_left. rewrite (assoc' _ i'). rewrite (to_Unel2 ip); unfold to_unel. rewrite zeroRight. rewrite lunax. rewrite assoc'. rewrite (assoc j'). rewrite (to_Unel2 jq);unfold to_unel. rewrite zeroLeft, zeroRight. reflexivity. } { rewrite rightDistribute, 2 leftDistribute. rewrite assoc. rewrite (assoc' _ i'). rewrite (assoc' _ ι₁). rewrite (assoc ι₁). rewrite (to_IdIn1 PQ). rewrite id_left. rewrite assoc. rewrite (assoc' q). rewrite (assoc _ _ (i' · j)). rewrite (to_Unel2 PQ); unfold to_unel. rewrite zeroLeft, zeroRight, runax. rewrite <- assocax. rewrite <- (leftDistribute _ _ j). rewrite 2 (assoc' q'). rewrite <- (rightDistribute q'). rewrite (to_BinOpId' ip). rewrite id_right. rewrite (assoc' _ ι₁). rewrite (assoc ι₁). rewrite (to_Unel1 PQ); unfold to_unel. rewrite zeroLeft, zeroRight, lunax. rewrite (assoc' q). rewrite (assoc ι₂). rewrite (to_IdIn2 PQ). rewrite id_left. exact (to_BinOpId' jq). } 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