proposition: Lemma IsomorphicToSplit {M:PreAdditive} (P Q : MorphismPair M) : MorphismPairIsomorphism P Q ⇒ isSplit P ⇒ isSplit Q.
proof: Proof. intros [f' [f [f'' [[e _] [e' _]]]]] ex. apply (squash_to_hProp ex); clear ex; intros [q [j su]]; apply hinhpr. exists (z_iso_inv f · q · f'). exists (z_iso_inv f'' · j · f). split. { intermediate_path (z_iso_inv f' · Mor1 P · q · f'). { rewrite 2 assoc. apply (maponpaths (λ k, k·f')). apply (maponpaths (λ k, k·q)). apply pathsinv0. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. exact e. } { rewrite 2 assoc'. rewrite (assoc _ q _). intermediate_path (z_iso_inv f' · (identity _ · f')). { apply maponpaths. apply (maponpaths (λ k, k·f')). exact (to_IdIn1 su). } { rewrite id_left. apply z_iso_after_z_iso_inv. } } } split. { rewrite assoc'. rewrite e'. rewrite assoc. rewrite (assoc' _ j _). apply wrap_inverse. apply (to_IdIn2 su). } split. { assert (r := to_Unel1 su); unfold to_unel in r. assert (r' := maponpaths (λ t, t · f'') r); cbn in r'; clear r. rewrite assoc' in r'. rewrite <- e' in r'. rewrite assoc in r'. rewrite <- e in r'. assert (r'' := maponpaths (λ t, z_iso_inv f' · t) r'); clear r'; cbn in r''. rewrite 2 assoc in r''. rewrite z_iso_after_z_iso_inv in r''. rewrite assoc' in r''. rewrite id_left in r''. rewrite zeroLeft,zeroRight in r''. exact r''. } split. { rewrite 2 assoc. rewrite (assoc' _ f _). rewrite z_iso_inv_after_z_iso. rewrite id_right. rewrite (assoc' _ j _). rewrite (to_Unel2 su). unfold to_unel. rewrite zeroRight, zeroLeft. reflexivity. } { apply (cancel_z_iso' f). rewrite id_right. rewrite rightDistribute. rewrite 3 (assoc f). rewrite z_iso_inv_after_z_iso, id_left. rewrite assoc'. rewrite e. rewrite assoc. rewrite (assoc f). rewrite e'. rewrite (assoc' _ f''). rewrite 2 (assoc f''). rewrite z_iso_inv_after_z_iso, id_left. rewrite assoc. rewrite <- leftDistribute. rewrite (to_BinOpId' su). rewrite id_left. reflexivity. } 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